Commit 01a9d67e authored by POTTIER Francois's avatar POTTIER Francois

Update [Unbound] so that the shared part of the environment

contains not only [current] but also [outer]. This should
allow [outer] to be used both inside and outside of [rec].
parent 53f58ab0
(*
type mode =
| ModeOutsideRec (* [inner] component is irrelevant; embedded subterms cannot be marked [inner] *)
| ModeRec1 (* [inner] and [outer] components both irrelevant; embedded subterms not visited *)
| ModeRec2 (* [inner] and [outer] components both relevant; embedded subterms visited *)
*)
type ('env, 'extra) penv = {
current: 'env ref; (* threaded left to right *)
outer: 'env; (* sent down only *)
extra: 'extra;
}
type 'env outside_rec_penv =
('env, 'env) penv (* [extra] is outer env *)
('env, unit) penv (* no [extra] info *)
type 'p abstraction =
'p
......@@ -28,6 +22,10 @@ type ('p, 't) rebind =
type ('p, 't) bind =
(('p, 't outer) rebind) abstraction (* = 'p * 't *)
type inside_rec_phase =
| DiscoveryPhase (* updating [current] and doing nothing else; embedded subterms not visited *)
| VisitPhase (* [inner] and [outer] components both relevant; embedded subterms visited; [Rebind], [Rec] forbidden *)
(*
type 't inner =
't
......@@ -40,18 +38,18 @@ class virtual ['self] libmap = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private visit_abstraction: 'p1 'p2 .
method private visit_abstraction: 'env 'p1 'p2 .
('env outside_rec_penv -> 'p1 -> 'p2) ->
'env -> 'p1 abstraction -> 'p2 abstraction
= fun visit_p env p1 ->
let penv = { current = ref env; extra = env } in
let penv = { current = ref env; outer = env; extra = () } in
visit_p penv p1
method private visit_outer: 't1 't2 .
method private visit_outer: 'env 'extra 't1 't2 .
('env -> 't1 -> 't2) ->
('env, 'env) penv -> 't1 outer -> 't2 outer
('env, 'extra) penv -> 't1 outer -> 't2 outer
= fun visit_t penv t1 ->
let env = penv.extra in
let env = penv.outer in
visit_t env t1
method private visit_binder: 'extra .
......@@ -60,6 +58,7 @@ class virtual ['self] libmap = object (self : 'self)
= fun visit_bn penv x1 ->
visit_bn penv.current x1
(* TEMPORARY cannot provide an implementation of visit_'bn! *)
method private visit_'bn:
'env ref -> 'bn1 -> 'bn2
= fun current x1 ->
......@@ -68,7 +67,7 @@ class virtual ['self] libmap = object (self : 'self)
current := env;
x2
method private visit_rebind: 'p1 'p2 'q1 'q2 .
method private visit_rebind: 'env 'p1 'p2 'q1 'q2 .
('env outside_rec_penv -> 'p1 -> 'p2) ->
('env outside_rec_penv -> 'q1 -> 'q2) ->
'env outside_rec_penv -> ('p1, 'q1) rebind -> ('p2, 'q2) rebind
......@@ -76,13 +75,13 @@ class virtual ['self] libmap = object (self : 'self)
let p2 = visit_p penv p1 in
(* Copy [current] into [outer]. This changes the meaning of [outer]
in the right-hand side of [rebind]. *)
let penv = { penv with extra = !(penv.current) } in
let penv = { penv with outer = !(penv.current) } in
let q2 = visit_q penv q1 in
p2, q2
(* could in principle be generated, if [visitors] supported dealing with
type parameters via functions, instead of via virtual methods. Future work. *)
method private visit_bind: 'p1 'p2 't1 't2 .
method private visit_bind: 'env 'p1 'p2 't1 't2 .
('env outside_rec_penv -> 'p1 -> 'p2) ->
('env -> 't1 -> 't2) ->
'env -> ('p1, 't1) rebind -> ('p2, 't2) rebind
......
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