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 ();;