Split off [BindingFormsAbs].

src/BindingForms.ml

-type void
-
-(* -------------------------------------------------------------------------- *)
-
-(* The main effect of a binding construct is to cause the environment to be
-   enriched when the abstraction is traversed. The following visitor methods
-   define where the environment is enriched. *)
-
-(* These methods do not know the type of the environment, and do not know how
-   it is enriched or looked up; the latter task is delegated to the virtual
-   methods [extend] and [lookup]. The implementation of these methods is
-   provided by separate ``kits''. *)
+(* This module merges the visitor classes defined in the following modules:
 
-(* We need several varieties of visitors, which is a bit painful. As of now,
-   [iter], [map], [endo], [iter2] are required: see [ToolboxInput]. *)
+   - [BindingFormsAbs], which provides abstractions of one name in one term;
 
-(* The visitor methods are polymorphic in the type of terms. This is
-   important, as it means that one can use several instances of a binding
-   construct in a single type definition and still be able to construct
-   well-typed visitors. *)
+   - [BindingFormsUnbound], which provides a much richer combinator language
+     for defining complex binding constructs.
 
-(* The virtual methods [extend] and [lookup] are not polymorphic in the types
-   of bound names and environments. On the contrary, each kit comes with
-   certain specific types of bound names and environments. *)
+   This module also defines dummy [visit_'bn] methods, which are never called
+   but must exist (because we expect the user-defined type of terms to be
+   parameterized over ['bn] and ['fn]). *)
 
 (* -------------------------------------------------------------------------- *)
 
-(* A universal, concrete type of single-name abstractions. *)
+(* The empty type [void] is used in the definition of the dummy methods
+   [visit_'bn] below. This allows us to statically ensure that these
+   methods are never called. *)
 
-(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
-   in de Bruijn style, etc. -- so we parameterize the abstraction over the
-   type ['bn] of the bound name and over the type ['term] of the body. This
-   makes this type definition almost trivial -- it is just a pair -- but it
-   still serves as a syntactic marker of where abstractions are located. *)
-
-type ('bn, 'term) abs =
-  'bn * 'term
+type void
 
 (* -------------------------------------------------------------------------- *)
 
 (* [iter] *)
 
-class virtual ['self] iter = object (self : 'self)
+class virtual ['self] iter = object (_ : 'self)
 
   method private visit_'bn: void -> void -> void
   = fun _ _ -> assert false
 
-  method private virtual extend: 'bn -> 'env -> 'env
-
-  method private visit_abs: 'term .
-    _ ->
-    ('env -> 'term -> unit) ->
-    'env -> ('bn, 'term) abs -> unit
-  = fun _ visit_term env (x, t) ->
-      let env' = self#extend x env in
-      visit_term env' t
+  inherit [_] BindingFormsAbs.iter
 
 end
 
@@ -61,20 +34,12 @@ end
 
 (* [iter2] *)
 
-class virtual ['self] iter2 = object (self : 'self)
+class virtual ['self] iter2 = object (_ : 'self)
 
   method private visit_'bn: void -> void -> void -> void
   = fun _ _ _ -> assert false
 
-  method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env
-
-  method private visit_abs: 'term1 'term2 .
-    _ ->
-    ('env -> 'term1 -> 'term2 -> 'z) ->
-    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
-  = fun _ visit_term env (x1, t1) (x2, t2) ->
-      let env' = self#extend x1 x2 env in
-      visit_term env' t1 t2
+  inherit [_] BindingFormsAbs.iter2
 
 end
 
@@ -82,21 +47,12 @@ end
 
 (* [map] *)
 
-class virtual ['self] map = object (self : 'self)
+class virtual ['self] map = object (_ : 'self)
 
   method private visit_'bn: void -> void -> void
   = fun _ _ -> assert false
 
-  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
-
-  method private visit_abs: 'term1 'term2 .
-    _ ->
-    ('env -> 'term1 -> 'term2) ->
-    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs
-  = fun _ visit_term env (x1, t1) ->
-      let x2, env' = self#extend x1 env in
-      let t2 = visit_term env' t1 in
-      x2, t2
+  inherit [_] BindingFormsAbs.map
 
 end
 
@@ -104,23 +60,11 @@ end
 
 (* [endo] *)
 
-class virtual ['self] endo = object (self : 'self)
+class virtual ['self] endo = object (_ : 'self)
 
   method private visit_'bn: void -> void -> void
   = fun _ _ -> assert false
 
-  method private virtual extend: 'bn -> 'env -> 'bn * 'env
-
-  method private visit_abs: 'term .
-    _ ->
-    ('env -> 'term -> 'term) ->
-    'env -> ('bn, 'term) abs -> ('bn, 'term) abs
-  = fun _ visit_term env ((x1, t1) as this) ->
-      let x2, env' = self#extend x1 env in
-      let t2 = visit_term env' t1 in
-      if x1 == x2 && t1 == t2 then
-        this
-      else
-        x2, t2
+  inherit [_] BindingFormsAbs.endo
 
 end

src/BindingFormsAbs.ml

+(* -------------------------------------------------------------------------- *)
+
+(* A universal, concrete type of single-name abstractions. *)
+
+(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
+   in de Bruijn style, etc. -- so we parameterize the abstraction over the
+   type ['bn] of the bound name and over the type ['term] of the body. This
+   makes this type definition almost trivial -- it is just a pair -- but it
+   still serves as a syntactic marker of where abstractions are located. *)
+
+type ('bn, 'term) abs =
+  'bn * 'term
+
+(* -------------------------------------------------------------------------- *)
+
+(* The main effect of a binding construct is to cause the environment to be
+   enriched when the abstraction is traversed. The following visitor methods
+   define where the environment is enriched. *)
+
+(* These methods do not know the type of the environment, and do not know how
+   it is enriched or looked up; the latter task is delegated to the virtual
+   methods [extend] and [lookup]. The implementation of these methods is
+   provided by separate ``kits''. *)
+
+(* We need several varieties of visitors, which is a bit painful. As of now,
+   [iter], [map], [endo], [iter2] are required: see [ToolboxInput]. *)
+
+(* The visitor methods are polymorphic in the type of terms. This is
+   important, as it means that one can use several instances of a binding
+   construct in a single type definition and still be able to construct
+   well-typed visitors. *)
+
+(* The virtual methods [extend] and [lookup] are not polymorphic in the types
+   of bound names and environments. On the contrary, each kit comes with
+   certain specific types of bound names and environments. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* [iter] *)
+
+class virtual ['self] iter = object (self : 'self)
+
+  method private virtual extend: 'bn -> 'env -> 'env
+
+  method private visit_abs: 'term .
+    _ ->
+    ('env -> 'term -> unit) ->
+    'env -> ('bn, 'term) abs -> unit
+  = fun _ visit_term env (x, t) ->
+      let env' = self#extend x env in
+      visit_term env' t
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [iter2] *)
+
+class virtual ['self] iter2 = object (self : 'self)
+
+  method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env
+
+  method private visit_abs: 'term1 'term2 .
+    _ ->
+    ('env -> 'term1 -> 'term2 -> 'z) ->
+    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
+  = fun _ visit_term env (x1, t1) (x2, t2) ->
+      let env' = self#extend x1 x2 env in
+      visit_term env' t1 t2
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [map] *)
+
+class virtual ['self] map = object (self : 'self)
+
+  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
+
+  method private visit_abs: 'term1 'term2 .
+    _ ->
+    ('env -> 'term1 -> 'term2) ->
+    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs
+  = fun _ visit_term env (x1, t1) ->
+      let x2, env' = self#extend x1 env in
+      let t2 = visit_term env' t1 in
+      x2, t2
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+(* [endo] *)
+
+class virtual ['self] endo = object (self : 'self)
+
+  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
+
+  method private visit_abs: 'term .
+    _ ->
+    ('env -> 'term -> 'term) ->
+    'env -> ('bn, 'term) abs -> ('bn, 'term) abs
+  = fun _ visit_term env ((x1, t1) as this) ->
+      let x2, env' = self#extend x1 env in
+      let t2 = visit_term env' t1 in
+      if x1 == x2 && t1 == t2 then
+        this
+      else
+        x2, t2
+
+end

src/alphaLib.mlpack

 Atom
 BindingForms
+BindingFormsAbs
 KitAvoid
 KitAvoids
 KitBa