tallyingTest.ml 15.6 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

Pietro Abate's avatar
Pietro Abate committed
188 189 190 191 192 193 194 195
  "{a=(`$A , `$B)}","{a=(Int , Bool)}", mk_s [
    [P(V "A","Empty")];
    [P(V "B","Empty")];
    [P(V "A","Int");P(V "B","Bool")]
  ];

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

196 197 198 199 200 201 202 203
  "(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
204
  ];
205 206

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
207 208
    [P(V "A","Int");P(V "B","Int")]
  ];
Pietro Abate's avatar
WIP  
Pietro Abate committed
209 210

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

214
  "Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
215 216

  "((`$A , Int) & (`$B , Bool))","(Int , (*Int & Bool*) Empty)",Tallying.CS.sat;
Pietro Abate's avatar
Pietro Abate committed
217 218 219 220 221

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

222 223 224
]

let test_norm =
225
  "norm" >:::
226 227 228 229 230
    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
231 232
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
233
      )
Pietro Abate's avatar
Pietro Abate committed
234
    ) (norm_tests ())
235 236
;;

Pietro Abate's avatar
Pietro Abate committed
237
let merge_tests () = [
238
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
239 240 241 242 243 244 245 246
    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;

247
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
248 249 250 251
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

252
  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
253 254 255 256 257 258 259 260 261 262 263
    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")]
    ]
];;
264 265

let test_merge =
266
  "merge" >:::
267 268
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
269
        let result =
270
          try
271 272 273
            Tallying.CS.S.fold (fun c acc ->
              Tallying.CS.union (Tallying.merge c) acc
            ) s Tallying.CS.S.empty
274
          with Tallying.UnSatConstr _ -> Tallying.CS.unsat
275
        in
276 277
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
278
      )
Pietro Abate's avatar
Pietro Abate committed
279
    ) (merge_tests ())
280 281
;;

282 283
let mk_e ll =
  List.map (fun l ->
284
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
285 286 287
  ) ll

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

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

  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
299 300
    [(V "A","Empty")];
    [(V "A","Int");(V "B","Bool")];
Pietro Abate's avatar
Pietro Abate committed
301 302
  ];

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

307 308 309 310 311 312
  [("((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")]
  ];
313 314
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
315 316

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

Pietro Abate's avatar
Pietro Abate committed
318
  (* map even *)
319 320 321 322 323 324 325
(*  [("(`$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)}")], [[]];
Pietro Abate's avatar
Pietro Abate committed
326 327 328
  (*
  [("{a=Bool -> Bool}","{b=Int -> `$A}")], [[]];
  [("{a=(Int -> Int) | (Bool -> Bool)}","{b=(`$A -> `$B)}")], [[]];
329
  [("{a=Int} -> Int", "{a=`$A} -> `$A")], [[]];
Pietro Abate's avatar
Pietro Abate committed
330
  *)
331 332
]

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

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
Pietro Abate's avatar
Pietro Abate committed
469
          let (sl,s,t,g) = Types.apply_raw Var.Set.empty s t in
470

471 472 473 474
          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
475 476

          assert_equal ~pp_diff:(fun fmt _ ->
477 478
            Format.fprintf fmt "t1 < 0 -> 1 = %a\n" Types.Print.print t1
          ) (Types.subtype t1 (parse_typ "Empty -> Any")) true;
479 480 481

          assert_equal ~pp_diff:(fun fmt _ ->
            Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
482 483 484
            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
485 486 487 488 489
        with Tallying.Step1Fail -> assert_equal [] []
      )
    ) apply_raw_tests 
;;

490 491
let suite =
  "tests" >::: [
492
    test_constraints;
493
    test_norm;
494
    test_merge;
495
    test_tallying;
496
    test_apply;
497
  ]
498

499
let main () =
500
  OUnit2.run_test_tt_main suite
501 502
;;

503
main ()