tests-boolvar.ml 3.87 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

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

16
module BoolAtoms : S with type bt = Atoms.t = struct 
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
  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)
*)

68
let atoms_tests = [
69 70 71 72 73 74 75
  "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";
Pietro Abate's avatar
Pietro Abate committed
76
  "splitvar vars empty", fst(BoolAtoms.splitvars (BAP.os "atm foo")), BAP.os "Empty";
77
  "splitvar atm empty", snd(BoolAtoms.splitvars (BAP.os "var alpha")), BAP.os "Empty";
Pietro Abate's avatar
Pietro Abate committed
78 79
  "splitvar vars 1 ", fst(BoolAtoms.splitvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "var alpha v var gamma";
  "splitvar atm 1", snd(BoolAtoms.splitvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "atm foo ^ var beta";
80
  "splitvar atm 2", snd(BoolAtoms.splitvars (BAP.os "var alpha v atm foo")), BAP.os "atm foo";
Pietro Abate's avatar
Pietro Abate committed
81
  "splitvar vars 2", fst(BoolAtoms.splitvars (BAP.os "var alpha v atm foo")), BAP.os "var alpha";
82 83
];;

84 85
let atoms_structure =
  "atoms structure" >::: 
86 87
    List.map (fun (descr, s1,s2) ->
      (Printf.sprintf "test %s" descr) >:: (fun _ ->
88
        (*
89 90 91 92
        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";
93
        *)
94 95
        assert_equal (BoolAtoms.equal s1 s2) true
      )
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
    ) atoms_tests
;;

let atoms_contains =
  "atoms contains" >:::
    List.map (fun (descr, i, s) -> 
      (Printf.sprintf "test %s" descr) >:: (fun _ ->
        let a = Atoms.V.mk_ascii i in
        let t = BAP.os s in
        assert_equal (Atoms.contains a (BoolAtoms.get t)) true
      )
    )
  [
    "foo in atm foo","foo","atm foo";
    "foo in (atm foo v atm bar)","foo","atm foo v atm bar";
    "foo in (atm foo v atm bar) ^ ^ var beta","foo","(atm foo v atm bar) ^ var beta";
  ]
113 114 115 116
;;

let all =
  "all tests" >::: [
117
    atoms_structure;
118 119 120 121 122 123 124 125
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ();;