New version of [Unbound].

No static distinction between outside and inside [rec].
A [lookup] method is needed to deal with [binder] on the second visit.

src/Unbound.ml

-type ('env, 'extra) penv = {
+type 'env mode =
+  | OutsideRec
+  | InsideRecDiscovery     (* updating [current] and doing nothing else; embedded subterms not visited *)
+  | InsideRecVisit of 'env (* [inner] component now known; embedded subterms visited *)
+
+type 'env penv = {
     current: 'env ref; (* threaded left to right *)
     outer: 'env; (* sent down only *)
-    extra: 'extra;
+    mode: 'env mode;
   }
 
-type 'env outside_rec_penv =
-  ('env, unit) penv (* no [extra] info *)
-
 type 'p abstraction =
   'p
 
@@ -22,13 +24,7 @@ type ('p, 't) rebind =
 type ('p, 't) bind =
   (('p, 't outer) rebind) abstraction (* = 'p * 't *)
 
-type 'env inside_rec_phase =
-  | DiscoveryPhase     (* updating [current] and doing nothing else; embedded subterms not visited *)
-  | VisitPhase of 'env (* [inner] component now known; embedded subterms visited *)
-
-type 'env inside_rec_penv =
-  ('env, 'env inside_rec_phase) penv
-
+(* [Abstraction] allowed only in an expression *)
 (* [Rebind], [Rec] forbidden under [Rec] *)
 (* [Outer], [Binder] allowed both outside and inside [Rec] *)
 (* [Inner] allowed only under [Rec]. *)
@@ -42,48 +38,67 @@ type 'p recursive =
 class virtual ['self] libmap = object (self : 'self)
 
   method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
+  method private virtual lookup: 'bn1 -> 'env -> 'bn2
 
   method private visit_abstraction: 'env 'p1 'p2 .
-    ('env outside_rec_penv -> 'p1 -> 'p2) ->
+    ('env penv -> 'p1 -> 'p2) ->
     'env -> 'p1 abstraction -> 'p2 abstraction
   = fun visit_p env p1 ->
-      let penv = { current = ref env; outer = env; extra = () } in
+      let penv = { current = ref env; outer = env; mode = OutsideRec } in
       visit_p penv p1
 
-  method private visit_outer: 'env 'extra 't1 't2 .
+  method private visit_outer: 'env 't1 't2 .
     ('env -> 't1 -> 't2) ->
-    ('env, 'extra) penv -> 't1 outer -> 't2 outer
+    'env penv -> 't1 outer -> 't2 outer
   = fun visit_t penv t1 ->
-      let env = penv.outer in
-      visit_t env t1
-      (* TEMPORARY must NOT visit [t1] when in discovery phase! *)
-
-  method private visit_binder: 'extra .
+      match penv.mode with
+      | OutsideRec
+      | InsideRecVisit _ ->
+          visit_t penv.outer t1
+      | InsideRecDiscovery ->
+          (* An [outer] subterm is NOT visited in discovery mode. *)
+          Obj.magic ()
+
+  method private visit_binder:
     _ ->
-    ('env, 'extra) penv -> 'bn1 binder -> 'bn2 binder
+    'env penv -> 'bn1 binder -> 'bn2 binder
   = fun _ penv x1 ->
-      let current = penv.current in
-      let env = !current in
-      let x2, env = self#extend x1 env in
-      current := env;
-      x2
+      match penv.mode with
+      | OutsideRec
+      | InsideRecDiscovery ->
+          let current = penv.current in
+          let env = !current in
+          let x2, env = self#extend x1 env in
+          current := env;
+          x2
+      | InsideRecVisit env ->
+          assert (env == !(penv.current)); (* TEMPORARY if always true, then we do not need to carry [env] *)
+          (* The environment should not be extended when in visit mode.
+             It has been extended already during the discovery phase. *)
+          self#lookup env x1
 
   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
+    ('env penv -> 'p1 -> 'p2) ->
+    ('env penv -> 'q1 -> 'q2) ->
+    'env 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 outer = !(penv.current) } in
-      let q2 = visit_q penv q1 in
-      p2, q2
+      match penv.mode with
+      | OutsideRec ->
+          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 outer = !(penv.current) } in
+          let q2 = visit_q penv q1 in
+          p2, q2
+      | InsideRecDiscovery
+      | InsideRecVisit _ ->
+          (* [rebind] forbidden under [rec] *)
+          assert false
 
   (* 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: 'env 'p1 'p2 't1 't2 .
-    ('env outside_rec_penv -> 'p1 -> 'p2) ->
+    ('env penv -> 'p1 -> 'p2) ->
     ('env -> 't1 -> 't2) ->
     'env -> ('p1, 't1) rebind -> ('p2, 't2) rebind
   = fun visit_p visit_t env pt1 ->
@@ -94,30 +109,36 @@ class virtual ['self] libmap = object (self : 'self)
 
   method private visit_inner: 'env 't1 't2 .
     ('env -> 't1 -> 't2) ->
-    'env inside_rec_penv -> 't1 inner -> 't2 inner
+    'env penv -> 't1 inner -> 't2 inner
   = fun visit_t penv t1 ->
-      match penv.extra with
-      | DiscoveryPhase ->
-          (* Just ignore this term. Return it unchanged. It will be dropped anyway... *)
-          (* TEMPORARY typing problem! *)
-          (Obj.magic t1)
-      | VisitPhase inner ->
-          visit_t inner t1
+      match penv.mode with
+      | OutsideRec ->
+          (* [inner] allowed only under [rec] *)
+          assert false
+      | InsideRecDiscovery ->
+          (* An [inner] subterm is NOT visited in discovery mode. *)
+          Obj.magic ()
+      | InsideRecVisit env ->
+          assert (env == !(penv.current));
+          visit_t env t1
 
   method private visit_recursive: 'env 'p1 'p2 .
-    ('env inside_rec_penv -> 'p1 -> 'p2) ->
-    'env outside_rec_penv -> 'p1 recursive -> 'p2 recursive
+    ('env penv -> 'p1 -> 'p2) ->
+    'env penv -> 'p1 recursive -> 'p2 recursive
   = fun visit_p penv p1 ->
-      (* Discovery phase. Result is discarded (fortunately, since we have used
-         [magic] to produce it, and it is entirely meaningless). *)
-      let penv = { penv with extra = DiscoveryPhase } in
-      let _ = visit_p penv p1 in
-      (* [!current] becomes [inner] *)
-      (* a dummy [current] ref. is allocated so that [Binder] does not break [current] -- TEMPORARY *)
-      let penv = { penv with
-                   current = ref !(penv.current);
-                   extra = VisitPhase !(penv.current) } in
-      visit_p penv p1
+      match penv.mode with
+      | OutsideRec ->
+          (* Discovery phase. Result is discarded (fortunately, since we have used
+             [magic] to produce it, and it is entirely meaningless). *)
+          let penv = { penv with mode = InsideRecDiscovery } in
+          let _ = visit_p penv p1 in
+          (* [!current] becomes [inner] *)
+          let penv = { penv with mode = InsideRecVisit !(penv.current) } in
+          visit_p penv p1
+      | InsideRecDiscovery
+      | InsideRecVisit _ ->
+          (* [rec] not allowed under [rec] *)
+          assert false
 
 end