tallyingTest.ml 6.43 KB
Newer Older
1
open OUnit
2
open Types
3
4
5
6
7
8
9
10

let parse_typ s =
  let st = Stream.of_string s in
  let astpat = Parser.pat st in 
  let nodepat = Typer.typ Builtin.env astpat in
  Types.descr nodepat
;;

11
12
13
14
15
16
let cup = Tallying.CS.cup
let cap = Tallying.CS.cap
let singleton = Tallying.CS.singleton

let mk_pos (alpha,t) = singleton (Tallying.Pos (`Var alpha,parse_typ t))
let mk_neg (t,alpha) = singleton (Tallying.Neg (parse_typ t,`Var alpha))
17

Pietro Abate's avatar
Pietro Abate committed
18
19
20
(* ^ => |
 * v => &
 *)
21
let norm_tests = [
22
23
24
25
26
27
28
29
30
31
32
33
  "(`$A -> Bool)", "(`$B -> `$B)", 
                    cup (mk_pos ("B","Empty"))
                      (cap 
                        (mk_neg ("`$B","A"))
                        (mk_neg ("Bool","B"))
                      );
  "`$B", "`$A", mk_neg ("`$B","A");
  "`$B", "Empty", mk_pos ("B","Empty");
  "Int", "`$B", mk_neg ("Int","B");
  "Int", "(`$A | `$B)", mk_neg ("Int \\ `$B","A");
  "(Int -> Bool)", "(`$A -> `$B)",
                    cup (mk_pos ("A","Empty")) 
34
                      (cap 
35
36
                        (mk_pos ("A","Int"))
                        (mk_neg ("Bool","B"))
37
                      );
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", 
                    cup 
                      (mk_pos ("A","Empty"))
                      (cup
                        (cup
                          (cap
                            (mk_pos ("A","Empty"))
                            (mk_neg ("Int","B"))
                          )
                          (cap
                            (mk_pos ("A","Empty"))
                            (mk_neg ("Bool","B"))
                          )
                        )
                        (cap 
                          (mk_pos ("A","Empty"))
                          (mk_neg ("Int | Bool","B"))
                        )

                      );
58
59
60
61
62
63
                      (*
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
  "(`$A , `$B)","(Int , Bool)",
                     cap
                        (mk_pos ("A","Int"))
Pietro Abate's avatar
Pietro Abate committed
64
65
66
                        (mk_pos ("B","Bool"));
  "(`$A & (`$B , `$C))","(Int , Int)",mk_pos ("A","(Int , Int) | (Any \\ (`$B , `$C))");
  "(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", cap (mk_pos ("A","Int")) (mk_pos ("B","Int"));
67
68
]

Pietro Abate's avatar
Pietro Abate committed
69
70
71
72
73
(* the abstract field is ignored in the comparison *)
let m_compare = 
  let a = Types.abstract Abstract.any in
  let cmp t1 t2 = Types.compare (diff t1 a) (diff t2 a) in
  Tallying.CS.M.compare cmp
74

75
module MList = OUnitDiff.ListSimpleMake (struct 
76
77
78
79
80
81
  type t = Tallying.CS.m
  let compare = m_compare
  let pp_printer = Tallying.CS.print_m
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

82
83
let test_norm =
  "test tallying norm" >:::
84
85
86
87
88
89
    List.map (fun (s,t,expected) ->
      (Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
        let s = parse_typ s in
        let t = parse_typ t in
        let result = Tallying.norm (diff s t) in
        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
90
        MList.assert_equal (elem expected) (elem result)
91
92
93
94
      )
    ) norm_tests
;;

95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
let merge_tests = [
  [("`$A", "Empty");("`$B", "Empty")], cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
  [("`$A", "Int | Bool");("Int","`$B");("`$B", "Empty")], Tallying.CS.unsat;
  [("Bool","`$B"); ("`$B", "`$A"); ("`$A", "Empty")], Tallying.CS.unsat;
  [("Bool","`$B"); ("Int","`$B"); ("`$B","`$A"); ("`$A", "Int | Bool")],
    cap 
      (mk_neg ("`$B","A")) (
        cap 
          (mk_pos ("A", "Int | Bool")) (
            cap
            (mk_neg ("Int | Bool","B"))
            (mk_pos ("B","Int | Bool"))
          )
        );
  [("`$A", "`$B")], mk_pos ("A","`$B");
  [("`$B", "Empty")], mk_pos ("B","Empty");
111
  [("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
112
113
114
115
]

let test_merge =
  let print_test l =
116
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s >= %s" s t) l)
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
  in
  "test tallying merge" >:::
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
        let n = List.fold_left (fun acc (s,t) ->
          let s = parse_typ s in
          let t = parse_typ t in
          Tallying.CS.cap acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l 
        in
        let result = Tallying.CS.S.fold (fun c acc ->
          try cup (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
          ) n Tallying.CS.S.empty
        in
        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
        MList.assert_equal (elem expected) (elem result)
      )
    ) merge_tests
;;

136
137
138
139
140
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

Pietro Abate's avatar
Pietro Abate committed
141
(* the abstract field is ignored in the comparison *)
142
let compare_constr (v1,t1) (v2,t2) = 
Pietro Abate's avatar
Pietro Abate committed
143
  let a = Types.abstract Abstract.any in
144
145
  if (v1,t1) == (v2,t2) then 0
  else let c = Var.compare v1 v2 in if c <> 0 then c
Pietro Abate's avatar
Pietro Abate committed
146
  else Types.compare (diff t1 a) (diff t2 a)
147
148
149
150
151
152
153
154

module EList = OUnitDiff.ListSimpleMake (struct 
  type t = (Var.var * Types.t)
  let compare = compare_constr
  let pp_printer ppf (`Var v,t) = Format.fprintf ppf "(%s = %s)" v (to_string Print.print t)
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

155
module SubSet = OUnitDiff.SetMake (struct 
156
157
158
159
160
161
162
163
164
165
166
167
168
169
  type t = EList.t
  let compare a b = EList.compare a b
  let pp_printer ppf l = EList.pp_printer ppf l
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

let mk_e ll =
  List.map (fun l ->
    List.map (fun (v,t) -> (`Var v),(parse_typ t)) l
  ) ll

let tallying_tests = [
  [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
    [("A","Int | Bool");("B","Int | Bool")]
170
171
172
173
174
  ];
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
    [("A","Empty");("B","Empty")];
  ];
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
Pietro Abate's avatar
Pietro Abate committed
175
  [("(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[("A","Int");("B","Int")]];
176
177
178
179
180
181
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
182
  "test tallying" >:::
183
184
185
186
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
        let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
        let result = Tallying.tallying l in
187
188
        let elem s = SubSet.of_list (List.map (fun l -> EList.of_list (List.sort compare_constr l)) s) in
        SubSet.assert_equal (elem expected) (elem result)
189
190
191
192
      )
    ) tallying_tests
;;

193
194
195
let all =
  "all tests" >::: [
    test_norm;
196
    test_merge;
197
    test_tallying;
198
199
200
201
202
203
204
205
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()