Safe Haskell | None |
---|---|
Language | Haskell2010 |
Build systems and the properties they should ensure.
Build
type Build c i k v = Tasks c k v -> k -> Store i k v -> Store i k v Source #
A build system takes a description of Tasks
, a target key, and a store,
and computes a new store, where the key and its dependencies are up to date.
Properties
correct :: (Ord k, Eq v) => Build Monad i k v -> Tasks Monad k v -> Bool Source #
Given a build
and tasks
, check that build
produces a correct result
for any initial store and a target key.
correctBuild :: (Ord k, Eq v) => Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool Source #
Given a description of tasks
, an initial store
, and a result
produced
by running a build system on a target key
, this function returns True
if
the result
is a correct build outcome. Specifically:
* result
and store
must agree on the values of all inputs. In other words,
no inputs were corrupted during the build.
* result
is consistent with the tasks
, i.e. for every non-input key,
the result of recomputing its task matches the value stored in the result
.