tallyingTest.ml 15.8 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
(* the abstract field is ignored in the comparison *)
12
module ESet = OUnitDiff.SetMake (struct
13
  type t = (Var.var * Types.t)
14
  let compare (v1,t1) (v2,t2) =
15 16 17 18
    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)
19
  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %a)" Var.print v Types.Print.pp_type t
20 21
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)
22

23
module SubStSet = OUnitDiff.SetMake (struct
24 25 26 27 28 29
  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)

30
module MSet = OUnitDiff.SetMake (struct
31
  type t = Tallying.CS.m
32
  let compare = Tallying.CS.M.compare
Pietro Abate's avatar
Pietro Abate committed
33
  let pp_printer = Tallying.CS.pp_m
34 35 36
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

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

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

  "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"));

83
  "prod var",mk_prod [N("('B)",V "A");P(V "B","Bool | Int")],
84
      mk_union_res
85
        [N("('B)",V "A");P(V "B","Bool | Int")]
86 87 88 89 90 91 92 93 94 95 96 97 98 99
        [];

  "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")],
100
      mk_union_res
101 102 103 104 105 106 107 108 109 110 111 112 113
      [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")],
114
      mk_union_res
115 116 117 118
        [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
        [P(V "A","Empty");P(V "B","Empty")];

]
119

120
let test_constraints =
121
  "constraints" >:::
122 123 124 125 126
    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
127
    ) (test_constraint_ops ())
128 129 130
;;

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

Pietro Abate's avatar
Pietro Abate committed
132
let norm_tests () = [
Pietro Abate's avatar
Pietro Abate committed
133 134 135 136
  "Int", "Empty", Tallying.CS.unsat;
  "(Int,Int)", "Empty", Tallying.CS.unsat;
  "Int -> Int", "Empty" , Tallying.CS.unsat;

137
  "Bool -> Bool","Int -> ('A)", Tallying.CS.unsat;
Pietro Abate's avatar
Pietro Abate committed
138 139
  "Int", "Bool", Tallying.CS.unsat;
  "Int", "Empty", Tallying.CS.unsat;
140
  "[] -> []","Int -> ('A)", Tallying.CS.unsat;
Pietro Abate's avatar
Pietro Abate committed
141 142 143 144

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

145
  "(('A) -> Bool)", "(('B) -> ('B))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
146
    [P(V "B","Empty")];
147
    [N("('B)",V "A");N("Bool",V "B")]
Pietro Abate's avatar
Pietro Abate committed
148
  ];
149

150 151 152 153
  "('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")]];
154

155
  "(Int -> Bool)", "(('A) -> ('B))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
156 157 158
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
159

160
  "(Int -> Int) | (Bool -> Bool)", "(('A) -> ('B))", mk_s [
161 162
     [P(V "A","Empty")];
    (* All these are subsumed as less general then (A <= 0) *)
Pietro Abate's avatar
Pietro Abate committed
163 164 165 166
    [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")]
  ];
167

168
  "(('A) -> ('B))", "(Int -> Int) | (Bool -> Bool)", mk_s [
169 170 171 172
    [P(V "B","Int");N("Int",V "A")];
    [P(V "B","Bool");N("Bool",V "A")];
  ];

Pietro Abate's avatar
Pietro Abate committed
173
  (*
174
  "([0--*] & `true)", "(('A) | Int) & ((Any \\ ('A)) | Bool)",
175
  *)
176

177
  "(('A) , ('B))","(Int , Bool)", mk_s [
178 179
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
180 181
    [P(V "A","Int");P(V "B","Bool")]
  ];
182

183
  "{a=(('A) , ('B))}","{a=(Int , Bool)}", mk_s [
Pietro Abate's avatar
Pietro Abate committed
184 185 186 187 188
    [P(V "A","Empty")];
    [P(V "B","Empty")];
    [P(V "A","Int");P(V "B","Bool")]
  ];

189
  "{a=(Int , Bool)}","{a=(('A) , ('B))}", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
Pietro Abate's avatar
Pietro Abate committed
190

191 192
  "(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")] ];
