add unify function and complete tallying problem

types/types.ml

@@ -136,6 +136,8 @@ 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 rec Descr : 
 sig
   (* each kind is represented as a union of itersection of types 
@@ -167,7 +169,10 @@ sig
     (* this is used in record to flag the fact that the type of a label is
      * 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
+    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
   }
   include Custom.T with type t = s
   val empty: t
@@ -182,7 +187,8 @@ struct
     arrow : BoolPair.t;
     record: BoolRec.t;
     abstract: Abstract.t;
-    absent: bool
+    absent: bool;
+    toplvars : tlvs
   }
   type t = s
 
@@ -208,6 +214,7 @@ struct
     chars = BoolChars.empty;
     abstract = Abstract.empty;
     absent= false;
+    toplvars = { s = Var.Set.empty ; b = true }
   }
 
   let equal a b =
@@ -331,6 +338,7 @@ let any =  {
   chars = BoolChars.full;
   abstract = Abstract.any;
   absent= false;
+  toplvars = { s = Var.Set.empty ; b = true }
 }
 
 let non_constructed =
@@ -341,7 +349,7 @@ 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))) }
+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 record label t = 
@@ -361,6 +369,7 @@ let var a =  {
   chars = BoolChars.vars a;
   abstract = Abstract.any;
   absent= false;
+  toplvars = { s = Var.Set.singleton a; b = true }
 }
 
 let char c = { empty with chars = BoolChars.atom (`Atm c) }
@@ -383,6 +392,7 @@ 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 }
   }
 
 (* intersection 
@@ -398,6 +408,7 @@ 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 }
   }
 
 (* 
@@ -419,6 +430,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 }
   }
     
 (* TODO: optimize disjoint check for boolean combinations *)
@@ -504,7 +516,54 @@ let get_record r =
     (labels,p,n)
   in
   List.map line (Rec.get r)
-   
+
+(* substitute all occurrences of v in t by s *)
+let rec subst v (t,s) =
+  let module C ( X : BoolVar.S ) = 
+    struct
+      let atom_aux ?f v (s,ss) = 
+        let open X in function
+          |`Var z when (Pervasives.compare (`Var z) v) = 0 -> ss
+          |`Var z -> vars (`Var z)
+          |`Atm constr ->
+              begin match f with
+              |None -> atom (`Atm constr)
+              |Some f -> f constr v (s,ss)
+              end
+          |_ -> assert false
+
+      let subst ?f v s bdd = 
+        let open X in
+        let atom z = atom_aux ?f v s z in
+        compute ~empty ~full ~cup ~cap ~diff ~atom bdd
+    end
+  in
+  let subtimes t v (s,_) =
+    List.fold_left (fun acc (left,rigth) ->
+      let deep_subst l = 
+        List.fold_left (fun acc (t1,t2) -> 
+          let d1 = cons (subst v (descr t1,s)) in 
+          let d2 = cons (subst v (descr t2,s)) in
+          BoolPair.cap acc (BoolPair.atom (`Atm (Pair.atom (d1,d2))))
+        ) BoolPair.full l
+      in
+      let acc1 = BoolPair.diff (deep_subst left) (deep_subst rigth) in
+      BoolPair.cup acc acc1
+    ) BoolPair.empty (Pair.get t)
+  in
+  {
+    atoms = (let module M = C(BoolAtoms) in M.subst) v (s,s.atoms) t.atoms;
+    ints  = (let module M = C(BoolIntervals) in M.subst) v (s,s.ints) t.ints;
+    chars = (let module M = C(BoolChars) in M.subst) v (s,s.chars) t.chars;
+    times = (let module M = C(BoolPair) in M.subst) ~f:subtimes v (s,s.times) t.times;
+    xml   = (let module M = C(BoolPair) in M.subst) ~f:subtimes v (s,s.xml) t.xml;
+    record= (let module M = C(BoolRec) in M.subst) v (s,s.record) t.record;
+    arrow = (let module M = C(BoolPair) in M.subst) ~f:subtimes v (s,s.arrow) t.arrow;
+    abstract = t.abstract;
+    absent= t.absent;
+    toplvars = { t.toplvars with s = Var.Set.remove v t.toplvars.s }
+  }
+
 (* Subtyping algorithm *)
 
 let diff_t d t = diff d (descr t)
@@ -2485,14 +2544,12 @@ module Tallying = struct
       CS.M.fold (fun (b,v) s acc ->
         try
           let t = CS.M.find (not b,v) m in
-          (*
-          try
-            let z = justavar t in
-            let acc1 = CS.E.add z (if b then (any,s) else (s,empty)) acc in
-            CS.E.add v (if b then (any,t) else (t,empty)) acc1
-          with Not_found -> 
-            *)
-          if b then aux v (t,s) acc else aux v (s,t) acc
+          if t.toplvars.b && (Var.Set.cardinal t.toplvars.s) = 1 then begin
+            let z = Var.Set.max_elt t.toplvars.s in
+            let acc1 = if b then aux v (empty,t) acc else aux v (t,any) acc in
+            if b then aux z (empty,any) acc else aux v (empty,any) acc1 
+          end else
+            if b then aux v (t,s) acc else aux v (s,t) acc
         with Not_found ->
           if b then aux v (any,s) acc else aux v (s,empty) acc
       ) m CS.E.empty
@@ -2502,25 +2559,22 @@ module Tallying = struct
       CS.S.fold (fun m acc -> (solve m)::acc) l []
     with UnSatConstr -> []
 
-(*
   let unify e =
-    let aux acc e =
-      if CS.E.is_empty e then []
+    let rec aux acc e =
+      if CS.E.is_empty e then acc
       else
-        let (v,t) = CS.E.pop e in
-        let e1 = CS.E.remove (v,t) e in
-        let x = fresh () in
+        let (alpha,t) = CS.E.min_binding e in
+        let e1 = CS.E.remove alpha e in
+        let x = Var.fresh () in
         (* replace in e1 all occurrences of a by ... *)
-        aux (t,a,x)::acc (subst e1 t a x)
+        let es = CS.E.fold (fun beta t acc -> CS.E.add beta (subst alpha (t,var x)) acc) e1 CS.E.empty in
+        aux (CS.E.add alpha (subst alpha (t,var x)) acc) es
     in
-    aux e
-*)
+    aux CS.E.empty e
+
   let tallying l =
     let n = List.fold_left (fun acc (s,t) -> CS.cap acc (norm(diff s t))) CS.S.empty l in
     let m = CS.S.fold (fun c acc -> acc @ (merge (c))) n [] in
-    m
-    (*
     List.fold_left (fun acc e -> (unify e)::acc) [] m
-    *)
 
 end

types/types.mli

@@ -142,6 +142,8 @@ val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
 val empty_closed_record: t
 val empty_open_record: t
 
+val subst : Var.var -> t * t -> t
+
 (** Positive systems and least solutions **)
 
 module Positive :
@@ -382,6 +384,7 @@ module Tallying : sig
 
   val norm : t -> CS.s
   val merge : CS.m -> CS.e list
+  val unify : CS.e -> CS.e
   val tallying : (t * t) list -> CS.e list
 
 end

types/var.ml

@@ -28,3 +28,9 @@ let fresh : unit -> var =
     let v = `Var (Printf.sprintf "_fresh_%d" !counter) in
     incr counter;
     v
+
+module Set = Set.Make(
+  struct 
+    type t = var
+    let compare = Pervasives.compare
+  end)