(* The conventional name of the visitor methods. *)
#define VISIT(term) \
CONCAT(visit_, term)
(* -------------------------------------------------------------------------- *)
(* [fa_term] computes the set of the free atoms of a term. *)
#define FA_CLASS __fa
#define FA_FUN(term) CONCAT(fa_, term)
#define __FA \
class FA_CLASS = object \
inherit [_] reduce \
inherit [_] KitFa.reduce \
end \
#define FA(term) \
let FA_FUN(term) t = \
new FA_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* [filter_term p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
(* [closed_term t] tests whether the term [t] is closed, that is, whether
[t] has no free atom. *)
(* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
#define FILTER_CLASS __filter
#define FILTER_FUN(term) CONCAT(filter_, term)
#define CLOSED_FUN(term) CONCAT(closed_, term)
#define OCCURS_FUN(term) CONCAT(occurs_, term)
#define __FILTER \
class FILTER_CLASS p = object \
inherit [_] iter \
inherit KitFa.filter p \
end \
#define FILTER(term) \
let FILTER_FUN(term) p t = \
KitFa.wrap ((new FILTER_CLASS p) # VISIT(term) KitFa.empty) t \
let CLOSED_FUN(term) t = \
match FILTER_FUN(term) (fun _ -> true) t with \
| None -> true \
| Some _ -> false \
let OCCURS_FUN(term) x t = \
match FILTER_FUN(term) (fun y -> Atom.equal x y) t with \
| None -> false \
| Some _ -> true \
(* -------------------------------------------------------------------------- *)
(* [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. *)
#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 \
end \
#define BA(term) \
let BA_FUN(term) t = \
new BA_CLASS # VISIT(term) () t \
let BAS_FUN(term) ts = \
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (BA_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 \
(* -------------------------------------------------------------------------- *)
(* [copy_term] returns a copy of its argument where every bound name has been
replaced with a fresh copy, and every free name is unchanged. *)
#define COPY_CLASS __copy
#define COPY_FUN(term) CONCAT(copy_, term)
#define __COPY \
class ['self] COPY_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitCopy.map \
end \
#define COPY(term) \
let COPY_FUN(term) t = \
new COPY_CLASS # VISIT(term) KitCopy.empty t \
(* -------------------------------------------------------------------------- *)
(* [avoid_term bad] returns a copy of its argument where some bound names have
been replaced with a fresh copy, so as to ensure that no bound name is in
the set [bad]. *)
#define AVOID_CLASS __avoid
#define AVOID_FUN(term) CONCAT(avoid_, term)
#define __AVOID \
class ['self] AVOID_CLASS bad = object (_ : 'self) \
inherit [_] map \
inherit [_] KitAvoid.map bad \
end \
#define AVOID(term) \
let AVOID_FUN(term) bad t = \
(new AVOID_CLASS bad) # VISIT(term) KitAvoid.empty t \
(* -------------------------------------------------------------------------- *)
(* [show_term] converts its argument to a raw term, in a NONHYGIENIC manner,
using [Atom.show] both at free name occurrences and bound name occurrences.
It is a debugging tool. *)
#define SHOW_CLASS __show
#define SHOW_FUN(term) CONCAT(show_, term)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* [import_term] converts a raw term to a nominal term that satisfies the
Global Uniqueness Hypothesis, that is, a nominal term where every binding
name occurrence is represented by a unique atom. [import] expects every
free name occurrence to be in the domain of [env]. If that is not the case,
the exception [Unbound] is raised. *)
(* TEMPORARY use string * loc so as to be able to give a location *)
#define IMPORT_CLASS __import
#define IMPORT_FUN(term) CONCAT(import_, term)
#define __IMPORT \
exception Unbound = KitImport.Unbound \
class ['self] IMPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
end \
#define IMPORT(term) \
let IMPORT_FUN(term) env t = \
new IMPORT_CLASS # VISIT(term) env t \
(* -------------------------------------------------------------------------- *)
(* [export_term] converts a nominal term to a raw term, in a hygienic manner.
This is the proper way of displaying a term. [export] expects every free
name occurrence to be in the domain of [env]. *)
#define EXPORT_CLASS __export
#define EXPORT_FUN(term) CONCAT(export_, term)
#define __EXPORT \
class ['self] EXPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitExport.map \
end \
#define EXPORT(term) \
let EXPORT_FUN(term) env t = \
new EXPORT_CLASS # VISIT(term) env t \
(* -------------------------------------------------------------------------- *)
(* [size_term] computes the size of its argument. *)
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
#define SIZE_CLASS __size
#define SIZE_FUN(term) CONCAT(size_, term)
#define __SIZE \
class ['self] SIZE_CLASS = object (_ : 'self) \
inherit [_] reduce as super \
inherit [_] KitTrivial.reduce \
inherit [_] VisitorsRuntime.addition_monoid \
method! VISIT(term) env t = \
1 + super # VISIT(term) env t \
end \
#define SIZE(term) \
let SIZE_FUN(term) t = \
new SIZE_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
#define EQUIV_CLASS __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
#define __EQUIV \
class EQUIV_CLASS = object \
inherit [_] iter2 \
inherit [_] KitEquiv.iter2 \
end \
#define EQUIV(term) \
let EQUIV_FUN(term) t1 t2 = \
VisitorsRuntime.wrap2 \
(new EQUIV_CLASS # VISIT(term) KitEquiv.empty) \
t1 t2 \
(* -------------------------------------------------------------------------- *)
(* [subst_thing_term] applies a substitution to a nominal term,
yielding a nominal term. *)
(* [subst_thing_term1] applies a singleton 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_CLASS(thing) CONCAT(__subst_, thing)
#define SUBST_FUN(thing, term) CONCAT(subst_, CONCAT(thing, CONCAT(_, term)))
#define SUBST_FUN1(thing, term) CONCAT(SUBST_FUN(thing, term), 1)
#define __SUBST(thing, Var) \
class SUBST_CLASS(thing) = object \
inherit [_] endo (* we could also use [map] *) \
inherit [_] KitSubst.map \
method! private VISIT(Var) sigma this x = \
KitSubst.apply COPY_FUN(thing) sigma this x \
end \
#define SUBST(thing, term) \
let SUBST_FUN(thing, term) sigma t = \
new SUBST_CLASS(thing) # VISIT(term) sigma t \
let SUBST_FUN1(thing, term) u x t = \
SUBST_FUN(thing, term) (Atom.Map.singleton x u) t \
(* -------------------------------------------------------------------------- *)