Commit fd366bf8 authored by POTTIER Francois's avatar POTTIER Francois

Modified [ba] to not require global uniqueness.

Renamed [wf] to [guq].
parent 52ee871a
......@@ -9,10 +9,7 @@ System F demo:
System F-type-term:
deal with both kinds of variables
Relax ba so as to not require well-formedness?
Define wf separately, relying on ba_wf internally.
Global uniqueness, or uniqueness along a branch?
Which wf criterion do we want? both?
Implement avoids. (Test for no-shadowing.)
Implement a subst that does not copy the grafted term?
Or parameterize subst over the copy operation that needs to be performed when grafting?
......@@ -43,6 +40,7 @@ Deal with more complex forms of binding.
How do we deal with forms where a name can have several binding occurrences?
e.g., or-patterns, join-calculus
let, let rec, multiple let, multiple let rec, telescopes
What about the distinction between expression types and pattern types?
Try dealing with binding and hash-consing at the same time.
......
......@@ -65,7 +65,7 @@ let () =
on_closed_nominal_terms (fun t ->
assert (closed_term t);
assert (Atom.Set.is_empty (fa_term t));
assert (wf_term t)
assert (guq_term t)
)
(* A collection of random (non-closed, non-well-formed) nominal terms. *)
......@@ -81,19 +81,19 @@ let on_arbitrary_nominal_terms f =
(* Copy them, so as to obtain well-formed (although non-closed) nominal terms. *)
let wf_nominal_terms : nominal_term list =
let guq_nominal_terms : nominal_term list =
printf "Copying these terms...\n%!";
List.map copy_term arbitrary_nominal_terms
let on_wf_nominal_terms f =
List.iter f wf_nominal_terms
let on_guq_nominal_terms f =
List.iter f guq_nominal_terms
(* These terms should be well-formed. *)
let () =
printf "Checking well-formedness...\n%!";
on_wf_nominal_terms (fun t ->
assert (wf_term t)
on_guq_nominal_terms (fun t ->
assert (guq_term t)
)
(* [size_term] should succeed. *)
......@@ -139,7 +139,7 @@ let () =
on_arbitrary_nominal_terms (fun t ->
assert (Atom.Set.is_empty (fa_term t) = closed_term t)
);
on_wf_nominal_terms (fun t ->
on_guq_nominal_terms (fun t ->
assert (Atom.Set.is_empty (fa_term t) = closed_term t)
)
......@@ -147,8 +147,8 @@ let () =
let () =
printf "Checking disjointness...\n%!";
assert (wf_terms closed_nominal_terms);
assert (wf_terms wf_nominal_terms)
assert (guq_terms closed_nominal_terms);
assert (guq_terms guq_nominal_terms)
(* [copy] should be the identity, up to alpha-equivalence. *)
......@@ -158,7 +158,7 @@ let test_copy t =
let () =
printf "Testing equiv/copy...\n%!";
on_arbitrary_nominal_terms test_copy;
on_wf_nominal_terms test_copy;
on_guq_nominal_terms test_copy;
on_closed_nominal_terms test_copy
(* Test substitution. *)
......@@ -168,7 +168,7 @@ let size_of_u = 100
let () =
printf "Testing substitution...\n%!";
let (=) = equiv_term in
on_wf_nominal_terms (fun t ->
on_guq_nominal_terms (fun t ->
(* TEMPORARY should choose randomly and efficiently *)
match Atom.Set.choose (fa_term t) with
| exception Not_found ->
......@@ -176,13 +176,13 @@ let () =
| x ->
let u = generate_nominal atoms size_of_u in
let t' = subst_term_term1 u x t in
assert (wf_term t');
assert (guq_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)));
assert (guq_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
......@@ -200,7 +200,7 @@ let () =
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 ->
on_guq_nominal_terms (fun t ->
assert (subst_term_term1 u x t = t);
assert (subst_term_term1 u x t == t) (* note physical equality *)
);
......@@ -210,6 +210,16 @@ let () =
assert (not (TVar x = TLambda (x, TVar x)));
assert (not (TLambda (x, TLambda (y, TVar x)) = TLambda (x, TLambda (y, TVar y))))
(* [fa] and [ba] should be consistent with each other. *)
let () =
printf "Checking fa and ba are consistent...\n%!";
on_guq_nominal_terms (fun t ->
let ba = ba_term t
and fa = fa_term t in
assert (Atom.Set.disjoint ba fa)
)
(* [fa] and [occurs] should be consistent with each other. *)
let () =
......@@ -220,7 +230,7 @@ let () =
assert (occurs_term a t); (* slow *)
) fa
);
on_wf_nominal_terms (fun t ->
on_guq_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));
......@@ -350,7 +360,7 @@ let () =
let print_wf t =
printf "wf(%a) = %b\n%!"
nhprint t
(wf_term t)
(guq_term t)
let () =
evaluate print_wf;
......
......@@ -78,6 +78,10 @@ __BA
BA(typ)
BA(term)
__GUQ
GUQ(typ)
GUQ(term)
__COPY
COPY(typ)
COPY(term)
......
......@@ -48,13 +48,13 @@ let extend_with_tyvar (env : env) (a : tyvar) : env =
(* Destructors. *)
let unfold ty =
assert (wf_typ ty);
assert (guq_typ ty);
match ty with
| TyMu (a, body) ->
(* No shadowing within [ty] implies [a # ba(body)]. *)
assert (not (Atom.Set.mem a (ba_typ body)));
(* The free names of [ty] are free in [body] too.
Strong well-formedness for [body] yields [fa(body) # ba(body)].
Global uniqueness for [body] yields [fa(body) # ba(body)].
Therefore, we have [fa(ty) # ba(body)]. *)
assert (Atom.Set.disjoint (fa_typ ty) (ba_typ body));
(* By the above, the bound names of [body] are disjoint with the
......@@ -131,9 +131,8 @@ let rec typeof env (t : nominal_term) : nominal_typ =
| TeTyApp (t, ty2) ->
let a, ty1 = as_forall (typeof env t) in
(* We need ba(ty1) # [ty2/a] for this substitution to be safe. *)
(* We have ba(ty1) # a because the type a.ty1 is well-formed. Weak uniqueness,
also known as no-shadowing, suffices. *)
assert (not (Atom.Set.mem a (ba_typ ty1))); (* TEMPORARY problem: ba is too strong *)
(* We have ba(ty1) # a because the type a.ty1 is satisfies no-shadowing. *)
assert (not (Atom.Set.mem a (ba_typ ty1)));
(* We have ba(ty1) # fa(ty2) because fa(ty2) is a subset of dom(env), that is,
env.tyvars, and typeof has the postcondition ba(\result) # env.tyvars. *)
subst_typ_typ1 ty2 a ty1
......
......@@ -55,33 +55,12 @@
(* -------------------------------------------------------------------------- *)
(* [ba_term] computes the set of bound atoms of a term and (at the same time)
checks that this term is well-formed, that is, no atom is bound twice. The
exception [IllFormed x] is raised if the atom [x] occurs twice in a binding
position. *)
(* [ba_terms] computes the set of bound atoms of a list of terms and at
the same time checks that no atom is bound twice, raising [IllFormed x]
if an atom [x] is bound twice -- possibly in different list elements. *)
(* [wf_term] is a variant of [ba_term] that returns a Boolean result. *)
(* [wf_terms] is a variant of [ba_term] that returns a Boolean result. The
call [wf_terms ts] tests whether the terms in the list [ts] are well-formed
and pairwise bound-atom-disjoint. *)
(* [wf_term] and [wf_terms] should be used only in debugging mode, typically
in an [assert] construct. They print the identity of one offending atom
on the standard error channel. *)
(* [ba_term] computes the set of bound atoms of a term. *)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
#define BAS_FUN(term) BA_FUN(CONCAT(term, s))
#define WF_FUN(term) CONCAT(wf_, term)
#define WFS_FUN(term) WF_FUN(CONCAT(term, s))
#define __BA \
exception IllFormed = KitBa.IllFormed \
class ['self] BA_CLASS = object (_ : 'self) \
inherit [_] reduce \
inherit [_] KitBa.reduce \
......@@ -90,14 +69,41 @@
#define BA(term) \
let BA_FUN(term) t = \
new BA_CLASS # VISIT(term) () t \
let BAS_FUN(term) ts = \
(* -------------------------------------------------------------------------- *)
(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
is bound twice within this term (not even along different branches). *)
(* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
no atom is bound twice within this list (not even within two distinct list
elements). *)
(* [guq_term] and [guq_terms] should be used only in debugging mode, typically
in an [assert] construct. They print the identity of one offending atom on
the standard error channel. *)
#define GUQ_CLASS __guq
#define GUQ_FUN(term) CONCAT(guq_, term)
#define GUQS_FUN(term) GUQ_FUN(CONCAT(term, s))
#define __GUQ \
class ['self] GUQ_CLASS = object (_ : 'self) \
inherit [_] reduce \
inherit [_] KitGuq.reduce \
end \
#define GUQ(term) \
let GUQ_FUN(term) t = \
new GUQ_CLASS # VISIT(term) () t \
let GUQS_FUN(term) ts = \
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (BA_FUN(term) t)) \
(fun accu t -> Atom.Set.disjoint_union accu (GUQ_FUN(term) t)) \
Atom.Set.empty ts \
let WF_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion BA_FUN(term) t \
let WFS_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion BAS_FUN(term) t \
let GUQ_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion GUQ_FUN(term) t \
let GUQS_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion GUQS_FUN(term) t \
(* -------------------------------------------------------------------------- *)
......
(* This kit serves to compute the set of ``bound atoms'' of a term, that is,
the set of all binding name occurrences. At the same time, we check that
the term is well-formed, that is, no atom is bound twice. The exception
[IllFormed x] is raised if the atom [x] occurs twice in a binding
position. *)
exception IllFormed = Atom.Set.NonDisjointUnion
type env = unit
the set of all binding name occurrences. *)
class ['self] reduce = object (_ : 'self)
......@@ -16,16 +9,11 @@ class ['self] reduce = object (_ : 'self)
method private visit_'fn () _x =
Atom.Set.empty
(* The monoid of sets of atoms, equipped with disjoint union, is used. *)
(* This can cause a [NonDisjointUnion] exception to be raised. *)
inherit [_] Atom.Set.disjoint_union_monoid
(* The monoid of sets of atoms is used. *)
inherit [_] Atom.Set.union_monoid
(* The atom [x] is added to the set of bound atoms when its scope is
exited. *)
(* An atom is added to the set of bound atoms when its scope is exited. *)
method private restrict x xs =
if Atom.Set.mem x xs then
raise (IllFormed x)
else
Atom.Set.add x xs
Atom.Set.add x xs
end
(* This kit serves to compute the set of ``bound atoms'' of a term (as in
[KitBa]) and at the same time, we check that the term satisfies ``global
uniqueness'', that is, no atom is bound twice inside this term (not even
along distinct branches). The exception [Atom.Set.NonDisjointUnion x] is
raised if the atom [x] occurs twice in a binding position. *)
class ['self] reduce = object (_ : 'self)
method private extend _x () =
()
method private visit_'fn () _x =
Atom.Set.empty
(* The monoid of sets of atoms, equipped with disjoint union, is used. *)
(* This can cause a [NonDisjointUnion] exception to be raised. *)
inherit [_] Atom.Set.disjoint_union_monoid
(* An atom is added to the set of bound atoms when its scope is exited. *)
method private restrict x xs =
if Atom.Set.mem x xs then
raise (Atom.Set.NonDisjointUnion x)
else
Atom.Set.add x xs
end
......@@ -41,6 +41,9 @@ module Make (Term : ToolboxInput.INPUT) = struct
__BA
BA(term)
__GUQ
GUQ(term)
__COPY
COPY(term)
......
......@@ -25,11 +25,9 @@ module Make (Term : ToolboxInput.INPUT) : sig
val closed_term: nominal_term -> bool
val occurs_term: Atom.t -> nominal_term -> bool
exception IllFormed of Atom.t (* = Atom.Set.NonDisjointUnion *)
val ba_term: nominal_term -> Atom.Set.t
val ba_terms: nominal_term list -> Atom.Set.t
val wf_term: nominal_term -> bool
val wf_terms: nominal_term list -> bool
val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool
val copy_term: nominal_term -> nominal_term
val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
......
......@@ -6,6 +6,7 @@ KitAvoid
KitEquiv
KitExport
KitFa
KitGuq
KitImport
KitShow
KitSubst
......
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