Commit 6f4371d8 authored by POTTIER Francois's avatar POTTIER Francois

Fix [Main] after a change of naming conventions.

parent f65ef79d
......@@ -22,26 +22,26 @@ let delta =
TLambda (x, delta_body)
let omega =
TApp (delta, copy delta)
TApp (delta, copy_term delta)
let samples = [
TVar y;
id;
TApp (id, TVar y);
TApp (id, TVar x);
TApp (id, copy id);
TApp (id, copy_term id);
delta;
omega;
import KitImport.empty (TLambda ("x", TVar "x"));
import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
import_term KitImport.empty (TLambda ("x", TVar "x"));
import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
]
let closed_samples = [
id;
TApp (id, copy id);
TApp (id, copy_term id);
delta;
omega;
import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
]
let evaluate f =
......@@ -51,13 +51,13 @@ let evaluate f =
of atoms, using [Atom.show]. *)
let nhprint oc t =
Print.term oc (show t)
Print.term oc (show_term t)
(* A hygienic term printer. This printer uses [export]. *)
let hprint oc t =
(* works for closed terms only, as of now *)
Print.term oc (export KitExport.empty t)
Print.term oc (export_term KitExport.empty t)
let () =
printf "Testing size...\n";
......@@ -65,20 +65,20 @@ let () =
TVar y, 1;
id, 2;
TApp (id, TVar y), 4;
TApp (id, copy id), 5;
TApp (id, copy_term id), 5;
delta, 4;
omega, 9;
] |> List.iter (fun (t, i) ->
assert (size t = i)
assert (size_term t = i)
)
let print_copy t =
printf "copy(%a) = %a\n%!"
let print_copy_term t =
printf "copy_term(%a) = %a\n%!"
nhprint t
nhprint (copy t)
nhprint (copy_term t)
let () =
evaluate print_copy
evaluate print_copy_term
let print_export t =
printf "export(%a) = %a\n%!"
......@@ -105,7 +105,7 @@ let () =
evaluate print_fa'
let print_subst1 u x t =
let t' = subst1 u x t in
let t' = subst_term_term1 u x t in
printf "substituting %a for %a in %a = ...\n %a\n%s\n%!"
nhprint u
Atom.print x
......@@ -117,7 +117,7 @@ let () =
print_subst1 (TVar y) x (TVar x);
print_subst1 (TVar y) x (TVar y);
print_subst1 delta x delta_body;
print_subst1 (copy delta) x (copy delta);
print_subst1 (copy_term delta) x (copy_term delta);
()
let print_equiv t1 t2 =
......@@ -130,13 +130,13 @@ let () =
print_equiv id id;
print_equiv id (TVar x);
print_equiv (TVar x) (TVar y);
print_equiv delta (copy delta);
print_equiv omega (copy omega);
print_equiv delta (copy_term delta);
print_equiv omega (copy_term omega);
print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar y));
print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar x));
print_equiv
(import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z"))))
(import KitImport.empty (TLambda ("z", TLambda ("y", TVar "z"))))
(import_term KitImport.empty (TLambda ("z", TLambda ("z", TVar "z"))))
(import_term KitImport.empty (TLambda ("z", TLambda ("y", TVar "z"))))
;
()
......
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