tallyingTest.ml 15.5 KB
Newer Older
1
2
(* TODO: Switch to OUnit2 when tests are fixed, then use tools/install_hooks.sh -d to check tallying before a commit *)
open OUnit(*2*)
3
open Types
4

5
let parse_typ s =
6
  let st = Stream.of_string s in
7
  let astpat = Parser.pat st in
8
  let nodepat = Typer.typ Builtin.env astpat in
9
10
11
  Types.descr nodepat
;;

12
13
14
15
16
17
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 *)
18
module ESet = OUnitDiff.SetMake (struct
19
  type t = (Var.var * Types.t)
20
  let compare (v1,t1) (v2,t2) =
21
22
23
24
    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)
Pietro Abate's avatar
Pietro Abate committed
25
  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.print v (to_string Print.print t)
26
27
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)
28

29
module SubStSet = OUnitDiff.SetMake (struct
30
31
32
33
34
35
  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)

36
module MSet = OUnitDiff.SetMake (struct
37
  type t = Tallying.CS.m
38
  let compare = Tallying.CS.M.compare
Pietro Abate's avatar
Pietro Abate committed
39
  let pp_printer = Tallying.CS.pp_m
40
41
42
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

Pietro Abate's avatar
Pietro Abate committed
43
44
45
46
type pp = P of vv * string | N of string * vv
and vv = V of string

let mk_s ll =
Pietro Abate's avatar
WIP    
Pietro Abate committed
47
48
  let aux l =
    List.fold_left (fun acc -> function
49
50
      |P(V alpha,t) -> Tallying.CS.M.add ((*true,*)Var.mk alpha) (Types.empty,parse_typ t) acc
      |N(t,V alpha) -> Tallying.CS.M.add ((*false,*)Var.mk alpha) (parse_typ t,Types.any) acc
Pietro Abate's avatar
WIP    
Pietro Abate committed
51
52
    ) Tallying.CS.M.empty l
  in
53
  List.fold_left (fun acc l ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
54
    Tallying.CS.S.add (aux l) acc
Pietro Abate's avatar
Pietro Abate committed
55
56
  ) Tallying.CS.S.empty ll

57
let mk_union_res l1 l2 =
58
  let aux l =
59
    List.fold_left (fun acc -> function
60
61
      |P(V v,s) -> Tallying.CS.M.merge acc (Tallying.CS.M.singleton (Var.mk v) (Types.empty, parse_typ s))
      |N(s,V v) -> Tallying.CS.M.merge acc (Tallying.CS.M.singleton (Var.mk v) (parse_typ s, Types.any))
62
    ) Tallying.CS.M.empty l
63
  in
64
65
66
67
68
69
  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
70
(* check invariants on the constraints sets *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
71
72
73
74
75
76
77
78
79
80
81
82
let mk_pp = function
  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))

let mk_prod l =
    List.fold_left (fun acc c ->
      Tallying.CS.prod (mk_pp c) acc
    ) 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
83
let test_constraint_ops () = [
84
85
86
87
88
89

  "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")],
90
91
      mk_union_res
        [N("`$B",V "A");P(V "B","Bool | Int")]
92
93
94
95
96
97
98
99
100
101
102
103
104
105
        [];

  "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")],
106
      mk_union_res
107
108
109
110
111
112
113
114
115
116
117
118
119
      [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")],
120
      mk_union_res
121
122
123
124
        [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
        [P(V "A","Empty");P(V "B","Empty")];

]
125

126
let test_constraints =
127
  "constraints" >:::
128
129
130
131
132
    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)
      )
Pietro Abate's avatar
Pietro Abate committed
133
    ) (test_constraint_ops ())
134
135
136
;;

(* ^ => & -- v => | *)
Pietro Abate's avatar
Pietro Abate committed
137

Pietro Abate's avatar
Pietro Abate committed
138
let norm_tests () = [
Pietro Abate's avatar
Pietro Abate committed
139
140
141
142
143
144
145
146
147
148
149
150
  "Int", "Empty", Tallying.CS.unsat;
  "(Int,Int)", "Empty", Tallying.CS.unsat;
  "Int -> Int", "Empty" , Tallying.CS.unsat;

  "Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
  "Int", "Bool", Tallying.CS.unsat;
  "Int", "Empty", Tallying.CS.unsat;
  "[] -> []","Int -> `$A", Tallying.CS.unsat;

  "Any", "Empty",  Tallying.CS.unsat;
  "Empty", "Empty",  Tallying.CS.sat;

Pietro Abate's avatar
Pietro Abate committed
151
152
153
154
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
155

Pietro Abate's avatar
Pietro Abate committed
156
157
158
159
  "`$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")]];
160

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

Pietro Abate's avatar
Pietro Abate committed
166
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
167
168
     [P(V "A","Empty")];
    (* All these are subsumed as less general then (A <= 0) *)
Pietro Abate's avatar
Pietro Abate committed
169
170
171
172
    [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")]
  ];
173
174
175
176
177
178

  "(`$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
