Add tests
This commit is contained in:
parent
2353ef4710
commit
487c1f1fb4
|
@ -14,7 +14,44 @@ let let_prod =
|
|||
LetProd ([x; f], App (Var p, Tuple []),
|
||||
App (Var f, Var x)))))
|
||||
|
||||
(* Inj<∀α. α → α + ∀βα. α → β> 1 Λα.λx:α.x *)
|
||||
let variant =
|
||||
let alpha, beta = 0, 1 in
|
||||
F.(
|
||||
Inj
|
||||
(
|
||||
[
|
||||
TyForall (alpha, TyArrow (TyVar alpha, TyVar alpha)) ;
|
||||
TyForall (beta, TyForall (alpha, TyArrow (TyVar alpha, TyVar beta)))
|
||||
],
|
||||
1,
|
||||
TyAbs (alpha, Abs("x", TyVar alpha, Var "x"))
|
||||
)
|
||||
)
|
||||
|
||||
(* Λαβ. λx. match x with (_, y) -> y end *)
|
||||
let match_with =
|
||||
let alpha, beta = 1, 0 in
|
||||
F.(
|
||||
TyAbs(alpha,
|
||||
TyAbs(beta,
|
||||
Abs("x",
|
||||
TyProduct [ TyVar alpha ; TyVar beta ],
|
||||
Match(TyVar beta,
|
||||
Var "x",
|
||||
[
|
||||
(PTuple [ PWildcard ; PVar "y" ] ,
|
||||
Var "y")
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
|
||||
let () =
|
||||
Test.(Log.with_log CheckF.test let_prod);
|
||||
Test.(Log.with_log CheckF.test variant);
|
||||
Test.(Log.with_log CheckF.test match_with);
|
||||
print_endline "TestF: all tests passed."
|
||||
|
|
Loading…
Reference in New Issue