Commit f1734bdd authored by POTTIER Francois's avatar POTTIER Francois

Renamed enriched environments to contexts.

parent cd724694
......@@ -59,8 +59,8 @@ type ('p, 't) bind =
(* When traversing a pattern, our visitors maintain a richer environment than
when traversing a term. If a normal term-traversal environment has type
['env], then an enriched pattern-traversal environment has type ['env penv]
as defined below. *)
['env], then a pattern-traversal context has type ['env context] as defined
below. *)
(* The meaning of the above combinators is defined by the manner in which they
extend or use this enriched environment. *)
......@@ -72,25 +72,26 @@ type ('p, 't) bind =
(* The [outer] component is an immutable environment. It is transmitted in
a top-down manner. *)
type 'env penv = {
type 'env context = {
current: 'env ref; (* do NOT replace this with a mutable field! *)
outer: 'env;
outer: 'env
}
(* -------------------------------------------------------------------------- *)
(* A few auxiliary functions. *)
(* [abstraction] initializes an enriched environment. [current] and [outer]
are initialized with the environment that exists outside the abstraction. *)
(* [abstraction] initializes a context environment. [current] and [outer] are
initialized with the environment that exists outside the abstraction. *)
let abstraction (env : 'env) : 'env penv =
let abstraction (env : 'env) : 'env context =
{ current = ref env; outer = env }
(* [rebind] copies the [current] component of the environment into the [outer]
(* [rebind] copies the [current] component of the context into the [outer]
component. In other words, it locally changes the meaning of [outer]. *)
let rebind (penv : 'env penv) : 'env penv =
{ penv with outer = !(penv.current) }
let rebind (ctx : 'env context) : 'env context =
{ ctx with outer = !(ctx.current) }
(* -------------------------------------------------------------------------- *)
......@@ -100,25 +101,25 @@ class virtual ['self] map = object (self : 'self)
method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
(* [visit_abstraction] initializes an enriched environment using the
auxiliary function [abstraction]. *)
(* [visit_abstraction] initializes a context using the auxiliary function
[abstraction]. *)
method private visit_abstraction: 'env 'p1 'p2 .
('env penv -> 'p1 -> 'p2) ->
('env context -> 'p1 -> 'p2) ->
'env -> 'p1 abstraction -> 'p2 abstraction
= fun visit_p env p1 ->
visit_p (abstraction env) p1
(* [binder] extends the environment via a call to the virtual method
[extend]. *)
(* [binder] extends the [current] component of the context via a call to the
virtual method [extend]. *)
method private visit_binder:
_ ->
'env penv -> 'bn1 binder -> 'bn2 binder
= fun _ penv x1 ->
let env = !(penv.current) in
'env context -> 'bn1 binder -> 'bn2 binder
= fun _ ctx x1 ->
let env = !(ctx.current) in
let env, x2 = self#extend env x1 in
penv.current := env;
ctx.current := env;
x2
(* [inner(p)] can be viewed as sugar for [rebind(outer(p))]. Therefore, this
......@@ -126,40 +127,39 @@ class virtual ['self] map = object (self : 'self)
method private visit_inner: 'env 't1 't2 .
('env -> 't1 -> 't2) ->
'env penv -> 't1 inner -> 't2 inner
= fun visit_t penv t1 ->
self#visit_rebind (self#visit_outer visit_t) penv t1
'env context -> 't1 inner -> 't2 inner
= fun visit_t ctx t1 ->
self#visit_rebind (self#visit_outer visit_t) ctx t1
(* An [outer] subterm is visited using the [outer] component of the enriched
environment. *)
(* An [outer] subterm is visited using the [outer] component of the context. *)
method private visit_outer: 'env 't1 't2 .
('env -> 't1 -> 't2) ->
'env penv -> 't1 outer -> 't2 outer
= fun visit_t penv t1 ->
visit_t penv.outer t1
'env context -> 't1 outer -> 't2 outer
= fun visit_t ctx t1 ->
visit_t ctx.outer t1
(* [visit_rebind] updates the enriched environment using the auxiliary
function [rebind]. *)
(* [visit_rebind] updates the context using the auxiliary function
[rebind]. *)
method private visit_rebind: 'env 'p1 'p2 .
('env penv -> 'p1 -> 'p2) ->
'env penv -> 'p1 rebind -> 'p2 rebind
= fun visit_p penv p1 ->
visit_p (rebind penv) p1
('env context -> 'p1 -> 'p2) ->
'env context -> 'p1 rebind -> 'p2 rebind
= fun visit_p ctx p1 ->
visit_p (rebind ctx) p1
(* [bind(p, t)] is sugar for [abstraction (p * rebind(outer(t)))].
Therefore, the following code should ideally be generated. We write it by
hand in a slightly simpler form, where [visit_abstraction] is inlined. *)
method private visit_bind: 'env 'p1 'p2 't1 't2 .
('env penv -> 'p1 -> 'p2) ->
('env context -> 'p1 -> 'p2) ->
('env -> 't1 -> 't2) ->
'env -> ('p1, 't1) bind -> ('p2, 't2) bind
= fun visit_p visit_t env (p1, t1) ->
let penv = abstraction env in
let p2 = visit_p penv p1 in
let t2 = self#visit_inner visit_t penv t1 in
let ctx = abstraction env in
let p2 = visit_p ctx p1 in
let t2 = self#visit_inner visit_t ctx t1 in
p2, t2
end
......@@ -173,44 +173,44 @@ class virtual ['self] iter = object (self : 'self)
method private virtual extend: 'env -> 'bn -> 'env
method private visit_abstraction: 'env 'p .
('env penv -> 'p -> unit) ->
('env context -> 'p -> unit) ->
'env -> 'p abstraction -> unit
= fun visit_p env p ->
visit_p (abstraction env) p
method private visit_binder:
_ ->
'env penv -> 'bn binder -> unit
= fun _ penv x ->
let env = !(penv.current) in
'env context -> 'bn binder -> unit
= fun _ ctx x ->
let env = !(ctx.current) in
let env = self#extend env x in
penv.current := env
ctx.current := env
method private visit_inner: 'env 't .
('env -> 't -> unit) ->
'env penv -> 't inner -> unit
= fun visit_t penv t ->
self#visit_rebind (self#visit_outer visit_t) penv t
'env context -> 't inner -> unit
= fun visit_t ctx t ->
self#visit_rebind (self#visit_outer visit_t) ctx t
method private visit_outer: 'env 't .
('env -> 't -> unit) ->
'env penv -> 't outer -> unit
= fun visit_t penv t ->
visit_t penv.outer t
'env context -> 't outer -> unit
= fun visit_t ctx t ->
visit_t ctx.outer t
method private visit_rebind: 'env 'p .
('env penv -> 'p -> unit) ->
'env penv -> 'p rebind -> unit
= fun visit_p penv p ->
visit_p (rebind penv) p
('env context -> 'p -> unit) ->
'env context -> 'p rebind -> unit
= fun visit_p ctx p ->
visit_p (rebind ctx) p
method private visit_bind: 'env 'p 't .
('env penv -> 'p -> unit) ->
('env context -> 'p -> unit) ->
('env -> 't -> unit) ->
'env -> ('p, 't) bind -> unit
= fun visit_p visit_t env (p, t) ->
let penv = abstraction env in
visit_p penv p;
self#visit_inner visit_t penv t
let ctx = abstraction env in
visit_p ctx p;
self#visit_inner visit_t ctx t
end
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