tallyingTest.ml 9.62 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
17
18
19
20
21
22
23
24
25
26
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

(* the abstract field is ignored in the comparison *)
module ESet = OUnitDiff.SetMake (struct 
  type t = (Var.var * Types.t)
  let compare (v1,t1) (v2,t2) = 
    let a = Types.abstract Abstract.any in
    if (v1,t1) == (v2,t2) then 0
    else let c = Var.compare v1 v2 in if c <> 0 then c
    else Types.compare (diff t1 a) (diff t2 a)
  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)
27

28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
module SubStSet = OUnitDiff.SetMake (struct 
  type t = ESet.t
  let compare a b = ESet.compare a b
  let pp_printer ppf l = ESet.pp_printer ppf l
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

module MSet = OUnitDiff.SetMake (struct 
  type t = Tallying.CS.m
  let compare = 
    (* the abstract field is ignored in the comparison *)
    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
  let pp_printer = Tallying.CS.print_m
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

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

Pietro Abate's avatar
Pietro Abate committed
49
50
51
type pp = P of vv * string | N of string * vv
and vv = V of string

52
53
54
55
56
57
58
59
60
61
62
63
let mk_pp = function
  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))

let mk_prod l =
    List.fold_left (fun acc2 c ->
      Tallying.CS.prod (mk_pp c) acc2
    ) Tallying.CS.sat l

let mk_union l1 l2 =
  Tallying.CS.union (mk_prod l1) (mk_prod l2)

Pietro Abate's avatar
Pietro Abate committed
64
65
let mk_s ll =
  List.fold_left (fun acc1 l ->
66
    Tallying.CS.union (mk_prod l) acc1
Pietro Abate's avatar
Pietro Abate committed
67
68
  ) Tallying.CS.S.empty ll

69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
let mk_union_res l1 l2 =
  let aux_merge k v1 v2 = match (k,v1,v2) with
    |(k,None,None) -> assert false
    |(k,Some v,None) -> Some v
    |(k,None,Some v) -> Some v
    |((_,v),Some x,Some y) when Types.equal x y -> Some x
    |((true,v),Some x,Some y) -> assert false
    |((false,v),Some x,Some y) -> assert false
  in
  let aux l = 
    List.fold_left (fun acc -> function
      |P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,`Var v) (parse_typ s))
      |N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,`Var v) (parse_typ s))
    ) Tallying.CS.M.empty l
  in 
  match l1,l2 with
  |[],[] -> Tallying.CS.sat
  |l1,[] -> (Tallying.CS.S.singleton (aux l1))
  |[],l2 -> (Tallying.CS.S.singleton (aux l2))
  |l1,l2 -> Tallying.CS.S.union (Tallying.CS.S.singleton (aux l1)) (Tallying.CS.S.singleton (aux l2))


