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