Moved the old implementation of [fa] to attic/.

src/AlphaLibMacros.cppo.ml

@@ -7,29 +7,9 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [fa] could be defined in terms of [reduce], as follows. *)
-
 #define FA_CLASS     __fa
 #define FA_FUN(term) CONCAT(fa_, term)
 
-#define __FA                                                                   \
-  class FA_CLASS = object                                                      \
-    inherit [_] reduce                                                         \
-    inherit [_] KitFa.reduce                                                   \
-  end                                                                          \
-
-#define FA(term)                                                               \
-  let FA_FUN(term) t =                                                         \
-    new FA_CLASS # VISIT(term) () t                                            \
-
-#undef __FA
-#undef FA
-
-(* -------------------------------------------------------------------------- *)
-
-(* We prefer to define [fa] in terms of [iter] because we wish to eliminate
-   our dependency on [reduce] visitors. *)
-
 #define __FA                                                                   \
   class FA_CLASS = object                                                      \
     inherit [_] iter                                                           \

src/KitFa.ml

@@ -62,29 +62,6 @@ end
 
 (* -------------------------------------------------------------------------- *)
 
-(* Computing the free atoms of a term, via [reduce]. *)
-
-(* In this style, no environment is required. *)
-
-(* type env = unit *)
-
-class ['self] reduce = object (_ : 'self)
-
-  (* The monoid of sets of atoms is used. *)
-  inherit [_] Atom.Set.union_monoid
-
-  method private extend _x () = ()
-
-  (* The atom [x] is removed from the set of free atoms when the scope of [x]
-     is exited. *)
-  method private restrict = Atom.Set.remove
-
-  method private visit_'fn () x = Atom.Set.singleton x
-
-end
-
-(* -------------------------------------------------------------------------- *)
-
 (* Testing whether a term has a free atom that satisfies a predicate [p]. *)
 
 exception Found of Atom.t

src/attic/KitFa.ml

+(* -------------------------------------------------------------------------- *)
+
+(* Computing the free atoms of a term, via [reduce]. *)
+
+(* In this style, no environment is required. *)
+
+(* type env = unit *)
+
+class ['self] reduce = object (_ : 'self)
+
+  (* The monoid of sets of atoms is used. *)
+  inherit [_] Atom.Set.union_monoid
+
+  method private extend _x () = ()
+
+  (* The atom [x] is removed from the set of free atoms when the scope of [x]
+     is exited. *)
+  method private restrict = Atom.Set.remove
+
+  method private visit_'fn () x = Atom.Set.singleton x
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+#define __FA                                                                   \
+  class FA_CLASS = object                                                      \
+    inherit [_] reduce                                                         \
+    inherit [_] KitFa.reduce                                                   \
+  end                                                                          \
+
+#define FA(term)                                                               \
+  let FA_FUN(term) t =                                                         \
+    new FA_CLASS # VISIT(term) () t                                            \