Add unit test infrastructure for BoolVar DS

cduce_boolvar.mlpack

+Upool
+Serialize
+Custom
+Encodings
+Imap
+State
+Pool
+Ns
+SortedList
+Atoms
+Bool
+Chars
+Ident
+Intervals
+Inttbl
+Normal
+Pretty
+Stats
+BoolVar
+BoolAtoms
+

tests/libtest/tests-boolvar.ml

+
+open OUnit
+
+module type S = sig
+  include BoolVar.S
+  val mk_var : string -> t
+  val mk_atm : string -> t
+end
+
+module BoolChars : S = struct
+  include BoolVar.Make(Chars)
+  let mk_var s = atom (Custom.Var s)
+  let mk_atm c = atom (Custom.Atm (Chars.atom (Chars.V.mk_char c.[0] )))
+end
+
+module BoolAtoms = struct 
+  include BoolVar.Make(Atoms)
+  let mk_var s = atom (Custom.Var s)
+  let mk_atm s = atom (Custom.Atm (Atoms.atom (Atoms.V.mk_ascii s)))
+end
+
+module BoolIntervals : S = struct
+  include BoolVar.Make(Intervals)
+  let mk_var s = atom (Custom.Var s)
+  let mk_atm s = atom (Custom.Atm (Intervals.atom (Intervals.V.mk s)))
+end
+
+module ExprParser (B : S) = struct
+  open Camlp4.PreCast
+
+  let expression = Gram.Entry.mk "expression"
+
+  EXTEND Gram
+    GLOBAL: expression;
+    expression:
+    [ "cap" LEFTA
+      [ x = SELF; "^"; y = SELF -> B.cap x y ]
+    | "cup" LEFTA
+      [ x = SELF; "v"; y = SELF -> B.cup x y
+      | x = SELF; "\\/\\/"; y = SELF -> B.diff x y ]
+    | "neg" RIGHTA
+      [ "-"; x = SELF-> B.diff B.full x ]
+    | "simple" NONA
+      ["Any" -> B.full
+      |"Empty" -> B.empty
+      |"atm"; x = LIDENT -> B.mk_atm x
+      |"var"; x = LIDENT -> B.mk_var x
+      |"("; x = SELF; ")" -> x ]
+    ];
+  END
+  ;;
+
+  let of_string s = Gram.parse_string expression Loc.ghost s
+  let os = of_string 
+
+end
+
+module BCP = ExprParser(BoolChars)
+module BAP = ExprParser(BoolAtoms)
+module BIP = ExprParser(BoolIntervals)
+(*
+XXX this needs much more infrastructure as in types.ml
+
+module BoolPair = BoolVar.Make(Pair)
+module BoolRec = BoolVar.Make(Rec)
+*)
+
+let boolvar_tests_atoms = [
+  "commutativity intersection", BAP.os "atm foo ^ atm bar", BAP.os "atm bar ^ atm foo";
+  "commutativity union", BAP.os "atm foo v atm bar", BAP.os "atm bar v atm foo";
+  "distributive intersection", BAP.os "(atm foo v atm bar) ^ atm baz", BAP.os "(atm foo ^ atm baz) v (atm bar ^ atm baz)";
+  "associativity intersection", BAP.os "(atm foo ^ atm bar) ^ atm baz", BAP.os "atm foo ^ (atm bar ^ atm baz)";
+  "associativity union", BAP.os "(atm foo v atm bar) v atm baz", BAP.os "atm foo v (atm bar v atm baz)";
+  "difference", BAP.os "(atm foo ^ atm bar) v var alpha", BAP.os "var alpha";
+  "difference empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
+  (* vars = Any -> no variables in the tree *)
+  "splitvar vars empty", fst(BoolAtoms.splitvars (BAP.os "atm foo")), BAP.os "Any";
+  "splitvar atm empty", snd(BoolAtoms.splitvars (BAP.os "var alpha")), BAP.os "Empty";
+  "splitvar vars 1 ", fst(BoolAtoms.splitvars (BAP.os "var alpha ^ (atm foo v var beta) ^ var gamma")), BAP.os "var alpha ^ var gamma";
+  "splitvar atm 1", snd(BoolAtoms.splitvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "var gamma v var alpha v ( atm foo ^ var beta)";
+  "splitvar atm 2", snd(BoolAtoms.splitvars (BAP.os "var alpha v atm foo")), BAP.os "atm foo";
+
+];;
+
+let test_boolvar_atoms =
+  "test boolvar atoms" >::: 
+    List.map (fun (descr, s1,s2) ->
+      (Printf.sprintf "test %s" descr) >:: (fun _ ->
+        List.iter (fun f -> f Format.std_formatter ) (BoolAtoms.print "Empty!" s1);
+        Format.printf "\n";
+        List.iter (fun f -> f Format.std_formatter ) (BoolAtoms.print "Empty!" s2);
+        Format.printf "\n";
+        assert_equal (BoolAtoms.equal s1 s2) true
+      )
+    ) boolvar_tests_atoms
+;;
+
+let all =
+  "all tests" >::: [
+    test_boolvar_atoms;
+  ]
+ 
+let main () =
+  OUnit.run_test_tt_main all
+;;
+ 
+main ();;
+