A more general definition of [def].

src/BindingForms.ml

@@ -16,12 +16,13 @@ type ('bn, 'term) abs =
 (* -------------------------------------------------------------------------- *)
 
 (* 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]. *)
+   The name [x] is in scope in [u], but not in [t].
+   The terms [t] and [u] need not belong to the same syntactic category. *)
 
-type ('bn, 'term) def =
-  'bn * 'term * 'term
+type ('bn, 't, 'u) def =
+  'bn * 't * 'u
 
-(* This type is isomorphic to ['term * ('bn, 'term) abs]. *)
+(* This type is isomorphic to ['t * ('bn, 'u) abs]. *)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -67,14 +68,15 @@ class virtual ['self] map = object (self : 'self)
       let x2, env' = self#extend x1 env in
       x2, f env' t1
 
-  method private visit_def: 'term1 'term2 .
+  method private visit_def: 't1 't2 'u1 'u2 .
     _ ->
-    ('env -> 'term1 -> 'term2) ->
-    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def
-  = fun _ f env (x1, t1, u1) ->
+    ('env -> 't1 -> 't2) ->
+    ('env -> 'u1 -> 'u2) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def
+  = fun _ f g env (x1, t1, u1) ->
       let x2, env' = self#extend x1 env in
       let t2 = f env t1 in
-      let u2 = f env' u1 in
+      let u2 = g env' u1 in
       x2, t2, u2
 
 end
@@ -102,14 +104,15 @@ class virtual ['self] endo = object (self : 'self)
       else
         x2, t2
 
-  method private visit_def: 'term .
+  method private visit_def: 't 'u .
     _ ->
-    ('env -> 'term -> 'term) ->
-    'env -> ('bn, 'term) def -> ('bn, 'term) def
-  = fun _ f env ((x1, t1, u1) as this) ->
+    ('env -> 't -> 't) ->
+    ('env -> 'u -> 'u) ->
+    'env -> ('bn, 't, 'u) def -> ('bn, 't, 'u) def
+  = fun _ f g env ((x1, t1, u1) as this) ->
       let x2, env' = self#extend x1 env in
       let t2 = f env t1 in
-      let u2 = f env' u1 in
+      let u2 = g env' u1 in
       if x1 == x2 && t1 == t2 && u1 == u2 then
         this
       else
@@ -140,14 +143,15 @@ class virtual ['self] reduce = object (self : 'self)
       let env' = self#extend x env in
       self#restrict x (f env' t)
 
-  method private visit_def: 'term .
+  method private visit_def: 't 'u .
     _ ->
-    ('env -> 'term -> 'z) ->
-    'env -> ('bn, 'term) def -> 'z
-  = fun _ f env (x, t, u) ->
+    ('env -> 't -> 'z) ->
+    ('env -> 'u -> 'z) ->
+    'env -> ('bn, 't, 'u) def -> 'z
+  = fun _ f g 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
+      let zu = self#restrict x (g env' u) in
       self#plus zt zu
 
 end
@@ -184,14 +188,15 @@ class virtual ['self] map2 = object (self : 'self)
       let x3, env' = self#extend x1 x2 env in
       x3, f env' t1 t2
 
-  method private visit_def: 'term1 'term2 'term3 .
+  method private visit_def: 't1 'u1 't2 'u2 't3 'u3 .
     _ ->
-    ('env -> 'term1 -> 'term2 -> 'term3) ->
-    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def -> ('bn3, 'term3) def
-  = fun _ f env (x1, t1, u1) (x2, t2, u2) ->
+    ('env -> 't1 -> 't2 -> 't3) ->
+    ('env -> 'u1 -> 'u2 -> 'u3) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> ('bn3, 't3, 'u3) def
+  = fun _ f g 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
+      let u3 = g env' u1 u2 in
       x3, t3, u3
 
 end
@@ -219,14 +224,15 @@ class virtual ['self] reduce2 = object (self : 'self)
       let env' = self#extend x1 x2 env in
       self#restrict x1 x2 (f env' t1 t2)
 
-  method private visit_def: 'term1 'term2 .
+  method private visit_def: 't1 'u1 't2 'u2 .
     _ ->
-    ('env -> 'term1 -> 'term2 -> 'z) ->
-    'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def -> 'z
-  = fun _ f env (x1, t1, u1) (x2, t2, u2) ->
+    ('env -> 't1 -> 't2 -> 'z) ->
+    ('env -> 'u1 -> 'u2 -> 'z) ->
+    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> 'z
+  = fun _ f g 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
+      let zu = self#restrict x1 x2 (g env' u1 u2) in
       self#plus zt zu
 
 end