Generalize substutution function in Types

- The substutution function can return types that are semantically
  equal but not phisically equal. All data structures now use
  a total order that checks semantic equality.

tests/libtest/typesTest.ml

@@ -39,6 +39,7 @@ let subst_tests = [
   "`$A | Int", "A", "Bool", "Bool | Int";
   "`$A | `$B | Int", "A", "Bool", "Bool | `$B | Int";
   "`$A -> `$B", "A", "Bool", "Bool -> `$B";
+  "Bool -> `$B", "A", "Bool", "Bool -> `$B";
   "(`$A , `$B)", "A", "Bool", "(Bool, `$B)";
   "(`$A , (`$B -> (Bool -> `$C)))", "C", "Int", "(`$A , (`$B -> (Bool -> Int)))";
 ];;
@@ -52,7 +53,7 @@ let test_set_operations =
           let s = parse_typ s in
           let expected = parse_typ expected in
           let result = Types.subst t (v,s) in
-          assert_equal ~cmp:Types.equal ~printer:(fun t -> Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)) expected result
+          assert_equal ~cmp:Types.equiv ~printer:(fun t -> Format.sprintf "dump = %s\nrepr = %s\n" (to_string Types.dump t) (to_string Types.Print.print t)) expected result
       )
     ) subst_tests
 ;;

types/types.ml

@@ -520,7 +520,7 @@ let get_record r =
   in
   List.map line (Rec.get r)
 
-(* substitute in t all occurrences of v by s *)
+(*
 let rec subst t (v,s) =
   let module C ( X : BoolVar.S ) = 
     struct
@@ -570,7 +570,103 @@ let rec subst t (v,s) =
     absent= t.absent;
     toplvars = { t.toplvars with s = Var.Set.remove v t.toplvars.s }
   }
+*)
+
+(* substitute variables occurring in t accoding to the function subvar *)
+let rec substfree_aux subvar t =
+  let module C ( X : BoolVar.S ) = 
+    struct
+      let atom_aux ?noderec subvar = 
+        let open X in function
+          (* this subvar is acutally specialized on subatoms, subints, etc ... *)
+          |`Var z -> subvar vars (`Var z)
+          |`Atm bdd when X.T.is_empty bdd || X.T.is_full bdd -> atom (`Atm bdd)
+          |`Atm bdd ->
+              begin match noderec with
+              |None -> atom (`Atm bdd)
+              |Some f -> f bdd (* f = subpairs ... *)
+              end
+          |_ -> assert false
 
+      let subst ?noderec subvar bdd = 
+        let open X in
+        let atom z = atom_aux ?noderec subvar z in
+        compute ~empty ~full:`True ~cup ~cap ~diff ~atom bdd
+    end
+  in
+  let subpairs bdd =
+    List.fold_left (fun acc (left,rigth) ->
+      let deep_subst f l = 
+        List.fold_left (fun acc (t1,t2) -> 
+          (* this subvar is the general one ! *)
+          let d1 = cons (substfree_aux subvar (descr t1)) in 
+          let d2 = cons (substfree_aux subvar (descr t2)) in
+          BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
+        ) BoolPair.full l
+      in
+      let neg_atm x = BoolPair.diff BoolPair.full x in
+      let pos_atm x = x in
+      let acc1 = BoolPair.cap (deep_subst pos_atm left) (deep_subst neg_atm rigth) in
+      BoolPair.cup acc acc1
+    ) BoolPair.empty (Pair.get bdd)
+  in
+  let subatoms vars v = match subvar v with |`Constr s -> s.atoms |`Var z -> vars (`Var z) in
+  let subints vars v = match subvar v with |`Constr s -> s.ints |`Var z -> vars (`Var z) in
+  let subchars vars v = match subvar v with |`Constr s -> s.chars |`Var z -> vars (`Var z) in
+  let subarrow vars v = match subvar v with |`Constr s -> s.arrow |`Var z -> vars (`Var z) in
+  let subxml vars v = match subvar v with |`Constr s -> s.xml |`Var z -> vars (`Var z) in
+  let subtimes vars v = match subvar v with |`Constr s -> s.times |`Var z -> vars (`Var z) in
+  let subrecord vars v = match subvar v with |`Constr s -> s.record |`Var z -> vars (`Var z) in
+  let tlv s =
+    Var.Set.fold (fun v acc ->
+      match subvar v with 
+      |`Var z -> Var.Set.add (`Var z) acc
+      |_ -> acc
+    ) s Var.Set.empty
+  in
+  {
+    atoms = (let module M = C(BoolAtoms) in M.subst) subatoms t.atoms;
+    ints  = (let module M = C(BoolIntervals) in M.subst) subints t.ints;
+    chars = (let module M = C(BoolChars) in M.subst) subchars t.chars;
+    times = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subtimes t.times;
+    xml   = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subxml t.xml;
+    (* XXX record still not done . need to define ~f:subrecord *)
+    record= (let module M = C(BoolRec) in M.subst) subrecord t.record;
+    arrow = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subarrow t.arrow;
+    abstract = t.abstract;
+    absent= t.absent;
+    toplvars = { t.toplvars with s = tlv (t.toplvars.s) }
+  }
+
+(* substitute in t all occurrences of v by the type s *)
+let subst t (v,s) =
+  let subvar (`Var v,s) (`Var z) =
+    if Var.equal (`Var v) (`Var z) then `Constr s else (`Var z)
+  in
+  substfree_aux (subvar (v,s)) t
+
+(* substitute in t all variables with a free variables *)
+(* using a Hashtbl here hides lots of in place modifications *)
+(* the hashtbl can be used to remember all substitutions *)
+let substfree t =
+  let subvar tbl v =
+    try Hashtbl.find tbl v
+    with Not_found -> begin
+      let z = Var.fresh () in
+      Hashtbl.add tbl v z;
+      z
+    end
+  in
+  substfree_aux (subvar (Hashtbl.create 197)) t
+(*
+let substvariance t =
+  let subvar ?(variance=`Variant) (`Var z) =
+    match variance with
+    |`Variant -> empty
+    |`CoVariant -> any
+  in
+  substfree subvar t 
+*)
 (* Subtyping algorithm *)
 
 let diff_t d t = diff d (descr t)
