A working version of telescopes in terms of [Unbound].

src/Unbound.ml

@@ -25,6 +25,9 @@ type 't outer =
 type ('p, 't) rebind =
   'p * 't
 
+type ('p, 't) bind =
+  (('p, 't outer) rebind) abstraction (* = 'p * 't *)
+
 (*
 type 't inner =
   't
@@ -77,6 +80,18 @@ class virtual ['self] libmap = object (self : 'self)
       let q2 = visit_q penv q1 in
       p2, q2
 
+  (* 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: 'p1 'p2 't1 't2 .
+    ('env outside_rec_penv -> 'p1 -> 'p2) ->
+    ('env -> 't1 -> 't2) ->
+    'env -> ('p1, 't1) rebind -> ('p2, 't2) rebind
+  = fun visit_p visit_t env pt1 ->
+      self#visit_abstraction
+        (self#visit_rebind visit_p (self#visit_outer visit_t))
+        env
+        pt1
+
 (*
   method private visit_inner: 't1 't2 .
     ('env -> 't1 -> 't2) ->
@@ -103,32 +118,13 @@ class virtual ['self] libmap = 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 =
+type ('bn, 'fn) 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
-  | 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
+  | TeleCons of ('bn binder * ('bn, 'fn) term outer, ('bn, 'fn) tele) rebind
 
+and ('bn, 'fn) term =
+  | Var of 'fn
+  | Pi  of (('bn, 'fn) tele, ('bn, 'fn) term) bind
+  | Lam of (('bn, 'fn) tele, ('bn, 'fn) term) bind
+  | App of ('bn, 'fn) term * ('bn, 'fn) term list
 [@@deriving visitors { variety = "map"; ancestors = ["libmap"] }]
- *)