Implement [avoid].

TODO

@@ -7,8 +7,8 @@ Relax ba so as to not require well-formedness?
 Global uniqueness, or uniqueness along a branch?
   Which wf criterion do we want? both?
 
-Implement avoid, which renames the bound names of a term so as to
-avoid a certain set of names.
+Implement a subst that does not copy the grafted term?
+Or parameterize subst over the copy operation that needs to be performed when grafting?
 
 Implement fused copy/subst, fused avoid/subst?
   Implement a kit that composes two kits, so as to easily implement fused operations.

demos/system-F-type/F.cppo.ml

@@ -69,6 +69,9 @@ type nominal_term =
 
 (* Operations based on visitors. *)
 
+(* We create more operations than we actually need in this demo.
+   This is just a way of testing that everything works. *)
+
 #include "AlphaLibMacros.cppo.ml"
 
 __FA
@@ -87,6 +90,10 @@ __COPY
 COPY(typ)
 COPY(term)
 
+__AVOID
+AVOID(typ)
+AVOID(term)
+
 __SHOW
 SHOW(typ)
 SHOW(term)

src/AlphaLibMacros.cppo.ml

@@ -119,6 +119,25 @@
 
 (* -------------------------------------------------------------------------- *)
 
+(* [avoid_term bad] returns a copy of its argument where some bound names have
+   been replaced with a fresh copy, so as to ensure that no bound name is in
+   the set [bad]. *)
+
+#define AVOID_CLASS     __avoid
+#define AVOID_FUN(term) CONCAT(avoid_, term)
+
+#define __AVOID                                                                \
+  class ['self] AVOID_CLASS bad = object (_ : 'self)                           \
+    inherit [_] map                                                            \
+    inherit [_] KitAvoid.map bad                                               \
+  end                                                                          \
+
+#define AVOID(term)                                                            \
+  let AVOID_FUN(term) bad t =                                                  \
+    (new AVOID_CLASS bad) # VISIT(term) KitAvoid.empty t                       \
+
+(* -------------------------------------------------------------------------- *)
+
 (* [show_term] converts its argument to a raw term, in a NONHYGIENIC manner,
    using [Atom.show] both at free name occurrences and bound name occurrences.
    It is a debugging tool. *)

src/Toolbox.cppo.ml

@@ -44,6 +44,9 @@ module Make (Term : ToolboxInput.INPUT) = struct
   __COPY
   COPY(term)
 
+  __AVOID
+  AVOID(term)
+
   __SHOW
   SHOW(term)
 

src/Toolbox.mli

@@ -32,6 +32,7 @@ module Make (Term : ToolboxInput.INPUT) : sig
   val wf_terms: nominal_term list -> bool
 
   val copy_term: nominal_term -> nominal_term
+  val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
 
   val show_term: nominal_term -> raw_term
 

src/alphaLib.mlpack

@@ -3,6 +3,7 @@ Abstraction
 Bn
 KitBa
 KitCopy
+KitAvoid
 KitEquiv
 KitExport
 KitFa