Commit faadeded authored by Danny Willems's avatar Danny Willems

Use file instead of 'hand-written' AST.

parent 5b8fa17f
......@@ -33,54 +33,11 @@ let check (t : raw_term) =
(* -------------------------------------------------------------------------- *)
(* Sample well-typed terms. *)
let identity =
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
let terms : raw_term list = [
identity;
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeApp (TeTyApp (identity, TyVar "A"), TeVar "x")
));
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeTyAbs ("B", TeAbs ("y", TyVar "B",
TeLet ("id", identity,
TePair (
TeApp (TeTyApp (TeVar "id", TyVar "A"), TeVar "x"),
TeApp (TeTyApp (TeVar "id", TyVar "B"), TeVar "y")
)
)
))));
]
let () =
List.iter check terms
(* -------------------------------------------------------------------------- *)
(* Sample ill-typed terms. *)
let ill_typed : raw_term list = [
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeApp (TeVar "x", TeVar "x")));
TeProj (1, identity);
TeTyAbs ("A",
TeLet ("id", TeAbs ("x", TyVar "A", TeVar "x"),
TeTyApp (TeVar "id", TyVar "A")
)
);
]
let () =
List.iter check ill_typed
let argc = Array.length Sys.argv in
if argc > 1 then
let f = open_in @@ Array.get Sys.argv 1 in
check @@ Parser.top_level Lexer.prog (Lexing.from_channel f);
close_in f
else print_endline "You must give a file."
(* TEMPORARY report unbound term variables, with locations. *)
(* TEMPORARY report unbound type variables, with locations. *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment