Skip to content

GitLab

A
alphaLib
Commit 69947333 authored by POTTIER Francois's avatar POTTIER Francois
Browse files
Options

More macros for naming conventions.

parent d5300557
Hide whitespace changes
Inline Side-by-side
Showing with 50 additions and 27 deletions
src/AlphaLibMacros.cppo.ml
View file @ 69947333
(* The conventional name of the visitor method. *)
(* The conventional name of the visitor methods. *)
#define VISIT(term) \
CONCAT(visit_, term)
......@@ -20,19 +20,22 @@
(* [wf_terms] is a variant of [ba_term] that returns no result, but can still
raise [IllFormed]. *)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
#define __BA \
exception IllFormed = KitBa.IllFormed \
class ['self] __ba = object (_ : 'self) \
class ['self] BA_CLASS = object (_ : 'self) \
inherit [_] reduce \
inherit [_] KitBa.reduce \
end
#define BA(term) \
let CONCAT(ba_, term) t = \
new __ba # VISIT(term) () t \
let BA_FUN(term) t = \
new BA_CLASS # VISIT(term) () t \
let CONCAT(ba_, CONCAT(term, s)) ts = \
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (CONCAT(ba_, term) t)) \
(fun accu t -> Atom.Set.disjoint_union accu (BA_FUN(term) t)) \
Atom.Set.empty ts \
(* -------------------------------------------------------------------------- *)
......@@ -40,15 +43,18 @@
(* [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 = object (_ : 'self) \
class ['self] COPY_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitCopy.map \
end
#define COPY(term) \
let CONCAT(copy_, term) t = \
new __copy # VISIT(term) KitCopy.empty t
let COPY_FUN(term) t = \
new COPY_CLASS # VISIT(term) KitCopy.empty t
(* -------------------------------------------------------------------------- *)
......@@ -56,15 +62,17 @@
using [Atom.show] both at free name occurrences and bound name occurrences.
It is a debugging tool. *)
#define SHOW_CLASS __show
#define __SHOW \
class ['self] __show = object (_ : 'self) \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end
#define SHOW(term) \
let CONCAT(show_, term) t = \
new __show # VISIT(term) () t
new SHOW_CLASS # VISIT(term) () t
(* -------------------------------------------------------------------------- *)
......@@ -76,16 +84,18 @@
(* TEMPORARY use string * loc so as to be able to give a location *)
#define IMPORT_CLASS __import
#define __IMPORT \
exception Unbound = KitImport.Unbound \
class ['self] __import = object (_ : 'self) \
class ['self] IMPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
end
#define IMPORT(term) \
let CONCAT(import_, term) env t = \
new __import # VISIT(term) env t
new IMPORT_CLASS # VISIT(term) env t
(* -------------------------------------------------------------------------- *)
......@@ -93,15 +103,17 @@
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 \
class ['self] __export = object (_ : 'self) \
class ['self] EXPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitExport.map \
end
#define EXPORT(term) \
let CONCAT(export_, term) env t = \
new __export # VISIT(term) env t
new EXPORT_CLASS # VISIT(term) env t
(* -------------------------------------------------------------------------- *)
......@@ -110,8 +122,10 @@
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
#define SIZE_CLASS __size
#define __SIZE \
class ['self] __size = object (_ : 'self) \
class ['self] SIZE_CLASS = object (_ : 'self) \
inherit [_] reduce as super \
inherit [_] KitTrivial.reduce \
inherit [_] VisitorsRuntime.addition_monoid \
......@@ -121,14 +135,16 @@
#define SIZE(term) \
let CONCAT(size_, term) t = \
new __size # VISIT(term) () t
new SIZE_CLASS # VISIT(term) () t
(* -------------------------------------------------------------------------- *)
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
#define EQUIV_CLASS __equiv
#define __EQUIV \
class __equiv = object \
class EQUIV_CLASS = object \
inherit [_] iter2 \
inherit [_] KitEquiv.iter2 \
end
......@@ -136,13 +152,16 @@
#define EQUIV(term) \
let equiv t1 t2 = \
VisitorsRuntime.wrap2 \
(new __equiv # VISIT(term) KitEquiv.empty) \
(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_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
......@@ -161,16 +180,20 @@
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 CONCAT(__subst_, thing) = object \
class SUBST_CLASS(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 \
method! private VISIT(Var) sigma this x = \
KitSubst.apply COPY_FUN(thing) sigma this x \
end
#define SUBST(thing, term) \
let CONCAT(subst_, CONCAT(thing, CONCAT(_, term))) sigma t = \
new CONCAT(__subst_, thing) # 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
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
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