Smart constructors in TestF.ml.

This commit is contained in:
Olivier 2022-09-07 12:14:48 +02:00
parent 0d65e0621f
commit 47ec0af486
1 changed files with 109 additions and 82 deletions

View File

@ -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) ()