From 1083149b06152d3e6ef24c36a7838e9aca23004b Mon Sep 17 00:00:00 2001
From: Olivier <olivier.martinot@inria.fr>
Date: Fri, 27 Jan 2023 14:53:33 +0100
Subject: [PATCH] Add tests for pattern-matching.
---
client/test/TestF.ml | 37 +++++++++++++++++++++++++++++++++++--
1 file changed, 35 insertions(+), 2 deletions(-)
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 7a766df..1c54e8d 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -83,7 +83,7 @@ let let_prod =
(app (var p) (tuple []))
(app (var f) (var x))
-(* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *)
+(* Λαβ. λx:{α*β}. match x with (_, y) -> y end *)
let match_with_prod =
let alpha, beta = 1, 0 in
tyabs alpha @@
@@ -93,6 +93,15 @@ let match_with_prod =
(ptuple [ pwildcard ; pvar "y" ]) , var"y"
]
+(* Λα. λx:{α*α}. match x with (y, y) -> y end *)
+let match_variable_bound_twice =
+ let alpha = 0 in
+ tyabs alpha @@
+ abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar alpha ]) @@
+ match_ (F.TyVar alpha) (var "x") [
+ (ptuple [ pvar "y" ; pvar "y" ]) , var"y"
+ ]
+
(* option *)
let option_env =
let option_typedecl =
@@ -157,6 +166,25 @@ let match_none =
(some_pattern , unit);
]
+(* Λα. λx:α.
+ match (x,Some x) with
+ | (y, None) -> y
+ | (y,Some y) -> y
+ end
+ *)
+let match_variable_bound_twice_under_tuple =
+ let alpha = 0 in
+ let none_label = Datatype.Label "None" in
+ let some_label = Datatype.Label "Some" in
+ let datatype = Datatype.Type "option", [ F.TyVar alpha ] in
+ tyabs alpha @@
+ abs "x" (F.TyVar alpha) @@
+ match_ (F.TyVar alpha)
+ (tuple [var "x"; variant some_label datatype (var "x")]) [
+ (ptuple [ pvar "y" ; pvariant none_label datatype unit_pattern ]) , var"y" ;
+ (ptuple [ pvar "y" ; pvariant some_label datatype (pvar "y") ]) , var"y"
+ ]
+
(* ( refl_{} : Eq(∀α.{} , {}) ) *)
let type_eq =
let alpha = 0 in
@@ -645,12 +673,17 @@ let test_suite =
"test F ast",
[ test_ok_from_ast "let prod" Datatype.Env.empty let_prod;
test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
+ test_type_error "match variable bound twice" Datatype.Env.empty
+ match_variable_bound_twice;
test_ok_from_ast "unit" option_env unit;
test_ok_from_ast "none" option_env none;
test_ok_from_ast "some" option_env some;
test_ok_from_ast "match none" option_env match_none;
+ test_type_error "match deep variable bound twice" option_env
+ match_variable_bound_twice_under_tuple;
test_type_error "type equality" Datatype.Env.empty type_eq;
- test_ok_from_ast "introduce type equality" Datatype.Env.empty introduce_type_eq;
+ test_ok_from_ast "introduce type equality" Datatype.Env.empty
+ introduce_type_eq;
test_ok_from_ast "symmetry" Datatype.Env.empty sym;
test_ok_from_ast "transitivity" Datatype.Env.empty trans;
test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall;
--
GitLab