Commit 455ef2f1 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add a new container to keep track of polymorphic variables in Descr.t

parent 8237f913
......@@ -136,7 +136,50 @@ module BoolIntervals : BoolVar.S with
module BoolChars : BoolVar.S with
type s = Chars.t = BoolVar.Make(Chars)
type tlvs = { s : Var.Set.t ; b : bool }
module TLV = struct
open Var
(* s : top level variables
* f : all free variables in the subtree
* b : true if the type contains only variables *)
type t = { s : Set.t ; f : Set.t ; b : bool }
let empty = { s = Set.empty ; f = Set.empty ; b = true }
let singleton v = { s = Set.singleton v; f = Set.singleton v; b = true }
(* return the max of top level variables *)
let max x = Set.max_elt x.s
let pair x y = {
b = false ;
s = Set.empty ;
f = Set.union x.f y.f
}
let union x y = {
b = x.b && y.b;
s = Set.union x.s y.s ;
f = Set.union x.f y.f ;
}
let inter x y = {
b = x.b && y.b;
s = Set.inter x.s y.s ;
f = Set.inter x.f y.f ;
}
let diff x y = {
s = Set.diff x.s y.s;
f = Set.diff x.f y.f;
b = x.b && y.b
}
(* true if it contains only one variable *)
let is_single x = x.b && (Set.cardinal x.f = 1) && (Set.cardinal x.s = 1)
let no_variables x = (x.b == false) && (Set.cardinal x.f = 0)
end
module rec Descr :
sig
......@@ -172,7 +215,7 @@ sig
absent: bool;
(* maintains the list of all toplevel type variables in s
* and a flag that is true if s contains only variables, false otherwise *)
toplvars : tlvs
toplvars : TLV.t
}
include Custom.T with type t = s
val empty: t
......@@ -188,7 +231,7 @@ struct
record: BoolRec.t;
abstract: Abstract.t;
absent: bool;
toplvars : tlvs
toplvars : TLV.t
}
type t = s
......@@ -217,7 +260,7 @@ struct
chars = BoolChars.empty;
abstract = Abstract.empty;
absent= false;
toplvars = { s = Var.Set.empty ; b = true }
toplvars = TLV.empty
}
let check a =
......@@ -328,6 +371,10 @@ let cons d =
incr count;
Node.mk !count d
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id
(* two representation possible. either all fields (except vars) are full, OR
* the field vars is full.
*)
......@@ -341,7 +388,7 @@ let any = {
chars = BoolChars.full;
abstract = Abstract.any;
absent= false;
toplvars = { s = Var.Set.empty ; b = true }
toplvars = TLV.empty
}
let non_constructed =
......@@ -352,14 +399,17 @@ let non_constructed_or_absent =
{ non_constructed with absent = true }
(* Descr.t type constructors *)
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = {empty.toplvars with b = false } }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
(* XXX toplevel variables are not properly set for records *)
let record label t =
{ empty with
record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
let record_fields x =
{ empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
let var a = {
(* Atm = Any ^ a *)
......@@ -372,18 +422,17 @@ let var a = {
chars = BoolChars.vars a;
abstract = Abstract.empty;
absent= false;
toplvars = { s = Var.Set.singleton a; b = true }
toplvars = TLV.singleton a
}
let is_var t = TLV.is_single t.toplvars
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = a }
let get_abstract t = t.abstract
(* union is component wise + a pass to extract variables
* Var = ( t1.Var v t2.Var ) v ( extracted variables )
*)
let cup x y =
if x == y then x else {
times = BoolPair.cup x.times y.times;
......@@ -395,11 +444,9 @@ let cup x y =
chars = BoolChars.cup x.chars y.chars;
abstract = Abstract.cup x.abstract y.abstract;
absent= x.absent || y.absent;
toplvars = { s = Var.Set.union x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
toplvars = TLV.union x.toplvars y.toplvars
}
(* intersection
*)
let cap x y =
if x == y then x else {
ints = BoolIntervals.cap x.ints y.ints;
......@@ -411,17 +458,9 @@ let cap x y =
chars = BoolChars.cap x.chars y.chars;
abstract = Abstract.cap x.abstract y.abstract;
absent= x.absent && y.absent;
toplvars = { s = Var.Set.inter x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
toplvars = TLV.inter x.toplvars y.toplvars
}
(*
*
* t1 // t2 = ( t1.Atm ^ - t2.Atm ^ t2.Var ) v
* ( t1.Var ^ t2.Var )
*
* Atm t1.Atm // ( t2.Atm v t2.Var )
* Var ( t1.Var // t2.Var ) v ( extracted variables )
*)
let diff x y =
if x == y then empty else {
times = BoolPair.diff x.times y.times;
......@@ -433,7 +472,7 @@ let diff x y =
chars = BoolChars.diff x.chars y.chars;
abstract = Abstract.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
toplvars = { s = Var.Set.diff x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
toplvars = TLV.diff x.toplvars y.toplvars
}
(* TODO: optimize disjoint check for boolean combinations *)
......@@ -448,10 +487,6 @@ let trivially_disjoint a b =
(Abstract.disjoint a.abstract b.abstract) &&
(not (a.absent && b.absent))
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id
let rec constant = function
| Integer i -> interval (Intervals.atom i)
| Atom a -> atom (Atoms.atom a)
......@@ -2073,6 +2108,7 @@ struct
with Not_found -> begin
DescrHash.add memo_decompose t None;
let s =
if TLV.no_variables t.toplvars then ty t else
cup [
decompose_aux atom (BoolAtoms.get t.atoms);
decompose_aux interval (BoolIntervals.get t.ints);
......@@ -2128,15 +2164,21 @@ struct
| _ -> var d
else var d
in
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
descr(solve x)
if TLV.no_variables t.toplvars then t
else begin
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
descr(solve x)
end
let substitute t (alpha,s) =
let subst s d = if Var.equal d alpha then s else var d in
let x = forward () in
define x (substitute_aux (decompose t) (subst (ty s)));
descr(solve x)
if TLV.no_variables t.toplvars then t
else begin
let subst s d = if Var.equal d alpha then s else var d in
let x = forward () in
define x (substitute_aux (decompose t) (subst (ty s)));
descr(solve x)
end
let substitutefree t =
let h = Hashtbl.create 17 in
......@@ -2733,8 +2775,8 @@ module Tallying = struct
let t = CS.M.find (not b,alpha) m in
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if t.toplvars.b && (Var.Set.cardinal t.toplvars.s) = 1 then begin
let beta = Var.Set.max_elt t.toplvars.s in
if is_var t then begin
let beta = TLV.max t.toplvars in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
if b then aux alpha (empty,t) acc1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment