Implemented [map2] and [reduce2] for telescopes.

src/BindingForms.ml

@@ -296,6 +296,31 @@ class virtual ['self] map2 = object (self : 'self)
       let u3 = visit_u env' u1 u2 in
       recursive1, x3, t3, u3
 
+  method private visit_tele: 't1 't2 't3 .
+    ('env -> 't1 -> 't2 -> 't3) ->
+    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> ('bn3, 't3) tele * 'env
+  = fun visit_t env xts1 xts2 ->
+      match xts1, xts2 with
+      | [], [] ->
+          [], env
+      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
+          let t3 = visit_t env t1 t2 in
+          let x3, env = self#extend x1 x2 env in
+          let xts3, env = self#visit_tele visit_t env xts1 xts2 in
+          (x3, t3) :: xts3, env
+      | _, _ ->
+          VisitorsRuntime.fail()
+
+  method private visit_telescope: 't1 't2 't3 'u1 'u2 'u3 .
+    _ ->
+    ('env -> 't1 -> 't2 -> 't3) ->
+    ('env -> 'u1 -> 'u2 -> 'u3) ->
+    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> ('bn3, 't3, 'u3) telescope
+  = fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
+      let xts3, env = self#visit_tele visit_t env xts1 xts2 in
+      let u3 = visit_u env u1 u2 in
+      xts3, u3
+
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -304,7 +329,7 @@ end
 
 class virtual ['self] reduce2 = object (self : 'self)
 
-  method private virtual plus: 'z -> 'z -> 'z
+  inherit ['z] VisitorsRuntime.monoid
 
   method private visit_'bn: void -> void -> void -> void
   = fun _ _ _ -> assert false
@@ -333,6 +358,31 @@ class virtual ['self] reduce2 = object (self : 'self)
       let zu = self#restrict x1 x2 (visit_u env' u1 u2) in
       self#plus zt zu
 
+  method private visit_tele: 't1 't2 .
+    ('env -> 't1 -> 't2 -> 'z) ->
+    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'z * 'env
+  = fun visit_t env xts1 xts2 ->
+      match xts1, xts2 with
+      | [], [] ->
+          self#zero, env
+      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
+          let zt = visit_t env t1 t2 in
+          let env = self#extend x1 x2 env in
+          let zxts, env = self#visit_tele visit_t env xts1 xts2 in
+          self#plus zt zxts, env
+      | _, _ ->
+          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 zxts, env = self#visit_tele visit_t env xts1 xts2 in
+      let zu = visit_u env u1 u2 in
+      self#plus zxts zu
+
 end
 
 (* -------------------------------------------------------------------------- *)