Skip to content

C
cduce
Commit 3e105c5e authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files
Options

Further refactoring of the tallying code.

parent b17ef0fc
Show whitespace changes
Inline Side-by-side
Showing with 194 additions and 182 deletions
compile/lambda.ml
View file @ 3e105c5e
......@@ -26,7 +26,7 @@ type iface = (Types.descr * Types.descr) list
type sigma =
| Identity (* this is basically as Types.Tallying.CS.sat *)
| List of Type_tallying.CS.sl
| List of Type_tallying.Constr.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......@@ -104,7 +104,7 @@ module Print = struct
) ppf
in
function
|List ll -> Type_tallying.CS.pp_sl ppf ll
|List ll -> Type_tallying.Constr.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_vloc x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......
compile/lambda.mli
View file @ 3e105c5e
......@@ -26,7 +26,7 @@ type iface = (Types.t * Types.t) list
type sigma =
| Identity
| List of Type_tallying.CS.sl
| List of Type_tallying.Constr.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......
runtime/value.ml
View file @ 3e105c5e
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Type_tallying.CS.sl
| List of Type_tallying.Constr.sl
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......@@ -313,7 +313,7 @@ module Print = struct
) ppf
in
function
|List ll -> Type_tallying.CS.pp_sl ppf ll
|List ll -> Type_tallying.Constr.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......
runtime/value.mli
View file @ 3e105c5e
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Type_tallying.CS.sl
| List of Type_tallying.Constr.sl
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......
types/sortedList.ml
View file @ 3e105c5e
......@@ -32,6 +32,7 @@ sig
type 'a map
external get: 'a map -> (Elem.t * 'a) list = "%identity"
val add: Elem.t -> 'a -> 'a map -> 'a map
val replace: Elem.t -> 'a -> 'a map -> 'a map
val mem: Elem.t -> 'a map -> bool
val length: 'a map -> int
val domain: 'a map -> t
......@@ -320,6 +321,14 @@ module Make(X : Custom.T) = struct
| (l1,[]) -> l1
let add x v = union_disj [(x,v)]
let rec replace x v m =
match m with
[] -> [ (x,v) ]
| ((y, w) as t) :: q ->
let c = Elem.compare x y in
if c == 0 then (x, v) :: q
else if c > 0 then t :: (replace x v q)
else (* c < 0 *) (x, v) :: m
let rec mem x l =
match l with
......
types/sortedList.mli
View file @ 3e105c5e
......@@ -32,6 +32,7 @@ sig
type 'a map
external get: 'a map -> (Elem.t * 'a) list = "%identity"
val add: Elem.t -> 'a -> 'a map -> 'a map
val replace: Elem.t -> 'a -> 'a map -> 'a map
val mem: Elem.t -> 'a map -> bool
val length: 'a map -> int
val domain: 'a map -> t
......
types/type_tallying.ml
View file @ 3e105c5e
......@@ -8,12 +8,14 @@ let cap_product any_left any_right l =
(any_left,any_right)
l
type constr =
|Pos of (Var.t * Types.t) (** alpha <= t | alpha \in P *)
|Neg of (Types.t * Var.t) (** t <= alpha | alpha \in N *)
| Pos of (Var.t * Types.t) (** alpha <= t | alpha \in P *)
| Neg of (Types.t * Var.t) (** t <= alpha | alpha \in N *)
exception UnSatConstr of string
module CS = struct
module VarMap = Var.Set.Map
module Constr = struct
let semantic_compare t1 t2 =
let inf12 = Types.subtype t1 t2 in
......@@ -24,18 +26,18 @@ module CS = struct
assert (c <> 0);
c
(* constraint set : map to store constraints of the form (s <= alpha <= t) *)
module M = struct
(* Line : is a conjunction of constraints represented as map from variables to
lower and upper bounds:
(s <= alpha <= t)
*)
module Line = struct
type t = (Types.t * Types.t) VarMap.map
module Key = struct
type t = Var.t
let compare v1 v2 = Var.compare v1 v2
end
type key = Key.t
module VarMap = Map.Make(Key)
type t = (Types.t * Types.t) VarMap.t
let singleton = VarMap.singleton
let cardinal = VarMap.cardinal
let length = VarMap.length
(* a set of constraints m1 subsumes a set of constraints m2,
that is the solutions for m1 contains all the solutions for
......@@ -44,16 +46,16 @@ module CS = struct
there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
*)
let subsumes map1 map2 =
VarMap.for_all (fun v (i1, s1) ->
try let i2, s2 = VarMap.find v map2 in
List.for_all (fun (v,(i1, s1)) ->
try let i2, s2 = VarMap.assoc v map2 in
subtype i1 i2 && subtype s2 s1
with Not_found -> false
) map1
) (VarMap.get map1)
let pp ppf map =
let print ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.print v Print.pp_type s
) ppf (VarMap.bindings map)
) ppf (VarMap.get map)
let compare map1 map2 =
VarMap.compare (fun (i1,s1) (i2,s2) ->
......@@ -62,21 +64,22 @@ module CS = struct
else c) map1 map2
let add delta v (inf, sup) map =
if Var.Set.mem delta v then map
else
let new_i, new_s =
try
let old_i, old_s = VarMap.find v map in
let old_i, old_s = VarMap.assoc v map in
cup old_i inf,
cap old_s sup
with
Not_found -> inf, sup
in
if Var.Set.mem delta v then map
else VarMap.add v (new_i, new_s) map
VarMap.replace v (new_i, new_s) map
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold
let empty = VarMap.empty
let for_all = VarMap.for_all
let for_all f m = List.for_all (fun (k,v) -> f k v) (VarMap.get m)
end
(* equation set : (s < alpha < t) stored as
......@@ -110,7 +113,7 @@ module CS = struct
that are pairwise "non-subsumable"
*)
type t = M.t list
type t = Line.t list
let elements t = t
......@@ -121,15 +124,15 @@ module CS = struct
match l with
[] -> m :: acc
| mm :: ll ->
if M.subsumes m mm then List.rev_append ll (m::acc)
else if M.subsumes mm m then List.rev_append ll (mm::acc)
if Line.subsumes m mm then List.rev_append ll (m::acc)
else if Line.subsumes mm m then List.rev_append ll (mm::acc)
else loop m ll (mm::acc)
in
loop m l []
let singleton m = add m empty
let pp ppf s = Utils.pp_list ~delim:("{","}") M.pp ppf s
let pp ppf s = Utils.pp_list ~delim:("{","}") Line.print ppf s
let fold f l a = List.fold_left (fun e a -> f a e) a l
......@@ -160,8 +163,8 @@ module CS = struct
match s2 with
[] -> accs2, e1::result
| e2 :: ss2 ->
if M.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
else if M.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
if Line.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
else if Line.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
else loop ss2 (e2::accs2)
in
loop s2 []
......@@ -181,7 +184,7 @@ module CS = struct
[], _ | _, [] -> []
| _ ->
(* Perform the cartesian product. For each constraint m1 in s1,
m2 in s2, we add M.inter m1 m2 to the result.
m2 in s2, we add Line.inter m1 m2 to the result.
Optimisations:
- we use add to ensure that we do not add something that subsumes
a constraint set that is already in the result
......@@ -190,9 +193,9 @@ module CS = struct
*)
fold (fun m1 acc1 ->
fold (fun m2 acc2 ->
let merged = if M.subsumes m1 m2 then m2
else if M.subsumes m2 m1 then m1
else M.inter delta m1 m2
let merged = if Line.subsumes m1 m2 then m2
else if Line.subsumes m2 m1 then m1
else Line.inter delta m1 m2
in
add merged acc2
)
......@@ -201,7 +204,7 @@ module CS = struct
end
type s = S.t
type m = M.t
type m = Line.t
type es = ES.t
type sigma = Types.t E.t
module SUB = SortedList.FiniteCofinite(struct
......@@ -218,28 +221,28 @@ module CS = struct
let singleton c =
let constr =
match c with
|Pos (v,s) -> M.singleton v (empty,s)
|Neg (s,v) -> M.singleton v (s,any)
|Pos (v,s) -> Line.singleton v (empty,s)
|Neg (s,v) -> Line.singleton v (s,any)
in
S.singleton constr
let pp_s = S.pp
let pp_m = M.pp
let pp_m = Line.print
let pp_e = E.pp
let pp_sl ppf ll = Utils.pp_list ~delim:("{","}") E.pp ppf ll
let sat = S.singleton M.empty
let sat = S.singleton Line.empty
let unsat = S.empty
let union = S.union
let prod delta = S.inter delta
let merge delta = M.inter delta
let merge delta = Line.inter delta
end
let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let normabstract (t,_,_) = if Abstracts.is_empty t then CS.sat else CS.unsat
let normatoms (t,_,_) = if Atoms.is_empty t then Constr.sat else Constr.unsat
let normchars (t,_,_) = if Chars.is_empty t then Constr.sat else Constr.unsat
let normints (t,_,_) = if Intervals.is_empty t then Constr.sat else Constr.unsat
let normabstract (t,_,_) = if Abstracts.is_empty t then Constr.sat else Constr.unsat
let single_aux constr (b,v,p,n) =
let aux f constr l =
......@@ -284,31 +287,31 @@ let toplevel delta single norm_rec mem p n =
match (p,n) with
|([], (`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton (Neg (t, x))
Constr.singleton (Neg (t, x))
|((`Var x)::pos,[]) ->
let t = single (true,x,pos,[]) in
CS.singleton (Pos (x,t))
Constr.singleton (Pos (x,t))
|((`Var x)::pos, (`Var y)::neg) ->
if _compare delta x y < 0 then
let t = single (true,x,pos,n) in
CS.singleton (Pos (x,t))
Constr.singleton (Pos (x,t))
else
let t = single (false,y,p,neg) in
CS.singleton (Neg (t, y))
Constr.singleton (Neg (t, y))
|([`Atm a], (`Var x)::neg) ->
let t = single (false,x,p,neg) in
CS.singleton (Neg (t,x))
Constr.singleton (Neg (t,x))
|([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false
let big_prod delta f acc l =
List.fold_left (fun acc (pos,neg) ->
(* if CS.S.is_empty acc then acc else *)
CS.prod delta acc (f pos neg)
(* if Constr.S.is_empty acc then acc else *)
Constr.prod delta acc (f pos neg)
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
......@@ -337,7 +340,7 @@ let rec norm (t,delta,mem) =
let finished, cst = NormMemoHash.find mem (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in local table, finished = %b @]@\n" finished);
if finished then cst else CS.sat
if finished then cst else Constr.sat
with
Not_found ->
begin
......@@ -345,48 +348,48 @@ let rec norm (t,delta,mem) =
(* base cases *)
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
CS.sat
Constr.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
CS.unsat
Constr.unsat
end else if is_var t then begin
let (v,p) = Variable.extract t in
if Var.Set.mem delta v then begin
DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
CS.unsat (* if it is monomorphic, unsat *)
Constr.unsat (* if it is monomorphic, unsat *)
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
Constr.singleton s
end
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in
let mem = NormMemoHash.add mem (t,delta) (false, Constr.sat); mem in
let t = Iter.simplify t in
let aux single norm_aux acc l =
big_prod delta (toplevel delta single norm_aux mem) acc l
in
let acc = aux single_atoms normatoms CS.sat VarAtoms.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_atoms normatoms Constr.sat VarAtoms.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_chars normchars acc VarChars.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_ints normints acc VarIntervals.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_times normpair acc VarTimes.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_xml normpair acc VarXml.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_arrow normarrow acc VarArrow.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_abstract normabstract acc VarAbstracts.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" Constr.pp_s acc);
(* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc VarRec.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" Constr.pp_s acc);
let acc = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) ->
Constr.S.filter
(fun m -> Constr.Line.for_all (fun v (s, t) ->
if Var.Set.mem delta v then
(* constraint on a monomorphic variables must be trivial *)
let x = var v in subtype s x && subtype x t
......@@ -395,7 +398,7 @@ let rec norm (t,delta,mem) =
) m)
acc
in
DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" Constr.pp_s acc);
DEBUG normrec (Format.eprintf "@]@\n");
acc
end
......@@ -406,7 +409,7 @@ let rec norm (t,delta,mem) =
DEBUG normrec (Format.eprintf
"Leaving norm rec(%a) = %a@]@\n%!"
Print.pp_type t
CS.pp_s res
Constr.pp_s res
);
res
......@@ -423,7 +426,7 @@ let rec norm (t,delta,mem) =
and normpair (t,delta,mem) =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> CS.unsat
|[] -> Constr.unsat
|(s1,s2) :: rest -> begin
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
......@@ -431,9 +434,9 @@ and normpair (t,delta,mem) =
let con2 = norm (z2, delta, mem) in
let con10 = aux z1 t2 rest in
let con20 = aux t1 z2 rest in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod delta con11 con22
let con11 = Constr.union con1 con10 in
let con22 = Constr.union con2 con20 in
Constr.prod delta con11 con22
end
in
(* cap_product return the intersection of all (fst pos,snd pos) *)
......@@ -441,30 +444,30 @@ and normpair (t,delta,mem) =
let con1 = norm (t1, delta, mem) in
let con2 = norm (t2, delta, mem) in
let con0 = aux t1 t2 neg in
CS.union (CS.union con1 con2) con0
Constr.union (Constr.union con1 con2) con0
in
big_prod delta norm_prod CS.sat (Pair.get t)
big_prod delta norm_prod Constr.sat (Pair.get t)
and normrec (t,delta,mem) =
let norm_rec ((oleft,left),rights) =
let rec aux accus seen = function
|[] -> CS.sat
|[] -> Constr.sat
|(false,_) :: rest when oleft -> aux accus seen rest
|(b,field) :: rest ->
let right = seen @ rest in
snd (Array.fold_left (fun (i,acc) t ->
let di = diff accus.(i) t in
let accus' = Array.copy accus in accus'.(i) <- di ;
(i+1,CS.prod delta acc (CS.prod delta (norm (di,delta,mem)) (aux accus' [] right)))
) (0,CS.sat) field
(i+1,Constr.prod delta acc (Constr.prod delta (norm (di,delta,mem)) (aux accus' [] right)))
) (0,Constr.sat) field
)
in
let c = Array.fold_left (fun acc t -> CS.union (norm (t,delta,mem)) acc) CS.sat left in
CS.prod delta (aux left [] rights) c
let c = Array.fold_left (fun acc t -> Constr.union (norm (t,delta,mem)) acc) Constr.sat left in
Constr.prod delta (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) ->
if CS.S.is_empty acc then acc else CS.prod delta acc (norm_rec (p,n))
) CS.sat (get_record t)
if Constr.S.is_empty acc then acc else Constr.prod delta acc (norm_rec (p,n))
) Constr.sat (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
......@@ -482,14 +485,14 @@ and normrec (t,delta,mem) =
and normarrow (t,delta,mem) =
let rec norm_arrow pos neg =
match neg with
|[] -> CS.unsat
|[] -> Constr.unsat
|(t1,t2) :: n ->
let con1 = norm (descr t1, delta, mem) in (* [t1] *)
let con2 = aux (descr t1) (diff any (descr t2)) pos in
let con0 = norm_arrow pos n in
CS.union (CS.union con1 con2) con0
Constr.union (Constr.union con1 con2) con0
and aux t1 acc = function
|[] -> CS.unsat
|[] -> Constr.unsat
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
......@@ -497,11 +500,11 @@ and normarrow (t,delta,mem) =
let con2 = norm (acc1, delta, mem) in (* [(Any \ t2) ^ s2] *)
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod delta con11 con22
let con11 = Constr.union con1 con10 in
let con22 = Constr.union con2 con20 in
Constr.prod delta con11 con22
in
big_prod delta norm_arrow CS.sat (Pair.get t)
big_prod delta norm_arrow Constr.sat (Pair.get t)
......@@ -515,7 +518,7 @@ let norm delta t =
(* merge needs delta because it calls norm recursively *)
let rec merge m delta cache =
let res =
CS.M.fold (fun v (inf, sup) acc ->
Constr.Line.fold (fun v (inf, sup) acc ->
(* no need to add new constraints *)
if subtype inf sup then acc
else
......@@ -524,20 +527,20 @@ let rec merge m delta cache =
else
let cache, _ = Cache.find ignore x cache in
let n = norm delta x in
if CS.S.is_empty n then
if Constr.S.is_empty n then
raise (UnSatConstr "merge2");
let c1 = CS.prod delta (CS.S.singleton m) n
let c1 = Constr.prod delta (Constr.S.singleton m) n
in
let c2 =
CS.S.fold
Constr.S.fold
(fun m1 acc ->
CS.union acc (merge m1 delta cache))
c1 CS.S.empty
Constr.union acc (merge m1 delta cache))
c1 Constr.S.empty
in
CS.union c2 acc
) m CS.S.empty
Constr.union c2 acc
) m Constr.S.empty
in
if CS.S.is_empty res then CS.S.singleton m else res
if Constr.S.is_empty res then Constr.S.singleton m else res
let merge delta m = merge m delta Cache.emp
......@@ -547,15 +550,15 @@ let solve delta s =
let aux alpha (s,t) acc =
(* we cannot solve twice the same variable *)
assert(not(CS.E.mem alpha acc));
assert(not(Constr.E.mem alpha acc));
let v = Var.mk ~internal:true (Printf.sprintf "#%s" (Var.ident alpha)) in
let b = var v in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
CS.E.add alpha (cap (cup s b) t) acc
Constr.E.add alpha (cap (cup s b) t) acc
in
let aux1 m =
let cache = Hashtbl.create 17 in
CS.M.fold (fun alpha (s,t) acc ->
Constr.Line.fold (fun alpha (s,t) acc ->
if Hashtbl.mem cache alpha then acc else begin
Hashtbl.add cache alpha ();
(* if t containts only a toplevel variable and nothing else
......@@ -571,38 +574,38 @@ let solve delta s =
(* alpha = ( s v fresh) ^ t *)
aux alpha (s,t) acc;
end
) m CS.E.empty
) m Constr.E.empty
in
CS.S.fold (fun m acc -> CS.ES.add (aux1 m) acc) s CS.ES.empty
Constr.S.fold (fun m acc -> Constr.ES.add (aux1 m) acc) s Constr.ES.empty
let unify e =
let rec aux sol e =
(* Format.printf "e = %a\n" CS.print_e e; *)
if CS.E.is_empty e then sol
(* Format.printf "e = %a\n" Constr.print_e e; *)
if Constr.E.is_empty e then sol
else begin
let (alpha,t) = CS.E.min_binding e in
let (alpha,t) = Constr.E.min_binding e in
(* Format.printf "Unify -> %a = %a\n" Var.print alpha Print.pp_type t; *)
let e1 = CS.E.remove alpha e in
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
let e1 = Constr.E.remove alpha e in
(* Format.printf "e1 = %a\n" Constr.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* solve_rectype remove also all previously introduced fresh variables *)
let x = Substitution.solve_rectype t alpha in
(* Format.printf "X = %a %a %a\n" Var.print alpha Print.print x dump t; *)
let es =
CS.E.fold (fun beta s acc ->
CS.E.add beta (Substitution.single s (alpha,x)) acc
) e1 CS.E.empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
let sigma = aux ((CS.E.add alpha x sol)) es in
let talpha = CS.E.fold (fun v sub acc -> Substitution.single acc (v,sub)) sigma x in
CS.E.add alpha talpha sigma
Constr.E.fold (fun beta s acc ->
Constr.E.add beta (Substitution.single s (alpha,x)) acc
) e1 Constr.E.empty
in
(* Format.printf "es = %a\n" Constr.print_e es; *)
let sigma = aux ((Constr.E.add alpha x sol)) es in
let talpha = Constr.E.fold (fun v sub acc -> Substitution.single acc (v,sub)) sigma x in
Constr.E.add alpha talpha sigma
end
in
(* Format.printf "Begin e = %a\n" CS.print_e e; *)
let r = aux CS.E.empty e in
(* Format.printf "r = %a\n" CS.print_e r; *)
(* Format.printf "Begin e = %a\n" Constr.print_e e; *)
let r = aux Constr.E.empty e in
(* Format.printf "r = %a\n" Constr.print_e r; *)
r
exception Step1Fail
......@@ -612,32 +615,32 @@ let tallying delta l =
let n =
List.fold_left (fun acc (s,t) ->
let d = diff s t in
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod delta acc (norm delta d)
) CS.sat l
if is_empty d then Constr.sat
else if no_var d then Constr.unsat
else Constr.prod delta acc (norm delta d)
) Constr.sat l
in
if Pervasives.(n = CS.unsat) then raise Step1Fail else
if Pervasives.(n = Constr.unsat) then raise Step1Fail else
let m =
CS.S.fold (fun c acc ->
try CS.ES.union (solve delta (merge delta c)) acc
Constr.S.fold (fun c acc ->
try Constr.ES.union (solve delta (merge delta c)) acc
with UnSatConstr _ -> acc
) n CS.ES.empty
) n Constr.ES.empty
in
if CS.ES.is_empty m then raise Step2Fail else
if Constr.ES.is_empty m then raise Step2Fail else
let el =
CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc ) m CS.ES.empty
Constr.ES.fold (fun e acc -> Constr.ES.add (unify e) acc ) m Constr.ES.empty
in
(CS.ES.elements el)
(Constr.ES.elements el)
(* apply sigma to t *)
let (>>) t si = CS.E.fold (fun v sub acc -> Substitution.single acc (v,sub)) si t
let (>>) t si = Constr.E.fold (fun v sub acc -> Substitution.single acc (v,sub)) si t
type symsubst = I | S of CS.sigma | A of (symsubst * symsubst)
type symsubst = I | S of Constr.sigma | A of (symsubst * symsubst)
let rec dom = function
|I -> Var.Set.empty
|S si -> CS.E.fold (fun v _ acc -> Var.Set.add v acc) si Var.Set.empty
|S si -> Constr.E.fold (fun v _ acc -> Var.Set.add v acc) si Var.Set.empty
|A (si,sj) -> Var.Set.cup (dom si) (dom sj)
(* composition of two symbolic substitution sets sigmaI, sigmaJ .
......@@ -654,7 +657,7 @@ let (++) sI sJ =
let (@@) t si =
let vst = ref Var.Set.empty in
let vsi = ref Var.Set.empty in
let get e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
let get e = Constr.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
let filter t si =
vsi := get si;
vst := all_vars t;
......@@ -675,26 +678,26 @@ let (@@) t si =
let domain sl =
List.fold_left (fun acc si ->
CS.E.fold (fun v _ acc ->
Constr.E.fold (fun v _ acc ->
Var.Set.add v acc
) si acc
) Var.Set.empty sl
let codomain ll =
List.fold_left (fun acc e ->
CS.E.fold (fun _ v acc ->
Constr.E.fold (fun _ v acc ->
Var.Set.cup (all_vars v)