Commit f65ef79d authored by POTTIER Francois's avatar POTTIER Francois

Macros for [subst].

And a change of internal naming conventions.
parent b853d25a
......@@ -4,14 +4,14 @@
replaced with a fresh copy, and every free name is unchanged. *)
#define __COPY \
class ['self] copy = object (_ : 'self) \
class ['self] __copy = object (_ : 'self) \
inherit [_] map \
inherit [_] KitCopy.map \
end
#define COPY(term) \
let CONCAT(copy_, term) t = \
new copy # CONCAT(visit_, term) KitCopy.empty t
new __copy # CONCAT(visit_, term) KitCopy.empty t
(* -------------------------------------------------------------------------- *)
......@@ -20,14 +20,14 @@
is a debugging tool. *)
#define __SHOW \
class ['self] show = object (_ : 'self) \
class ['self] __show = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end
#define SHOW(term) \
let CONCAT(show_, term) t = \
new show # CONCAT(visit_, term) () t
new __show # CONCAT(visit_, term) () t
(* -------------------------------------------------------------------------- *)
......@@ -40,14 +40,14 @@
(* TEMPORARY use string * loc so as to be able to give a location *)
#define __IMPORT \
class ['self] import = object (_ : 'self) \
class ['self] __import = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
end
#define IMPORT(term) \
let CONCAT(import_, term) env t = \
new import # CONCAT(visit_, term) env t
new __import # CONCAT(visit_, term) env t
(* -------------------------------------------------------------------------- *)
......@@ -56,14 +56,14 @@
occurrence to be in the domain of [env]. *)
#define __EXPORT \
class ['self] export = object (_ : 'self) \
class ['self] __export = object (_ : 'self) \
inherit [_] map \
inherit [_] KitExport.map \
end
#define EXPORT(term) \
let CONCAT(export_, term) env t = \
new export # CONCAT(visit_, term) env t
new __export # CONCAT(visit_, term) env t
(* -------------------------------------------------------------------------- *)
......@@ -73,7 +73,7 @@
nodes of other types. *)
#define __SIZE \
class ['self] size = object (_ : 'self) \
class ['self] __size = object (_ : 'self) \
inherit [_] reduce as super \
inherit [_] KitTrivial.reduce \
inherit [_] VisitorsRuntime.addition_monoid \
......@@ -83,14 +83,14 @@
#define SIZE(term) \
let CONCAT(size_, term) t = \
new size # CONCAT(visit_, term) () t
new __size # CONCAT(visit_, term) () t
(* -------------------------------------------------------------------------- *)
(* [equiv] tests whether two terms are alpha-equivalent. *)
#define __EQUIV \
class equiv = object \
class __equiv = object \
inherit [_] iter2 \
inherit [_] KitEquiv.iter2 \
end
......@@ -98,5 +98,40 @@
#define EQUIV(term) \
let equiv t1 t2 = \
VisitorsRuntime.wrap2 \
(new equiv # CONCAT(visit_, term) KitEquiv.empty) \
(new __equiv # CONCAT(visit_, term) KitEquiv.empty) \
t1 t2
(* -------------------------------------------------------------------------- *)
(* [subst] applies a substitution to a nominal term, yielding a nominal term. *)
(* A substitution is a finite map of atoms to nominal things. Things need not
be terms: this is a thing-in-term substitution, substituting things for
variables in terms. *)
(* When applying a substitution [sigma] to a term [t], the GUH guarantees that
the free atoms of (the codomain of) [sigma] cannot be captured by a binder
within [t]. The GUH also guarantees that a binder within [t] cannot appear
in the domain of [sigma], which means that we can go down into [t] and apply
[sigma] to every variable. *)
(* The GUH is preserved by copying the things that are grafted into [t]. Thus,
it is not even necessary that [sigma] and [t] be disjoint, or that the
things in the codomain of [sigma] be pairwise disjoint. One should note,
however, that the result of the substitution is not disjoint with [t], so
one should no longer use [t] after the substitution (or, one should apply
the substitution to a copy). *)
#define __SUBST(thing, Var) \
class CONCAT(__subst_, thing) = object \
inherit [_] endo (* we could also use [map] *) \
inherit [_] KitSubst.map \
method! private CONCAT(visit_, Var) sigma this x = \
KitSubst.apply CONCAT(copy_, thing) sigma this x \
end
#define SUBST(thing, term) \
let CONCAT(subst_, CONCAT(thing, CONCAT(_, term))) sigma t = \
new CONCAT(__subst_, thing) # CONCAT(visit_, term) sigma t \
let CONCAT(subst_, CONCAT(thing, CONCAT(_, CONCAT(term, 1)))) u x t = \
CONCAT(subst_, CONCAT(thing, CONCAT(_, term))) (Atom.Map.singleton x u) t
......@@ -102,6 +102,9 @@ SIZE(term)
__EQUIV
EQUIV(term)
__SUBST(term, TVar)
SUBST(term, term)
(* -------------------------------------------------------------------------- *)
(* [fa] computes the free atoms of a term. *)
......@@ -126,47 +129,6 @@ let fa' : nominal_term -> Atom.Set.t =
(* -------------------------------------------------------------------------- *)
(* [subst] applies a substitution to a nominal term, yielding a nominal term. *)
(* A substitution is a finite map of atoms to nominal terms. *)
type substitution =
nominal_term Atom.Map.t
(* When applying a substitution [sigma] to a term [t], the GUH guarantees that
the free atoms of (the codomain of) [sigma] cannot be captured by a binder
within [t]. The GUH also guarantees that a binder within [t] cannot appear
in the domain of [sigma], which means that we can go down into [t] and apply
[sigma] to every variable. *)
(* The GUH is preserved by copying the terms that are grafted into [t]. Thus,
it is not even necessary that [sigma] and [t] be disjoint, or that the
terms in the codomain of [sigma] be pairwise disjoint. One should note,
however, that the result of the substitution is not disjoint with [t], so
one should no longer use [t] after the substitution (or, one should apply
the substitution to a copy). *)
class subst = object
inherit [_] endo (* we could also use [map] *)
inherit [_] KitSubst.map
method! private visit_TVar sigma this x =
match Atom.Map.find x sigma with
| u ->
(* Do not forget to copy the term that is being grafted, so as
to maintain the GUH. *)
copy_term u
| exception Not_found ->
this
end
let subst : substitution -> nominal_term -> nominal_term =
new subst # visit_term
let subst1 u x t =
subst (Atom.Map.singleton x u) t
(* -------------------------------------------------------------------------- *)
(* [ba] 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
......
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