Commit 3fc62150 authored by POTTIER Francois's avatar POTTIER Francois

A worthless manual test.

parent 0a216213
......@@ -2,3 +2,36 @@ open AlphaLib
open Term
module T =
Toolbox.Make(Term)
let builtin = [
"*"
]
let ienv, xenv =
List.fold_left (fun (ienv, xenv) x ->
let ienv, a = KitImport.extend ienv x in
let xenv, _ = KitExport.extend xenv a in
ienv, xenv
) (KitImport.empty, KitExport.empty) builtin
let identity =
TLam (
TeleCons ("x", TVar "*", TeleNil),
TVar "x"
)
let defs =
TeleCons ("x", TApp (identity, [identity]),
TeleCons ("y", TApp (identity, [TVar "x"]),
TeleNil))
let test t =
let t = T.import_term ienv t in
let t = T.export_term xenv t in
()
let () =
List.iter test [
identity;
TLam (defs, TApp (identity, [TVar "x"; TVar "y"]))
]
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