193

194
  "(('A) | (('B) , ('C)))","(Int , Int)", mk_s [
195 196 197 198
    [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
199
  ];
200

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

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

209
  "Int -> Bool", "('A)", mk_s [[N("Int -> Bool",V "A")]];
210

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

213
  "((('A) , Int) | (('B) , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
214 215 216
    [P(V "A","Int");P(V "B","Int")]
  ];

217 218 219
]

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

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

240
  "unsat 2", mk_s [[N("Bool",V "B"); N("('B)", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;
241

242
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("('B)",V "A"); P(V "A", "Int | Bool")]],
243
    mk_s [
244
      [N("('B)", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
245 246
    ];

247 248
  "add one", mk_s [[N("('B)", V "A");P(V "A","Int | Bool")]],
    mk_s [[N("('B)", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];
249

250
  "A B", mk_s [[P(V "A", "('B)")]], mk_pp (P(V "A","('B)"));
251 252 253 254 255 256 257 258

  "", 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")]
    ]
];;
259 260

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

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

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

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

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

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

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

311
  [("((('A) , Int) & (('B) , Bool))","(Int , (Int & Bool))")], [[]];
312

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

  (* records *)
  [("{a=Int}","Any")], [[]];
319
  [("{a=('A)}","Any")], [[]];
320
  [("{a=Int}","{a=(Int|Bool)}")], [[]];
Pietro Abate's avatar
Pietro Abate committed
321
  (*
322 323 324
  [("{a=Bool -> Bool}","{b=Int -> ('A)}")], [[]];
  [("{a=(Int -> Int) | (Bool -> Bool)}","{b=(('A) -> ('B))}")], [[]];
  [("{a=Int} -> Int", "{a=('A)} -> ('A)")], [[]];
Pietro Abate's avatar
Pietro Abate committed
325
  *)
326 327
]

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

354 355
let apply_raw_tests = [
  "iter  hd",
356
   "(('A) -> []) -> [ ('A)* ] -> []","[ ('A0)* ] -> ('A0)";
357 358

  "iteri  assoc",
359
   "(Int -> ('A) -> []) -> [ ('A)* ] -> []","('A1) -> [ (('A1) , ('B1))* ] -> ('B1)";
360 361

  "map  length",
362
   "(('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","[ ('A3)* ] -> Int";
363 364

  "map  length & hd",
365
   "(('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","([ ('A3)* ] -> Int) & ([ ('A4)* ] -> ('A4))";
366 367

  "mapi  mem",
368
   "(Int -> ('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","('A45) -> [ ('A45)* ] -> Bool";
369 370

  "mapi  mem & memq",
371
   "(Int -> ('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","(('A45) -> [ ('A45)* ] -> Bool) & (('A46) -> [ ('A46)* ] -> Bool)";
372 373

  "rev_map  length",
374
   "(('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","[ ('A53)* ] -> Int";
375 376

  "rev_map  length & hd",
377
   "(('A) -> ('B)) -> [ ('A)* ] -> [ ('B)* ]","([ ('A53)* ] -> Int) & ([ ('A54)* ] -> ('A54))";
378 379

  "fold_left  append",
380
   "(('A) -> ('B) -> ('A)) -> ('A) -> [ ('B)* ] -> ('A)","[ ('A95)* ] -> [ ('A95)* ] -> [ ('A95)* ]";
381 382

  "fold_right  hd",
383
   "(('A) -> ('B) -> ('B)) -> [ ('A)* ] -> ('B) -> ('B)","[ ('A103)* ] -> ('A103)";
384 385

  "iter2  hd",
386
   "(('A) -> ('B) -> []) -> [ ('A)* ] -> [ ('B)* ] -> []","[ ('A117)* ] -> ('A117)";
387 388

  "map2  hd",
389
   "(('A) -> ('B) -> ('C)) -> [ ('A)* ] -> [ ('B)* ] -> [ ('C)* ]","[ ('A124)* ] -> ('A124)";
390 391

  "rev_map2  hd",
392
   "(('A) -> ('B) -> ('C)) -> [ ('A)* ] -> [ ('B)* ] -> [ ('C)* ]","[ ('A160)* ] -> ('A160)";
393 394

  "fold_left2  assoc",
395
   "(('A) -> ('B) -> ('C) -> ('A)) -> ('A) -> [ ('B)* ] -> [ ('C)* ] -> ('A)","('A196) -> [ (('A196) , ('B196))* ] -> ('B196)";
396 397

  "for_all  hd",
398
   "(('A) -> Bool) -> [ ('A)* ] -> Bool","[ ('A198)* ] -> ('A198)";
399 400

  "exists  hd",
401
   "(('A) -> Bool) -> [ ('A)* ] -> Bool","[ ('A199)* ] -> ('A199)";
402 403

  "for_all2  hd",
404
   "(('A) -> ('B) -> Bool) -> [ ('A)* ] -> [ ('B)* ] -> Bool","[ ('A200)* ] -> ('A200)";
405 406

  "exists2  hd",
407
   "(('A) -> ('B) -> Bool) -> [ ('A)* ] -> [ ('B)* ] -> Bool","[ ('A211)* ] -> ('A211)";
408 409

  "mem  length",
410
   "('A) -> [ ('A)* ] -> Bool","[ ('A222)* ] -> Int";
411 412

  "memq  length",
413
   "('A) -> [ ('A)* ] -> Bool","[ ('A264)* ] -> Int";
414 415

  "find  hd",
416
   "(('A) -> Bool) -> [ ('A)* ] -> ('A)","[ ('A306)* ] -> ('A306)";
417 418

  "filter  hd",
419
   "(('A) -> Bool) -> [ ('A)* ] -> [ ('A)* ]","[ ('A307)* ] -> ('A307)";
420 421

  "find_all  hd",
422
   "(('A) -> Bool) -> [ ('A)* ] -> [ ('A)* ]","[ ('A308)* ] -> ('A308)";
423 424

  "partition  hd",
425
   "(('A) -> Bool) -> [ ('A)* ] ->( [ ('A)* ] , [ ('A)* ])","[ ('A309)* ] -> ('A309)";
426 427

  "assoc  length",
428
   "('A) -> [ (('A) , ('B))* ] -> ('B)","[ ('A310)* ] -> Int";
429 430

  "assoc  length & hd",
431
   "('A) -> [ (('A) , ('B))* ] -> ('B)","([ ('A310)* ] -> Int) & ([ ('A311)* ] -> ('A311))";
432 433

  "mem_assoc  length",
434
   "('A) -> [ (('A) , ('B))* ] -> Bool","[ ('A394)* ] -> Int";
435 436

  "mem_assoc  length & hd",
437
   "('A) -> [ (('A) , ('B))* ] -> Bool","([ ('A394)* ] -> Int) & ([ ('A395)* ] -> ('A395))";
438 439

  "mem_assq  length",
440
   "('A) -> [ (('A) , ('B))* ] -> Bool","[ ('A436)* ] -> Int";
441 442

  "mem_assq  length & hd",
443
   "('A) -> [ (('A) , ('B))* ] -> Bool","([ ('A436)* ] -> Int) & ([ ('A437)* ] -> ('A437))";
444 445

  "remove_assoc  length",
446
   "('A) -> [ (('A) , ('B))* ] -> [ (('A) , ('B))* ]","[ ('A478)* ] -> Int";
447 448

  "remove_assoc  length & hd",
449
   "('A) -> [ (('A) , ('B))* ] -> [ (('A) , ('B))* ]","([ ('A478)* ] -> Int) & ([ ('A479)* ] -> ('A479))";
450 451 452 453 454 455 456 457 458 459 460 461 462 463
]

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
464
          let (sl,s,t,g) = Types.apply_raw Var.Set.empty s t in
465

466 467 468 469
          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
470 471

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

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

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

494
let main () =
495
  OUnit2.run_test_tt_main suite
496 497
;;

498
main ()