tallyingTest.ml 15.6 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 464 465 466 467 468
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

          let s_sigma = sigmacup sl s in
          let t_sigma = sigmacup sl t in
          let t_sigma_domain = (Types.Arrow.domain(Types.Arrow.get t_sigma)) in

          assert_equal ~pp_diff:(fun fmt _ ->
Julien Lopez's avatar
Julien Lopez committed
469
            Format.fprintf fmt "t @@ sl < 0 -> 1 = %a\n" Types.Print.print t_sigma
470 471 472 473 474 475 476 477 478 479 480 481 482 483
          ) (Types.subtype t_sigma (parse_typ "Empty -> Any")) true;

          assert_equal ~pp_diff:(fun fmt _ ->
            Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
            Format.fprintf fmt "(s @@ sl) = %a\n" Types.Print.print s_sigma;
            Format.fprintf fmt "(t @@ sl) = %a\n" Types.Print.print t_sigma;
            Format.fprintf fmt "g = %a\n" Types.Print.print g;
            Format.fprintf fmt "domain(t @@ sl) = %a\n" Types.Print.print t_sigma_domain
          ) (Types.subtype s_sigma t_sigma) true
        with Tallying.Step1Fail -> assert_equal [] []
      )
    ) apply_raw_tests 
;;

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

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

497
main ()