API change BoolVar.get -> BoolVar.leafconf

BoolVar.get not is reinstated to return a list of pairs
Add new unit test for Types.witness (WIP)

tests/libtest/typesTest.ml

@@ -78,12 +78,6 @@ let subtype_tests = [
   "(`$A -> `$C) & (`$B -> `$C)", "(`$A | `$B) -> `$C", true;
   "((`$A -> `$C) & (`$B -> `$C))", "((`$A | `$B) -> `$C)", true;
   "((`$A | `$B) -> `$C)", "((`$A -> `$C) & (`$B -> `$C))", true;
-  "(`$A -> `$B)", "(Any -> Any)", false;
-  (* { (any , omega) } *)
-  "(`A , `$X)", "((`A , (Any \\ `A)) | (`$X , `A))", false;
-  (* (a , a^[ X ]) *)
-  "(`$X & (`$X , `A))", "`C", false;
-  (* (any^[ X ] , A)^[ X ] *) 
   "(((`$A , `$C) -> `$D1) & ((`$B , `$C) -> `$D2))", "(((`$A | `$B) , `$C) -> (`$D1 | `$D2))", true;
   "(`$A & (`$A , `T))", "`$A", true;
   "(Any -> Empty)","(`$A -> `$B)", true;
@@ -91,10 +85,6 @@ let subtype_tests = [
   "(`$B & `$A) | (`$B & (Any \\ `$A))","`$B", true;
   "`$B","(`$B & `$A) | (`$B & (Any \\ `$A))", true;
   "Any","(Any \\ (Any \\ ((`$B & `$A) | (`$B & (Any \\ `$A))) | Empty) | (Any \\ (`$B | Empty)))", true;
-  "(`$A & (`$A , `T))","(`T1 -> `T2)", false;
-  (* (any^[ A ] , t)^[ A ] *)
-  "(x where x = (`$A & ((`$A , x) | `nil)))", "Empty", false;
-  (* nil^[ A ] *)
   "(Any \\ (`$A -> `$B))","((Any -> Empty) -> `$B)", false;
 ];;
 
@@ -115,10 +105,52 @@ let test_subtype =
     ) subtype_tests
 ;;
 
+let witness_tests = [
+  "(`$A -> Bool, `$B -> `$B)", "(Int | Bool -> Int, `$A -> `$B)", false;
+  (* ({ (int , true) } , {  }) *)
+  "Int -> Int", "`$A -> `$A", false;
+  (* { (true^[ A ] , any) } *)
+
+  "(`$A -> `$B)", "(Any -> Any)", false;
+  (* { (any , omega) } *)
+  "(`A , `$X)", "((`A , (Any \\ `A)) | (`$X , `A))", false;
+  (* (a , a^[ X ]) *)
+  "(`$X & (`$X , `A))", "`C", false;
+  (* (any^[ X ] , A)^[ X ] *) 
+
+  "(`$A & (`$A , `T))","(`T1 -> `T2)", false;
+  (* (any^[ A ] , t)^[ A ] *)
+  "(x where x = (`$A & ((`$A , x) | `nil)))", "Empty", false;
+  (* nil^[ A ] *)
+];;
+
+let test_witness =
+  "test subtype" >::: 
+    List.map (fun (s1,s2,expected) ->
+      (Printf.sprintf " %s <: %s " s1 s2) >:: (fun _ ->
+          let t1 = parse_typ s1 in
+          let t2 = parse_typ s2 in
+          let d = Types.diff t1 t2 in
+          let result = Types.witness d in
+          Format.printf "subtyping %s <: %s\n" s1 s2;
+          Format.printf "witness : %a\n" Types.Witness.print_witness result;
+          Format.printf "diff : %a\n" Types.Print.print d;
+          (*
+          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 true true
+      )
+    ) witness_tests
+;;
 
 let all =
   "all tests" >::: [
     test_subtype;
+    test_witness;
   ]
  
 let main () =

types/boolVar.ml

@@ -26,20 +26,12 @@ sig
     | `False
     | `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]
 
-  (*
-  include Custom.T 
-  *)
-  type t = elem bdd
-  val dump : Format.formatter -> t -> unit
-  val check : t -> unit
-  val equal : t -> t -> bool
-  val hash : t -> int
-  val compare : t -> t -> int
+  include Custom.T with type t = elem bdd
 
   (* returns the union of all leaves in the BDD *)
