Topological / Suspending Recursive Builder #
This module defines a recursive build function that topologically (ι.e., via a depth-first search with memoization) builds the elements of a build store.
This is called a suspending scheduler in Build systems à la carte.
Recursive Fetching #
In this section, we define the primitives that make up a builder.
A dependently typed monadic fetch function.
That is, a function within the monad m
and takes an input a : α
describing what to fetch and and produces some output b : β a
(dependently
typed) or b : B
(not) describing what was fetched. All build functions are
fetch functions, but not all fetch functions need build something.
Instances For
In order to nest builds / fetches within one another,
we equip the monad m
with a fetch function of its own.
We can then use the such a monad as the basis for a fetch function itself.
A DFetchFn
that provides its base DRecFetchFn
with itself.
The basic recFetch
can fail to terminate in a variety of ways,
it can even cycle (i.e., a
fetches b
which fetches a
). Thus, we
define the acyclicRecFetch
below to guard against such cases.
A recFetch
augmented by a CycleT
to guard against recursive cycles.
If the set of visited keys is finite, this function should provably terminate.
We use keyOf
to the derive the unique key of a fetch from its descriptor
a : α
. We do this because descriptors may not be comparable and/or contain
more information than necessary to determine uniqueness.
Instances For
When building, we usually do not want to build the same thing twice during
a single build pass. At the same time, separate builds may both wish to fetch
the same thing. Thus, we need to store past build results to return them upon
future fetches. This is what recFetchMemoize
below does.
recFetchAcyclic
augmented with a MonadDStore
to
memoize fetch results and thus avoid computing the same result twice.
Instances For
Building #
In this section, we use the abstractions we have just created to define the desired topological recursive build function (a.k.a. a suspending scheduler).
Recursively builds objects for the keys κ
, avoiding cycles.
Instances For
Dependently typed version of buildTop
.
Instances For
Recursively fills a MonadStore
of key-object pairs by
building objects topologically (ι.e., depth-first with memoization).
If a cycle is detected, the list of keys traversed is thrown.