boolvarTest.ml 4 KB
Newer Older
1 2 3 4 5 6 7

open OUnit

module type S = sig
  include BoolVar.S
  val mk_var : string -> t
  val mk_atm : string -> t
8
  val to_string : t -> string
9 10
end

11 12 13 14
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Printf.sprintf "->%s<-" (Format.flush_str_formatter ())

15 16
module BoolAtoms : S with type s = Atoms.t = struct 
  include BoolVar.Make(Atoms)
17
  let mk_var s = atom (Var.mk s)
18
  let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
19
  let to_string = to_string pp_print
20 21
end

22 23 24
(*
module BoolChars : S with type s = Chars.t = struct
  include BoolVar.Make(Chars)
25
  let mk_var s = atom (`Var s)
26
  let mk_atm c = atom (`Atm (Chars.atom (Chars.V.mk_char c.[0] )))
27
  let to_string = to_string pp_print
28 29
end

30
module BoolIntervals : S with type s = Intervals.t = struct
31
  include BoolVar.Make(Intervals)
32 33
  let mk_var s = atom (`Var s)
  let mk_atm s = atom (`Atm (Intervals.atom (Intervals.V.mk s)))
34
  let to_string = to_string pp_print
35
end
36
*)
37

38 39 40 41 42 43 44 45 46 47 48 49
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
50
      | x = SELF; "-"; y = SELF -> B.diff x y ]
51
    | "neg" RIGHTA
52
      [ "~"; x = SELF-> B.diff B.full x ]
53 54 55 56 57
    | "simple" NONA
      ["Any" -> B.full
      |"Empty" -> B.empty
      |"atm"; x = LIDENT -> B.mk_atm x
      |"var"; x = LIDENT -> B.mk_var x
58

59 60 61 62 63 64 65 66 67 68 69
      |"("; x = SELF; ")" -> x ]
    ];
  END
  ;;

  let of_string s = Gram.parse_string expression Loc.ghost s
  let os = of_string 

end

module BAP = ExprParser(BoolAtoms)
70 71
(*
module BCP = ExprParser(BoolChars)
72
module BIP = ExprParser(BoolIntervals)
73
*)
74

75
let atoms_tests = [
76 77 78
  "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)";
79
  "distributive intersection var", BAP.os "(var alpha v atm bar) ^ atm baz", BAP.os "(var alpha ^ atm baz) v (atm bar ^ atm baz)";
80
  "associativity intersection", BAP.os "(atm foo ^ atm bar) ^ atm baz", BAP.os "atm foo ^ (atm bar ^ atm baz)";
81
  "associativity intersection var", BAP.os "(atm foo ^ atm bar) ^ var alpha", BAP.os "atm foo ^ (atm bar ^ var alpha)";
82
  "associativity union", BAP.os "(atm foo v atm bar) v atm baz", BAP.os "atm foo v (atm bar v atm baz)";
83 84 85 86 87 88 89 90
  "associativity union var", BAP.os "(atm foo v var alpha) v atm baz", BAP.os "atm foo v (var alpha v atm baz)";
  "intersection", BAP.os "(atm foo ^ atm bar) v var alpha", BAP.os "var alpha";
  "intersection 2", BAP.os "(atm foo v var alpha ) ^ var alpha", BAP.os "var alpha";
  "intersection empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
  "difference", BAP.os "(atm foo v var alpha) - (var alpha)", BAP.os "atm foo ^ ~ var alpha";
  "difference", BAP.os "(atm foo v var alpha) - (atm foo)", BAP.os "var alpha ^ ~ atm foo";
  "difference any 1", BAP.os "~ var alpha", BAP.os "Any - var alpha";
  "difference any 2", BAP.os "~ var alpha", BAP.os "Any ^ ~ var alpha";
91 92
];;

93 94
let atoms_structure =
  "atoms structure" >::: 
95
    List.map (fun (descr, result,expected) ->
96
      (Printf.sprintf "test %s" descr) >:: (fun _ ->
97
        assert_equal ~cmp:BoolAtoms.equal ~printer:(BoolAtoms.to_string) expected result
98
      )
99 100 101 102 103 104 105 106 107
    ) 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
108
        assert_equal (Atoms.contains a (BoolAtoms.leafconj t)) true
109 110 111 112 113 114 115
      )
    )
  [
    "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";
  ]
116 117 118 119
;;

let all =
  "all tests" >::: [
120
    atoms_structure;
121
    atoms_contains;
122 123 124 125 126 127 128 129
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ();;