All visitor methods for the type [def].

src/BindingForms.ml

@@ -15,23 +15,14 @@ type ('bn, 'term) abs =
 
 (* -------------------------------------------------------------------------- *)
 
-(* A definition is a binding form of the form [let x = t1 in t2].
-   The name [x] is in scope in [t2], but not in [t1]. *)
+(* A definition is a binding form of the form [let x = t in u].
+   The name [x] is in scope in [u], but not in [t]. *)
 
 type ('bn, 'term) def =
   'bn * 'term * 'term
 
 (* This type is isomorphic to ['term * ('bn, 'term) abs]. *)
 
-(* This isomorphism is exploited below; it facilitates the construction of
-   visitor methods for [def], based on visitor methods for [abs]. *)
-
-let into : 'term * ('bn, 'term) abs -> ('bn, 'term) def =
-  fun (t1, (x, t2)) -> (x, t1, t2)
-
-let outof : ('bn, 'term) def -> 'term * ('bn, 'term) abs =
-  fun (x, t1, t2) -> (t1, (x, t2))
-
 (* -------------------------------------------------------------------------- *)
 
 (* The main effect of an abstraction is to cause the environment to be
@@ -80,22 +71,11 @@ class virtual ['self] map = object (self : 'self)
     _ ->
     ('env -> 'term1 -> 'term2) ->
     'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def
-  = fun b f env def ->
-      let t1, a2 = outof def in
-      into (
-        f env t1,
-        self#visit_abs b f env a2
-      )
-
-  (* TEMPORARY direct version:
-  method private visit_def: 'term1 'term2 .
-    _ ->
-    ('env -> 'term1 -> 'term2) ->
-    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def
-  = fun _ f env (x, t1, t2) ->
+  = fun _ f env (x, t, u) ->
       let x', env' = self#extend x env in
-      x', f env t1, f env' t2
-   *)
+      let t' = f env t in
+      let u' = f env' u in
+      x', t', u'
 
 end
 
@@ -122,6 +102,19 @@ class virtual ['self] endo = object (self : 'self)
       else
         x', body'
 
+  method private visit_def: 'term .
+    _ ->
+    ('env -> 'term -> 'term) ->
+    'env -> ('bn, 'term) def -> ('bn, 'term) def
+  = fun _ f env ((x, t, u) as this) ->
+      let x', env' = self#extend x env in
+      let t' = f env t in
+      let u' = f env' u in
+      if x == x' && t == t' && u == u' then
+        this
+      else
+        x', t', u'
+
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -130,6 +123,8 @@ end
 
 class virtual ['self] reduce = object (self : 'self)
 
+  method private virtual plus: 'z -> 'z -> 'z
+
   method private visit_'bn: void -> void -> void
   = fun _ _ -> assert false
 
@@ -145,6 +140,16 @@ class virtual ['self] reduce = object (self : 'self)
       let env' = self#extend x env in
       self#restrict x (f env' body)
 
+  method private visit_def: 'term .
+    _ ->
+    ('env -> 'term -> 'z) ->
+    'env -> ('bn, 'term) def -> 'z
+  = fun _ f env (x, t, u) ->
+      let env' = self#extend x env in
+      let zt = f env t in
+      let zu = self#restrict x (f env' u) in
+      self#plus zt zu
+
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -178,6 +183,16 @@ class virtual ['self] map2 = object (self : 'self)
       let x3, env' = self#extend x1 x2 env in
       x3, f env' body1 body2
 
+  method private visit_def: 'term1 'term2 'term3 .
+    _ ->
+    ('env -> 'term1 -> 'term2 -> 'term3) ->
+    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def -> ('bn3, 'term3) def
+  = fun _ f env (x1, t1, u1) (x2, t2, u2) ->
+      let x3, env' = self#extend x1 x2 env in
+      let t3 = f env t1 t2 in
+      let u3 = f env' u1 u2 in
+      x3, t3, u3
+
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -186,6 +201,8 @@ end
 
 class virtual ['self] reduce2 = object (self : 'self)
 
+  method private virtual plus: 'z -> 'z -> 'z
+
   method private visit_'bn: void -> void -> void -> void
   = fun _ _ _ -> assert false
 
@@ -201,6 +218,16 @@ class virtual ['self] reduce2 = object (self : 'self)
       let env' = self#extend x1 x2 env in
       self#restrict x1 x2 (f env' body1 body2)
 
+  method private visit_def: 'term1 'term2 .
+    _ ->
+    ('env -> 'term1 -> 'term2 -> 'z) ->
+    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def -> 'z
+  = fun _ f env (x1, t1, u1) (x2, t2, u2) ->
+      let env' = self#extend x1 x2 env in
+      let zt = f env t1 t2 in
+      let zu = self#restrict x1 x2 (f env' u1 u2) in
+      self#plus zt zu
+
 end
 
 (* -------------------------------------------------------------------------- *)