tests.ml 2.53 KB
Newer Older
Pietro Abate's avatar
Pietro Abate committed
1
open OUnit
2
3
4
5
6
7

(* open Types *)

let parse_typ s =
  let st = Stream.of_string s in
  let astpat = Parser.pat st in 
Pietro Abate's avatar
Pietro Abate committed
8
  let nodepat = Typer.typ Builtin.env astpat in
9
10
11
  Types.descr nodepat
;;

Pietro Abate's avatar
Pietro Abate committed
12
(*
13
14
15
let t1 = Types.descr (Typer.typ Builtin.env (Parser.pat (Stream.of_string "`A :> Int")) );;
let t2 = Types.descr (Typer.typ Builtin.env (Parser.pat (Stream.of_string "Any")) );;
Types.subtype  t1 t2 ;;
Pietro Abate's avatar
Pietro Abate committed
16
17
18
19
*)

let subtype_tests = [
  "Int" , "Any", true;
20
21
22
23
24
25
26
27
28
  "`A | Int" , "`A", false;
  "`A | ( 0--* | *--0)" , "`A", false;
  "42 | Int" , "42", false;
  "Int" , "Empty", false;
  "'c' | Int" , "1", false;
  "`A | Char" , "`A", false;
  "`A | (`A,`B)" , "`A", false;
  "`A -> `B | Int" , "`A -> `B", false;
  "(`A,`B) | Int" , "(`A,`B)", false;
Pietro Abate's avatar
Pietro Abate committed
29
30
31
32
33
34
35
36
37
38
  "Any" , "Any", true;
  "Empty" , "Empty", true;
  "Empty" , "Any", true;

  "0--*" , "Int", true;
  "1--5" , "0--*", true;
  "0--*" , "Int", true;
  "1--5" , "1--*", true;
  "1--5" , "1--5", true;

39
  "Any -> `A" , "Any", true;
Pietro Abate's avatar
Pietro Abate committed
40

41
  "`A -> `B" , "`A -> `B", true;
Pietro Abate's avatar
Pietro Abate committed
42
  "Any -> `a" , "Any -> Any", true;
43
44
45
46
47
48
  "`A -> `B" , "Empty -> Any", true;
  "(`A -> `C) | (`B -> `C)" , "(`A & `B) -> `C", true;
  "(`A & `B) | (`A & `C)" , "`A & (`B | `C)", true;
  "`A & (`B | `C)" , "(`A & `B) | (`A & `C)", true;
  "(`A,`B) | (`C,`D)" , "((`A | `C) , (`B | `D))", true;
  "(`A , `B & `C)" , "(`A,`B) & (`A,`C)", true;
Pietro Abate's avatar
Pietro Abate committed
49
50
51
52
53
54
55
  (*
  "mu x . Int -> (Nat , x)" , "mu x . Nat -> (Int , x)", true;
  "mu x . (a,x)" , "mu y . (a,y)", true;
  *)
  "Any" , "Int", false ;
  "Any" , "Empty", false ;

56
57
58
59
  "`A -> `B" , "`A", false ;
  "Any -> `A" , "Empty", false ;
  "Any -> `A" , "Any -> Empty", false ;
  "`A -> `B" , "`A -> `C", false ;
Pietro Abate's avatar
Pietro Abate committed
60
61
62
63
64

  "Int" , "0--*", false ;
  "1--5" , "1--4", false ;
  "Int" , "0--*", false ;

65
  "`$X" , "Any", true;
66
67
68
69
70
  "`$X | Int" , "Any", true;
  "Any", "`$X | (Any \\ `$X)", true;
  "Any", "(42 & `$X) | (Any \\ (42 & `$X))", true;
  "Any", "(41 & `$X) | (Any \\ (42 & `$X))", false;
  "Any", "Any \\ Char", false;
Pietro Abate's avatar
Pietro Abate committed
71
72
73
74
75
76
77
78
];;

let test_subtype =
  "test subtype" >::: 
    List.map (fun (s1,s2,expected) ->
      (Printf.sprintf " %s <: %s " s1 s2) >:: (fun _ ->
          let t1 = parse_typ s1 in
          let t2 = parse_typ s2 in
79
          let result = Types.subtype t1 t2 in
Pietro Abate's avatar
Pietro Abate committed
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
          if result <> expected then
            begin
              (* Printf.printf "subtyping error %s <: %s\n" s1 s2; *)
              Printf.printf "found %b, should be %b\n" result expected
            end;
          assert_equal result expected
      )
    ) subtype_tests
;;


let all =
  "all tests" >::: [
    test_subtype;
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()
101