Commit 068b44ae authored by POTTIER Francois's avatar POTTIER Francois

Add macros to generate a [rename] function.

parent 6a0f8842
......@@ -226,6 +226,21 @@
(* -------------------------------------------------------------------------- *)
#define RENAME_CLASS __rename
#define RENAME_FUN(term) CONCAT(rename_, term)
#define __RENAME \
class RENAME_CLASS = object \
inherit [_] endo (* we could also use [map] *) \
inherit [_] KitRename.map \
end \
#define RENAME(term) \
let RENAME_FUN(term) rho t = \
(new RENAME_CLASS) # VISIT(term) rho t \
(* -------------------------------------------------------------------------- *)
#define SUBST_CLASS(Var) CONCAT(__subst_, Var)
#define SUBST_FUN(Var, term) CONCAT(subst_, CONCAT(Var, CONCAT(_, term)))
#define SUBST_FUN1(Var, term) CONCAT(SUBST_FUN(Var, term), 1)
......@@ -261,6 +276,7 @@
__SHOW \
__SIZE \
__EQUIV \
__RENAME \
#define ALL(term) \
FA(term) \
......@@ -275,5 +291,6 @@
SHOW(term) \
SIZE(term) \
EQUIV(term) \
RENAME(term) \
(* -------------------------------------------------------------------------- *)
(* This kit serves to construct a [rename] function for terms -- a function
that substitutes atoms for atoms. *)
(* An environment is a map of atoms to atoms. We require every binder [x]
encountered along the way to be fresh with respect to [env]. *)
type env =
Atom.t Atom.Map.t
let extend env x =
(* We would like to check that [x] is fresh for [env], but can only
perform the domain check. The codomain check cannot be performed
since the type of things is abstract here. *)
assert (not (Atom.Map.mem x env));
(* Since [x] is fresh for [env], no capture is possible. Thus, no
freshening of the bound name is required. Thus, we can keep the
substitution [env], unchanged, under the binder. *)
env, x
let lookup env x =
try
Atom.Map.find x env
with Not_found ->
assert false
class ['self] map = object (_ : 'self)
method private extend = extend
method private lookup = lookup
method private visit_'fn = lookup
end
......@@ -12,6 +12,7 @@ KitExport
KitFa
KitGuq
KitImport
KitRename
KitShow
KitSubst
KitToDeBruijn
......
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