Comments about the usage of the JuvixCore recursors

src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs

@@ -4,6 +4,29 @@ import Data.Functor.Identity
 import Juvix.Compiler.Core.Extra.Recursors.Base
 import Juvix.Compiler.Core.Extra.Recursors.Fold
 
+{-
+
+There are three major versions of folding recursors.
+
+1. `ufold f g t` folds the term `t` bottom-up, first using `g` to map the
+   current subterm into a value `a`, and then using `f` to combine `a` with the
+   values for children.
+2. `walk f t` combines the applicative actions obtained by applying `f` to each
+   subterm of `t`.
+3. `gather f a t` goes through all subterms of `t` applying `f` to the current
+   value and the subterm to obtain the next value, with `a` being the initial
+   value.
+
+The suffixes of `ufold`, etc., indicate the exact form of the folding functions,
+with similar conventions as with the mapping recursors (see
+Core/Extra/Recursors/Map/Named.hs).
+
+\* A: Applicative version.
+\* L: Provide the binder list.
+\* N: Provide the de Bruijn level.
+
+-}
+
 ufoldA :: (Applicative f) => (a -> [a] -> a) -> (Node -> f a) -> Node -> f a
 ufoldA uplus f = ufoldG unitCollector uplus (const f)
 

src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs

@@ -5,6 +5,40 @@ import Juvix.Compiler.Core.Extra.Recursors.Base
 import Juvix.Compiler.Core.Extra.Recursors.Map
 import Juvix.Compiler.Core.Extra.Recursors.Parameters
 
+{-
+
+The mapping recursors come in two major variants: dmap and umap. They map each
+subterm of a given term. The invocation `dmap f t` goes through the node `t`
+top-down, applying the function `f` to `t` first, and then recursively
+descending into the children of `f t`. The invocation `umap f t` goes through
+the term `t` bottom-up, first recursively descending into the children of `t`
+and mapping them with `umap f`, then reassembling `t` with the mapped children
+into `t'`, and finally applying `f` to `t'`.
+
+The suffixes of `dmap` and `umap` indicate the exact form of the mapping
+function `f`, what arguments are provided to it and how its return value is
+interpreted.
+
+\* M: Monadic version. The return value of the mapping function `f` is wrapped in
+  a monad.
+\* L: The function `f` receives as an argument the list of binders upwards in the
+  term. The n-th element of the binder list corresponds to the free variable of
+  the current subterm with de Bruijn index n.
+\* N: The function `f` receives as an argument the number of binders upwards in
+  the term, i.e., the current de Bruijn level.
+\* ': When combined with L or N, makes it possible to supply the initial binder
+  list or de Bruijn level. This is useful when mapping a subterm with free
+  variables.
+\* R: The function `f` returns an element of the `Recur` (or `Recur'`) datatype,
+  indicating whether `dmap` should descend into the children or stop the
+  traversal.
+\* C: Enables collecting an arbitrary value while going downward in the term tree
+  with `dmap`. The initial value is provided to `dmap`. The function `f`
+  receives as an argument the current collected value and returns the value for
+  the children, in addition to the new node.
+
+-}
+
 dmapLRM :: (Monad m) => (BinderList Binder -> Node -> m Recur) -> Node -> m Node
 dmapLRM f = dmapLRM' (mempty, f)