{-# LANGUAGE ImpredicativeTypes, ConstraintKinds #-}

-- | Build systems and the properties they should ensure.
module Build (
    -- * Build
    Build,

    -- * Properties
    correctBuild
    ) where

import Build.Task
import Build.Task.Monad
import Build.Store
import Build.Utilities

-- | 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.
type Build c i k v = Tasks c k v -> k -> Store i k v -> Store i k v

-- | 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@.
correctBuild :: (Ord k, Eq v) => Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool
correctBuild :: forall k v i.
(Ord k, Eq v) =>
Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool
correctBuild Tasks Monad k v
tasks Store i k v
store Store i k v
result = (k -> Bool) -> [k] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all k -> Bool
correct ([k] -> Bool) -> (k -> [k]) -> k -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k -> [k]) -> k -> [k]
forall k. Ord k => (k -> [k]) -> k -> [k]
reachable k -> [k]
deps
  where
    deps :: k -> [k]
deps = [k] -> (Task Monad k v -> [k]) -> Maybe (Task Monad k v) -> [k]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Task Monad k v
task -> (v, [k]) -> [k]
forall a b. (a, b) -> b
snd ((v, [k]) -> [k]) -> (v, [k]) -> [k]
forall a b. (a -> b) -> a -> b
$ Task Monad k v -> (k -> v) -> (v, [k])
forall k v. Task Monad k v -> (k -> v) -> (v, [k])
trackPure (k -> f v) -> f v
Task Monad k v
task (k -> Store i k v -> v
forall k i v. k -> Store i k v -> v
`getValue` Store i k v
result)) (Maybe (Task Monad k v) -> [k]) -> Tasks Monad k v -> k -> [k]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tasks Monad k v
tasks
    correct :: k -> Bool
correct k
k = case Tasks Monad k v
tasks k
k of
        Maybe (Task Monad k v)
Nothing   -> k -> Store i k v -> v
forall k i v. k -> Store i k v -> v
getValue k
k Store i k v
result v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== k -> Store i k v -> v
forall k i v. k -> Store i k v -> v
getValue k
k Store i k v
store
        Just Task Monad k v
task -> k -> Store i k v -> v
forall k i v. k -> Store i k v -> v
getValue k
k Store i k v
result v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== Task Monad k v -> Store i k v -> v
forall k v i. Task Monad k v -> Store i k v -> v
compute (k -> f v) -> f v
Task Monad k v
task Store i k v
result