179
  (*
180
181
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
182

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

  "(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
197
  ];
198
199

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
200
201
    [P(V "A","Int");P(V "B","Int")]
  ];
Pietro Abate's avatar
WIP    
Pietro Abate committed
202
203

  "(`$A -> `$B) -> [ `$A ] -> [ `$B ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$Gamma", mk_s [
Pietro Abate's avatar
Pietro Abate committed
204
205
    [P(V "A","Empty")]
  ];
206

207
  "Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
208
209

  "((`$A , Int) & (`$B , Bool))","(Int , (*Int & Bool*) Empty)",Tallying.CS.sat;
Pietro Abate's avatar
Pietro Abate committed
210
211
212
213
214

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

215
216
217
]

let test_norm =
218
  "norm" >:::
219
220
221
222
223
    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
224
225
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
226
      )
Pietro Abate's avatar
Pietro Abate committed
227
    ) (norm_tests ())
228
229
;;

Pietro Abate's avatar
Pietro Abate committed
230
let merge_tests () = [
231
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
232
233
234
235
236
237
238
239
    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;

240
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
241
242
243
244
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

245
  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
246
247
248
249
250
251
252
253
254
255
256
    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")]
    ]
];;
257
258

let test_merge =
259
  "merge" >:::
260
261
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
262
        let result =
263
          try
264
265
266
            Tallying.CS.S.fold (fun c acc ->
              Tallying.CS.union (Tallying.merge c) acc
            ) s Tallying.CS.S.empty
267
          with Tallying.UnSatConstr _ -> Tallying.CS.unsat
268
        in
269
270
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
271
      )
Pietro Abate's avatar
Pietro Abate committed
272
    ) (merge_tests ())
273
274
;;

275
276
let mk_e ll =
  List.map (fun l ->
277
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
278
279
280
  ) ll

let tallying_tests = [
Pietro Abate's avatar
Pietro Abate committed
281
282
283
284
285
  [("((Int | Bool) -> Int)", "(`$A -> `$B)")], mk_e [
    [(V "A","Empty")];
    [(V "A","Int | Bool");(V "B","Int")]
  ];

286
  [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
287
288
    [(V "A","Int | Bool");(V "B","Int | Bool")];
    [(V "A","Empty");(V "B","Empty")]
289
  ];
Pietro Abate's avatar
Pietro Abate committed
290
291

  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
292
293
    [(V "A","Empty")];
    [(V "A","Int");(V "B","Bool")];
Pietro Abate's avatar
Pietro Abate committed
294
295
  ];

296
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
297
    [(V "A","Empty")];
298
  ];
Pietro Abate's avatar
Pietro Abate committed
299

300
301
302
303
304
305
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [
    [(V "A", "(Int,Int)"); (V "B","Int")]
  ];
  [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
    [(V "A","Int");(V "B","Int")]
  ];
306
307
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
308
309

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

Pietro Abate's avatar
Pietro Abate committed
311
  (* map even *)
