Commit f2afe36f authored by POTTIER Francois's avatar POTTIER Francois

A better [Main].

parent 84ccbc74
......@@ -3,17 +3,23 @@ open AlphaLib
open F
open FTypeChecker
let identity : raw_term =
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
let check (t : raw_term) =
printf "Raw term:\n%a\n"
Print.term t;
let t : nominal_term =
import_term KitImport.empty t
in
printf "Imported (and reexported) term:\n%a\n"
Print.term (export_term KitExport.empty t);
let ty : nominal_typ =
typeof t
in
printf "Inferred type:\n%a\n"
Print.typ (export_typ KitExport.empty ty)
let identity : nominal_term =
import_term KitImport.empty identity
let ty : nominal_typ =
typeof identity
let ty : raw_typ =
export_typ KitExport.empty ty
let terms : raw_term list = [
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"));
]
let () =
printf "Success.\nThis term has type %a.\n%!" (PPrintAux.adapt Print.typ) ty
List.iter check terms
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