Add test cases for Types.subst

- There is still an error in the type representation that
  is the result of a substitution.

parser/ast.ml

@@ -103,7 +103,7 @@ and branches = (ppat * pexpr) list
 
 and ppat = ppat' located
 and ppat' =
-  | TVar of Var.t (** type variables *)
+  | TVar of Var.t (** polymorphic type variables *)
   | PatVar of U.t list
   | Cst of pexpr
   | NsT of U.t

tests/libtest/boolvarTest.ml

@@ -12,17 +12,18 @@ let to_string pp t =
   Format.fprintf Format.str_formatter "%a@." pp t;
   Printf.sprintf "->%s<-" (Format.flush_str_formatter ())
 
-module BoolChars : S with type s = Chars.t = struct
-  include BoolVar.Make(Chars)
+module BoolAtoms : S with type s = Atoms.t = struct 
+  include BoolVar.Make(Atoms)
   let mk_var s = atom (`Var s)
-  let mk_atm c = atom (`Atm (Chars.atom (Chars.V.mk_char c.[0] )))
+  let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
   let to_string = to_string pp_print
 end
 
-module BoolAtoms : S with type s = Atoms.t = struct 
-  include BoolVar.Make(Atoms)
+(*
+module BoolChars : S with type s = Chars.t = struct
+  include BoolVar.Make(Chars)
   let mk_var s = atom (`Var s)
-  let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
+  let mk_atm c = atom (`Atm (Chars.atom (Chars.V.mk_char c.[0] )))
   let to_string = to_string pp_print
 end
 
@@ -32,6 +33,7 @@ module BoolIntervals : S with type s = Intervals.t = struct
   let mk_atm s = atom (`Atm (Intervals.atom (Intervals.V.mk s)))
   let to_string = to_string pp_print
 end
+*)
 
 module ExprParser (B : S) = struct
   open Camlp4.PreCast
@@ -53,6 +55,7 @@ module ExprParser (B : S) = struct
       |"Empty" -> B.empty
       |"atm"; x = LIDENT -> B.mk_atm x
       |"var"; x = LIDENT -> B.mk_var x
+
       |"("; x = SELF; ")" -> x ]
     ];
   END
@@ -63,9 +66,11 @@ module ExprParser (B : S) = struct
 
 end
 
-module BCP = ExprParser(BoolChars)
 module BAP = ExprParser(BoolAtoms)
+(*
+module BCP = ExprParser(BoolChars)
 module BIP = ExprParser(BoolIntervals)
+*)
 
 let atoms_tests = [
   "commutativity intersection", BAP.os "atm foo ^ atm bar", BAP.os "atm bar ^ atm foo";

tests/libtest/tallyingTest.ml

@@ -267,13 +267,24 @@ let mk_e ll =
 
 let tallying_tests = [
   [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
-    [("A","Int | Bool");("B","Int | Bool")]
+    [("A","Int | Bool");("B","Int | Bool")];
+    [("A","Empty");("B","Empty")]
   ];
+
+  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
+    [("A","Empty")];
+    [("A","Int");("B","Bool")];
+  ];
+
   [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
-    [("A","Empty");("B","Empty")];
+    [("A","Empty")];
   ];
+
   [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
-  [("(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[("A","Int");("B","Int")]];
+
+  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[]];
+
+  [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [[("A","Int");("B","Int")]];
 ]
 
 let test_tallying =

tests/libtest/typesTest.ml

@@ -9,11 +9,10 @@ let parse_typ s =
   Types.descr nodepat
 ;;
 
-(*
-let t1 = Types.descr (Typer.typ Builtin.env (Parser.pat (Stream.of_string "`A :> Int")) );;
-let t2 = Types.descr (Typer.typ Builtin.env (Parser.pat (Stream.of_string "Any")) );;
-Types.subtype  t1 t2 ;;
-*)
+let to_string pp t =
+  Format.fprintf Format.str_formatter "%a@." pp t;
+  Format.flush_str_formatter ()
+;;
 
 let set_op_tests = [
   "Int & `$B", "`$B & Int";
@@ -29,11 +28,34 @@ let test_set_operations =
       (Printf.sprintf " %s <: %s " s1 s2) >:: (fun _ ->
           let t1 = parse_typ s1 in
           let t2 = parse_typ s2 in
-          assert_equal ~cmp:Types.equal (* ~printer:(fun t -> Format.sprintf "%a" Types.Print.print t) *) t1 t2
+          assert_equal ~cmp:Types.equal ~printer:(to_string Types.Print.print) t1 t2
       )
     ) set_op_tests
 ;;
 
+let subst_tests = [
+  "`$A", "A", "Bool", "Bool";
+  "`$A", "A", "`$B", "`$B";
+  "`$A | Int", "A", "Bool", "Bool | Int";
+  "`$A | `$B | Int", "A", "Bool", "Bool | `$B | Int";
+  "`$A -> `$B", "A", "Bool", "Bool -> `$B";
+  "(`$A , `$B)", "A", "Bool", "(Bool, `$B)";
+  "(`$A , (`$B -> (Bool -> `$C)))", "C", "Int", "(`$A , (`$B -> (Bool -> Int)))";
+];;
+
+let test_set_operations =
+  "test set operations" >::: 
+    List.map (fun (t,v,s,expected) ->
+      (Printf.sprintf "[%s]{%s/%s}") t v s >:: (fun _ ->
+          let t = parse_typ t in
+          let v = `Var v in
+          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
+      )
+    ) subst_tests
+;;
 
 let subtype_tests = [
   "Int" , "Any", true;
@@ -115,12 +137,7 @@ let test_subtype =
           let t1 = parse_typ s1 in
           let t2 = parse_typ s2 in
           let result = Types.subtype t1 t2 in
-          if result <> expected then
-            begin
-              (* Printf.printf "subtyping error %s <: %s\n" s1 s2; *)
-              Printf.printf "found %b, should be %b\n" result expected
-            end;
-          assert_equal result expected
+          assert_equal expected result
       )
     ) subtype_tests
 ;;

types/boolVar.ml

@@ -17,7 +17,15 @@ module type E = sig
 end
 
 module type S = sig
+
   type s
+
+  module T : sig
+    include E
+    val is_empty : s -> bool
+    val is_full : s -> bool
+  end
+
   type elem = s Var.pairvar
   type 'a bdd =
     [ `True
@@ -40,7 +48,7 @@ module type S = sig
   val cap   : t -> t -> t
   val diff  : t -> t -> t
   val atom  : elem -> t
-  val neg_atom  : elem -> t
+  (* val neg_atom  : elem -> t *)
 
   val trivially_disjoint: t -> t -> bool
 
@@ -93,6 +101,12 @@ struct
   (* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
    * `Var are String
    *)
+  module T = struct
+    include T
+    let is_empty t = (empty == t)
+    let is_full t = (full == t)
+  end
+
   type s = T.t
   module X = Var.Make(T)
   type elem = s Var.pairvar
@@ -133,7 +147,7 @@ struct
   let rec hash = function
     | `True -> 1
     | `False -> 0
-    | `Split(h, _,_,_,_) -> h
+    | `Split(h,_,_,_,_) -> h
 
   let compute_hash x p i n = 
 	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
@@ -151,10 +165,12 @@ struct
   let atom x =
     let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
     `Split (h, x,`True,`False,`False)
- 
+
+   (* 
   let neg_atom x =
     let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
     `Split (h, x,`False,`False,`True)
+   *)
 
   let vars v =
     let a = atom (`Atm T.full) in 

types/types.ml

@@ -526,42 +526,46 @@ let rec subst t (v,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 when (Var.equal (`Var z) v) -> ss
           |`Var z -> vars (`Var z)
-          |`Atm constr ->
+          |`Atm bdd when X.T.is_empty bdd || X.T.is_full bdd -> atom (`Atm bdd)
+          |`Atm bdd ->
               begin match f with
-              |None -> atom (`Atm constr)
-              |Some f -> f constr v (s,ss)
+              |None -> atom (`Atm bdd)
+              |Some f -> f bdd 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
+        compute ~empty ~full:`True ~cup ~cap ~diff ~atom bdd
     end
   in
-  let subtimes t v (s,_) =
+  let subpairs bdd v (s,_) =
     List.fold_left (fun acc (left,rigth) ->
-      let deep_subst l = 
+      let deep_subst f l = 
         List.fold_left (fun acc (t1,t2) -> 
           let d1 = cons (subst (descr t1) (v,s)) in 
           let d2 = cons (subst (descr t2) (v,s)) in
-          BoolPair.cap acc (BoolPair.atom (`Atm (Pair.atom (d1,d2))))
+          BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
         ) BoolPair.full l
       in
-      let acc1 = BoolPair.diff (deep_subst left) (deep_subst rigth) 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 t)
+    ) BoolPair.empty (Pair.get bdd)
   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;
+    times = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.times) t.times;
+    xml   = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.xml) t.xml;
+    (* XXX record still not done . need to define ~f:subrecord *)
     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;
+    arrow = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.arrow) t.arrow;
     abstract = t.abstract;
     absent= t.absent;
     toplvars = { t.toplvars with s = Var.Set.remove v t.toplvars.s }
@@ -915,10 +919,10 @@ and check_arrow (left,right) s =
     let rec aux w1 w2 accu1 accu2 left = match left with
       | (t1,t2)::left ->
           let accu1' = diff_t accu1 t1 in 
-	  guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
+          guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
 
           let accu2' = cap_t  accu2 t2 in 
-	  guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
+          guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
       | [] -> 
 	  let f = match f with Witness.WFun (f,_) -> f | _ -> assert false in
 	  set s (Witness.wfun ((w1,w2)::f))
@@ -2408,15 +2412,15 @@ module Tallying = struct
   let normints (t,_) = if Intervals.is_empty t then CS.sat else CS.unsat
 
   let single_aux constr (b,v,p,n) =
-    let aux f constr acc l = 
+    let aux f constr l = 
       List.fold_left (fun acc ->
         function 
           |`Var a -> cap acc (f(var (`Var a)))
           |`Atm a -> cap acc (f(constr a))
-      ) acc l
+      ) any l
     in
     let id = (fun x -> x) in
-    let t = cap (aux id constr any p) (aux neg constr any n) in
+    let t = cap (aux id constr p) (aux neg constr n) in
     (* XXX the abstract field could be messed up ... maybe *)
     if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
       { (neg t) with abstract = Abstract.empty } 
@@ -2601,7 +2605,7 @@ module Tallying = struct
   let merge m = merge (m,DescrSet.empty)
 
   let solve s =
-    (* Add constraints of the form { alpha = ( s v fresh) ^ t } *)
+    (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
     let aux v (s,t) acc =
       if CS.E.mem v acc then assert false else
       if equal s empty && equal t any then
@@ -2644,10 +2648,11 @@ module Tallying = struct
     let rec aux (sol,acc) e =
       if CS.E.is_empty e then sol
       else
-        let (alpha,t) = CS.E.max_binding e in
+        let ((`Var v as alpha),t) = CS.E.max_binding e in
+        Format.printf "%s = %a\n" v Print.print t;
         let e1 = CS.E.remove alpha e in
-        (* XXX ... let x = Var.fresh () in *)
-        (* replace in e1 all occurrences of a by ... *)
+        (* remove from E \ { (alpha,t) } every occurrences of alpha 
+         * by mu X . (t{X/alpha}) with X fresh *)
         let es = CS.E.fold (fun beta s acc -> CS.E.add beta (subst s (alpha,t)) acc) e1 CS.E.empty in
         aux ((CS.E.add alpha t sol),(CS.E.add alpha (subst t (alpha,t)) acc)) es
     in