Commit bf21cee1 authored by POTTIER Francois's avatar POTTIER Francois

Progress on [Unbound].

parent 35255836
type 'env patenv =
| ModeNormal of { outer: 'env; inner: 'env; mutable current: 'env }
(*
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 't outer =
't
type ('env, 'extra) penv = {
current: 'env ref; (* threaded left to right *)
extra: 'extra;
}
type 't inner =
type 'env outside_rec_penv =
('env, 'env) penv (* [extra] is outer env *)
type 'p abstraction =
'p
type 't outer =
't
type ('p, 't) rebind =
'p * 't
type 't recursive =
(*
type 't inner =
't
type 'p recursive =
'p
*)
class virtual ['self] map = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private visit_'bn (patenv : 'env patenv) (x1 : 'bn1) : 'bn2 =
match patenv with
| ModeNormal r ->
let env = r.current in
let x2, env = self#extend x1 env in
r.current <- env;
x2
method private visit_abstraction: '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
visit_p penv p1
method private visit_outer: 't1 't2 .
('env -> 't1 -> 't2) ->
'env patenv -> 't1 outer -> 't2 outer
= fun visit_t patenv t1 ->
match patenv with
| ModeNormal r ->
let env = r.outer in
visit_t env t1
('env, 'env) penv -> 't1 outer -> 't2 outer
= fun visit_t penv t1 ->
let env = penv.extra in
visit_t env t1
method private visit_'bn: 'extra .
('env, 'extra) penv -> 'bn1 -> 'bn2
= fun penv x1 ->
let env = !(penv.current) in
let x2, env = self#extend x1 env in
penv.current := env;
x2
method private visit_rebind: '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
= fun visit_p visit_q penv (p1, q1) ->
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 q2 = visit_q penv q1 in
p2, q2
(*
method private visit_inner: 't1 't2 .
('env -> 't1 -> 't2) ->
'env patenv -> 't1 inner -> 't2 inner
= fun visit_t patenv t1 ->
match patenv with
| ModeNormal r ->
let env = r.inner in
visit_t env t1
(* [inner] outside of [rec] does not make sense. *)
assert false
method private visit_rebind: 'p1 'p2 'q1 'q2 .
*)
(*
method private visit_recursive: 'p1 'p2 .
('env patenv -> 'p1 -> 'p2) ->
('env patenv -> 'q1 -> 'q2) ->
'env patenv -> ('p1, 'q1) rebind -> ('p2, 'q2) rebind
= fun visit_p visit_q patenv (p1, q1) ->
let p2 = visit_p patenv p1 in
(* Copy [current] into [outer]. This changes the meaning of [outer]
in the right-hand side of [rebind]. *)
let patenv =
match patenv with
| ModeNormal r ->
ModeNormal { r with outer = r.current }
in
let q2 = visit_q patenv q1 in
p2, q2
(* TEMPORARY
method private visit_freeze: 'env 't1 't2 .
('env mode -> 't1 -> 't2) ->
'env mode -> 't1 -> 't2
= fun visit_t mode t1 ->
visit_t (freeze mode) t1
method private visit_embed: 'env 't1 't2 .
('env -> 't1 -> 't2) ->
'env mode -> 't1 -> 't2
= fun visit_t mode t1 ->
visit_t (embed mode) t1
method private visit_bind: 'env 'p1 'p2 't1 't2 .
('env mode -> 'p1 -> 'p2) ->
('env -> 't1 -> 't2) ->
'env -> ('p1, 't1) bind -> ('p2, 't2) bind
= fun visit_p visit_t env (p1, t1) ->
let envref = ref env in
let p2 = visit_p (ModePattern envref) p1 in
let env = !envref in
let t2 = visit_t env t1 in
p2, t2
'env patenv -> 'p1 recursive -> 'p2 recursive
= fun visit_p patenv p1 ->
match patenv with
| ModeNormal r ->
let patenv = ModeRecPhase1 { current = r.current } in
visit_p patenv p1;
let inner = patenv.current in
let patenv = ModeRecPhase2 { current = r.current
*)
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