Commit 77240a60 authored by POTTIER Francois's avatar POTTIER Francois

Renaming.

parent 40990b1d
(* This kit serves to construct a [subst] function for terms -- a function
that substitutes things (possibly terms) for atoms. *)
(* An environment is a map [sigma] of atoms to things. We require every binder
[x] encountered along the way to be fresh with respect to [sigma]. *)
(* An environment is a map of atoms to things. We require every binder [x]
encountered along the way to be fresh with respect to [env]. *)
type 'thing env =
'thing Atom.Map.t
let extend x sigma =
(* We would like to check that [x] is fresh for [sigma], but can only
let extend x env =
(* 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 sigma));
(* Since [x] is fresh for [sigma], no capture is possible. Thus, no
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 [sigma], unchanged, under the binder. *)
x, sigma
substitution [env], unchanged, under the binder. *)
x, env
class ['self] map = object (_ : 'self)
method private extend = extend
(* [visit_'fn] is not implemented, as it is up to the user to identify
variable nodes and replace them. This requires overriding a suitable
visitor method. *)
method private visit_'fn _sigma _x = assert false
method private visit_'fn _env _x = assert false
end
let apply (copy : 'thing -> 'thing)
(sigma : 'thing env)
(env : 'thing env)
(this : 'thing) (x : Atom.t)
: 'thing =
match Atom.Map.find x sigma with
match Atom.Map.find x env with
| u ->
(* Copy the term that is grafted, so as to maintain global uniqueness. *)
copy u
......
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