From c5f9153773ac25aa66edb40f9d2e1e4eec880449 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Thu, 16 Feb 2017 17:03:35 +0100
Subject: [PATCH] Implement [ba] on top of [iter] instead of [reduce].

---
 src/AlphaLibMacros.cppo.ml | 22 ++++++++++++++++++++++
 src/KitBa.ml               | 18 ++++++++++++++++++
 2 files changed, 40 insertions(+)

diff --git a/src/AlphaLibMacros.cppo.ml b/src/AlphaLibMacros.cppo.ml
index 59bf89f..7bdd2d7 100644
--- a/src/AlphaLibMacros.cppo.ml
+++ b/src/AlphaLibMacros.cppo.ml
@@ -69,6 +69,8 @@
 
 (* -------------------------------------------------------------------------- *)
 
+(* [ba] could be defined in terms of [reduce], as follows. *)
+
 #define BA_CLASS     __ba
 #define BA_FUN(term) CONCAT(ba_, term)
 
@@ -82,6 +84,26 @@
   let BA_FUN(term) t =                                                         \
     new BA_CLASS # VISIT(term) () t                                            \
 
+#undef __BA
+#undef BA
+
+(* -------------------------------------------------------------------------- *)
+
+(* We prefer to define [ba] in terms of [iter] because we wish to eliminate
+   our dependency on [reduce] visitors. *)
+
+#define __BA                                                                   \
+  class ['self] BA_CLASS = object (_ : 'self)                                  \
+    inherit [_] iter                                                           \
+    inherit [_] KitBa.iter                                                     \
+  end                                                                          \
+
+#define BA(term)                                                               \
+  let BA_FUN(term) t =                                                         \
+    let o = new BA_CLASS in                                                    \
+    o # VISIT(term) () t;                                                      \
+    o # accu                                                                   \
+
 (* -------------------------------------------------------------------------- *)
 
 #define AVOIDS_CLASS     __avoids
diff --git a/src/KitBa.ml b/src/KitBa.ml
index ddf240c..58f574a 100644
--- a/src/KitBa.ml
+++ b/src/KitBa.ml
@@ -1,6 +1,24 @@
 (* This kit serves to compute the set of ``bound atoms'' of a term, that is,
    the set of all binding name occurrences. *)
 
+(* This computation can be performed either on top of an [iter] visitor, or
+   on top of a [reduce] visitor. *)
+
+class ['self] iter = object (_ : 'self)
+
+  val mutable accu = Atom.Set.empty
+
+  method accu = accu (* must be public *)
+
+  (* A bound atom is added to the accumulator when its scope is entered. *)
+  method private extend x () =
+    accu <- Atom.Set.add x accu
+
+  method private visit_'fn () _x =
+    ()
+
+end
+
 class ['self] reduce = object (_ : 'self)
 
   method private extend _x () =
-- 
GitLab