tests.ml 3.8 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 66
(* polymorphic cduce extension *)

67
  "`$X" , "Any", true;
68 69 70 71 72
  "`$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;
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  "(`$A -> Bool, `$B -> `$B)", "(Int | Bool -> Int, `$A -> `$B)", false;
  (* ({ (int , true) } , {  }) *)
  "Int -> Int", "`$A -> `$A", false;
  (* { (true^[ A ] , any) } *)
  "Int -> Int", "Empty -> Any", true;
  "(`$A -> `$C) & (`$B -> `$C)", "(`$A | `$B) -> `$C", true;
  "((`$A -> `$C) & (`$B -> `$C))", "((`$A | `$B) -> `$C)", true;
  "((`$A | `$B) -> `$C)", "((`$A -> `$C) & (`$B -> `$C))", true;
  "(`$A -> `$B)", "(Any -> Any)", false;
  (* { (any , omega) } *)
  "(`A , `$X)", "((`A , (Any \\ `A)) | (`$X , `A))", false;
  (* (a , a^[ X ]) *)
  "(`$X & (`$X , `A))", "`C", false;
  (* (any^[ X ] , A)^[ X ] *) 
  "(((`$A , `$C) -> `$D1) & ((`$B , `$C) -> `$D2))", "(((`$A | `$B) , `$C) -> (`$D1 | `$D2))", true;
  "(`$A & (`$A , `T))", "`$A", true;
  "(Any -> Empty)","(`$A -> `$B)", true;
  "(`$A -> `$B)","(Empty -> Any)",true;
  "(`$B & `$A) | (`$B & (Any \\ `$A))","`$B", true;
  "`$B","(`$B & `$A) | (`$B & (Any \\ `$A))", true;
  "Any","(Any \\ (Any \\ ((`$B & `$A) | (`$B & (Any \\ `$A))) | Empty) | (Any \\ (`$B | Empty)))", true;
  "(`$A & (`$A , `T))","(`T1 -> `T2)", false;
  (* (any^[ A ] , t)^[ A ] *)
  "(x where x = (`$A & ((`$A , x) | `nil)))", "Empty", false;
  (* nil^[ A ] *)
  "(Any \\ (`$A -> `$B))","((Any -> Empty) -> `$B)", false;
Pietro Abate's avatar
Pietro Abate committed
99 100 101 102 103 104 105 106
];;

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
107
          let result = Types.subtype t1 t2 in
Pietro Abate's avatar
Pietro Abate committed
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
          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 ()
129