Commit 9390af13 authored by POTTIER Francois's avatar POTTIER Francois

More tests.

parent ad79b4f9
......@@ -35,6 +35,8 @@ let hprint oc t =
(* Test parameters. *)
(* TEMPORARY test with small parameters first, then increase. *)
let number = 1000
let size = 1000
let atoms = 100
......@@ -94,14 +96,42 @@ let () =
assert (wf_term t)
)
(* The size computation should succeed. *)
(* [size_term] should succeed. *)
let () =
printf "Computing sizes...\n%!";
on_wf_nominal_terms (fun t ->
printf "Testing size...\n%!";
on_arbitrary_nominal_terms (fun t ->
ignore (size_term t : int)
)
(* [show_term] should succeed. *)
let () =
printf "Testing show...\n%!";
on_arbitrary_nominal_terms (fun t ->
ignore (show_term t : raw_term)
)
(* On a closed term, [show] is actually hygienic. *)
let () =
printf "Testing show on closed terms...\n%!";
on_closed_nominal_terms (fun t ->
let u : raw_term = show_term t in
let v : nominal_term = import_term KitImport.empty u in
assert (equiv_term t v)
)
(* Round-trip property of [import] and [export] on closed terms. *)
let () =
printf "Testing import/export round-trip...\n%!";
on_closed_nominal_terms (fun t ->
let u : raw_term = export_term KitExport.empty t in
let v : nominal_term = import_term KitImport.empty u in
assert (equiv_term t v)
)
(* [fa] and [occurs] should be consistent with each other. *)
let () =
......@@ -131,6 +161,55 @@ let () =
on_wf_nominal_terms test_copy;
on_closed_nominal_terms test_copy
(* Test substitution. *)
let size_of_u = 100
let () =
printf "Testing substitution...\n%!";
let (=) = equiv_term in
on_wf_nominal_terms (fun t ->
(* TEMPORARY should choose randomly and efficiently *)
match Atom.Set.choose (fa_term t) with
| exception Not_found ->
()
| x ->
let u = generate_nominal atoms size_of_u in
let t' = subst_term_term1 u x t in
assert (wf_term t');
assert (Atom.Set.equal
(fa_term t')
(Atom.Set.union (fa_term u) (Atom.Set.remove x (fa_term t)))
);
assert (t' = subst_term_term1 u x t);
assert (wf_term (TLambda (x, t)));
(* subst_term_term1 u x (TLambda (x, t)) = TLambda (x, t) *)
(* cannot be checked as these are illegal arguments to substitution *)
begin match t with
| TVar _ -> assert false
| TLambda (y, t) ->
assert (subst_term_term1 u x (TLambda (y, t)) =
TLambda (y, subst_term_term1 u x t))
| TApp (t1, t2) ->
assert (subst_term_term1 u x (TApp (t1, t2)) =
TApp (subst_term_term1 u x t1, subst_term_term1 u x t2))
end
);
let x = Atom.freshh "x"
and y = Atom.freshh "y" in
let u = generate_nominal atoms size_of_u in
assert (subst_term_term1 u x (TVar x) = u);
assert (subst_term_term1 u x (TVar y) = TVar y);
on_wf_nominal_terms (fun t ->
assert (subst_term_term1 u x t = t);
assert (subst_term_term1 u x t == t) (* note physical equality *)
);
(* Test that [equiv] distinguishes certain terms. *)
assert (not (TVar x = TVar y));
assert (not (TLambda (x, TVar x) = TLambda (y, TVar x)));
assert (not (TVar x = TLambda (x, TVar x)));
assert (not (TLambda (x, TLambda (y, TVar x)) = TLambda (x, TLambda (y, TVar y))))
(* [fa] and [occurs] should be consistent with each other. *)
let () =
......@@ -150,6 +229,8 @@ let () =
) ba
)
(* TEMPORARY cleanup beyond this line *)
(* Sample terms. *)
let x =
......
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