{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BlockArguments #-}
module Dep.SimpleChecked (
CheckedEnv,
checkedDep,
getUnchecked,
checkEnv,
DepGraph (..),
SomeMonadConstraintRep (..),
monadConstraintRep,
mempty
) where
import Data.Functor.Compose
import Data.HashSet (HashSet)
import Data.HashSet qualified as HashSet
import Data.Hashable
import Data.Kind
import Data.Proxy
import Data.SOP (K (..))
import Data.SOP qualified as SOP
import Data.SOP.NP
import Dep.Has
import Dep.Dynamic
import Dep.Dynamic.Internal
import Dep.Env
import GHC.TypeLits
import Type.Reflection qualified as R
import Data.Functor
import Algebra.Graph
import qualified Algebra.Graph.Bipartite.AdjacencyMap as Bipartite
data CheckedEnv h m = CheckedEnv DepGraph (DynamicEnv (h `Compose` Constructor (DynamicEnv Identity m)) m)
checkedDep ::
forall r_ rs mcs h m.
( SOP.All R.Typeable rs,
SOP.All R.Typeable mcs,
R.Typeable r_,
R.Typeable h,
R.Typeable m,
HasAll rs m (DynamicEnv Identity m),
Monad m,
MonadSatisfiesAll mcs m
) =>
( forall e n.
( HasAll rs n e,
Monad m,
MonadSatisfiesAll mcs n
) =>
(h `Compose` Constructor e) (r_ n)
) ->
CheckedEnv h m ->
CheckedEnv h m
checkedDep :: forall (r_ :: (* -> *) -> *) (rs :: [(* -> *) -> *])
(mcs :: [(* -> *) -> Constraint]) (h :: * -> *) (m :: * -> *).
(All Typeable rs, All Typeable mcs, Typeable r_, Typeable h,
Typeable m, HasAll rs m (DynamicEnv Identity m), Monad m,
MonadSatisfiesAll mcs m) =>
(forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose h (Constructor e) (r_ n))
-> CheckedEnv h m -> CheckedEnv h m
checkedDep forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose h (Constructor e) (r_ n)
f (CheckedEnv DepGraph {HashSet SomeDepRep
provided :: DepGraph -> HashSet SomeDepRep
provided :: HashSet SomeDepRep
provided,HashSet SomeDepRep
required :: DepGraph -> HashSet SomeDepRep
required :: HashSet SomeDepRep
required,Graph SomeDepRep
depToDep :: DepGraph -> Graph SomeDepRep
depToDep :: Graph SomeDepRep
depToDep,AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad :: DepGraph -> AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad :: AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad} DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
de) =
let demoteDep :: forall (x :: (Type -> Type) -> Type). R.Typeable x => K SomeDepRep x
demoteDep :: forall (x :: (* -> *) -> *). Typeable x => K SomeDepRep x
demoteDep = forall k a (b :: k). a -> K a b
K (forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @x)
depReps :: [SomeDepRep]
depReps = forall {k} a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP @R.Typeable @rs forall {k} (t :: k). Proxy t
Proxy forall (x :: (* -> *) -> *). Typeable x => K SomeDepRep x
demoteDep
demoteMonadConstraint :: forall (x :: (Type -> Type) -> Constraint). R.Typeable x => K SomeMonadConstraintRep x
demoteMonadConstraint :: forall (x :: (* -> *) -> Constraint).
Typeable x =>
K SomeMonadConstraintRep x
demoteMonadConstraint = forall k a (b :: k). a -> K a b
K (forall (a :: (* -> *) -> Constraint).
TypeRep a -> SomeMonadConstraintRep
SomeMonadConstraintRep (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x))
monadConstraintReps :: [SomeMonadConstraintRep]
monadConstraintReps = forall {k} a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP @R.Typeable @mcs forall {k} (t :: k). Proxy t
Proxy forall (x :: (* -> *) -> Constraint).
Typeable x =>
K SomeMonadConstraintRep x
demoteMonadConstraint
provided' :: HashSet SomeDepRep
provided' = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_) HashSet SomeDepRep
provided
required' :: HashSet SomeDepRep
required' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert HashSet SomeDepRep
required [SomeDepRep]
depReps
depGraph' :: DepGraph
depGraph' = DepGraph {
provided :: HashSet SomeDepRep
provided = HashSet SomeDepRep
provided'
, required :: HashSet SomeDepRep
required = HashSet SomeDepRep
required'
, depToDep :: Graph SomeDepRep
depToDep = forall a. Graph a -> Graph a -> Graph a
overlay Graph SomeDepRep
depToDep forall a b. (a -> b) -> a -> b
$ forall a. [(a, a)] -> Graph a
edges forall a b. (a -> b) -> a -> b
$ (forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeDepRep]
depReps
, depToMonad :: AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad = forall a b.
(Ord a, Ord b) =>
AdjacencyMap a b -> AdjacencyMap a b -> AdjacencyMap a b
Bipartite.overlay AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad forall a b. (a -> b) -> a -> b
$ forall a b. (Ord a, Ord b) => [(a, b)] -> AdjacencyMap a b
Bipartite.edges forall a b. (a -> b) -> a -> b
$ (forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeMonadConstraintRep]
monadConstraintReps
}
in forall (h :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv h m
CheckedEnv DepGraph
depGraph' (forall (r_ :: (* -> *) -> *) (h :: * -> *) (m :: * -> *).
(Typeable r_, Typeable h, Typeable m) =>
h (r_ m) -> DynamicEnv h m -> DynamicEnv h m
insertDep (forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose h (Constructor e) (r_ n)
f @(DynamicEnv Identity m) @m) DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
de)
instance Semigroup (CheckedEnv h m) where
CheckedEnv DepGraph
g1 DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
env1 <> :: CheckedEnv h m -> CheckedEnv h m -> CheckedEnv h m
<> CheckedEnv DepGraph
g2 DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
env2 = forall (h :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv h m
CheckedEnv (DepGraph
g1 forall a. Semigroup a => a -> a -> a
<> DepGraph
g2) (DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
env1 forall a. Semigroup a => a -> a -> a
<> DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
env2)
instance Monoid (CheckedEnv h m) where
mempty :: CheckedEnv h m
mempty = forall (h :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv h m
CheckedEnv forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
getUnchecked :: CheckedEnv h m -> (DepGraph, DynamicEnv (h `Compose` Constructor (DynamicEnv Identity m)) m)
getUnchecked :: forall (h :: * -> *) (m :: * -> *).
CheckedEnv h m
-> (DepGraph,
DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m)
getUnchecked (CheckedEnv DepGraph
g DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
d) = (DepGraph
g, DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
d)
checkEnv :: CheckedEnv h m -> Either (HashSet SomeDepRep) (DepGraph, DynamicEnv (h `Compose` Constructor (DynamicEnv Identity m)) m)
checkEnv :: forall (h :: * -> *) (m :: * -> *).
CheckedEnv h m
-> Either
(HashSet SomeDepRep)
(DepGraph,
DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m)
checkEnv (CheckedEnv g :: DepGraph
g@DepGraph {HashSet SomeDepRep
required :: HashSet SomeDepRep
required :: DepGraph -> HashSet SomeDepRep
required,HashSet SomeDepRep
provided :: HashSet SomeDepRep
provided :: DepGraph -> HashSet SomeDepRep
provided} DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
d) =
let missing :: HashSet SomeDepRep
missing = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference HashSet SomeDepRep
required HashSet SomeDepRep
provided
in if forall a. HashSet a -> Bool
HashSet.null HashSet SomeDepRep
missing
then forall a b. b -> Either a b
Right (DepGraph
g, DynamicEnv (Compose h (Constructor (DynamicEnv Identity m))) m
d)
else forall a b. a -> Either a b
Left HashSet SomeDepRep
missing