{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Props.Internal.PropT
( Prop
, PropT
, newPVar
, constrain
, solveT
, solveAllT
, solve
, solveAll
, readPVar
, PVar
) where
import Props.Internal.Graph
import qualified Props.Internal.Props as P
import Control.Monad.State
import Control.Lens
import Data.Typeable
import Data.Dynamic
import Data.Maybe
type Prop a = PropT Identity a
newtype PropT m a =
PropT { runGraphM :: StateT Graph m a
}
deriving newtype (Functor, Applicative, Monad, MonadIO, MonadTrans)
data PVar (f :: * -> *) a where
PVar :: (Typeable a, Typeable f) => Vertex -> PVar f a
instance Eq (PVar f a) where
(PVar v) == (PVar t) = v == t
instance Ord (PVar f a) where
PVar v <= PVar t = v <= t
instance Show (PVar f a) where
show (PVar _) = unwords ["PVar", show (typeRep (Proxy @f)), show (typeRep (Proxy @a))]
newPVar :: (Monad m, Foldable f, Typeable f, Typeable a) => f a -> PropT m (PVar f a)
newPVar xs = PropT $ do
v <- vertexCount <+= 1
vertices . at v ?= (Quantum (Unknown xs), mempty)
return (PVar (Vertex v))
constrain :: Monad m
=> PVar f a
-> PVar g b
-> (a -> g b -> g b)
-> PropT m ()
constrain (PVar from') (PVar to') f = PropT $ do
edgeBetween from' to' ?= toDyn f
readPVar :: Graph -> PVar f a -> a
readPVar g (PVar v) =
fromMaybe (error "readPVar called on unsolved graph")
$ (g ^? valueAt v . folding unpackQuantum)
unpackQuantum :: (Typeable a) => Quantum -> Maybe a
unpackQuantum (Quantum (Observed xs)) = cast xs
unpackQuantum (Quantum _) = Nothing
buildGraph :: PropT m a -> m (a, Graph)
buildGraph = flip runStateT emptyGraph . runGraphM
solveT :: forall m a r.
Monad m
=> ((forall f x. PVar f x -> x) -> a -> r)
-> PropT m a
-> m (Maybe r)
solveT f m = do
(a, g) <- buildGraph m
case P.solve g of
Nothing -> return Nothing
Just solved -> return . Just $ f (readPVar solved) a
solveAllT :: forall m a r.
Monad m
=> ((forall f x. PVar f x -> x) -> a -> r)
-> PropT m a
-> m [r]
solveAllT f m = do
(a, g) <- buildGraph m
let gs = P.solveAll g
return $ gs <&> \g' -> f (readPVar g') a
solve :: forall a r.
((forall f x. PVar f x -> x) -> a -> r)
-> Prop a
-> (Maybe r)
solve f = runIdentity . solveT f
solveAll :: forall a r.
((forall f x. PVar f x -> x) -> a -> r)
-> Prop a
-> [r]
solveAll f = runIdentity . solveAllT f