Commit 8c3b8777 authored by POTTIER Francois's avatar POTTIER Francois

Implemented [avoids].

Run tests with increasing parameter sizes.
parent 8688d800
...@@ -8,6 +8,10 @@ module T = ...@@ -8,6 +8,10 @@ module T =
open T open T
let ( ** ) = Atom.Set.union
(* -------------------------------------------------------------------------- *)
(* [interval i j] constructs a list representation of the semi-open interval (* [interval i j] constructs a list representation of the semi-open interval
[i..j). *) [i..j). *)
...@@ -22,6 +26,30 @@ let rec interval i j : int list = ...@@ -22,6 +26,30 @@ let rec interval i j : int list =
let init i j (f : int -> 'a) : 'a list = let init i j (f : int -> 'a) : 'a list =
List.map f (interval i j) List.map f (interval i j)
(* [take n xs] returns the first [n] elements of [xs]. *)
let rec take n xs =
match n, xs with
| 0, _
| _, [] ->
[]
| _, (x :: xs as input) ->
let xs' = take (n - 1) xs in
if xs == xs' then
input
else
x :: xs'
(* [split xs] splits the set of atoms [xs] in two halves. *)
let halve xs =
let xs = Atom.Set.elements xs in
let n = List.length xs in
let xs = take (n/2) xs in
Atom.Set.of_list xs
(* -------------------------------------------------------------------------- *)
(* A non-hygienic printer of arbitrary terms. This printer shows the internal (* A non-hygienic printer of arbitrary terms. This printer shows the internal
identity of atoms, using [Atom.show]. *) identity of atoms, using [Atom.show]. *)
...@@ -33,13 +61,23 @@ let nhprint oc t = ...@@ -33,13 +61,23 @@ let nhprint oc t =
let hprint oc t = let hprint oc t =
Print.term oc (export_term KitExport.empty t) Print.term oc (export_term KitExport.empty t)
(* Test parameters. *) (* -------------------------------------------------------------------------- *)
(* A test run. *)
module Run (P : sig
(* TEMPORARY test with small parameters first, then increase. *) (* Test parameters. *)
let number = 1000 val number: int
let size = 1000 val size: int
let atoms = 100 val atoms: int
end) = struct open P
let () =
printf "Test run: number = %d, size = %d, atoms = %d.\n%!"
number size atoms
(* A collection of closed raw terms. *) (* A collection of closed raw terms. *)
...@@ -79,7 +117,7 @@ let arbitrary_nominal_terms : nominal_term list = ...@@ -79,7 +117,7 @@ let arbitrary_nominal_terms : nominal_term list =
let on_arbitrary_nominal_terms f = let on_arbitrary_nominal_terms f =
List.iter f arbitrary_nominal_terms List.iter f arbitrary_nominal_terms
(* Copy them, so as to obtain well-formed (although non-closed) nominal terms. *) (* Copy them, so as to obtain guq (although non-closed) nominal terms. *)
let guq_nominal_terms : nominal_term list = let guq_nominal_terms : nominal_term list =
printf "Copying these terms...\n%!"; printf "Copying these terms...\n%!";
...@@ -88,6 +126,12 @@ let guq_nominal_terms : nominal_term list = ...@@ -88,6 +126,12 @@ let guq_nominal_terms : nominal_term list =
let on_guq_nominal_terms f = let on_guq_nominal_terms f =
List.iter f guq_nominal_terms List.iter f guq_nominal_terms
let all_atoms_of_guq_nominal_terms =
List.fold_left (fun atoms t ->
atoms ** ba_term t ** fa_term t
) Atom.Set.empty guq_nominal_terms
(* These terms should be well-formed. *) (* These terms should be well-formed. *)
let () = let () =
...@@ -179,7 +223,7 @@ let () = ...@@ -179,7 +223,7 @@ let () =
assert (guq_term t'); assert (guq_term t');
assert (Atom.Set.equal assert (Atom.Set.equal
(fa_term t') (fa_term t')
(Atom.Set.union (fa_term u) (Atom.Set.remove x (fa_term t))) (fa_term u ** Atom.Set.remove x (fa_term t))
); );
assert (t' = subst_term_term1 u x t); assert (t' = subst_term_term1 u x t);
assert (guq_term (TLambda (x, t))); assert (guq_term (TLambda (x, t)));
...@@ -217,7 +261,24 @@ let () = ...@@ -217,7 +261,24 @@ let () =
on_guq_nominal_terms (fun t -> on_guq_nominal_terms (fun t ->
let ba = ba_term t let ba = ba_term t
and fa = fa_term t in and fa = fa_term t in
assert (Atom.Set.disjoint ba fa) assert (Atom.Set.disjoint ba fa);
assert (avoids_term fa t)
)
(* Test [avoid] and [avoids]. Must use guq terms because [avoids] requires
no shadowing. *)
let () =
printf "Computing all atoms of our guq terms...\n%!";
let some_atoms = halve (halve (all_atoms_of_guq_nominal_terms)) in
printf "Testing avoids on %d of %d atoms...\n%!"
(Atom.Set.cardinal some_atoms)
(Atom.Set.cardinal all_atoms_of_guq_nominal_terms)
;
on_guq_nominal_terms (fun t ->
let t' = avoid_term some_atoms t in
assert (equiv_term t t');
assert (avoids_term some_atoms t')
) )
(* [fa] and [occurs] should be consistent with each other. *) (* [fa] and [occurs] should be consistent with each other. *)
...@@ -239,7 +300,23 @@ let () = ...@@ -239,7 +300,23 @@ let () =
) ba ) ba
) )
(* TEMPORARY cleanup beyond this line *) end
(* -------------------------------------------------------------------------- *)
(* Run tests with increasing parameter sizes. *)
let rec run number size atoms =
if size <= 3000 then
let module R = Run(struct
let number = number
let size = size
let atoms = atoms
end) in
run number (3 * size) (2 * atoms)
let () =
run 1000 1 1
(* Sample terms. *) (* Sample terms. *)
...@@ -357,14 +434,14 @@ let () = ...@@ -357,14 +434,14 @@ let () =
; ;
() ()
let print_wf t = let print_guq t =
printf "wf(%a) = %b\n%!" printf "guq(%a) = %b\n%!"
nhprint t nhprint t
(guq_term t) (guq_term t)
let () = let () =
evaluate print_wf; evaluate print_guq;
print_wf (TApp (id, id)) print_guq (TApp (id, id))
(* (*
let () = let () =
......
...@@ -72,6 +72,26 @@ ...@@ -72,6 +72,26 @@
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
that is, no atom is bound twice along a branch. It returns [true] if these
two conditions are satisfied. *)
#define AVOIDS_CLASS __avoids
#define AVOIDS_FUN(term) CONCAT(avoids_, term)
#define __AVOIDS \
class ['self] AVOIDS_CLASS = object (_ : 'self) \
inherit [_] iter \
inherit [_] KitAvoids.iter \
end \
#define AVOIDS(term) \
let AVOIDS_FUN(term) env t = \
KitAvoids.handle_Shadowing (new AVOIDS_CLASS # VISIT(term)) env t \
(* -------------------------------------------------------------------------- *)
(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom (* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
is bound twice within this term (not even along different branches). *) is bound twice within this term (not even along different branches). *)
......
(* This kit serves to test whether the bound atoms of a term avoid a certain
set of in-scope atoms and at the same time check that there is no shadowing
inside this term (i.e., no atom is bound twice along a branch). *)
exception Shadowing of Atom.t
class ['self] iter = object (_ : 'self)
method private extend x env =
if Atom.Set.mem x env then
(* There is shadowing: the atom [x] is already in scope. *)
raise (Shadowing x)
else
Atom.Set.add x env
method private visit_'fn _env _x = ()
end
let handle_Shadowing f env x =
try
f env x; true
with Shadowing x ->
Printf.eprintf "Shadowing: %s\n%!" (Atom.show x);
false
...@@ -41,6 +41,9 @@ module Make (Term : ToolboxInput.INPUT) = struct ...@@ -41,6 +41,9 @@ module Make (Term : ToolboxInput.INPUT) = struct
__BA __BA
BA(term) BA(term)
__AVOIDS
AVOIDS(term)
__GUQ __GUQ
GUQ(term) GUQ(term)
......
...@@ -26,6 +26,7 @@ module Make (Term : ToolboxInput.INPUT) : sig ...@@ -26,6 +26,7 @@ module Make (Term : ToolboxInput.INPUT) : sig
val occurs_term: Atom.t -> nominal_term -> bool val occurs_term: Atom.t -> nominal_term -> bool
val ba_term: nominal_term -> Atom.Set.t val ba_term: nominal_term -> Atom.Set.t
val avoids_term: Atom.Set.t -> nominal_term -> bool
val guq_term: nominal_term -> bool val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool val guq_terms: nominal_term list -> bool
......
Atom Atom
BindingForms BindingForms
KitAvoid
KitAvoids
KitBa KitBa
KitCopy KitCopy
KitAvoid
KitEquiv KitEquiv
KitExport KitExport
KitFa KitFa
......
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