Progress on [Unbound].

src/Unbound.ml

@@ -16,6 +16,9 @@ type 'env outside_rec_penv =
 type 'p abstraction =
   'p
 
+type 'bn binder =
+  'bn
+
 type 't outer =
   't
 
@@ -30,7 +33,7 @@ type 'p recursive =
   'p
  *)
 
-class virtual ['self] map = object (self : 'self)
+class virtual ['self] libmap = object (self : 'self)
 
   method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
 
@@ -48,12 +51,18 @@ class virtual ['self] map = object (self : 'self)
       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
+  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
+
+  method private visit_'bn:
+    'env ref -> 'bn1 -> 'bn2
+  = fun current x1 ->
+      let env = !current in
       let x2, env = self#extend x1 env in
-      penv.current := env;
+      current := env;
       x2
 
   method private visit_rebind: 'p1 'p2 'q1 'q2 .
@@ -94,6 +103,19 @@ class virtual ['self] map = object (self : 'self)
 
 end
 
+type ('p, 't) bind =
+  (('p, 't outer) rebind) abstraction
+[@@deriving visitors { variety = "map"; name = "bind_map"; ancestors = ["libmap"]; public = [] }]
+
+type ('bn, 'term) tele =
+  | TeleNil
+  | TeleCons of ('bn binder * 'term outer, ('bn, 'term) tele) rebind
+[@@deriving visitors { variety = "map"; name = "tele_map"; ancestors = ["libmap"]; public = [] }]
+
+type ('bn, 'fn) term =
+  | TVar of 'fn
+  | TPi of (('bn, ('bn, 'fn) term) tele, ('bn, 'fn) term) bind
+
 (*
 type 'bn pat =
   | PZero