Pietro Abate's avatar
Pietro Abate committed
91
(* check invariants on the constraints sets *)
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
let test_constraint_ops = [

  "prod pos",mk_prod [P(V "A","Int");P(V "A","Bool")], mk_pp (P(V "A","Int & Bool"));

  "prod neg",mk_prod [N("Int",V "B");N("Bool",V "B")], mk_pp (N("Int | Bool",V "B"));

  "prod var",mk_prod [N("`$B",V "A");P(V "B","Bool | Int")],
      mk_union_res 
        [N("`$B",V "A");P(V "B","Bool | Int")] 
        [];

  "empty", mk_union [P(V "A","Empty")] [P(V "A","Empty")], mk_pp (P(V "A","Empty"));

  "empty <= int 1", mk_union [P(V "A","Int")] [P(V "A","Empty")], mk_pp (P(V "A","Int"));
  "empty <= int 2", mk_union [P(V "A","Empty")] [P(V "A","Int")], mk_pp (P(V "A","Int"));

  "int v bool <= int", mk_union [P(V "A","Int | Bool")] [P(V "A","Int")], mk_pp (P(V "A","Int | Bool"));

  "0 -> 1 <= a -> b", mk_union [P(V "A","Empty -> Any")] [P(V "A","Int -> Bool")], mk_pp (P(V "A","Empty -> Any"));

  "union 1",mk_union [P(V "A","Empty")] [P(V "A","Empty");N("Int",V "B")], mk_pp (P(V "A","Empty"));

  "union 2",mk_union [P(V "A","Empty")] [P(V "A","Int");P(V "A","Bool")],
      mk_union_res 
      [P(V "A","Int & Bool")]
      [P(V "A","Empty")];

  "union 2 comm",mk_union [P(V "A","Int");P(V "A","Bool")] [P(V "A","Empty")],
      mk_union_res
        [P(V "A","Int & Bool")]
        [(P(V "A","Empty"))];

  "union 3",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Empty")], mk_pp (P(V "A","Empty"));

  "union 4",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Int")], mk_pp (P(V "A","Empty"));

  "union 5",mk_union [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")] [P(V "A","Empty");P(V "B","Empty")],
      mk_union_res 
        [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
        [P(V "A","Empty");P(V "B","Empty")];

]
134

135
136
137
138
139
140
141
142
143
144
145
let test_constraints =
  "test tallying data structures" >:::
    List.map (fun (test,result,expected) ->
      test >:: (fun _ ->
        let elem s = (MSet.of_list (Tallying.CS.S.elements s)) in
        MSet.assert_equal (elem expected) (elem result)
      )
    ) test_constraint_ops
;;

(* ^ => & -- v => | *)
Pietro Abate's avatar
Pietro Abate committed
146
147
148
149
150
151

let norm_tests = [
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
152

Pietro Abate's avatar
Pietro Abate committed
153
154
155
156
  "`$B", "`$A", mk_s [[N("`$B",V "A")]];
  "`$B", "Empty", mk_s [[P(V "B","Empty")]];
  "Int", "`$B", mk_s [[N("Int",V "B")]];
  "Int", "(`$A | `$B)", mk_s [[N("Int \\ `$B",V "A")]];
157

Pietro Abate's avatar
Pietro Abate committed
158
159
160
161
  "(Int -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
162

Pietro Abate's avatar
Pietro Abate committed
163
164
165
166
167
168
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Empty");N("Int",V "B")];
    [P(V "A","Empty");N("Bool",V "B")];
    [P(V "A","Empty");N("Int | Bool",V "B")]
  ];
169
170
171
172
173
174

  "(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
    [P(V "B","Int");N("Int",V "A")];
    [P(V "B","Bool");N("Bool",V "A")];
  ];

Pietro Abate's avatar
Pietro Abate committed
175
  (*
176
177
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
178

Pietro Abate's avatar
Pietro Abate committed
179
  "(`$A , `$B)","(Int , Bool)", mk_s [
180
181
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
182
183
    [P(V "A","Int");P(V "B","Bool")]
  ];
184
185
186
187
188
189
190
191
192

  "(Int , Bool)","(`$A , `$B)", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
  "(Bool , Bool)","(`$A , `$B)", mk_s [ [N("Bool", V "A");N("Bool", V "B")] ];

  "(`$A | (`$B , `$C))","(Int , Int)", mk_s [
    [P(V "A","(Int , Int)"); P(V "B","Empty")];
    [P(V "A","(Int , Int)"); P(V "C","Empty")];
    [P(V "A","(Int , Int)"); P(V "B","Int"); P(V "C","Int")];

Pietro Abate's avatar
Pietro Abate committed
193
  ];
194
195

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
196
197
    [P(V "A","Int");P(V "B","Int")]
  ];
198
(*
Pietro Abate's avatar
Pietro Abate committed
199
200
201
  "(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
    [P(V "A","Empty")]
  ];
202
  *)
203
204
205
206
]

let test_norm =
  "test tallying norm" >:::
207
208
209
210
211
    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
212
213
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
214
215
216
217
      )
    ) norm_tests
;;

218
let merge_tests = [
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]], 
    mk_s [
      [P(V "A","Empty");P(V "B","Empty")]
    ];

  "unsat 1", mk_s [[P(V "A", "Int | Bool");N("Int",V "B");P(V "B", "Empty")]], Tallying.CS.unsat;

  "unsat 2", mk_s [[N("Bool",V "B"); N("`$B", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;

  "quad", mk_s [[N("Bool | Int",V "B"); N("`$B",V "A"); P(V "A", "Int | Bool")]],
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]], 
    mk_s [[N("`$B", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];

  "A B", mk_s [[P(V "A", "`$B")]], mk_pp (P(V "A","`$B"));

  "", mk_s [[P(V "B", "Empty")]], mk_pp (P(V "B","Empty"));

  "", mk_s [[P(V "A", "Int");P(V "B", "Bool"); P(V "A", "Empty")]],
    mk_s [
      [P(V "A","Empty");P(V "B","Bool")]
    ]
];;
245
246
247

let test_merge =
  "test tallying merge" >:::
248
249
250
251
252
253
254
255
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
        let result = 
          try 
            Tallying.CS.S.fold (fun c acc ->
              Tallying.CS.union (Tallying.merge c) acc
            ) s Tallying.CS.S.empty
          with Tallying.UnSatConstr -> Tallying.CS.unsat
256
        in
257
258
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
259
260
261
262
      )
    ) merge_tests
;;

263
264
265
266
267
268
269
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 [
Pietro Abate's avatar
Pietro Abate committed
270
271
    [("A","Int | Bool");("B","Int | Bool")];
    [("A","Empty");("B","Empty")]
272
  ];
Pietro Abate's avatar
Pietro Abate committed
273
274
275
276
277
278

  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
    [("A","Empty")];
    [("A","Int");("B","Bool")];
  ];

279
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
Pietro Abate's avatar
Pietro Abate committed
280
    [("A","Empty")];
281
  ];
Pietro Abate's avatar
Pietro Abate committed
282

283
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
Pietro Abate's avatar
Pietro Abate committed
284
285
286
287

  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[]];

  [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [[("A","Int");("B","Int")]];
288
289
290
291
292
293
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
294
  "test tallying" >:::
295
296
297
298
    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
299
300
        let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
        SubStSet.assert_equal (elem expected) (elem result)
301
302
303
304
      )
    ) tallying_tests
;;

305
306
let all =
  "all tests" >::: [
307
    test_constraints;
308
    test_norm;
309
    test_merge;
310
    test_tallying;
311
312
313
314
315
316
317
318
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()