Moved the direct implementation of telescopes to the attic.

src/BindingForms.ml

@@ -15,19 +15,6 @@ type ('bn, 'term) abs =
 
 (* -------------------------------------------------------------------------- *)
 
-(* A telescope is represented as a pair of a tele and a scope. A tele is a
-   list of bindings, where, in [(x, t) :: xts], the name [x] is considered
-   bound in [xts]. Furthermore, in a telescope [xts, u], all of the names
-   in the domain of [xts] are considered bound in [u]. *)
-
-type ('bn, 't) tele =
-  ('bn * 't) list
-
-type ('bn, 't, 'u) telescope =
-  ('bn, 't) tele * 'u
-
-(* -------------------------------------------------------------------------- *)
-
 (* The main effect of an abstraction is to cause the environment to be
    enriched when the abstraction is traversed. The following classes define
    where the environment is enriched. *)
@@ -68,27 +55,6 @@ class virtual ['self] iter = object (self : 'self)
       let env' = self#extend x env in
       visit_term env' t
 
-  method private visit_tele: 't .
-    ('env -> 't -> unit) ->
-    'env -> ('bn, 't) tele -> 'env
-  = fun visit_t env xts ->
-      match xts with
-      | [] ->
-          env
-      | (x, t) :: xts ->
-          visit_t env t;
-          let env = self#extend x env in
-          self#visit_tele visit_t env xts
-
-  method private visit_telescope: 't 'u.
-    _ ->
-    ('env -> 't -> unit) ->
-    ('env -> 'u -> unit) ->
-    'env -> ('bn, 't, 'u) telescope -> unit
-  = fun _ visit_t visit_u env (xts, u) ->
-      let env = self#visit_tele visit_t env xts in
-      visit_u env u
-
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -110,29 +76,6 @@ class virtual ['self] iter2 = object (self : 'self)
       let env' = self#extend x1 x2 env in
       visit_term env' t1 t2
 
-  method private visit_tele: 't1 't2 .
-    ('env -> 't1 -> 't2 -> 'z) ->
-    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'env
-  = fun visit_t env xts1 xts2 ->
-      match xts1, xts2 with
-      | [], [] ->
-          env
-      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
-          visit_t env t1 t2;
-          let env = self#extend x1 x2 env in
-          self#visit_tele visit_t env xts1 xts2
-      | _, _ ->
-          VisitorsRuntime.fail()
-
-  method private visit_telescope: 't1 't2 'u1 'u2.
-    _ ->
-    ('env -> 't1 -> 't2 -> 'z) ->
-    ('env -> 'u1 -> 'u2 -> 'z) ->
-    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> 'z
-  = fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
-      let env = self#visit_tele visit_t env xts1 xts2 in
-      visit_u env u1 u2;
-
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -155,29 +98,6 @@ class virtual ['self] map = object (self : 'self)
       let t2 = visit_term env' t1 in
       x2, t2
 
