module UniqueLogic.ST.Example.Label
{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
 where

import qualified UniqueLogic.ST.Example.Term as Term
import qualified UniqueLogic.ST.Expression as Expr
import qualified UniqueLogic.ST.Rule as Rule
import qualified UniqueLogic.ST.System.Label as Sys
import qualified UniqueLogic.ST.Duplicate as Duplicate
import UniqueLogic.ST.Expression ((=:=))

import qualified Control.Monad.Trans.Writer as MW
import qualified Control.Monad.Trans.Class as MT
import Control.Monad.Trans.Writer (writer, )
import Control.Monad.ST (ST, runST, )
import Control.Monad (liftM2, liftM3, )

import qualified Prelude as P
import Prelude hiding (max, log)



data Assign = Assign Term.Name Term.T
   deriving (Int -> Assign -> ShowS
[Assign] -> ShowS
Assign -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Assign] -> ShowS
$cshowList :: [Assign] -> ShowS
show :: Assign -> String
$cshow :: Assign -> String
showsPrec :: Int -> Assign -> ShowS
$cshowsPrec :: Int -> Assign -> ShowS
Show)

type Assigns = [Assign]

type Variable s = Sys.Variable Assigns s (Duplicate.Ignore Term.T)

globalVariable :: Term.Name -> ST s (Variable s)
globalVariable :: forall s. String -> ST s (Variable s)
globalVariable String
name =
   forall w a s.
(Monoid w, C a) =>
(a -> Writer w a) -> ST s (Variable w s a)
Sys.globalVariable forall a b. (a -> b) -> a -> b
$
      \(Duplicate.Ignore T
x) ->
         forall (m :: * -> *) a w. Monad m => (a, w) -> WriterT w m a
writer (forall a. a -> Ignore a
Duplicate.Ignore forall a b. (a -> b) -> a -> b
$ String -> T
Term.Var String
name, [String -> T -> Assign
Assign String
name T
x])

constant :: Rational -> Sys.T Assigns s (Variable s)
constant :: forall s. Rational -> T [Assign] s (Variable s)
constant = forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
a -> T w s (Variable w s a)
Sys.constant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational


{- |
> x=1
> y=2
> z=3

> x+y=3
> y*z=6
> z=3
-}
rule :: ((Maybe Term.T, Maybe Term.T, Maybe Term.T), Assigns)
rule :: ((Maybe T, Maybe T, Maybe T), [Assign])
rule =
   forall a. (forall s. ST s a) -> a
runST (do
      Variable s
x <- forall s. String -> ST s (Variable s)
globalVariable String
"x"
      Variable s
y <- forall s. String -> ST s (Variable s)
globalVariable String
"y"
      Variable s
z <- forall s. String -> ST s (Variable s)
globalVariable String
"z"
      forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
MW.runWriterT forall a b. (a -> b) -> a -> b
$ do
         forall (w :: (* -> *) -> * -> *) s a. C w => T w s a -> w (ST s) a
Sys.solve forall a b. (a -> b) -> a -> b
$ do
            Variable s
c3 <- forall s. Rational -> T [Assign] s (Variable s)
constant Rational
3
            Variable s
c6 <- forall s. Rational -> T [Assign] s (Variable s)
constant Rational
6
            forall a (w :: (* -> *) -> * -> *) s.
(Num a, C w) =>
Variable w s a -> Variable w s a -> Variable w s a -> T w s ()
Rule.add Variable s
x Variable s
y Variable s
c3
            forall a (w :: (* -> *) -> * -> *) s.
(Fractional a, C w) =>
Variable w s a -> Variable w s a -> Variable w s a -> T w s ()
Rule.mul Variable s
y Variable s
z Variable s
c6
            forall (w :: (* -> *) -> * -> *) s a.
C w =>
Variable w s a -> Variable w s a -> T w s ()
Rule.equ Variable s
z Variable s
c3
         forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3
            (,,)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s (Ignore a) -> ST s (Maybe a)
Sys.queryIgnore Variable s
x)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s (Ignore a) -> ST s (Maybe a)
Sys.queryIgnore Variable s
y)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s (Ignore a) -> ST s (Maybe a)
Sys.queryIgnore Variable s
z))

expression :: ((Maybe Term.T, Maybe Term.T), Assigns)
expression :: ((Maybe T, Maybe T), [Assign])
expression =
   forall a. (forall s. ST s a) -> a
runST (do
      Variable s
xv <- forall s. String -> ST s (Variable s)
globalVariable String
"x"
      Variable s
yv <- forall s. String -> ST s (Variable s)
globalVariable String
"y"
      forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
MW.runWriterT forall a b. (a -> b) -> a -> b
$ do
         forall (w :: (* -> *) -> * -> *) s a. C w => T w s a -> w (ST s) a
Sys.solve forall a b. (a -> b) -> a -> b
$ do
            let x :: T (WriterT [Assign]) s (Ignore T)
x = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a
Expr.fromVariable Variable s
xv
                y :: T (WriterT [Assign]) s (Ignore T)
y = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a
Expr.fromVariable Variable s
yv
            T (WriterT [Assign]) s (Ignore T)
xforall a. Num a => a -> a -> a
*T (WriterT [Assign]) s (Ignore T)
3 forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s ()
=:= T (WriterT [Assign]) s (Ignore T)
yforall a. Fractional a => a -> a -> a
/T (WriterT [Assign]) s (Ignore T)
2
            T (WriterT [Assign]) s (Ignore T)
5 forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s ()
=:= T (WriterT [Assign]) s (Ignore T)
2forall a. Num a => a -> a -> a
+T (WriterT [Assign]) s (Ignore T)
x
         forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s (Ignore a) -> ST s (Maybe a)
Sys.queryIgnore Variable s
xv)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s (Ignore a) -> ST s (Maybe a)
Sys.queryIgnore Variable s
yv))