From a288ae3a09182334d69c492e23d4ce0da5406f08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Wed, 8 Feb 2023 12:49:06 +0100
Subject: [PATCH] Comments about the usage of the JuvixCore recursors (#1818)

---
 .../Core/Extra/Recursors/Fold/Named.hs        | 23 +++++++++++++
 .../Core/Extra/Recursors/Map/Named.hs         | 34 +++++++++++++++++++
 2 files changed, 57 insertions(+)

diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
index fcee5a971..6469a8c42 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
+++ b/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)
 
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
index a957bfbac..18e79a990 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
+++ b/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)