Add tests for ML.

This commit is contained in:
Olivier 2023-02-25 16:29:49 +01:00
parent 2f94234ce2
commit cbb649ecbd
3 changed files with 51 additions and 8 deletions

View File

@ -50,6 +50,31 @@ let _app_pair = (* ill-typed *)
let unit =
ML.Tuple (None, [])
let for_ tyvars t =
ML.For (None, tyvars, t)
let annot t ty_annot =
ML.Annot (None, t, ty_annot)
let abs x t =
ML.Abs (None, x, t)
let arrow ty1 ty2 =
ML.TyArrow (None, ty1, ty2)
let alpha = ML.TyVar (None, "'a")
let beta = ML.TyVar (None, "'b")
let annot_id =
for_ ["'a"] @@
annot (abs "x" x) @@
(ML.Flexible, [], arrow alpha alpha)
let first_proj =
for_ ["'a"; "'b"] @@
annot (abs "x" (abs "y" x)) @@
(ML.Flexible, [], arrow alpha (arrow beta alpha))
(* "let x1 = (...[], ...[]) in ...[] x1" *)
let regression1 =
ML.Let (None, ML.Non_recursive,
@ -305,6 +330,8 @@ let test_suite =
test_case "leaf" tree_env leaf ;
test_case "node" tree_env node ;
test_case "abs match with" empty abs_match_with ;
test_case "annot id" empty annot_id;
test_case "first proj" empty first_proj;
test_case "match none" option_env match_none ;
test_case "match some" option_env match_some ;
test_case "boom 0" empty (boom 0);
@ -325,10 +352,11 @@ let testable_term =
in
Alcotest.testable pprint Test.CheckML.equal_term
let test_ok ?(typedecl="") s expected =
let (datatype_env, t) = Test.CheckML.from_string typedecl s in
let test_ok ?(typedecl="") s t =
let (datatype_env, expected) = Test.CheckML.from_string typedecl s in
Alcotest.check' testable_term ~msg:"equal" ~expected ~actual:t;
Alcotest.(check bool) "type inference" (Test.CheckML.test ~rectypes:false datatype_env t) true
Alcotest.(check bool) "type inference" true @@
(Test.CheckML.test ~rectypes:false datatype_env t)
let test_error_parsing ?(typedecl="") s =
let ok =
@ -457,6 +485,16 @@ let test_match_some_annotated () =
end|}
match_some_annotated
let test_annot_id () =
test_ok
"for 'a. (fun x -> x : 'a -> 'a)"
annot_id
let test_first_proj () =
test_ok
"for 'a 'b. (fun x y -> x : 'a -> 'b -> 'a)"
first_proj
(** Regressions *)
let test_regression1 () =
test_ok
@ -468,21 +506,18 @@ let test_regression2 () =
"let f = fun x -> let g = fun y -> (x, y) in g in fun x -> fun y -> f"
regression2
let a = ML.TyVar (None, "'a")
let b = ML.TyVar (None, "'b")
let id_annot annot =
ML.(Annot (None, Abs(None, "x", Var (None, "x")), annot))
let test_id_rigid () =
test_ok
"(fun x -> x : for 'a. 'a -> 'a)"
(id_annot (ML.Rigid, ["'a"], ML.TyArrow (None, a, a)))
(id_annot (ML.Rigid, ["'a"], ML.TyArrow (None, alpha, alpha)))
let test_id_flexible () =
test_ok
"(fun x -> x : some 'a 'b. 'a -> 'b)"
(id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (None, a, b)))
(id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (None, alpha, beta)))
let test_suite =
let open Alcotest in
@ -495,6 +530,8 @@ let test_suite =
test_case "id id error" `Quick test_idid_error;
test_case "delta delta error" `Quick test_delta_delta_error;
test_case "unit" `Quick test_unit;
test_case "annot id" `Quick test_annot_id;
test_case "first proj" `Quick test_first_proj;
test_case "regression1" `Quick test_regression1;
test_case "regression2" `Quick test_regression2;
test_case "abs match with" `Quick test_abs_match_with;

View File

@ -0,0 +1,2 @@
let _ =
for 'a 'b. (fun x -> fun y -> x : 'a -> 'b -> 'a)

View File

@ -264,6 +264,10 @@ Variable scope escape
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat first-proj.midml
$ midml first-proj.midml
# Pattern-matching
$ cat match-tuple.midml