anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-13 11:16:48 +03:00
Code Issues Projects Releases Wiki Activity

Comments about the usage of the JuvixCore recursors (#1818)

Browse Source
This commit is contained in:
Łukasz Czajka 2023-02-08 12:49:06 +01:00 committed by GitHub
parent 151bba5113
commit a288ae3a09
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 57 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
View File

@ -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)

34
src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
View File

@ -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)