PropT.hs

{-# 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

-- | Pure version of 'PropT'
type Prop a = PropT Identity a


{-|
A monad transformer for setting up constraint problems.
-}
newtype PropT m a =
    PropT { runGraphM :: StateT Graph m a
           }
    deriving newtype (Functor, Applicative, Monad, MonadIO, MonadTrans)

{-|
A propagator variable where the possible values @a@ are contained in the container @f@.
-}
data PVar (f :: * -> *) a where
  PVar :: (Typeable a, Typeable f) => Vertex -> PVar f a

-- | Nominal equality, Ignores contents
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))]

{-|
Used to create a new propagator variable within the setup for your problem.

@f@ is any Foldable container which contains each of the possible states which the variable could take.

E.g. For a sudoku solver you would use 'newPVar' to create a variable for each cell, passing a @Set Int@ containing the numbers @[1..9]@.
-}
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' the relationship between two 'PVar's. Note that this is a ONE WAY relationship; e.g. @constrain a b f@ will propagate constraints from @a@ to @b@ but not vice versa.

Given @PVar f a@ and @PVar g b@ as arguments, provide a function which will filter/alter the options in @g@ according to the choice.

For a sudoku puzzle you'd have two @Pvar Set Int@'s, each representing a cell on the board.
You can constrain @b@ to be a different value than @a@ with the following call:

> constrain a b $ \elementA setB -> S.delete elementA setB)

Take a look at some linking functions which are already provided: 'disjoint', 'equal', 'require'
-}
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

{-|
Provide an initialization action which constrains the problem, and a finalizer, and 'solveT' will return a result if one exists.

The finalizer is an annoyance caused by the fact that GHC does not yet support Impredicative Types.

For example, if you wrote a solution to the nQueens problem, you might run it like so:

> -- Set up the problem for 'n' queens and return their PVar's as a list.
> initNQueens :: Int -> Prop [PVar S.Set Coord]
> initNQueens = ...
>
> solution :: [Coord]
> solution = solve (\readPVar vars -> fmap readPVar vars) (initNQueens 8)
> -- or more simply:
> solution = solve fmap (initNQueens 8)
which converts 'PVar's into a result.Given an action which initializes and constrains a problem 'solveT' will  and returns some container of 'PVar's, 'solveT' will attempt to find a solution which passes all valid constraints.
-}
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


{-|
Like 'solveT', but finds ALL possible solutions. There will likely be duplicates.
-}
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

{-|
Pure version of 'solveT'
-}
solve :: forall a r.
        ((forall f x. PVar f x -> x) -> a -> r)
      -> Prop a
      -> (Maybe r)
solve f = runIdentity . solveT f

{-|
Pure version of 'solveAllT'
-}
solveAll :: forall a r.
            ((forall f x. PVar f x -> x) -> a -> r)
          -> Prop a
          -> [r]
solveAll f = runIdentity . solveAllT f