{-# LANGUAGE ConstraintKinds, RankNTypes, TypeApplications #-}
module Build (
Build,
correct, correctBuild, idempotent
) where
import Build.Task
import Build.Task.Monad
import Build.Task.Wrapped
import Build.Store
import Build.Utilities
type Build c i k v = Tasks c k v -> k -> Store i k v -> Store i k v
correctBuild :: (Ord k, Eq v) => Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool
correctBuild tasks store result = all correct . reachable deps
where
deps = maybe [] (\t -> snd $ track (unwrap @Monad t) (flip getValue result)) . tasks
correct k = case tasks k of
Nothing -> getValue k result == getValue k store
Just t -> getValue k result == compute (unwrap @Monad t) (flip getValue result)
correct :: (Ord k, Eq v) => Build Monad i k v -> Tasks Monad k v -> Bool
correct build tasks = forall $ \(key, store) ->
correctBuild tasks store (build tasks key store) key
idempotent :: Eq v => Build Monad i k v -> Tasks Monad k v -> Bool
idempotent build tasks = forall $ \(key, store1) ->
let store2 = build tasks key store1
store3 = build tasks key store2
in forall $ \k -> getValue k store2 == getValue k store3