Moved comments from AlphaLibMacros to ToolboxOutput.

src/AlphaLibMacros.cppo.ml

@@ -3,9 +3,9 @@
 #define VISIT(term)                                                            \
   CONCAT(visit_, term)
 
-(* -------------------------------------------------------------------------- *)
+(* For comments about the operations that follow, see [ToolboxOutput.ml].     *)
 
-(* [fa_term] computes the set of the free atoms of a term. *)
+(* -------------------------------------------------------------------------- *)
 
 #define FA_CLASS     __fa
 #define FA_FUN(term) CONCAT(fa_, term)
@@ -22,14 +22,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [filter_term p t] returns a free atom of the term [t] that satisfies the
-   predicate [p], if such an atom exists. *)
-
-(* [closed_term t] tests whether the term [t] is closed, that is, whether
-   [t] has no free atom. *)
-
-(* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
-
 #define FILTER_CLASS     __filter
 #define FILTER_FUN(term) CONCAT(filter_, term)
 #define CLOSED_FUN(term) CONCAT(closed_, term)
@@ -55,8 +47,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [ba_term] computes the set of bound atoms of a term. *)
-
 #define BA_CLASS     __ba
 #define BA_FUN(term) CONCAT(ba_, term)
 
@@ -72,11 +62,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
-   that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
-   that is, no atom is bound twice along a branch. It returns [true] if these
-   two conditions are satisfied. *)
-
 #define AVOIDS_CLASS     __avoids
 #define AVOIDS_FUN(term) CONCAT(avoids_, term)
 
@@ -92,17 +77,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
-   is bound twice within this term (not even along different branches). *)
-
-(* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
-   no atom is bound twice within this list (not even within two distinct list
-   elements). *)
-
-(* [guq_term] and [guq_terms] should be used only in debugging mode, typically
-   in an [assert] construct. They print the identity of one offending atom on
-   the standard error channel. *)
-
 #define GUQ_CLASS      __guq
 #define GUQ_FUN(term)  CONCAT(guq_, term)
 #define GUQS_FUN(term) GUQ_FUN(CONCAT(term, s))
@@ -127,9 +101,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [copy_term] returns a copy of its argument where every bound name has been
-   replaced with a fresh copy, and every free name is unchanged. *)
-
 #define COPY_CLASS     __copy
 #define COPY_FUN(term) CONCAT(copy_, term)
 
@@ -145,10 +116,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [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)
 
@@ -164,10 +131,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [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. *)
-
 #define SHOW_CLASS     __show
 #define SHOW_FUN(term) CONCAT(show_, term)
 
@@ -183,12 +146,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [import_term] converts a raw term to a nominal term that satisfies the
-   Global Uniqueness Hypothesis, that is, a nominal term where every binding
-   name occurrence is represented by a unique atom. [import] expects every
-   free name occurrence to be in the domain of [env]. If that is not the case,
-   the exception [Unbound] is raised. *)
-
 (* TEMPORARY use string * loc so as to be able to give a location *)
 
 #define IMPORT_FUN(term) CONCAT(import_, term)
@@ -205,10 +162,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [export_term] converts a nominal term to a raw term, in a hygienic manner.
-   This is the proper way of displaying a term. [export] expects every free
-   name occurrence to be in the domain of [env]. *)
-
 #define EXPORT_CLASS     __export
 #define EXPORT_FUN(term) CONCAT(export_, term)
 
@@ -224,11 +177,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [size_term] computes the size of its argument. *)
-
-(* Beware: this counts the nodes whose type is [term], but does not count the
-   nodes of other types. *)
-
 #define SIZE_CLASS     __size
 #define SIZE_FUN(term) CONCAT(size_, term)
 
@@ -247,8 +195,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [equiv_term] tests whether two terms are alpha-equivalent. *)
-
 #define EQUIV_CLASS     __equiv
 #define EQUIV_FUN(term) CONCAT(equiv_, term)
 
@@ -266,26 +212,6 @@
 
 (* -------------------------------------------------------------------------- *)
 
-(* [subst_thing_term] applies a substitution to a nominal term,
-   yielding a nominal term. *)
-
-(* [subst_thing_term1] applies a singleton substitution to a nominal term,
-   yielding a nominal term. *)
-
-(* A substitution is a finite map of atoms to nominal things. Things need not
-   be terms: this is a thing-in-term substitution, substituting things for
-   variables in terms. *)
-
-(* When applying a substitution [sigma] to a term [t], the GUH guarantees that
-   the free atoms of (the codomain of) [sigma] cannot be captured by a binder
-   within [t]. The GUH also guarantees that a binder within [t] cannot appear
-   in the domain of [sigma], which means that we can go down into [t] and apply
-   [sigma] to every variable. *)
-
-(* Global uniqueness can be preserved, if desired, by copying the things that
-   are grafted into [t]. The user decides which [copy] operation should be used.
-   It could be [copy_thing], or it could be the identity. *)
-
 #define SUBST_CLASS(Var)      CONCAT(__subst_, Var)
 #define SUBST_FUN(Var, term)  CONCAT(subst_, CONCAT(Var, CONCAT(_, term)))
 #define SUBST_FUN1(Var, term) CONCAT(SUBST_FUN(Var, term), 1)

