The beginning of an Unbound emulation.

src/BindingForms.ml

@@ -396,3 +396,4 @@ class virtual ['self] iter2 = object (_ : 'self)
 end
 
 open MLPatternExample (* TEMPORARY work in progress *)
+open Unbound

src/Unbound.ml

+type 'env patenv =
+  | ModeNormal of { outer: 'env; inner: 'env; mutable current: 'env }
+
+type 't outer =
+  't
+
+type 't inner =
+  't
+
+type ('p, 't) rebind =
+  'p * 't
+
+type 't recursive =
+  't
+
+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_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
+
+  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
+
+  method private visit_rebind: 'p1 'p2 'q1 'q2 .
+    ('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
+ *)
+end
+
+(*
+type 'bn pat =
+  | PZero
+  | POne
+  | PVar of 'bn
+  | PTuple of 'bn pat list
+  | PConj of 'bn pat * 'bn pat
+  | PDisj of 'bn pat * 'bn pat
+
+and ('bn, 'fn) expr =
+  | EVar of 'fn
+  | EAdd of ('bn, 'fn) expr * ('bn, 'fn) expr
+  | ELet of ('bn pat, ('bn, 'fn) expr) bind
+
+[@@deriving visitors { variety = "map"; ancestors = ["libmap"] }]
+ *)