Add new unit tests for the subtyping algorithm

tests/libtest/tests.ml

@@ -62,12 +62,40 @@ let subtype_tests = [
   "1--5" , "1--4", false ;
   "Int" , "0--*", false ;
 
+(* polymorphic cduce extension *)
+
   "`$X" , "Any", true;
   "`$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;
+  "(`$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;
 ];;
 
 let test_subtype =