src/ToolboxOutput.ml

@@ -20,33 +20,118 @@ module type OUTPUT = sig
   type nominal_term =
     (Atom.t, Atom.t) term
 
+  (* [fa_term] computes the set of the free atoms of a term. *)
+
   val fa_term: nominal_term -> Atom.Set.t
+
+  (* [filter_term p t] returns a free atom of the term [t] that satisfies the
+     predicate [p], if such an atom exists. *)
+
   val filter_term: (Atom.t -> bool) -> nominal_term -> Atom.t option
+
+  (* [closed_term t] tests whether the term [t] is closed, that is, whether
+     [t] has no free atom. *)
+
   val closed_term: nominal_term -> bool
+
+  (* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
+
   val occurs_term: Atom.t -> nominal_term -> bool
 
+  (* [ba_term] computes the set of bound atoms of a term. *)
+
   val ba_term: nominal_term -> Atom.Set.t
+
+  (* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
+     that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
+     that is, no atom is bound twice along a branch. It returns [true] if these
+     two conditions are satisfied. *)
+
   val avoids_term: Atom.Set.t -> nominal_term -> bool
+
+  (* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
+     is bound twice within this term (not even along different branches). *)
+
+  (* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
+     no atom is bound twice within this list (not even within two distinct list
+     elements). *)
+
+  (* [guq_term] and [guq_terms] should be used only in debugging mode, typically
+     in an [assert] construct. They print the identity of one offending atom on
+     the standard error channel. *)
+
   val guq_term: nominal_term -> bool
   val guq_terms: nominal_term list -> bool
 
+  (* [copy_term] returns a copy of its argument where every bound name has been
+     replaced with a fresh copy, and every free name is unchanged. *)
+
   val copy_term: nominal_term -> nominal_term
+
+  (* [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]. *)
+
   val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
 
+  (* [show_term] converts its argument to a raw term using [Atom.show] both at
+     free name occurrences and bound name occurrences. It is in principle a
+     debugging tool only, as the strings produced by [Atom.show] do not make
+     sense (at free atoms) and are not beautiful. It is nevertheless a correct
+     printer IF the term is closed. *)
+
   val show_term: nominal_term -> raw_term
 
+  (* [import_term] converts a raw term to a nominal term that satisfies the
+     Global Uniqueness Hypothesis, that is, a nominal term where every binding
+     name occurrence is represented by a unique atom. [import] expects every
+     free name occurrence to be in the domain of [env]. If that is not the case,
+     the exception [Unbound] is raised. *)
+
   exception Unbound of string
   val import_term: KitImport.env -> raw_term -> nominal_term
 
+  (* [export_term] converts a nominal term to a raw term, in a hygienic manner.
+     This is the proper way of displaying a term. [export] expects every free
+     name occurrence to be in the domain of [env]. *)
+
   val export_term: KitExport.env -> nominal_term -> raw_term
 
+  (* [size_term] computes the size of its argument. Beware: this counts the
+     nodes whose type is [term], but does not count the nodes of other types. *)
+
   val size_term: (_, _) term -> int
 
+  (* [equiv_term] tests whether two terms are alpha-equivalent. *)
+
   val equiv_term: nominal_term -> nominal_term -> bool
 
+  (* [subst_TVar_term] applies a substitution to a nominal term, yielding a
+     nominal term. This is a substitution of things for variables; in the
+     general case, [TVar] could be a constructor of some type [thing] other
+     than [term]. *)
+
+  (* A substitution is a finite map of atoms to things. *)
+
+  (* When applying a substitution [sigma] to a term [t], the precondition of this
+     operation is that the bound atoms of [t] are fresh for [sigma], that is, do
+     not appear in the domain or codomain of [sigma]. This guarantees two things:
+     1- the free atoms in the codomain of [sigma] cannot be captured by a binder
+     within [t]; and 2- an atom in the domain of [sigma] cannot be masked by a
+     binder within [t], so we can go down into [t] and apply [sigma] to every
+     variable. *)
+
+  (* Global uniqueness can be preserved, if desired, by copying the things that
+     are grafted into [t]. The user decides which [copy] operation should be used.
+     It could be [copy_thing], or it could be the identity. *)
+
   val subst_TVar_term:
     (nominal_term -> nominal_term) ->
     nominal_term Atom.Map.t -> nominal_term -> nominal_term
+
+  (* [subst_TVar_term1] applies a singleton substitution to a nominal term,
+     yielding a nominal term. *)
+
   val subst_TVar_term1:
     (nominal_term -> nominal_term) ->
     nominal_term  -> Atom.t -> nominal_term -> nominal_term