{-# 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.Undirected.AdjacencyMap as Bipartite
data CheckedEnv phases m = CheckedEnv DepGraph (DynamicEnv (phases `Compose` Constructor (DynamicEnv Identity m)) m)
checkedDep ::
forall r_ rs mcs phases m.
( SOP.All R.Typeable rs,
SOP.All R.Typeable mcs,
R.Typeable r_,
R.Typeable phases,
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
) =>
(phases `Compose` Constructor e) (r_ n)
) ->
CheckedEnv phases m ->
CheckedEnv phases m
checkedDep :: (forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose phases (Constructor e) (r_ n))
-> CheckedEnv phases m -> CheckedEnv phases m
checkedDep forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose phases (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 phases (Constructor (DynamicEnv Identity m))) m
de) =
let demoteDep :: forall (x :: (Type -> Type) -> Type). R.Typeable x => K SomeDepRep x
demoteDep :: K SomeDepRep x
demoteDep = SomeDepRep -> K SomeDepRep x
forall k a (b :: k). a -> K a b
K (Typeable x => SomeDepRep
forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @x)
depReps :: [SomeDepRep]
depReps = NP (K SomeDepRep) rs -> [SomeDepRep]
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP (NP (K SomeDepRep) rs -> [SomeDepRep])
-> NP (K SomeDepRep) rs -> [SomeDepRep]
forall a b. (a -> b) -> a -> b
$ Proxy Typeable
-> (forall (a :: (* -> *) -> *). Typeable a => K SomeDepRep a)
-> NP (K SomeDepRep) rs
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 Proxy Typeable
forall k (t :: k). Proxy t
Proxy forall (a :: (* -> *) -> *). Typeable a => K SomeDepRep a
demoteDep
demoteMonadConstraint :: forall (x :: (Type -> Type) -> Constraint). R.Typeable x => K SomeMonadConstraintRep x
demoteMonadConstraint :: K SomeMonadConstraintRep x
demoteMonadConstraint = SomeMonadConstraintRep -> K SomeMonadConstraintRep x
forall k a (b :: k). a -> K a b
K (TypeRep x -> SomeMonadConstraintRep
forall (a :: (* -> *) -> Constraint).
TypeRep a -> SomeMonadConstraintRep
SomeMonadConstraintRep (Typeable x => TypeRep x
forall k (a :: k). Typeable a => TypeRep a
R.typeRep @x))
monadConstraintReps :: [SomeMonadConstraintRep]
monadConstraintReps = NP (K SomeMonadConstraintRep) mcs -> [SomeMonadConstraintRep]
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP (NP (K SomeMonadConstraintRep) mcs -> [SomeMonadConstraintRep])
-> NP (K SomeMonadConstraintRep) mcs -> [SomeMonadConstraintRep]
forall a b. (a -> b) -> a -> b
$ Proxy Typeable
-> (forall (a :: (* -> *) -> Constraint).
Typeable a =>
K SomeMonadConstraintRep a)
-> NP (K SomeMonadConstraintRep) mcs
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 Proxy Typeable
forall k (t :: k). Proxy t
Proxy forall (a :: (* -> *) -> Constraint).
Typeable a =>
K SomeMonadConstraintRep a
demoteMonadConstraint
provided' :: HashSet SomeDepRep
provided' = SomeDepRep -> HashSet SomeDepRep -> HashSet SomeDepRep
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (Typeable r_ => SomeDepRep
forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_) HashSet SomeDepRep
provided
required' :: HashSet SomeDepRep
required' = (SomeDepRep -> HashSet SomeDepRep -> HashSet SomeDepRep)
-> HashSet SomeDepRep -> [SomeDepRep] -> HashSet SomeDepRep
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SomeDepRep -> HashSet SomeDepRep -> HashSet SomeDepRep
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert HashSet SomeDepRep
required [SomeDepRep]
depReps
depGraph' :: DepGraph
depGraph' = DepGraph :: HashSet SomeDepRep
-> HashSet SomeDepRep
-> Graph SomeDepRep
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
-> DepGraph
DepGraph {
provided :: HashSet SomeDepRep
provided = HashSet SomeDepRep
provided'
, required :: HashSet SomeDepRep
required = HashSet SomeDepRep
required'
, depToDep :: Graph SomeDepRep
depToDep = Graph SomeDepRep -> Graph SomeDepRep -> Graph SomeDepRep
forall a. Graph a -> Graph a -> Graph a
overlay Graph SomeDepRep
depToDep (Graph SomeDepRep -> Graph SomeDepRep)
-> Graph SomeDepRep -> Graph SomeDepRep
forall a b. (a -> b) -> a -> b
$ [(SomeDepRep, SomeDepRep)] -> Graph SomeDepRep
forall a. [(a, a)] -> Graph a
edges ([(SomeDepRep, SomeDepRep)] -> Graph SomeDepRep)
-> [(SomeDepRep, SomeDepRep)] -> Graph SomeDepRep
forall a b. (a -> b) -> a -> b
$ (Typeable r_ => SomeDepRep
forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_,) (SomeDepRep -> (SomeDepRep, SomeDepRep))
-> [SomeDepRep] -> [(SomeDepRep, SomeDepRep)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeDepRep]
depReps
, depToMonad :: AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad = AdjacencyMap SomeDepRep SomeMonadConstraintRep
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
forall a b.
(Ord a, Ord b) =>
AdjacencyMap a b -> AdjacencyMap a b -> AdjacencyMap a b
Bipartite.overlay AdjacencyMap SomeDepRep SomeMonadConstraintRep
depToMonad (AdjacencyMap SomeDepRep SomeMonadConstraintRep
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep)
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
forall a b. (a -> b) -> a -> b
$ [(SomeDepRep, SomeMonadConstraintRep)]
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
forall a b. (Ord a, Ord b) => [(a, b)] -> AdjacencyMap a b
Bipartite.edges ([(SomeDepRep, SomeMonadConstraintRep)]
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep)
-> [(SomeDepRep, SomeMonadConstraintRep)]
-> AdjacencyMap SomeDepRep SomeMonadConstraintRep
forall a b. (a -> b) -> a -> b
$ (Typeable r_ => SomeDepRep
forall (r_ :: (* -> *) -> *). Typeable r_ => SomeDepRep
depRep @r_,) (SomeMonadConstraintRep -> (SomeDepRep, SomeMonadConstraintRep))
-> [SomeMonadConstraintRep]
-> [(SomeDepRep, SomeMonadConstraintRep)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeMonadConstraintRep]
monadConstraintReps
}
in DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
forall (phases :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
CheckedEnv DepGraph
depGraph' (Compose phases (Constructor (DynamicEnv Identity m)) (r_ m)
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
forall (r_ :: (* -> *) -> *) (h :: * -> *) (m :: * -> *).
(Typeable r_, Typeable h, Typeable m) =>
h (r_ m) -> DynamicEnv h m -> DynamicEnv h m
insertDep ((HasAll rs m (DynamicEnv Identity m), Monad m,
MonadSatisfiesAll mcs m) =>
Compose phases (Constructor (DynamicEnv Identity m)) (r_ m)
forall e (n :: * -> *).
(HasAll rs n e, Monad m, MonadSatisfiesAll mcs n) =>
Compose phases (Constructor e) (r_ n)
f @(DynamicEnv Identity m) @m) DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
de)
instance Semigroup (CheckedEnv phases m) where
CheckedEnv DepGraph
g1 DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
env1 <> :: CheckedEnv phases m -> CheckedEnv phases m -> CheckedEnv phases m
<> CheckedEnv DepGraph
g2 DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
env2 = DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
forall (phases :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
CheckedEnv (DepGraph
g1 DepGraph -> DepGraph -> DepGraph
forall a. Semigroup a => a -> a -> a
<> DepGraph
g2) (DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
env1 DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
forall a. Semigroup a => a -> a -> a
<> DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
env2)
instance Monoid (CheckedEnv phases m) where
mempty :: CheckedEnv phases m
mempty = DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
forall (phases :: * -> *) (m :: * -> *).
DepGraph
-> DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m
-> CheckedEnv phases m
CheckedEnv DepGraph
forall a. Monoid a => a
mempty DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
forall a. Monoid a => a
mempty
getUnchecked :: CheckedEnv phases m -> (DepGraph, DynamicEnv (phases `Compose` Constructor (DynamicEnv Identity m)) m)
getUnchecked :: CheckedEnv phases m
-> (DepGraph,
DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m)
getUnchecked (CheckedEnv DepGraph
g DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
d) = (DepGraph
g, DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
d)
checkEnv :: CheckedEnv phases m -> Either (HashSet SomeDepRep) (DepGraph, DynamicEnv (phases `Compose` Constructor (DynamicEnv Identity m)) m)
checkEnv :: CheckedEnv phases m
-> Either
(HashSet SomeDepRep)
(DepGraph,
DynamicEnv
(Compose phases (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 phases (Constructor (DynamicEnv Identity m))) m
d) =
let missing :: HashSet SomeDepRep
missing = HashSet SomeDepRep -> HashSet SomeDepRep -> HashSet SomeDepRep
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference HashSet SomeDepRep
required HashSet SomeDepRep
provided
in if HashSet SomeDepRep -> Bool
forall a. HashSet a -> Bool
HashSet.null HashSet SomeDepRep
missing
then (DepGraph,
DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m)
-> Either
(HashSet SomeDepRep)
(DepGraph,
DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m)
forall a b. b -> Either a b
Right (DepGraph
g, DynamicEnv (Compose phases (Constructor (DynamicEnv Identity m))) m
d)
else HashSet SomeDepRep
-> Either
(HashSet SomeDepRep)
(DepGraph,
DynamicEnv
(Compose phases (Constructor (DynamicEnv Identity m))) m)
forall a b. a -> Either a b
Left HashSet SomeDepRep
missing