-  val get: t -> s
+  val leafconj: t -> s
 
-  (* val get': t -> (elem list * (elem list) list) list *)
+  val get: t -> (elem list * elem list) list
 
   val empty : t
   val full  : t
@@ -200,32 +192,33 @@ struct
     | `False -> []
     | c -> [ fun ppf -> print X.dump ppf c ]
 
-  (*
-  let rec get accu pos neg = function
-    | `True -> (pos,neg) :: accu
-    | `False -> accu
-    | `Split (_,x, p,i,n) ->
-	(*OPT: can avoid creating this list cell when pos or neg =`False *)
-	let accu = get accu (x::pos) neg p in
-	let accu = get accu pos (x::neg) n in
-	let accu = get accu pos neg i in
-	accu
-	  
-  let get x = get [] [] [] x
-  *)
-
-  let rec get accu = function
-    | `True -> accu
-    | `False -> accu
-    | `Split (_,`Atm x, `True,`False,`False) -> x :: accu
-    | `Split (_,`Atm x, _,_,_) -> assert false
-    | `Split (_,`Var x, p,i,n) ->
-	let accu = get accu p in
-	let accu = get accu n in
-	let accu = get accu i in
-	accu
-
-  let get x = List.fold_left T.cup T.empty (get [] x)
+  (* return a list of pairs, where each pair holds the list
+   * of positive and negative elements on a branch *)
+  let get x =
+    let rec aux accu pos neg = function
+      | `True -> (pos,neg) :: accu
+      | `False -> accu
+      | `Split (_,x, p,i,n) ->
+        (*OPT: can avoid creating this list cell when pos or neg =`False *)
+        let accu = aux accu (x::pos) neg p in
+        let accu = aux accu pos (x::neg) n in
+        let accu = aux accu pos neg i in
+        accu
+    in aux [] [] [] x
+
+  let leafconj x = 
+    let rec aux accu = function
+      | `True -> accu
+      | `False -> accu
+      | `Split (_,`Atm x, `True,`False,`False) -> x :: accu
+      | `Split (_,`Atm x, _,_,_) -> assert false
+      | `Split (_,`Var x, p,i,n) ->
+        let accu = aux accu p in
+        let accu = aux accu n in
+        let accu = aux accu i in
+        accu
+    in
+    List.fold_left T.cup T.empty (aux [] x)
 
 (*      
   let rec get' accu pos neg = function

types/builtin.ml

@@ -340,8 +340,8 @@ binary_op_cst "dump_to_file_utf8"
 (* Integer operators *)
 
 let intop f x y =
-  let s = Types.BoolIntervals.get x in
-  let t = Types.BoolIntervals.get y in
+  let s = Types.BoolIntervals.leafconj x in
+  let t = Types.BoolIntervals.leafconj y in
   Types.BoolIntervals.atom (`Atm (f s t))
 ;;
 

types/patterns.ml

@@ -858,8 +858,8 @@ module Compile = struct
 	  
   let split_kind basic prod xml record = {
     basic = basic;
-    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.BoolAtoms.get (Types.Atom.get t), r) basic);
-    chars = Chars.mk_map (List.map (fun (t,r) -> Types.BoolChars.get (Types.Char.get t), r) basic);
+    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.BoolAtoms.leafconj (Types.Atom.get t), r) basic);
+    chars = Chars.mk_map (List.map (fun (t,r) -> Types.BoolChars.leafconj (Types.Char.get t), r) basic);
     prod = prod; 
     xml = xml; 
     record = record

types/types.ml

@@ -697,18 +697,20 @@ module Witness = struct
 	      r)
     | w -> type_has (descr n) w
 
+  (* type_has checks if a witness is contained in the union of
+   * the leafs of a bdd, ignoring all variables. *)
   and type_has t = function
-    | WInt i -> Intervals.contains i (BoolIntervals.get t.ints)
-    | WChar c -> Chars.contains c (BoolChars.get t.chars)
-    | WAtom a -> Atoms.contains_sample a (BoolAtoms.get t.atoms)
+    | WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints)
+    | WChar c -> Chars.contains c (BoolChars.leafconj t.chars)
+    | WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms)
     | WPair (w1,w2,_) -> 
 	bool_pair 
 	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2) 
-	  (BoolPair.get t.times)
+	  (BoolPair.leafconj t.times)
     | WXml (w1,w2,_) ->
 	bool_pair 
 	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
