Moved the type [def] and its visitors to the attic.

src/BindingForms.ml

@@ -15,27 +15,6 @@ type ('bn, 'term) abs =
 
 (* -------------------------------------------------------------------------- *)
 
-(* A definition is a binding form of the form [let (rec) x = t in u]. The name
-   [x] is in scope in [u]. It is in scope in [t] if the definition is marked
-   recursive; otherwise, it is not. The terms [t] and [u] need not belong to the
-   same syntactic category. *)
-
-type recursive =
-  | NonRecursive
-  | Recursive
-
-type ('bn, 't, 'u) def =
-  recursive * 'bn * 't * 'u
-
-let choose recursive env env' =
-  match recursive with
-  | NonRecursive ->
-      env
-  | Recursive ->
-      env'
-
-(* -------------------------------------------------------------------------- *)
-
 (* 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
@@ -89,17 +68,6 @@ class virtual ['self] map = object (self : 'self)
       let t2 = visit_term env' t1 in
       x2, t2
 
-  method private visit_def: 't1 't2 'u1 'u2 .
-    _ ->
-    ('env -> 't1 -> 't2) ->
-    ('env -> 'u1 -> 'u2) ->
-    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def
-  = fun _ visit_t visit_u env (recursive, x1, t1, u1) ->
-      let x2, env' = self#extend x1 env in
-      let t2 = visit_t (choose recursive env env') t1 in
-      let u2 = visit_u env' u1 in
-      recursive, x2, t2, u2
-
   method private visit_tele: 't1 't2 .
     ('env -> 't1 -> 't2) ->
     'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele * 'env
@@ -148,20 +116,6 @@ class virtual ['self] endo = object (self : 'self)
       else
         x2, t2
 
-  method private visit_def: 't 'u .
-    _ ->
-    ('env -> 't -> 't) ->
-    ('env -> 'u -> 'u) ->
-    'env -> ('bn, 't, 'u) def -> ('bn, 't, 'u) def
-  = fun _ visit_t visit_u env ((recursive, x1, t1, u1) as this) ->
-      let x2, env' = self#extend x1 env in
-      let t2 = visit_t (choose recursive env env') t1 in
-      let u2 = visit_u env' u1 in
-      if x1 == x2 && t1 == t2 && u1 == u2 then
-        this
-      else
-        recursive, x2, t2, u2
-
   method private visit_tele: 't .
     ('env -> 't -> 't) ->
     'env -> ('bn, 't) tele -> ('bn, 't) tele * 'env
@@ -212,16 +166,6 @@ class virtual ['self] iter = object (self : 'self)
       let env' = self#extend x env in
       visit_term env' t
 
-  method private visit_def: 't 'u .
-    _ ->
-    ('env -> 't -> unit) ->
-    ('env -> 'u -> unit) ->
-    'env -> ('bn, 't, 'u) def -> unit
-  = fun _ visit_t visit_u env (recursive, x, t, u) ->
-      let env' = self#extend x env in
-      visit_t (choose recursive env env') t;
-      visit_u env' u
-
   method private visit_tele: 't .
     ('env -> 't -> unit) ->
     'env -> ('bn, 't) tele -> 'env
@@ -264,18 +208,6 @@ class virtual ['self] map2 = object (self : 'self)
       let x3, env' = self#extend x1 x2 env in
       x3, visit_term env' t1 t2
 
-  method private visit_def: 't1 'u1 't2 'u2 't3 'u3 .
-    _ ->
-    ('env -> 't1 -> 't2 -> 't3) ->
-    ('env -> 'u1 -> 'u2 -> 'u3) ->
-    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> ('bn3, 't3, 'u3) def
-  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
-      if recursive1 <> recursive2 then VisitorsRuntime.fail();
-      let x3, env' = self#extend x1 x2 env in
-      let t3 = visit_t (choose recursive1 env env') t1 t2 in
-      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
@@ -326,18 +258,6 @@ class virtual ['self] reduce2 = object (self : 'self)
       let env' = self#extend x1 x2 env in
       self#restrict x1 x2 (visit_term env' t1 t2)
 
-  method private visit_def: 't1 'u1 't2 'u2 .
-    _ ->
-    ('env -> 't1 -> 't2 -> 'z) ->
-    ('env -> 'u1 -> 'u2 -> 'z) ->
-    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> 'z
-  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
-      if recursive1 <> recursive2 then VisitorsRuntime.fail();
-      let env' = self#extend x1 x2 env in
-      let zt = visit_t (choose recursive1 env env') t1 t2 in
-      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

src/attic/BindingFormsDef.ml

+(* -------------------------------------------------------------------------- *)
+
+(* A definition is a binding form of the form [let (rec) x = t in u]. The name
+   [x] is in scope in [u]. It is in scope in [t] if the definition is marked
+   recursive; otherwise, it is not. The terms [t] and [u] need not belong to the
+   same syntactic category. *)
+
+type recursive =
+  | NonRecursive
+  | Recursive
+
+type ('bn, 't, 'u) def =
+  recursive * 'bn * 't * 'u
+
+let choose recursive env env' =
+  match recursive with
+  | NonRecursive ->
+      env
+  | Recursive ->
+      env'
+
+class virtual ['self] map = object (self : 'self)
+
+  method private visit_def: 't1 't2 'u1 'u2 .
+    _ ->
+    ('env -> 't1 -> 't2) ->
+    ('env -> 'u1 -> 'u2) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def
+  = fun _ visit_t visit_u env (recursive, x1, t1, u1) ->
+      let x2, env' = self#extend x1 env in
+      let t2 = visit_t (choose recursive env env') t1 in
+      let u2 = visit_u env' u1 in
+      recursive, x2, t2, u2
+
+end
+
+class virtual ['self] endo = object (self : 'self)
+
+  method private visit_def: 't 'u .
+    _ ->
+    ('env -> 't -> 't) ->
+    ('env -> 'u -> 'u) ->
+    'env -> ('bn, 't, 'u) def -> ('bn, 't, 'u) def
+  = fun _ visit_t visit_u env ((recursive, x1, t1, u1) as this) ->
+      let x2, env' = self#extend x1 env in
+      let t2 = visit_t (choose recursive env env') t1 in
+      let u2 = visit_u env' u1 in
+      if x1 == x2 && t1 == t2 && u1 == u2 then
+        this
+      else
+        recursive, x2, t2, u2
+
+end
+
+class virtual ['self] iter = object (self : 'self)
+
+  method private visit_def: 't 'u .
+    _ ->
+    ('env -> 't -> unit) ->
+    ('env -> 'u -> unit) ->
+    'env -> ('bn, 't, 'u) def -> unit
+  = fun _ visit_t visit_u env (recursive, x, t, u) ->
+      let env' = self#extend x env in
+      visit_t (choose recursive env env') t;
+      visit_u env' u
+
+end
+
+class virtual ['self] map2 = object (self : 'self)
+
+  method private visit_def: 't1 'u1 't2 'u2 't3 'u3 .
+    _ ->
+    ('env -> 't1 -> 't2 -> 't3) ->
+    ('env -> 'u1 -> 'u2 -> 'u3) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> ('bn3, 't3, 'u3) def
+  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
+      if recursive1 <> recursive2 then VisitorsRuntime.fail();
+      let x3, env' = self#extend x1 x2 env in
+      let t3 = visit_t (choose recursive1 env env') t1 t2 in
+      let u3 = visit_u env' u1 u2 in
+      recursive1, x3, t3, u3
+
+end
+
+class virtual ['self] reduce2 = object (self : 'self)
+
+  method private visit_def: 't1 'u1 't2 'u2 .
+    _ ->
+    ('env -> 't1 -> 't2 -> 'z) ->
+    ('env -> 'u1 -> 'u2 -> 'z) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> 'z
+  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
+      if recursive1 <> recursive2 then VisitorsRuntime.fail();
+      let env' = self#extend x1 x2 env in
+      let zt = visit_t (choose recursive1 env env') t1 t2 in
+      let zu = self#restrict x1 x2 (visit_u env' u1 u2) in
+      self#plus zt zu
+
+end