Implement [guq] using [iter] instead of [reduce].

src/AlphaLibMacros.cppo.ml

@@ -87,17 +87,16 @@
 
 #define __GUQ                                                                  \
   class ['self] GUQ_CLASS = object (_ : 'self)                                 \
-    inherit [_] reduce                                                         \
-    inherit [_] KitGuq.reduce                                                  \
+    inherit [_] iter                                                           \
+    inherit [_] KitGuq.iter                                                    \
   end                                                                          \
 
 #define GUQ(term)                                                              \
   let GUQ_FUN(term) t =                                                        \
     new GUQ_CLASS # VISIT(term) () t                                           \
   let GUQS_FUN(term) ts =                                                      \
-    List.fold_left                                                             \
-      (fun accu t -> Atom.Set.disjoint_union accu (GUQ_FUN(term) t))           \
-      Atom.Set.empty ts                                                        \
+    let o = new GUQ_CLASS in                                                   \
+    List.iter (o # VISIT(term) ()) ts                                          \
   let GUQ_FUN(term) t =                                                        \
     Atom.Set.handle_NonDisjointUnion GUQ_FUN(term) t                           \
   let GUQS_FUN(term) t =                                                       \

src/KitGuq.ml

-(* This kit serves to compute the set of ``bound atoms'' of a term (as in
-   [KitBa]) and at the same time, we check that the term satisfies ``global
-   uniqueness'', that is, no atom is bound twice inside this term (not even
-   along distinct branches). The exception [Atom.Set.NonDisjointUnion x] is
-   raised if the atom [x] occurs twice in a binding position. *)
+(* This kit serves to check that a term satisfies ``global uniqueness'', that
+   is, no atom is bound twice inside this term (not even along distinct
+   branches). The exception [Atom.Set.NonDisjointUnion x] is raised if the
+   atom [x] occurs twice in a binding position. *)
 
-class ['self] reduce = object (_ : 'self)
+class ['self] iter = object (_ : 'self)
 
-  method private extend _x () =
-    ()
-
-  method private visit_'fn () _x =
-    Atom.Set.empty
-
-  (* The monoid of sets of atoms, equipped with disjoint union, is used. *)
-  (* This can cause a [NonDisjointUnion] exception to be raised. *)
-  inherit [_] Atom.Set.disjoint_union_monoid
+  val mutable accu = Atom.Set.empty
 
-  (* An atom is added to the set of bound atoms when its scope is exited. *)
-  method private restrict x xs =
-    if Atom.Set.mem x xs then
+  (* A bound atom is added to the accumulator when its scope is entered. *)
+  method private extend x () =
+    if Atom.Set.mem x accu then
       raise (Atom.Set.NonDisjointUnion x)
     else
-      Atom.Set.add x xs
+      accu <- Atom.Set.add x accu
+
+  method private visit_'fn () _x =
+    ()
 
 end

src/attic/KitGuq.ml

+(* -------------------------------------------------------------------------- *)
+
+(* This [reduce] kit serves to compute the set of ``bound atoms'' of a term
+   (as in [KitBa]) and at the same time, check that the term satisfies
+   ``global uniqueness'', that is, no atom is bound twice inside this term
+   (not even along distinct branches). [Atom.Set.NonDisjointUnion x] is raised
+   if the atom [x] occurs twice in a binding position. *)
+
+class ['self] reduce = object (_ : 'self)
+
+  method private extend _x () =
+    ()
+
+  method private visit_'fn () _x =
+    Atom.Set.empty
+
+  (* The monoid of sets of atoms, equipped with disjoint union, is used. *)
+  (* This can cause a [NonDisjointUnion] exception to be raised. *)
+  inherit [_] Atom.Set.disjoint_union_monoid
+
+  (* An atom is added to the set of bound atoms when its scope is exited. *)
+  method private restrict x xs =
+    if Atom.Set.mem x xs then
+      raise (Atom.Set.NonDisjointUnion x)
+    else
+      Atom.Set.add x xs
+
+end
+
+(* -------------------------------------------------------------------------- *)
+
+#define __GUQ                                                                  \
+  class ['self] GUQ_CLASS = object (_ : 'self)                                 \
+    inherit [_] reduce                                                         \
+    inherit [_] KitGuq.reduce                                                  \
+  end                                                                          \
+
+#define GUQ(term)                                                              \
+  let GUQ_FUN(term) t =                                                        \
+    new GUQ_CLASS # VISIT(term) () t                                           \
+  let GUQS_FUN(term) ts =                                                      \
+    List.fold_left                                                             \
+      (fun accu t -> Atom.Set.disjoint_union accu (GUQ_FUN(term) t))           \
+      Atom.Set.empty ts                                                        \
+  let GUQ_FUN(term) t =                                                        \
+    Atom.Set.handle_NonDisjointUnion GUQ_FUN(term) t                           \
+  let GUQS_FUN(term) t =                                                       \
+    Atom.Set.handle_NonDisjointUnion GUQS_FUN(term) t                          \