-  method private visit_tele: 't1 't2 .
-    ('env -> 't1 -> 't2) ->
-    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele * 'env
-  = fun visit_t env xts1 ->
-      match xts1 with
-      | [] ->
-          [], env
-      | (x1, t1) :: xts1 ->
-          let t2 = visit_t env t1 in
-          let x2, env = self#extend x1 env in
-          let xts2, env = self#visit_tele visit_t env xts1 in
-          (x2, t2) :: xts2, env
-
-  method private visit_telescope: 't1 't2 'u1 'u2 .
-    _ ->
-    ('env -> 't1 -> 't2) ->
-    ('env -> 'u1 -> 'u2) ->
-    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope
-  = fun _ visit_t visit_u env (xts1, u1) ->
-      let xts2, env = self#visit_tele visit_t env xts1 in
-      let u2 = visit_u env u1 in
-      xts2, u2
-
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -203,33 +123,4 @@ class virtual ['self] endo = object (self : 'self)
       else
         x2, t2
 
-  method private visit_tele: 't .
-    ('env -> 't -> 't) ->
-    'env -> ('bn, 't) tele -> ('bn, 't) tele * 'env
-  = fun visit_t env xts1 ->
-      match xts1 with
-      | [] ->
-          [], env
-      | ((x1, t1) :: xts1) as this ->
-          let t2 = visit_t env t1 in
-          let x2, env = self#extend x1 env in
-          let xts2, env = self#visit_tele visit_t env xts1 in
-          if x1 == x2 && t1 == t2 && xts1 == xts2 then
-            this, env
-          else
-            (x2, t2) :: xts2, env
-
-  method private visit_telescope: 't 'u .
-    _ ->
-    ('env -> 't -> 't) ->
-    ('env -> 'u -> 'u) ->
-    'env -> ('bn, 't, 'u) telescope -> ('bn, 't, 'u) telescope
-  = fun _ visit_t visit_u env ((xts1, u1) as this) ->
-      let xts2, env = self#visit_tele visit_t env xts1 in
-      let u2 = visit_u env u1 in
-      if xts1 == xts2 && u1 == u2 then
-        this
-      else
-        xts2, u2
-
 end

src/attic/BindingFormsTelescope.ml

+(* -------------------------------------------------------------------------- *)
+
+(* A telescope is represented as a pair of a tele and a scope. A tele is a
+   list of bindings, where, in [(x, t) :: xts], the name [x] is considered
+   bound in [xts]. Furthermore, in a telescope [xts, u], all of the names
+   in the domain of [xts] are considered bound in [u]. *)
+
+type ('bn, 't) tele =
+  ('bn * 't) list
+
+type ('bn, 't, 'u) telescope =
+  ('bn, 't) tele * 'u
+
+(* -------------------------------------------------------------------------- *)
+
+(* [iter] *)
+
+class virtual ['self] iter = object (self : 'self)
+
+  method private visit_tele: 't .
+    ('env -> 't -> unit) ->
+    'env -> ('bn, 't) tele -> 'env
+  = fun visit_t env xts ->
+      match xts with
+      | [] ->
+          env
+      | (x, t) :: xts ->
+          visit_t env t;
+          let env = self#extend x env in
+          self#visit_tele visit_t env xts
+
+  method private visit_telescope: 't 'u.
+    _ ->
+    ('env -> 't -> unit) ->
+    ('env -> 'u -> unit) ->
+    'env -> ('bn, 't, 'u) telescope -> unit
+  = fun _ visit_t visit_u env (xts, u) ->
+      let env = self#visit_tele visit_t env xts in
+      visit_u env u
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [iter2] *)
+
+class virtual ['self] iter2 = object (self : 'self)
+
+  method private visit_tele: 't1 't2 .
+    ('env -> 't1 -> 't2 -> 'z) ->
+    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'env
+  = fun visit_t env xts1 xts2 ->
+      match xts1, xts2 with
+      | [], [] ->
+          env
+      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
+          visit_t env t1 t2;
+          let env = self#extend x1 x2 env in
+          self#visit_tele visit_t env xts1 xts2
+      | _, _ ->
+          VisitorsRuntime.fail()
+
+  method private visit_telescope: 't1 't2 'u1 'u2.
+    _ ->
+    ('env -> 't1 -> 't2 -> 'z) ->
+    ('env -> 'u1 -> 'u2 -> 'z) ->
+    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> 'z
+  = fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
+      let env = self#visit_tele visit_t env xts1 xts2 in
+      visit_u env u1 u2;
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [map] *)
+
+class virtual ['self] map = object (self : 'self)
+
+  method private visit_tele: 't1 't2 .
+    ('env -> 't1 -> 't2) ->
+    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele * 'env
+  = fun visit_t env xts1 ->
+      match xts1 with
+      | [] ->
+          [], env
+      | (x1, t1) :: xts1 ->
+          let t2 = visit_t env t1 in
+          let x2, env = self#extend x1 env in
+          let xts2, env = self#visit_tele visit_t env xts1 in
+          (x2, t2) :: xts2, env
+
+  method private visit_telescope: 't1 't2 'u1 'u2 .
+    _ ->
+    ('env -> 't1 -> 't2) ->
+    ('env -> 'u1 -> 'u2) ->
+    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope
+  = fun _ visit_t visit_u env (xts1, u1) ->
+      let xts2, env = self#visit_tele visit_t env xts1 in
+      let u2 = visit_u env u1 in
+      xts2, u2
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [endo] *)
+
+class virtual ['self] endo = object (self : 'self)
+
+  method private visit_tele: 't .
+    ('env -> 't -> 't) ->
+    'env -> ('bn, 't) tele -> ('bn, 't) tele * 'env
+  = fun visit_t env xts1 ->
+      match xts1 with
+      | [] ->
+          [], env
+      | ((x1, t1) :: xts1) as this ->
+          let t2 = visit_t env t1 in
+          let x2, env = self#extend x1 env in
+          let xts2, env = self#visit_tele visit_t env xts1 in
+          if x1 == x2 && t1 == t2 && xts1 == xts2 then
+            this, env
+          else
+            (x2, t2) :: xts2, env
+
+  method private visit_telescope: 't 'u .
+    _ ->
+    ('env -> 't -> 't) ->
+    ('env -> 'u -> 'u) ->
+    'env -> ('bn, 't, 'u) telescope -> ('bn, 't, 'u) telescope
+  = fun _ visit_t visit_u env ((xts1, u1) as this) ->
+      let xts2, env = self#visit_tele visit_t env xts1 in
+      let u2 = visit_u env u1 in
+      if xts1 == xts2 && u1 == u2 then
+        this
+      else
+        xts2, u2
+
+end