@@ -993,7 +1089,6 @@ let subtype d1 d2 = is_empty (diff d1 d2)
 
 let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
 
-
 module Cache = struct
 
   type 'a cache =
@@ -2035,19 +2130,25 @@ end
 
 module Positive =
 struct
-  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
+  type rhs = [
+    |`Type of descr
+    |`Cup of v list
+    |`Cap of v list
+    |`Arrow of v * v 
+    |`Times of v * v
+    |`Xml of v * v ]
   and v = { mutable def : rhs; mutable node : node option }
 
-
   let rec make_descr seen v =
     if List.memq v seen then empty
     else
       let seen = v :: seen in
       match v.def with
 	| `Type d -> d
-	| `Cup vl -> 
-	    List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
+	| `Cup vl -> List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
+	| `Cap vl -> List.fold_left (fun acc v -> cap acc (make_descr seen v)) any vl
 	| `Times (v1,v2) -> times (make_node v1) (make_node v2)
+	| `Arrow (v1,v2) -> arrow (make_node v1) (make_node v2)
 	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
 
   and make_node v =
@@ -2065,7 +2166,9 @@ struct
   let cons d = let v = forward () in def v d; v
   let ty d = cons (`Type d)
   let cup vl = cons (`Cup vl)
+  let cap vl = cons (`Cap vl)
   let times d1 d2 = cons (`Times (d1,d2))
+  let arrow d1 d2 = cons (`Arrow (d1,d2))
   let xml d1 d2 = cons (`Xml (d1,d2))
   let define v1 v2 = def v1 (`Cup [v2]) 
 
@@ -2274,7 +2377,6 @@ module Tallying = struct
       |[] -> Format.fprintf ppf "{}"
       |_ -> Format.fprintf ppf "{ %a }" aux l
 
-
     (* constraint set : map to store constraints of the form (alpha,t) or (t,alpha) *)
     module M = struct 
       include Map.Make(struct
@@ -2284,7 +2386,6 @@ module Tallying = struct
           else Pervasives.compare b1 b2
       end)
 
-
       let print ppf m =
         print_lst (fun ppf -> fun ((b,`Var v),s) ->
           if b then
@@ -2310,11 +2411,18 @@ module Tallying = struct
 
     end
 
+    (* we require that types are semantically equivalent and not structurally
+     * equivalent *)
+    let semantic_compare t1 t2 =
+      if Descr.equal t1 t2 then 0
+      else if equiv t1 t2 then 0
+      else Descr.compare t1 t2
+
     (* Set of equation sets *)
     module ES = struct
       include Set.Make(struct
         type t = Descr.s E.t
-        let compare = E.compare Descr.compare
+        let compare = E.compare semantic_compare
       end)
 
       let print ppf s = print_lst E.print ppf (elements s)
@@ -2324,7 +2432,7 @@ module Tallying = struct
     module S = struct
       include Set.Make(struct
         type t = Descr.s M.t
-        let compare = M.compare Descr.compare
+        let compare = M.compare semantic_compare
 
       end)
 
@@ -2351,7 +2459,7 @@ module Tallying = struct
         |(k,None,None) -> assert false
         |(k,Some v,None) -> Some v
         |(k,None,Some v) -> Some v
-        |((_,v),Some x,Some y) when Descr.equal x y -> Some x
+        |((_,v),Some x,Some y) when equiv x y -> Some x
         |((true,v),Some x,Some y) -> Some (cap x y)
         |((false,v),Some x,Some y) -> Some (cup x y)
       in
@@ -2381,7 +2489,7 @@ module Tallying = struct
       |false,false ->
           S.fold (fun m1 acc ->
             S.fold (fun m2 acc1 ->
-              if (M.compare Descr.compare m1 m2) = 0 then S.add m1 acc1 else
+              if (M.compare semantic_compare m1 m2) = 0 then S.add m1 acc1 else
               if M.is_empty m1 then S.add m2 acc1 else
               if M.is_empty m2 then S.add m1 acc1 else
               begin match (lessgeneral m1 m2),(lessgeneral m2 m1) with