Commit b17ef0fc authored by Kim Nguyễn's avatar Kim Nguyễn

Refactor the Var module to use saner names.

parent d53ca3c7
......@@ -16,7 +16,7 @@ let pp_vars ppf vars =
Ident.pp_env pp_item ppf vars
let pp_xi ppf xi =
let pp_item ppf (s,t) = Format.fprintf ppf "%s : %a" s Var.Set.pp t in
let pp_item ppf (s,t) = Format.fprintf ppf "%s : %a" s Var.Set.print t in
Ident.pp_idmap pp_item ppf xi
let pp_env ppf env =
......
......@@ -8,8 +8,8 @@ let cap_product any_left any_right l =
(any_left,any_right)
l
type constr =
|Pos of (Var.var * Types.t) (** alpha <= t | alpha \in P *)
|Neg of (Types.t * Var.var) (** 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
......@@ -28,7 +28,7 @@ module CS = struct
module M = struct
module Key = struct
type t = Var.var
type t = Var.t
let compare v1 v2 = Var.compare v1 v2
end
type key = Key.t
......@@ -52,7 +52,7 @@ module CS = struct
let pp ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.pp v Print.pp_type s
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.print v Print.pp_type s
) ppf (VarMap.bindings map)
let compare map1 map2 =
......@@ -83,13 +83,13 @@ module CS = struct
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module E = struct
include Map.Make(struct
type t = Var.var
type t = Var.t
let compare = Var.compare
end)
let pp ppf e =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
Format.fprintf ppf "%a = %a@," Var.print v Print.pp_type t
) ppf (bindings e)
end
......@@ -548,7 +548,7 @@ let solve delta s =
let aux alpha (s,t) acc =
(* we cannot solve twice the same variable *)
assert(not(CS.E.mem alpha acc));
let v = Var.mk (Printf.sprintf "#fr_%s" (Var.id alpha)) in
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
......@@ -581,14 +581,14 @@ let unify e =
if CS.E.is_empty e then sol
else begin
let (alpha,t) = CS.E.min_binding e in
(* Format.printf "Unify -> %a = %a\n" Var.pp alpha Print.pp_type t; *)
(* 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; *)
(* 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.pp alpha Print.print x dump t; *)
(* 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
......
open Types
type constr =
| Pos of (Var.var * t) (** alpha <= t | alpha \in P *)
| Neg of (t * Var.var) (** t <= alpha | alpha \in N *)
| Pos of (Var.t * t) (** alpha <= t | alpha \in P *)
| Neg of (t * Var.t) (** t <= alpha | alpha \in N *)
exception UnSatConstr of string
exception Step1Fail
......@@ -10,7 +10,7 @@ exception Step2Fail
module CS : sig
module M : sig
type key = Var.var
type key = Var.t
type t
val compare : t -> t -> int
val empty : t
......@@ -20,7 +20,7 @@ module CS : sig
val inter : Var.Set.t -> t -> t -> t
end
module E : sig
include Map.S with type key = Var.var
include Map.S with type key = Var.t
val pp : Format.formatter -> descr t -> unit
end
module ES : sig
......
......@@ -1882,7 +1882,7 @@ module Print = struct
let is_regexp t = subtype t seqs_descr
type gname = string * Ns.QName.t * (Var.var * t) list
type gname = string * Ns.QName.t * (Var.t * t) list
type nd = {
id : int;
......@@ -2246,7 +2246,7 @@ module Print = struct
in
let print_vars l =
Var.Set.fold
(fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) [] l
(fun acc v -> (Atomic (fun ppf -> Var.print ppf v)) :: acc) [] l
in
let print_pnvars l =
List.fold_left (fun acc (p,n) ->
......@@ -3001,7 +3001,7 @@ module Positive = struct
type rhs = [
|`Type of descr
|`Variable of Var.var
|`Variable of Var.t
|`Neg of v
|`Cup of v list
|`Cap of v list
......@@ -3034,7 +3034,7 @@ module Positive = struct
MemoHash.add memo v node_name;
match v.def with
|`Type d -> Format.fprintf ppf "`Type(%a)" Print.pp_type d
|`Variable d -> Format.fprintf ppf "`Var(%a)" Var.pp d
|`Variable d -> Format.fprintf ppf "`Var(%a)" Var.print d
|`Cup vl -> Format.fprintf ppf "`Cup(%a)" (Utils.pp_list aux) vl
|`Cap vl -> Format.fprintf ppf "`Cap(%a)" (Utils.pp_list aux) vl
|`Times (v1,v2) -> Format.fprintf ppf "`Times(%a,%a)" aux v1 aux v2
......@@ -3188,7 +3188,7 @@ struct
let print ppf m =
Utils.pp_list (fun ppf (v, t) -> Format.fprintf ppf "%a:%a"
Var.pp v Print.pp_type t) ppf (Map.get m)
Var.print v Print.pp_type t) ppf (Map.get m)
let add v t m =
if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
......@@ -3279,13 +3279,7 @@ struct
let freshen delta t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.fresh v)) vars in
app_subst t subst
let kind delta k t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.set_kind k v)) vars in
let subst = Map.init (fun v -> var (Var.refresh v)) vars in
app_subst t subst
let solve_rectype t alpha =
......@@ -3305,26 +3299,11 @@ struct
Var.Set.pp pos Var.Set.pp neg Var.Set.pp all Var.Set.pp _tlv);
let vars = Var.Set.diff all delta in
if Var.Set.is_empty vars then t else
let idx = ref 0 in
let rec freshvar () =
let rec pretty i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^
(String.make 1 (OldChar.chr (OldChar.code 'a' + nm)))
in
if ni == 0 then acc else pretty ni acc
in
let x = Var.mk (pretty !idx "") in
if Var.Set.mem delta x then
(* if the name is taken by a variable in delta, restart *)
(incr idx; freshvar ())
else x
in
let subst = Map.init
(fun v ->
let is_pos = Var.Set.mem pos v in
let is_neg = Var.Set.mem neg v in
if is_pos && is_neg then var (freshvar ())
if is_pos && is_neg then var (Var.gen delta)
else if is_pos then empty else any
) vars
in
......@@ -3351,811 +3330,3 @@ struct
app_subst t subst
end
module Tallying = struct
type constr =
|Pos of (Var.var * Descr.t) (** alpha <= t | alpha \in P *)
|Neg of (Descr.t * Var.var) (** t <= alpha | alpha \in N *)
exception UnSatConstr of string
module CS = struct
(* we require that types are semantically equivalent and not structurally
* equivalent *)
let semantic_compare t1 t2 =
let c = Descr.compare t1 t2 in
if c = 0 then 0 else
if equiv t1 t2 then 0
else c
(* constraint set : map to store constraints of the form (s <= alpha <= t) *)
module M = struct
module Key = struct
type t = Var.var
let compare v1 v2 = Var.compare v1 v2
end
type key = Key.t
module VarMap = Map.Make(Key)
type t = (Descr.t * Descr.t) VarMap.t
let singleton = VarMap.singleton
let cardinal = VarMap.cardinal
(* a set of constraints m1 subsumes a set of constraints m2,
that is the solutions for m1 contains all the solutions for
m2 if:
forall i1 <= v <= s1 in m1,
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
subtype i1 i2 && subtype s2 s1
with Not_found -> false
) map1
let pp ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.pp v Print.pp_type s
) ppf (VarMap.bindings map)
let compare map1 map2 =
VarMap.compare (fun (i1,s1) (i2,s2) ->
let c = semantic_compare i1 i2 in
if c == 0 then semantic_compare s1 s2
else c) map1 map2
let add delta v (inf, sup) map =
let new_i, new_s =
try
let old_i, old_s = VarMap.find 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
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
end
(* equation set : (s < alpha < t) stored as
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module E = struct
include Map.Make(struct
type t = Var.var
let compare = Var.compare
end)
let pp ppf e =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
) ppf (bindings e)
end
(* Set of equation sets *)
module ES = struct
include Set.Make(struct
type t = Descr.t E.t
let compare = E.compare semantic_compare
end)
let pp ppf s = Utils.pp_list ~delim:("{","}") E.pp ppf (elements s)
end
(* Set of constraint sets *)
module S = struct
(* A set of constraint-sets is just a list of constraint-sets,
that are pairwise "non-subsumable"
*)
type t = M.t list
let elements t = t
let empty = []
let add m l =
let rec loop m l acc =
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)
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 fold f l a = List.fold_left (fun e a -> f a e) a l
let is_empty l = l == []
(* Square union : *)
let union s1 s2 =
match s1, s2 with
[], _ -> s2
| _, [] -> s1
| _ ->
(* Invariant: all elements of s1 (resp s2) are pairwise
incomparable (they don't subsume one another)
let e1 be an element of s1:
- if e1 subsumes no element of s2, add e1 to the result
- if e1 subsumes an element e2 of s2, add e1 to the
result and remove e2 from s2
- if an element e2 of s2 subsumes e1, add e2 to the
result and remove e2 from s2 (and discard e1)
once we are done for all e1, add the remaining elements from
s2 to the result.
*)
let append e1 s2 result =
let rec loop s2 accs2 =
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
else loop ss2 (e2::accs2)
in
loop s2 []
in
let rec loop s1 s2 result =
match s1 with
[] -> List.rev_append s2 result
| e1 :: ss1 ->
let new_s2, new_result = append e1 s2 result in
loop ss1 new_s2 new_result
in
loop s1 s2 []
(* Square intersection *)
let inter delta s1 s2 =
match s1,s2 with
[], _ | _, [] -> []
| _ ->
(* Perform the cartesian product. For each constraint m1 in s1,
m2 in s2, we add M.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
- if m1 subsumes m2, it means that whenever m2 holds, so does m1, so
we only add m2 (note that the condition is reversed w.r.t. union).
*)
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
in
add merged acc2
)
s2 acc1) s1 []
let filter = List.filter
end
type s = S.t
type m = M.t
type es = ES.t
type sigma = Descr.t E.t
module SUB = SortedList.FiniteCofinite(struct
type t = Descr.t E.t
let compare = E.compare compare
let equal = E.equal equal
let hash = Hashtbl.hash
let dump = E.pp
let check _ = ()
end)
type sl = sigma list
let singleton c =
let constr =
match c with
|Pos (v,s) -> M.singleton v (empty,s)
|Neg (s,v) -> M.singleton v (s,any)
in
S.singleton constr
let pp_s = S.pp
let pp_m = M.pp
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 unsat = S.empty
let union = S.union
let prod delta = S.inter delta
let merge delta = M.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 single_aux constr (b,v,p,n) =
let aux f constr l =
List.fold_left (fun acc ->
function
|`Var a -> cap acc (f(var a))
|`Atm a -> cap acc (f(constr a))
) any l
in
let id = (fun x -> x) in
let t = cap (aux id constr p) (aux neg constr n) in
(* t = bigdisj ... alpha \in P --> alpha <= neg t *)
(* t = bigdisj ... alpha \in N --> t <= alpha *)
if b then (neg t) else t
let single_atoms = single_aux atom
let single_abstract = single_aux abstract
let single_chars = single_aux char
let single_ints = single_aux interval
let single_times = single_aux (fun p -> { empty with times = VarTimes.atom (`Atm p) })
let single_xml = single_aux (fun p -> { empty with xml = VarXml.atom (`Atm p) })
let single_record = single_aux (fun p -> { empty with record = VarRec.atom (`Atm p) })
let single_arrow = single_aux (fun p -> { empty with arrow = VarArrow.atom (`Atm p) })
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
let _compare delta v1 v2 =
let monov1 = Var.Set.mem delta v1 in
let monov2 = Var.Set.mem delta v2 in
if monov1 == monov2 then
Var.compare v1 v2
else
if monov1 then 1 else -1
in
match (p,n) with
|([], (`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton (Neg (t, x))
|((`Var x)::pos,[]) ->
let t = single (true,x,pos,[]) in
CS.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))
else
let t = single (false,y,p,neg) in
CS.singleton (Neg (t, y))
|([`Atm a], (`Var x)::neg) ->
let t = single (false,x,p,neg) in
CS.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)
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17
let () = Format.pp_set_margin Format.err_formatter 100
let rec norm (t,delta,mem) =
DEBUG normrec (
Format.eprintf
" @[Entering norm rec(%a):@\n" Print.pp_type t);
let res =
try
(* If we find it in the global hashtable, we are finished *)
let res = NormMemoHash.find memo_norm (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in global table @]@\n");
res
with
Not_found ->
try
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
with
Not_found ->
begin
let res =
(* base cases *)
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
CS.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
CS.unsat
end else if is_var t then begin
let (v,p) = extract_variable 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 *)
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
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 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 t.atoms) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_chars normchars acc (VarChars.get t.chars) in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_ints normints acc (VarIntervals.get t.ints) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_times normpair acc (VarTimes.get t.times) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_xml normpair acc (VarXml.get t.xml) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_arrow normarrow acc (VarArrow.get t.arrow) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_abstract normabstract acc (VarAbstracts.get t.abstract) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
(* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc (VarRec.get t.record) in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);
let acc = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.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
else true (*
subtype s t || (non_empty (cap s t)) *)
) m)
acc
in
DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@]@\n");
acc
end
in
NormMemoHash.replace mem (t, delta) (true,res); res
end
in
DEBUG normrec (Format.eprintf
"Leaving norm rec(%a) = %a@]@\n%!"
Print.pp_type t
CS.pp_s res
);
res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
* [t1] v [t2] v ( [t1 \ s1] ^ [t2 \ s2] ^
* [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ... )
*
* prod(p,n) = [t1] v [t2] v prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
* ([t2\s2] v prod'(t1,t2\s2,n))
* *)
and normpair (t,delta,mem) =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> CS.unsat
|(s1,s2) :: rest -> begin
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
let con1 = norm (z1, delta, mem) in
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
end
in
(* cap_product return the intersection of all (fst pos,snd pos) *)
let (t1,t2) = cap_product any any pos in
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
in
big_prod delta norm_prod CS.sat (Pair.get t)
and normrec (t,delta,mem) =
let norm_rec ((oleft,left),rights) =
let rec aux accus seen = function
|[] -> CS.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
)
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
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)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
([t1\s1] v arrow'(t1\s1,acc,p)) ^
([acc ^ {s2}] v arrow'(t1,acc ^ {s2},p))
t1 -> t2 \ s1 -> s2 =
[t1] v (([t1\s1] v {[]}) ^ ([t2\s2] v {[]}))
Bool -> Bool \ Int -> A =
[Bool] v (([Bool\Int] v {[]}) ^ ([Bool\A] v {[]})
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
and normarrow (t,delta,mem) =
let rec norm_arrow pos neg =
match neg with
|[] -> CS.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
and aux t1 acc = function
|[] -> CS.unsat
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, delta, mem) in (* [t1 \ s1] *)
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
in
big_prod delta norm_arrow CS.sat (Pair.get t)
let norm delta t =
try NormMemoHash.find memo_norm (t,delta)
with Not_found -> begin
let res = norm (t,delta,NormMemoHash.create 17) in
NormMemoHash.add memo_norm (t,delta) res; res
end
(* merge needs delta because it calls norm recursively *)
let rec merge m delta cache =
let res =
CS.M.fold (fun v (inf, sup) acc ->
(* no need to add new constraints *)