From a7006dcbb8ef880414f4e0956a9cf944433ddf84 Mon Sep 17 00:00:00 2001
From: Olivier <olivier.martinot@inria.fr>
Date: Wed, 7 Sep 2022 12:14:48 +0200
Subject: [PATCH] Smart constructors in TestF.ml.
---
client/test/TestF.ml | 191 ++++++++++++++++++++++++-------------------
1 file changed, 109 insertions(+), 82 deletions(-)
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 1bcf5c6..851fc5b 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -1,125 +1,152 @@
open Client
+(* -------------------------------------------------------------------------- *)
+
+(* AST helper functions *)
+
+let (-->) ty1 ty2 =
+ F.TyArrow (ty1, ty2)
+
+let unit =
+ F.Tuple (F.dummy_range, [])
+
+let unit_type =
+ F.TyProduct []
+
+let unit_pattern =
+ F.PTuple (F.dummy_range, [])
+
+let var x =
+ F.(Var (dummy_range, x))
+
+let _annot ty t =
+ F.(Annot (dummy_range, ty, t))
+
+let abs x ty t =
+ F.(Abs (dummy_range, x, ty, t))
+
+let app t u =
+ F.(App (dummy_range, t, u))
+
+let tyabs x t =
+ F.(TyAbs (dummy_range, x, t))
+
+let _tyapp t ty =
+ F.(TyApp (dummy_range, t, ty))
+
+let tuple ts =
+ F.(Tuple (dummy_range, ts))
+
+let letprod xs t u =
+ F.(LetProd (dummy_range, xs, t, u))
+
+let variant lbl datatype t =
+ F.(Variant (dummy_range, lbl, datatype, t))
+
+let match_ ty scrutinee branches =
+ F.(Match (dummy_range, ty, scrutinee, branches))
+
+let pvar x =
+ F.(PVar (dummy_range, x))
+
+let pwildcard =
+ F.(PWildcard dummy_range)
+
+let ptuple ps =
+ F.(PTuple (dummy_range, ps))
+
+let pvariant lbl datatype t =
+ F.(PVariant (dummy_range, lbl, datatype, t))
+
+(* -------------------------------------------------------------------------- *)
+
(* ∀a b. ({} -> (a * (a -> b))) -> b
Λa b. fun (p : {} -> (a * (a -> b))) ->
let (x, f) = p () in f x
*)
let let_prod =
- let open F in
let alpha, beta = 0, 1 in
let p, f, x = "p", "f", "x" in
- TyAbs (dummy_range, alpha, TyAbs (dummy_range, beta,
- Abs (dummy_range, p, TyArrow (TyProduct [],
- TyProduct [TyVar alpha; TyArrow (TyVar alpha, TyVar beta)]),
- LetProd (dummy_range, [x; f],
- App (dummy_range,
- Var (dummy_range, p),
- Tuple (dummy_range, [])),
- App (dummy_range, Var (dummy_range, f), Var (dummy_range, x))))))
+ tyabs alpha @@
+ tyabs beta @@
+ abs p (unit_type --> F.(TyProduct [TyVar alpha; TyVar alpha --> TyVar beta])) @@
+ letprod [x; f]
+ (app (var p) (tuple []))
+ (app (var f) (var x))
(* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *)
let match_with_prod =
let alpha, beta = 1, 0 in
- F.(
- TyAbs(dummy_range, alpha,
- TyAbs(dummy_range, beta,
- Abs(dummy_range, "x",
- TyProduct [ TyVar alpha ; TyVar beta ],
- Match(dummy_range, TyVar beta,
- Var (dummy_range, "x"),
- [
- (PTuple (dummy_range,
- [ PWildcard dummy_range ; PVar (dummy_range, "y") ]) ,
- Var (dummy_range, "y"))
- ]
- )
- )
- )
- )
- )
+ tyabs alpha @@
+ tyabs beta @@
+ abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar beta ]) @@
+ match_ (F.TyVar beta) (var "x") [
+ (ptuple [ pwildcard ; pvar "y" ]) , var"y"
+ ]
(* option *)
let option_env =
let option_typedecl =
let open Datatype in {
- name = Type "option";
- type_params = [ 0 ];
- data_kind = Variant;
- labels_descr = [
- {
- label_name = Label "None";
- type_name = Type "option";
- arg_type = F.TyProduct [];
- } ; {
- label_name = Label "Some";
- type_name = Type "option";
- arg_type = F.TyVar 0;
- }
- ];
- }
+ name = Type "option";
+ type_params = [ 0 ];
+ data_kind = Variant;
+ labels_descr = [
+ {
+ label_name = Label "None";
+ type_name = Type "option";
+ arg_type = F.TyProduct [];
+ } ; {
+ label_name = Label "Some";
+ type_name = Type "option";
+ arg_type = F.TyVar 0;
+ }
+ ];
+ }
in
Datatype.Env.add_decl Datatype.Env.empty option_typedecl
-let unit = F.Tuple (F.dummy_range, [])
-let unit_pattern = F.PTuple (F.dummy_range, [])
-
(* None *)
let none =
let alpha = 0 in
- F.(
- Variant (dummy_range,
- Datatype.Label "None", (Datatype.Type "option", [TyForall (alpha, TyVar alpha)]), unit)
- )
+ let label = Datatype.Label "None" in
+ let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+ variant label datatype unit
let none_pattern =
let alpha = 0 in
- F.(
- PVariant (dummy_range,
- Datatype.Label "None",
- (Datatype.Type "option", [TyForall (alpha, TyVar alpha)]),
- unit_pattern
- )
- )
+ let label = Datatype.Label "None" in
+ let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+ pvariant label datatype unit_pattern
(* Some Λα.λx:α.x *)
let some =
let alpha = 0 in
- F.(
- Variant (dummy_range,
- Datatype.Label "Some",
- (Datatype.Type "option", [ TyForall (alpha, TyArrow (TyVar alpha, TyVar alpha)) ]),
- TyAbs (dummy_range, alpha, Abs (dummy_range, "x", TyVar alpha, Var (dummy_range, "x")))
- )
- )
+ let label = Datatype.Label "Some" in
+ let datatype = Datatype.Type "option",
+ [ F.TyForall (alpha, F.TyVar alpha --> F.TyVar alpha) ] in
+ variant label datatype @@
+ tyabs alpha @@
+ abs "x" (F.TyVar alpha) @@
+ var "x"
let some_pattern =
let alpha = 0 in
- F.(
- PVariant (dummy_range,
- Datatype.Label "Some",
- (Datatype.Type "option", [ TyForall (alpha, TyVar alpha) ]),
- PWildcard dummy_range
- )
- )
+ let label = Datatype.Label "Some" in
+ let datatype = Datatype.Type "option", [ F.TyForall (alpha, F.TyVar alpha) ] in
+ pvariant label datatype pwildcard
(* Λα. match None with
| None -> ()
| Some (_) -> ()
*)
-let match_none = F.(
+let match_none =
let alpha = 0 in
- TyAbs(dummy_range, alpha,
- Match (dummy_range,
- TyProduct [] ,
- none,
- [
- (none_pattern , unit)
- ;
- (some_pattern , unit)
- ]
- )
- )
- )
+ tyabs alpha @@
+ match_ unit_type none @@ [
+ (none_pattern , unit);
+ (some_pattern , unit);
+ ]
let test_ok_from_ast datatype_env t () =
Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
--
GitLab