-	  (BoolPair.get t.xml)
+	  (BoolPair.leafconj t.xml)
     | WFun (f,_) ->
 	bool_pair 
 	  (fun (n1,n2) ->
@@ -718,7 +720,7 @@ module Witness = struct
 		    (match y with None -> false
 		       | Some y -> node_has n2 y))
 	       f) 
-	  (BoolPair.get t.arrow)
+	  (BoolPair.leafconj t.arrow)
     | WRecord (f,o,_) ->
 	bool_rec 
 	  (fun (o',f') ->
@@ -737,7 +739,7 @@ module Witness = struct
 		      because of an invariant. Otherwise, we must
 		      check that all are WAbsent here. *)
 	       with Exit -> false))
-	  (BoolRec.get t.record)
+	  (BoolRec.leafconj t.record)
     | WAbsent -> t.absent
     | WAbstract a -> Abstract.contains_sample a t.abstract
 end
@@ -792,12 +794,12 @@ let rec slot d =
   incr complex;
   Stats.Counter.incr count_subtype; 
   if d.absent then slot_nempty Witness.WAbsent
-  else if not (Intervals.is_empty (BoolIntervals.get d.ints)) 
-  then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.get d.ints)))
-  else if not (Atoms.is_empty (BoolAtoms.get d.atoms)) 
-  then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.get d.atoms)))
-  else if not (Chars.is_empty (BoolChars.get d.chars)) 
-  then slot_nempty (Witness.WChar (Chars.sample (BoolChars.get d.chars)))
+  else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints)) 
+  then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints)))
+  else if not (Atoms.is_empty (BoolAtoms.leafconj d.atoms)) 
+  then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms)))
+  else if not (Chars.is_empty (BoolChars.leafconj d.chars)) 
+  then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
   else if not (Abstract.is_empty d.abstract) 
   then slot_nempty (Witness.WAbstract (Abstract.sample d.abstract))
   else try DescrHash.find memo d
@@ -805,10 +807,10 @@ let rec slot d =
     let s = { status = Maybe; active = false; notify = Nothing } in
     DescrHash.add memo d s;
     (try
-       iter_s s check_times (Pair.get (BoolPair.get d.times));
-       iter_s s check_xml (Pair.get (BoolPair.get d.xml)); 
-       iter_s s check_arrow (Pair.get (BoolPair.get d.arrow));
-       iter_s s check_record (get_record (BoolRec.get d.record));
+       iter_s s check_times (Pair.get (BoolPair.leafconj d.times));
+       iter_s s check_xml (Pair.get (BoolPair.leafconj d.xml)); 
+       iter_s s check_arrow (Pair.get (BoolPair.leafconj d.arrow));
+       iter_s s check_record (get_record (BoolRec.leafconj d.record));
        if s.active then marks := s :: !marks else s.status <- Empty;
      with NotEmpty -> ());
     s
@@ -1051,7 +1053,7 @@ struct
 	    ) right in
 	if non_empty !resid1 then accu := (!resid1, d2) :: !accu 
     in
