Commit 4c953ff3 authored by POTTIER Francois's avatar POTTIER Francois


parent 95476c03
......@@ -25,14 +25,16 @@ class ['self] map = object (_ : 'self)
method private visit_'fn _sigma _x = assert false
(* TEMPORARY could we abandon the runtime check and use []
instead? *)
let apply (copy : 'thing -> 'thing) (sigma : 'thing env) (this : 'thing) (x : Atom.t) : 'thing =
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 the term that is grafted, so as to maintain global uniqueness. *)
copy u
| exception Not_found ->
(* [x] is not affected by the substitution, so the original thing is
returned. [this] should be [Var x], where [Var] is the constructor
for variables in the syntax of things. *)
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