312
313
314
315
316
317
318
319
(*  [("(`$A -> `$B) -> [`$A ] -> [`$B ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];*)
  [("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e [];

  (* records *)
  [("{a=Int}","Any")], [[]];
  [("{a=`$A}","Any")], [[]];
  [("{a=Int}","{a=(Int|Bool)}")], [[]];
  [("{a=Int} -> Int", "{a=`$A} -> `$A")], [[]];
320
321
]

Pietro Abate's avatar
Pietro Abate committed
322
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
323
324
325
326
let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
327
  "tallying" >:::
328
329
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
330
331
        try
          let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
332
          let sigma = Tallying.tallying l in
333
          List.iter (fun (s,t) ->
Pietro Abate's avatar
Pietro Abate committed
334
            List.iter (fun sigma ->
Pietro Abate's avatar
Pietro Abate committed
335
336
              let s_sigma = Tallying.(s $$ sigma) in
              let t_sigma = Tallying.(t $$ sigma) in
337
              assert_equal ~pp_diff:(fun fmt _ ->
Pietro Abate's avatar
Pietro Abate committed
338
339
340
                  Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
                  Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
              ) (Types.subtype s_sigma t_sigma) true
341
            ) sigma
Pietro Abate's avatar
Pietro Abate committed
342
343
          ) l
          (*
344
345
          let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
          SubStSet.assert_equal (elem expected) (elem result)
Pietro Abate's avatar
Pietro Abate committed
346
      *)
347
        with Tallying.Step1Fail -> assert_equal expected []
348
349
350
351
      )
    ) tallying_tests
;;

352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
let apply_raw_tests = [
  "iter  hd",
   "(`$A -> []) -> [ `$A* ] -> []","[ `$A0* ] -> `$A0";

  "iteri  assoc",
   "(Int -> `$A -> []) -> [ `$A* ] -> []","`$A1 -> [ (`$A1 , `$B1)* ] -> `$B1";

  "map  length",
   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A3* ] -> Int";

  "map  length & hd",
   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A3* ] -> Int) & ([ `$A4* ] -> `$A4)";

  "mapi  mem",
   "(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","`$A45 -> [ `$A45* ] -> Bool";

  "mapi  mem & memq",
   "(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","(`$A45 -> [ `$A45* ] -> Bool) & (`$A46 -> [ `$A46* ] -> Bool)";

  "rev_map  length",
   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A53* ] -> Int";

  "rev_map  length & hd",
   "(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A53* ] -> Int) & ([ `$A54* ] -> `$A54)";

  "fold_left  append",
   "(`$A -> `$B -> `$A) -> `$A -> [ `$B* ] -> `$A","[ `$A95* ] -> [ `$A95* ] -> [ `$A95* ]";

  "fold_right  hd",
   "(`$A -> `$B -> `$B) -> [ `$A* ] -> `$B -> `$B","[ `$A103* ] -> `$A103";

  "iter2  hd",
   "(`$A -> `$B -> []) -> [ `$A* ] -> [ `$B* ] -> []","[ `$A117* ] -> `$A117";

  "map2  hd",
   "(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A124* ] -> `$A124";

  "rev_map2  hd",
   "(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A160* ] -> `$A160";

  "fold_left2  assoc",
   "(`$A -> `$B -> `$C -> `$A) -> `$A -> [ `$B* ] -> [ `$C* ] -> `$A","`$A196 -> [ (`$A196 , `$B196)* ] -> `$B196";

  "for_all  hd",
   "(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A198* ] -> `$A198";

  "exists  hd",
   "(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A199* ] -> `$A199";

  "for_all2  hd",
   "(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A200* ] -> `$A200";

  "exists2  hd",
   "(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A211* ] -> `$A211";

  "mem  length",
   "`$A -> [ `$A* ] -> Bool","[ `$A222* ] -> Int";

  "memq  length",
   "`$A -> [ `$A* ] -> Bool","[ `$A264* ] -> Int";

  "find  hd",
   "(`$A -> Bool) -> [ `$A* ] -> `$A","[ `$A306* ] -> `$A306";

  "filter  hd",
   "(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A307* ] -> `$A307";

  "find_all  hd",
   "(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A308* ] -> `$A308";

  "partition  hd",
   "(`$A -> Bool) -> [ `$A* ] ->( [ `$A* ] , [ `$A* ])","[ `$A309* ] -> `$A309";

  "assoc  length",
   "`$A -> [ (`$A , `$B)* ] -> `$B","[ `$A310* ] -> Int";

  "assoc  length & hd",
   "`$A -> [ (`$A , `$B)* ] -> `$B","([ `$A310* ] -> Int) & ([ `$A311* ] -> `$A311)";

  "mem_assoc  length",
   "`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A394* ] -> Int";

  "mem_assoc  length & hd",
   "`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A394* ] -> Int) & ([ `$A395* ] -> `$A395)";

  "mem_assq  length",
   "`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A436* ] -> Int";

  "mem_assq  length & hd",
   "`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A436* ] -> Int) & ([ `$A437* ] -> `$A437)";

  "remove_assoc  length",
   "`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","[ `$A478* ] -> Int";

  "remove_assoc  length & hd",
   "`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","([ `$A478* ] -> Int) & ([ `$A479* ] -> `$A479)";
]

let test_apply =
  let print_test msg s t = Printf.sprintf "%s : (%s) o (%s)\n" msg s t in
  "apply" >:::
    let sigmacup sl t =
      List.fold_left (fun acc sigma -> 
        Types.cap acc Tallying.(t $$ sigma)
      ) Types.any sl
    in
    List.map (fun (msg,s,t) ->
      (print_test msg s t) >:: (fun _ ->
        try
          let (s,t) = (parse_typ s,parse_typ t) in
          let (sl,s,t,g) = Types.apply_raw s t in

464
465
466
467
          let gamma = Types.cons (Types.var (Var.mk "Gamma")) in

          let t1 = sigmacup sl s in
          let t2_gamma = sigmacup sl (Types.arrow (Types.cons t) gamma) in
468
469

          assert_equal ~pp_diff:(fun fmt _ ->
470
471
            Format.fprintf fmt "t1 < 0 -> 1 = %a\n" Types.Print.print t1
          ) (Types.subtype t1 (parse_typ "Empty -> Any")) true;
472
473
474

          assert_equal ~pp_diff:(fun fmt _ ->
            Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
475
476
477
            Format.fprintf fmt "t1 = %a\n" Types.Print.print t1;
            Format.fprintf fmt "t2 -> gamma = %a\n" Types.Print.print t2_gamma;
          ) (Types.subtype t1 t2_gamma) true
478
479
480
481
482
        with Tallying.Step1Fail -> assert_equal [] []
      )
    ) apply_raw_tests 
;;

483
484
let suite =
  "tests" >::: [
485
    test_constraints;
486
    test_norm;
487
    test_merge;
488
    test_tallying;
489
    test_apply;
490
  ]
491

492
let main () =
493
  OUnit(*2*).run_test_tt_main suite
494
495
;;

496
main ()