tallyingTest.ml 15.4 KB
Newer Older
1
open OUnit2
2
open Types
3

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

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

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

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

Pietro Abate's avatar
Pietro Abate committed
42
43
44
45
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
46
47
  let aux l =
    List.fold_left (fun acc -> function
48
49
      |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
50
51
    ) Tallying.CS.M.empty l
  in
52
  List.fold_left (fun acc l ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
53
    Tallying.CS.S.add (aux l) acc
Pietro Abate's avatar
Pietro Abate committed
54
55
  ) Tallying.CS.S.empty ll

56
let mk_union_res l1 l2 =
57
  let aux l =
58
    List.fold_left (fun acc -> function
59
60
      |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))
61
    ) Tallying.CS.M.empty l
62
  in
63
64
65
66
67
68
  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
69
(* check invariants on the constraints sets *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
70
71
72
73
74
75
76
77
78
79
80
81
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
82
let test_constraint_ops () = [
83
84
85
86
87
88

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

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

]
124

125
let test_constraints =
126
  "constraints" >:::
127
128
129
130
131
    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
132
    ) (test_constraint_ops ())
133
134
135
;;

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

Pietro Abate's avatar
Pietro Abate committed
137
let norm_tests () = [
Pietro Abate's avatar
Pietro Abate committed
138
139
140
141
142
143
144
145
146
147
148
149
  "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
150
151
152
153
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
154

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

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

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

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

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

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

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

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

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

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

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

214
215
216
]

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

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

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

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

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

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

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

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

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

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

299
300
301
302
303
304
  [("((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")]
  ];
305
306
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
307
308

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

Pietro Abate's avatar
Pietro Abate committed
310
  (* map even *)
311
312
313
314
315
316
317
318
(*  [("(`$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")], [[]];
319
320
]

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

351
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
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

463
464
465
466
          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
467
468

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

          assert_equal ~pp_diff:(fun fmt _ ->
            Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
474
475
476
            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
477
478
479
480
481
        with Tallying.Step1Fail -> assert_equal [] []
      )
    ) apply_raw_tests 
;;

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

491
let main () =
492
  OUnit2.run_test_tt_main suite
493
494
;;

495
main ()