{-# language FlexibleContexts #-}
{-# language RankNTypes #-}
{-# language StandaloneDeriving #-}
{-# language TemplateHaskell #-}
{-# language UndecidableInstances #-}
module Rock.Traces where

import Control.Monad.IO.Class
import Data.Constraint.Extras
import Data.Dependent.HashMap(DHashMap)
import qualified Data.Dependent.HashMap as DHashMap
import Data.Dependent.Sum
import Data.Functor.Classes
import Data.GADT.Compare
import Data.GADT.Show
import Data.Hashable
import Data.Some
import Text.Show.Deriving

data ValueDeps f dep a = ValueDeps
  { forall (f :: * -> *) (dep :: * -> *) a. ValueDeps f dep a -> a
value :: !a
  , forall (f :: * -> *) (dep :: * -> *) a.
ValueDeps f dep a -> DHashMap f dep
dependencies :: !(DHashMap f dep)
  }

return []

deriving instance (Show a, GShow f, Has' Show f dep) => Show (ValueDeps f dep a)

instance (GShow f, Has' Show f dep) => Show1 (ValueDeps f dep) where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> ValueDeps f dep a -> ShowS
liftShowsPrec = $(makeLiftShowsPrec ''ValueDeps)

type Traces f dep = DHashMap f (ValueDeps f dep)

verifyDependencies
  :: (MonadIO m, GEq f, Has' Eq f dep)
  => (forall a'. f a' -> m a')
  -> (forall a'. f a' -> a' -> m (dep a'))
  -> ValueDeps f dep a
  -> m (Maybe a)
verifyDependencies :: forall (m :: * -> *) (f :: * -> *) (dep :: * -> *) a.
(MonadIO m, GEq f, Has' Eq f dep) =>
(forall a'. f a' -> m a')
-> (forall a'. f a' -> a' -> m (dep a'))
-> ValueDeps f dep a
-> m (Maybe a)
verifyDependencies forall a'. f a' -> m a'
fetch forall a'. f a' -> a' -> m (dep a')
createDependencyRecord (ValueDeps a
value_ DHashMap f dep
deps) = do
  Bool
upToDate <- [DSum f dep] -> (DSum f dep -> m Bool) -> m Bool
forall (m :: * -> *) a. Monad m => [a] -> (a -> m Bool) -> m Bool
allM (DHashMap f dep -> [DSum f dep]
forall (k :: * -> *) (v :: * -> *). DHashMap k v -> [DSum k v]
DHashMap.toList DHashMap f dep
deps) ((DSum f dep -> m Bool) -> m Bool)
-> (DSum f dep -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \(f a
depKey :=> dep a
dep) -> do
    a
depValue <- f a -> m a
forall a'. f a' -> m a'
fetch f a
depKey
    dep a
newDep <- f a -> a -> m (dep a)
forall a'. f a' -> a' -> m (dep a')
createDependencyRecord f a
depKey a
depValue
    Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ f a -> f a -> dep a -> dep a -> Bool
forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
EqTag tag f =>
tag a -> tag a -> f a -> f a -> Bool
eqTagged f a
depKey f a
depKey dep a
dep dep a
newDep
  Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ if Bool
upToDate
    then a -> Maybe a
forall a. a -> Maybe a
Just a
value_
    else Maybe a
forall a. Maybe a
Nothing
  where
    allM :: Monad m => [a] -> (a -> m Bool) -> m Bool
    allM :: forall (m :: * -> *) a. Monad m => [a] -> (a -> m Bool) -> m Bool
allM [] a -> m Bool
_ = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    allM (a
x:[a]
xs) a -> m Bool
p = do
      Bool
b <- a -> m Bool
p a
x
      if Bool
b then
        [a] -> (a -> m Bool) -> m Bool
forall (m :: * -> *) a. Monad m => [a] -> (a -> m Bool) -> m Bool
allM [a]
xs a -> m Bool
p
      else
        Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

record
  :: (GEq f, Hashable (Some f))
  => f a
  -> a
  -> DHashMap f g
  -> Traces f g
  -> Traces f g
record :: forall (f :: * -> *) a (g :: * -> *).
(GEq f, Hashable (Some f)) =>
f a -> a -> DHashMap f g -> Traces f g -> Traces f g
record f a
k a
v DHashMap f g
deps
  = f a
-> ValueDeps f g a
-> DHashMap f (ValueDeps f g)
-> DHashMap f (ValueDeps f g)
forall (k :: * -> *) a (v :: * -> *).
(GEq k, Hashable (Some k)) =>
k a -> v a -> DHashMap k v -> DHashMap k v
DHashMap.insert f a
k
  (ValueDeps f g a
 -> DHashMap f (ValueDeps f g) -> DHashMap f (ValueDeps f g))
-> ValueDeps f g a
-> DHashMap f (ValueDeps f g)
-> DHashMap f (ValueDeps f g)
forall a b. (a -> b) -> a -> b
$ a -> DHashMap f g -> ValueDeps f g a
forall (f :: * -> *) (dep :: * -> *) a.
a -> DHashMap f dep -> ValueDeps f dep a
ValueDeps a
v DHashMap f g
deps