diff --git a/demos/system-F-type/Main.ml b/demos/system-F-type/Main.ml index 7c8787c1c6c3503af2bb561983c574e0493e3e84..fca04810a93aa759875ae68d9394d1a61e6fee3b 100644 --- a/demos/system-F-type/Main.ml +++ b/demos/system-F-type/Main.ml @@ -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