module UniqueLogic.ST.System.Label (
   -- * Preparation
   Variable,
   globalVariable,
   -- * Posing statements
   T,
   Sys.localVariable,
   Sys.constant,
   Sys.assignment2,
   Sys.assignment3,
   Sys.Apply, Sys.arg, Sys.runApply,
   -- * Solution
   Sys.solve,
   Sys.query,
   Sys.queryForbid,
   Sys.queryIgnore,
   Sys.queryVerify,
   ) where

import qualified UniqueLogic.ST.System as Sys
import qualified UniqueLogic.ST.MonadTrans as UMT
import qualified UniqueLogic.ST.Duplicate as Duplicate

import qualified Control.Monad.Trans.Writer as MW
import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT, )
import Control.Monad.ST (ST, )

import Data.Monoid (Monoid, )
import Data.Traversable (traverse, )

import Prelude hiding (log, )


type T w = Sys.T (MW.WriterT w)
type Variable w = Sys.Variable (MW.WriterT w)

globalVariable ::
   (Monoid w, Duplicate.C a) =>
   (a -> MW.Writer w a) -> ST s (Variable w s a)
globalVariable :: forall w a s.
(Monoid w, C a) =>
(a -> Writer w a) -> ST s (Variable w s a)
globalVariable a -> Writer w a
log =
   forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
SimpleUpdater w s a -> ST s (Variable w s a)
Sys.globalVariable
      (\STRef s [Update (WriterT w) s]
al STRef s (Maybe a)
av -> forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => Updater w s a
Sys.updateIfNew STRef s [Update (WriterT w) s]
al STRef s (Maybe a)
av forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w a b s.
Monoid w =>
(a -> Writer w b)
-> MaybeT (ST s) a -> MaybeT (Wrap (WriterT w) (ST s)) b
wrap a -> Writer w a
log)

wrap ::
   (Monoid w) =>
   (a -> MW.Writer w b) ->
   MaybeT (ST s) a -> MaybeT (UMT.Wrap (MW.WriterT w) (ST s)) b
wrap :: forall w a b s.
Monoid w =>
(a -> Writer w b)
-> MaybeT (ST s) a -> MaybeT (Wrap (WriterT w) (ST s)) b
wrap a -> Writer w b
log =
   forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b
mapMaybeT forall a b. (a -> b) -> a -> b
$
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
t m a -> Wrap t m a
UMT.wrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
MW.WriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall w a. Writer w a -> (a, w)
MW.runWriter forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> Writer w b
log)
--      UMT.wrap . MW.writer . MW.runWriter . traverse log <=< UMT.lift