Skip to content

GitLab

Commit e8ebd69d authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Rework the type variable infrastructure. Remove it from the type structure and... 

Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
parent 8ff33414
Hide whitespace changes
Inline Side-by-side
Showing with 205 additions and 167 deletions
types/types.ml
View file @ e8ebd69d
......@@ -137,69 +137,69 @@ module BoolChars : BoolVar.S with
module BoolAbstracts : BoolVar.S with
type s = Abstracts.t = BoolVar.Make(Abstracts)
module TLV = struct
module Set = struct
include Set.Make(
struct
type t = (Var.var * bool)
let compare (v1,p1) (v2,p2) =
let c = Var.compare v1 v2 in
if c == 0 then
if p1 == p2 then 0
else if p1 then 1 else -1
else c
end)
let pp_aux ppf pp_elem s =
let f ppf = function
|(v,true) -> Format.fprintf ppf "%a" pp_elem v
|(v,false) -> Format.fprintf ppf "~ %a" pp_elem v
in
Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s)
let dump ppf s = pp_aux ppf Var.dump s
let pp ppf s = pp_aux ppf Var.pp s
let printf = pp Format.std_formatter
end
(* tlv : top level variables
* fv : all free variables in the subtree *)
type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool }
let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true }
(* return the max of top level variables *)
let max x = Set.max_elt x.tlv
let pair x y = {
tlv = Set.empty ;
fv = Var.Set.union x.fv y.fv ;
isvar = false
}
let record x = {
tlv = Set.empty ;
fv = x.fv ;
isvar = false
}
(* true if it contains only one variable *)
let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1)
let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0)
let has_toplevel t = Set.cardinal t.tlv > 0
let pp ppf x = Set.pp ppf x.tlv
let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv
let printf = pp Format.std_formatter
let mem v x = Set.mem v x.tlv
end
(* module TLV = struct *)
(* module Set = struct *)
(* include Set.Make( *)
(* struct *)
(* type t = (Var.var * bool) *)
(* let compare (v1,p1) (v2,p2) = *)
(* let c = Var.compare v1 v2 in *)
(* if c == 0 then *)
(* if p1 == p2 then 0 *)
(* else if p1 then 1 else -1 *)
(* else c *)
(* end) *)
(* let pp_aux ppf pp_elem s = *)
(* let f ppf = function *)
(* |(v,true) -> Format.fprintf ppf "%a" pp_elem v *)
(* |(v,false) -> Format.fprintf ppf "~ %a" pp_elem v *)
(* in *)
(* Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s) *)
(* let dump ppf s = pp_aux ppf Var.dump s *)
(* let pp ppf s = pp_aux ppf Var.pp s *)
(* let printf = pp Format.std_formatter *)
(* end *)
(* (\* tlv : top level variables *)
(* * fv : all free variables in the subtree *\) *)
(* type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool } *)
(* let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true } *)
(* (\* return the max of top level variables *\) *)
(* let max x = Set.max_elt x.tlv *)
(* let pair x y = { *)
(* tlv = Set.empty ; *)
(* fv = Var.Set.union x.fv y.fv ; *)
(* isvar = false *)
(* } *)
(* let record x = { *)
(* tlv = Set.empty ; *)
(* fv = x.fv ; *)
(* isvar = false *)
(* } *)
(* (\* true if it contains only one variable *\) *)
(* let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1) *)
(* let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0) *)
(* let has_toplevel t = Set.cardinal t.tlv > 0 *)
(* let pp ppf x = Set.pp ppf x.tlv *)
(* let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv *)
(* let printf = pp Format.std_formatter *)
(* let mem v x = Set.mem v x.tlv *)
(* end *)
module rec Descr :
sig
......@@ -233,9 +233,6 @@ sig
* absent . It is used for optional arguments in functions as ?Int
* is the union of Int ^ undef where undef is a type with absent : true *)
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 : TLV.t
}
include Custom.T with type t = s
val empty: t
......@@ -253,12 +250,11 @@ struct
record: BoolRec.t;
abstract: BoolAbstracts.t;
absent: bool;
toplvars : TLV.t
}
type t = s
let dump ppf d =
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n%a"
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n"
BoolAtoms.dump d.atoms
BoolIntervals.dump d.ints
BoolChars.dump d.chars
......@@ -268,7 +264,6 @@ struct
BoolPair.dump d.xml
BoolAbstracts.dump d.abstract
d.absent
TLV.dump d.toplvars
let empty = {
times = BoolPair.empty;
......@@ -279,8 +274,7 @@ struct
atoms = BoolAtoms.empty;
chars = BoolChars.empty;
abstract = BoolAbstracts.empty;
absent= false;
toplvars = TLV.empty
absent = false;
}
(*
......@@ -297,7 +291,6 @@ struct
chars = BoolChars.full;
abstract = BoolAbstracts.full;
absent= false;
toplvars = TLV.any
}
let check a =
......@@ -430,30 +423,15 @@ 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 = 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 }
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))) }
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 record label t =
{ empty with
record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t)));
toplvars = TLV.record (descr t).toplvars }
let tlv_from_rec (_, l) =
let rec aux acc = function
| (_, n) :: rest -> aux (TLV.pair acc (descr n).toplvars) rest
| [] -> acc in
aux TLV.empty (Ident.LabelMap.get l)
{ 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));
toplvars = tlv_from_rec x }
{ empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
......@@ -467,71 +445,25 @@ let var a = {
atoms = BoolAtoms.vars a;
chars = BoolChars.vars a;
abstract = BoolAbstracts.vars a;
absent= false;
toplvars = TLV.singleton (a,true)
absent = false;
}
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
let update_tlv x y t =
let open TLV in
let tlv t =
let aux get bdd : Set.t =
let l =
List.fold_left (fun acc (p,n) ->
let acc1 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,true))
|_ -> acc
) Set.empty p
in
let acc2 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,false))
|_ -> assert false
) acc1 n
in acc2::acc
) [] (get bdd)
in
match l with
|[] -> Set.empty
|[h] -> h
|h::l -> List.fold_left Set.union h l
in
List.fold_left Set.union
(aux BoolChars.get t.chars)
[
(aux BoolIntervals.get t.ints);
(aux BoolAtoms.get t.atoms);
(aux BoolPair.get t.arrow);
(aux BoolPair.get t.xml);
(aux BoolRec.get t.record)
]
in
let fv t =
if Descr.is_empty t || equal t Descr.any then Var.Set.empty
else Var.Set.union x.toplvars.fv y.toplvars.fv
in
let toplvars = { tlv = tlv t ; fv = fv t ; isvar = t.toplvars.isvar } in
{ t with toplvars = 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 = BoolAbstracts.atom (`Atm a) }
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.fv
let all_tlv t = t.toplvars.TLV.tlv
module type BVS =
sig
type elem
type t
val get : t -> (elem list* elem list) list
end
let is_closed delta t = (no_var t) || (Var.Set.is_empty (Var.Set.diff (all_vars t) delta))
let cup x y =
if x == y then x else
let t = {
{
times = BoolPair.cup x.times y.times;
xml = BoolPair.cup x.xml y.xml;
arrow = BoolPair.cup x.arrow y.arrow;
......@@ -540,15 +472,12 @@ let cup x y =
atoms = BoolAtoms.cup x.atoms y.atoms;
chars = BoolChars.cup x.chars y.chars;
abstract = BoolAbstracts.cup x.abstract y.abstract;
absent= x.absent || y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
absent = x.absent || y.absent;
}
let cap x y =
if x == y then x else
let t = {
{
ints = BoolIntervals.cap x.ints y.ints;
times = BoolPair.cap x.times y.times;
xml = BoolPair.cap x.xml y.xml;
......@@ -558,14 +487,11 @@ let cap x y =
chars = BoolChars.cap x.chars y.chars;
abstract = BoolAbstracts.cap x.abstract y.abstract;
absent= x.absent && y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
}
let diff x y =
if x == y then empty else
let t = {
{
times = BoolPair.diff x.times y.times;
xml = BoolPair.diff x.xml y.xml;
arrow = BoolPair.diff x.arrow y.arrow;
......@@ -575,10 +501,7 @@ let diff x y =
chars = BoolChars.diff x.chars y.chars;
abstract = BoolAbstracts.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
toplvars = TLV.empty
} in
let isvar = (equal x any && is_var y) || (is_var x && equal y empty) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
}
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
......@@ -1084,6 +1007,122 @@ let subtype d1 d2 = is_empty (diff d1 d2)
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
(* functions on variables need the subtyping relation *)
let get_variables =
let memo_descr = DescrHash.create 17 in
fun t ->
let get_vars_conj get_atom pos acc l =
List.fold_left (fun acc e ->
get_atom pos acc e) acc l
in
let get_vars_bdd (type s) (type e)
(module BV : BVS with type elem = e and type t = s)
get_atom _pos acc bdd
=
List.fold_left (fun ((tlvp, tlvn, vars) as acc) (p, n) ->
let acc' = get_vars_conj get_atom true acc p in
get_vars_conj get_atom false acc' n
) acc (BV.get bdd)
in
let get_vars_boolvar get_atom pos (tlvp, tlvn, vars) = function
| (`Var v ) as x when pos -> Var.Set.add x tlvp, tlvn, Var.Set.add x vars
| (`Var v ) as x -> tlvp, Var.Set.add x tlvn, Var.Set.add x vars
| `Atm x ->
let _, _, vars' = get_atom pos (Var.Set.empty, Var.Set.empty, vars) x
in
tlvp, tlvn, vars'
in
let get_nothing _ acc _ = acc in
let rec get_pair pos acc (t1, t2) =
let acc1 = get_variables pos acc (descr t1) in
get_variables pos acc1 (descr t2)
and get_record pos acc (_, lmap) =
LabelMap.fold (fun _ t acc -> get_variables pos acc (descr t)) lmap acc
and get_bdd_pair pos = get_vars_bdd (module Pair) (get_pair) pos
and get_bdd_record pos = get_vars_bdd (module Rec) (get_record) pos
and get_bv_pairs pos = get_vars_bdd (module BoolPair)
(get_vars_boolvar get_bdd_pair) pos
and get_bv_recs pos = get_vars_bdd (module BoolRec)
(get_vars_boolvar get_bdd_record) pos
and get_variables pos (tvpos,tvneg,vars) t =
let tpos, tneg, tvars =
try
let r = DescrHash.find memo_descr t in
r
with
Not_found ->
let acc = Var.Set.(empty,empty,empty) in
DescrHash.add memo_descr t acc;
let acc = get_vars_bdd (module BoolIntervals)
(get_vars_boolvar get_nothing) pos acc t.ints in
let acc = get_vars_bdd (module BoolChars)
(get_vars_boolvar get_nothing) pos acc t.chars in
let acc = get_vars_bdd (module BoolAtoms)
(get_vars_boolvar get_nothing) pos acc t.atoms in
let acc = get_vars_bdd (module BoolAbstracts)
(get_vars_boolvar get_nothing) pos acc t.abstract in
let acc = get_bv_pairs pos acc t.times in
let acc = get_bv_pairs pos acc t.xml in
let acc = get_bv_pairs pos acc t.arrow in
let acc = get_bv_recs pos acc t.record in
DescrHash.replace memo_descr t acc;
acc
in
(Var.Set.union tvpos tpos,
Var.Set.union tvneg tneg,
Var.Set.union tvars vars)
in
try
DescrHash.find memo_descr t
with
Not_found ->
let res = get_variables true Var.Set.(empty,empty,empty) t in
DescrHash.add memo_descr t res;
res
let check_var =
let aux t =
let tvpos, tvneg, tvars = get_variables t in
match Var.Set.(cardinal tvpos, cardinal tvneg, cardinal tvars) with
1, 0, 1 -> let v = Var.Set.choose tvpos in
if equiv (var v) t then `Pos v else `NotVar
| 0, 1, 1 -> let v = Var.Set.choose tvneg in
if equiv (diff any (var v)) t then `Neg v else `NotVar
| _ -> `NotVar
in
let memo_descr = DescrHash.create 17 in
fun t -> try DescrHash.find memo_descr t with
Not_found ->
let res = aux t in
DescrHash.add memo_descr t res;
res
let is_var t = match check_var t with `NotVar -> false | _ -> true
let no_var t =
let _, _, s = get_variables t in Var.Set.is_empty s
let has_tlv t =
let p, n, _ = get_variables t in
not Var.Set.(is_empty p && is_empty n)
let all_vars t =
let _, _, s = get_variables t in s
let all_tlv t =
let p , n, _ = get_variables t in Var.Set.union p n
let is_closed delta t =
Var.Set.(is_empty (diff (all_vars t) delta))
let extract_variable t =
match check_var t with
`Pos v -> v, true
| `Neg v -> v, false
| _ -> assert false
module Cache = struct
type 'a cache =
......@@ -3266,14 +3305,13 @@ module Tallying = struct
else begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
if is_var t then
let (v,p) = TLV.max t.toplvars in
let (v,p) = extract_variable t in
if Var.Set.mem v delta then CS.unsat
else
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton delta s
(* if there are no vars, and it is not empty then unsat *)
else if (*no_var t*) Var.Set.subset t.toplvars.TLV.fv delta
then CS.unsat
else if no_var t then CS.unsat
else begin
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in
......@@ -3439,7 +3477,7 @@ module Tallying = struct
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if is_var t then begin
let (beta,_) = TLV.max t.toplvars in
let (beta,_) = extract_variable t in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
aux alpha (s,t) acc1
......@@ -3565,7 +3603,7 @@ module Tallying = struct
let codomain ll =
List.fold_left (fun acc e ->
CS.E.fold (fun _ v acc ->
Var.Set.union v.toplvars.TLV.fv acc
Var.Set.union (all_vars v) acc
) e acc
) Var.Set.empty ll
......
types/var.ml
View file @ e8ebd69d
module V = struct
type t = { id : string; repr : string }
let dump ppf t =
......
types/var.mli
View file @ e8ebd69d
......@@ -30,6 +30,7 @@ module Set : sig
val cardinal : t -> int
val from_list : var list -> t
val fold : ('a -> var -> 'a) -> 'a -> t -> 'a
val choose : t -> var
end
type 'a pairvar = [ `Atm of 'a | var ]
......
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