-    List.iter line (Pair.get (BoolPair.get d));
+    List.iter line (Pair.get (BoolPair.leafconj d));
     !accu
 (* Maybe, can improve this function with:
      (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
@@ -1224,7 +1226,7 @@ struct
 	   | [] -> (p,accu) :: b in
 	 aux_p [] p)
       []
-      (Rec.get (BoolRec.get d.record))
+      (Rec.get (BoolRec.leafconj d.record))
 
   let split (d : descr) l =
     TR.boolean (aux_split d l)
@@ -1257,15 +1259,15 @@ struct
     let aux (_,r) =
       let ls = LabelMap.domain r in
       res := LabelSet.cup ls !res in
-    (* XXX every times I use BoolRec.get I'm trowing away all variables ! *)
-    Rec.iter aux (BoolRec.get d.record);
+    (* XXX every times I use BoolRec.leafconj I'm trowing away all variables ! *)
+    Rec.iter aux (BoolRec.leafconj d.record);
     !res
 
   let first_label d =
     let min = ref Label.dummy in
     let aux (_,r) = match LabelMap.get r with
 	(l,_)::_ -> min := Label.min l !min | _ -> () in
-    Rec.iter aux (BoolRec.get d.record);
+    Rec.iter aux (BoolRec.leafconj d.record);
     !min
 
   let empty_cases d =
@@ -1278,7 +1280,7 @@ struct
 		       assert (LabelMap.get r == []);
 		       if o then 3 else 1
 		    )
-	      (BoolRec.get d.record) in
+	      (BoolRec.leafconj d.record) in
     (x land 2 <> 0, x land 1 <> 0)
 
   let has_empty_record d =
@@ -1290,7 +1292,7 @@ struct
 	         (fun (l,t) -> (descr t).absent)
 	         (LabelMap.get r)
 	    )
-      (BoolRec.get d.record)
+      (BoolRec.leafconj d.record)
     
 (*TODO: optimize merge
    - pre-compute the sequence of labels
@@ -1520,7 +1522,7 @@ struct
 	       add (Name n)
 	     with Not_found ->
 	       let tag = 
-		 match Atoms.print_tag (BoolAtoms.get t1.atoms) with
+		 match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
 		   | Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
 		   | _ -> `Type (prepare t1) in
 	       assert (equal { t2 with times = empty.times } empty);
@@ -1535,7 +1537,7 @@ struct
 	     let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
 	     add (Record (r,some,none)))
 	  (Record.get not_seq);
-	(match Chars.is_char (BoolChars.get not_seq.chars) with
+	(match Chars.is_char (BoolChars.leafconj not_seq.chars) with
 	   | Some c -> add (Char c)
 	   | None ->
 	       List.iter (fun x -> add (Atomic x)) (BoolChars.print "" not_seq.chars));
@@ -1547,7 +1549,7 @@ struct
 	     let aux (t,s) = prepare (descr t), prepare (descr s) in
 	     let p = List.map aux p and n = List.map aux n in
 	     add (Arrows (p,n)))
-	  (Pair.get (BoolPair.get not_seq.arrow));
+	  (Pair.get (BoolPair.leafconj not_seq.arrow));
 	if not_seq.absent then add (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT"));
 	slot.def <- List.rev slot.def;
 	slot
@@ -1559,7 +1561,7 @@ struct
 	 let tr = Product.merge_same_first tr in
 	 let tr = Product.clean_normal tr in
 
-	 let eps = Atoms.contains nil_atom (BoolAtoms.get t.atoms) in
+	 let eps = Atoms.contains nil_atom (BoolAtoms.leafconj t.atoms) in
 	 let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in
 
 	 try
@@ -2049,7 +2051,7 @@ struct
     not (List.exists (check_simple left) right)
 
   let sample t =
-    let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.get t.arrow)) in
+    let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
     List.fold_left (fun accu (t,s) -> cap accu (arrow t s)) 
       { empty with arrow = any.arrow } left
 	
@@ -2078,7 +2080,7 @@ struct
 	   (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
 	  || (aux rem)
     in
-    aux (Pair.get (BoolPair.get s.arrow))
+    aux (Pair.get (BoolPair.leafconj s.arrow))
 
   type t = descr * (descr * descr) list list
 
@@ -2093,7 +2095,7 @@ struct
 	 else accu
       )
       (any, [])
-      (Pair.get (BoolPair.get t.arrow))
+      (Pair.get (BoolPair.leafconj t.arrow))
 
   let domain (dom,_) = dom
 
@@ -2134,23 +2136,22 @@ struct
   let is_empty (_,arr) = arr == []
 end
   
-
 module Int = struct
-  let has_int d i = Intervals.contains i (BoolIntervals.get d.ints)
+  let has_int d i = Intervals.contains i (BoolIntervals.leafconj d.ints)
   let get d = d.ints
   let any = { empty with ints = any.ints }
   let any = { empty with ints = BoolIntervals.full }
 end
 
 module Atom = struct
-  let has_atom d a = Atoms.contains a (BoolAtoms.get d.atoms)
+  let has_atom d a = Atoms.contains a (BoolAtoms.leafconj d.atoms)
   let get d = d.atoms
   let any = { empty with atoms = any.atoms }
 end
 
 module Char = struct
-  let has_char d c = Chars.contains c (BoolChars.get d.chars)
-  let is_empty d = Chars.is_empty (BoolChars.get d.chars)
+  let has_char d c = Chars.contains c (BoolChars.leafconj d.chars)
+  let is_empty d = Chars.is_empty (BoolChars.leafconj d.chars)
   let get d = d.chars
   let any = { empty with chars = any.chars }
 end