tallyingTest.ml 16 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
module ESet = OUnitDiff.SetMake (struct
12
  type t = (Var.var * Types.t)
13
  let compare (v1,t1) (v2,t2) =
14 15
    if (v1,t1) == (v2,t2) then 0
    else let c = Var.compare v1 v2 in if c <> 0 then c
16
    else Types.compare t1 t2
17
  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %a)" Var.pp v Types.Print.pp_type t
18 19
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)
20

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

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

Pietro Abate's avatar
Pietro Abate committed
35 36 37 38
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
39 40
  let aux l =
    List.fold_left (fun acc -> function
41 42
      |P(V alpha,t) -> Tallying.CS.M.add Var.Set.empty (Var.mk alpha) (Types.empty,parse_typ t) acc
      |N(t,V alpha) -> Tallying.CS.M.add Var.Set.empty (Var.mk alpha) (parse_typ t,Types.any) acc
Pietro Abate's avatar
WIP  
Pietro Abate committed
43 44
    ) Tallying.CS.M.empty l
  in
45
  List.fold_left (fun acc l ->
Pietro Abate's avatar
WIP  
Pietro Abate committed
46
    Tallying.CS.S.add (aux l) acc
Pietro Abate's avatar
Pietro Abate committed
47 48
  ) Tallying.CS.S.empty ll

49
let mk_union_res l1 l2 =
50
  let aux l =
51
    List.fold_left (fun acc -> function
52 53
      |P(V v,s) -> Tallying.CS.M.inter Var.Set.empty acc (Tallying.CS.M.singleton (Var.mk v) (Types.empty, parse_typ s))
      |N(s,V v) -> Tallying.CS.M.inter Var.Set.empty acc (Tallying.CS.M.singleton (Var.mk v) (parse_typ s, Types.any))
54
    ) Tallying.CS.M.empty l
55
  in
56 57 58 59 60 61
  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
62
(* check invariants on the constraints sets *)
Pietro Abate's avatar
WIP  
Pietro Abate committed
63
let mk_pp = function
64 65
  |P(V alpha,t) -> Tallying.CS.singleton Var.Set.empty (Tallying.Pos (Var.mk alpha,parse_typ t))
  |N(t,V alpha) -> Tallying.CS.singleton Var.Set.empty (Tallying.Neg (parse_typ t,Var.mk alpha))
Pietro Abate's avatar
WIP  
Pietro Abate committed
66 67 68

let mk_prod l =
    List.fold_left (fun acc c ->
69
      Tallying.CS.prod Var.Set.empty (mk_pp c) acc
Pietro Abate's avatar
WIP  
Pietro Abate committed
70 71 72 73 74
    ) 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
75
let test_constraint_ops () = [
76 77 78 79 80

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

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

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

]
117

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

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

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

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

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

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

148 149 150 151
  "'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")]];
152

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

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

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

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

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

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

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

189 190
  "(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")] ];
191

192
  "('A | ('B , ('C)))","(Int , Int)", mk_s [
193 194 195 196
    [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 204
  "('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
205
  ];
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
  "(('A , Int) | ('B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
212 213 214
    [P(V "A","Int");P(V "B","Int")]
  ];

215 216 217
]

let test_norm =
218
  "norm" >:::
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
223
        let result = Tallying.norm Var.Set.empty (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
    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;

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

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

245 246
  "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")]];
247

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

  "", 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
            Tallying.CS.S.fold (fun c acc ->
265
              Tallying.CS.union (Tallying.merge Var.Set.empty c) acc
266
            ) 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 = [
281
  [("((Int | Bool) -> Int)", "('A -> 'B)")], mk_e [
Pietro Abate's avatar
Pietro Abate committed
282 283 284 285
    [(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
  [("((Int,Int) , (Int | Bool))","('A,Int) | (('B,Int),Bool)")], mk_e [
301 302
    [(V "A", "(Int,Int)"); (V "B","Int")]
  ];
303
  [("(('A , Int) | ('B , Bool))","(Int , (Int | Bool))")], mk_e [
304 305
    [(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
(*  [("('A -> 'B) -> ['A ] -> ['B ]","((Int -> Bool) & (('A \\ Int) -> ('A \\ Int)))")], [[]];*)
  [("('A -> 'A)", "((Int -> Int) & (Bool -> Bool)) -> ('T)")], mk_e [];
314 315 316

  (* records *)
  [("{a=Int}","Any")], [[]];
317
  [("{a='A}","Any")], [[]];
318
  [("{a=Int}","{a=(Int|Bool)}")], [[]];
Pietro Abate's avatar
Pietro Abate committed
319
  (*
320 321 322
  [("{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
323
  *)
324 325
]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501
let squaresubtype_tests = [
  "'A -> 'A", "Bool -> Bool", [], true;
  "'A -> 'B", "Int -> Bool", [], true;
  "'A -> 'B", "Int -> Bool", ["A"], false;
  "'A -> 'A", "(Int -> Int) & (Bool -> Bool)", [], true;
]

let test_squaresubtype =
  "test squaresubtype" >:::
    List.map (fun (s,t,delta,expected) ->
      (Printf.sprintf " %s [= %s " s t) >:: (fun _ ->
          let t1 = parse_typ s in
          let t2 = parse_typ t in
          let delta = List.fold_left (fun acc v -> Var.Set.add (Var.mk v) acc) Var.Set.empty delta in
          assert_equal (Types.is_squaresubtype delta t1 t2) expected
      )
    ) squaresubtype_tests
;;

502 503
let suite =
  "tests" >::: [
504
    test_constraints;
505
    test_norm;
506
    test_merge;
507
    test_tallying;
508
    test_apply;
509
    test_squaresubtype;
510
  ]
511

512
let main () =
513
  OUnit2.run_test_tt_main suite
514 515
;;

516
main ()