Commit b853d25a authored by POTTIER Francois's avatar POTTIER Francois

Add [KitSubst.apply].

parent 542e762d
......@@ -4,8 +4,8 @@
(* 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]. *)
type 'term env =
'term Atom.Map.t
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
......@@ -20,9 +20,19 @@ let extend x sigma =
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. *)
variable nodes and replace them. This requires overriding a suitable
visitor method. *)
method private visit_'fn _sigma _x = assert false
end
(* TEMPORARY could we abandon the runtime check and use [KitTrivial.map]
instead? *)
let apply (copy : 'thing -> 'thing) (sigma : 'thing env) (this : 'thing) (x : Atom.t) : 'thing =
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 u
| exception Not_found ->
this
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