Commit ad79b4f9 authored by POTTIER Francois's avatar POTTIER Francois

More tests.

parent 8070b7a1
......@@ -105,15 +105,49 @@ let () =
(* [fa] and [occurs] should be consistent with each other. *)
let () =
printf "Comparing fa and occurs...\n%!";
printf "Comparing fa and closed...\n%!";
on_arbitrary_nominal_terms (fun t ->
let atoms = fa_term t in
assert (Atom.Set.is_empty (fa_term t) = closed_term t)
);
on_wf_nominal_terms (fun t ->
assert (Atom.Set.is_empty (fa_term t) = closed_term t)
)
(* Our well-formed terms should be disjoint. *)
let () =
printf "Checking disjointness...\n%!";
assert (wf_terms closed_nominal_terms);
assert (wf_terms wf_nominal_terms)
(* [copy] should be the identity, up to alpha-equivalence. *)
let test_copy t =
assert (equiv_term t (copy_term t))
let () =
printf "Testing equiv/copy...\n%!";
on_arbitrary_nominal_terms test_copy;
on_wf_nominal_terms test_copy;
on_closed_nominal_terms test_copy
(* [fa] and [occurs] should be consistent with each other. *)
let () =
printf "Comparing fa and occurs... (quadratic)\n%!";
on_arbitrary_nominal_terms (fun t ->
let fa = fa_term t in
Atom.Set.iter (fun a ->
if not (occurs_term a t) then begin
printf "Atom %a does not occur in term %a" Atom.print a nhprint t
end;
assert (occurs_term a t); (* slow *)
) atoms
) fa
);
on_wf_nominal_terms (fun t ->
let ba = ba_term t in
let fa = fa_term t in
assert (Atom.Set.is_empty (Atom.Set.inter ba fa));
Atom.Set.iter (fun a ->
assert (not (occurs_term a t)) (* slow *)
) ba
)
(* Sample 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