Add tests for ML.

This commit is contained in:
Olivier 2023-02-25 16:29:49 +01:00
parent edb3f6296d
commit 16502a9dba
8 changed files with 105 additions and 8 deletions

View File

@ -700,6 +700,10 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
let loc = get_loc t in
let b = Buffer.create 128 in
PPrint.ToBuffer.pretty 0.9 80 b @@
(Solver.pprint (let0 (exist (hastype env t))));
Printf.printf "%s\n" (Buffer.contents b);
let+ (vs, t) =
correlate loc (let0 (exist (hastype env t))) in
(* [vs] are the binders that we must introduce *)

View File

@ -50,6 +50,43 @@ 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 app t u =
ML.App (None, t, u)
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 for_a_in_id =
app annot_id unit
let for_a_in_id_wrong =
for_ ["'a"] @@
app
(annot (abs "x" x) @@ (ML.Flexible, [], arrow alpha alpha))
unit
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 +342,10 @@ 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 "for a in id" empty for_a_in_id;
test_case "for a in wrong" empty for_a_in_id_wrong;
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 +366,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 +499,26 @@ let test_match_some_annotated () =
end|}
match_some_annotated
let test_annot_id () =
test_ok
"for 'a in (fun x -> x : 'a -> 'a)"
annot_id
let test_for_a_in_id () =
test_ok
"(for 'a in (fun x -> x : 'a -> 'a)) ()"
for_a_in_id
let test_for_a_in_id_wrong () =
test_ok
"for 'a in (fun x -> x : 'a -> 'a) ()"
for_a_in_id_wrong
let test_first_proj () =
test_ok
"for 'a 'b in (fun x y -> x : 'a -> 'b -> 'a)"
first_proj
(** Regressions *)
let test_regression1 () =
test_ok
@ -468,21 +530,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 +554,10 @@ 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 "for a in id" `Quick test_for_a_in_id;
test_case "for a in id wrong" `Quick test_for_a_in_id_wrong;
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 in (fun x -> fun y -> x : 'a -> 'b -> 'a)) ()

View File

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

View File

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

View File

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

View File

@ -0,0 +1,2 @@
let _ =
for 'a in fun x -> x

View File

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