A possibly working version of the Unbound combinators.

src/Unbound.ml

@@ -22,17 +22,22 @@ 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 '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
+
+(* [Rebind], [Rec] forbidden under [Rec] *)
+(* [Outer], [Binder] allowed both outside and inside [Rec] *)
+(* [Inner] allowed only under [Rec]. *)
 
-(*
 type 't inner =
   't
 
 type 'p recursive =
   'p
- *)
 
 class virtual ['self] libmap = object (self : 'self)
 
@@ -51,17 +56,13 @@ class virtual ['self] libmap = object (self : 'self)
   = 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 .
-    ('env ref -> 'bn1 -> 'bn2) ->
+    _ ->
     ('env, 'extra) penv -> 'bn1 binder -> 'bn2 binder
-  = 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 ->
+  = fun _ penv x1 ->
+      let current = penv.current in
       let env = !current in
       let x2, env = self#extend x1 env in
       current := env;
@@ -91,29 +92,32 @@ class virtual ['self] libmap = object (self : 'self)
         env
         pt1
 
-(*
-  method private visit_inner: 't1 't2 .
+  method private visit_inner: 'env 't1 't2 .
     ('env -> 't1 -> 't2) ->
-    'env patenv -> 't1 inner -> 't2 inner
-  = fun visit_t patenv t1 ->
-      match patenv with
-      | ModeNormal r ->
-          (* [inner] outside of [rec] does not make sense. *)
-          assert false
-
- *)
-(*
-  method private visit_recursive: 'p1 'p2 .
-    ('env patenv -> 'p1 -> 'p2) ->
-    '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
- *)
+    'env inside_rec_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
+
+  method private visit_recursive: 'env 'p1 'p2 .
+    ('env inside_rec_penv -> 'p1 -> 'p2) ->
+    'env outside_rec_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
 
 end