module UniqueLogic.ST.Example.Verify
{-# 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.System as Sys
import qualified UniqueLogic.ST.Duplicate as Duplicate
import qualified UniqueLogic.ST.MonadTrans as UMT
import UniqueLogic.ST.Expression ((=:=))

import qualified Control.Monad.Exception.Synchronous as ME
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.Trans.Maybe (MaybeT, mapMaybeT, )
import Control.Monad.ST (ST, runST, )
import Control.Monad (liftM, liftM2, ap, )
import Control.Applicative (Applicative, pure, (<*>), )

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]

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

tn1 :: (Term.T -> Term.T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b
tn1 :: forall a b.
(T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b
tn1 T -> T
f a -> b
g (TrackedNumber T
xt a
xn) = forall a. T -> a -> TrackedNumber a
TrackedNumber (T -> T
f T
xt) (a -> b
g a
xn)

tn2 :: (Term.T -> Term.T -> Term.T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c
tn2 :: forall a b c.
(T -> T -> T)
-> (a -> b -> c)
-> TrackedNumber a
-> TrackedNumber b
-> TrackedNumber c
tn2 T -> T -> T
f a -> b -> c
g (TrackedNumber T
xt a
xn) (TrackedNumber T
yt b
yn) =
   forall a. T -> a -> TrackedNumber a
TrackedNumber (T -> T -> T
f T
xt T
yt) (a -> b -> c
g a
xn b
yn)

instance Num a => Num (TrackedNumber a) where
   fromInteger :: Integer -> TrackedNumber a
fromInteger Integer
n = forall a. T -> a -> TrackedNumber a
TrackedNumber (forall a. Num a => Integer -> a
fromInteger Integer
n) (forall a. Num a => Integer -> a
fromInteger Integer
n)
   + :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a
(+) = forall a b c.
(T -> T -> T)
-> (a -> b -> c)
-> TrackedNumber a
-> TrackedNumber b
-> TrackedNumber c
tn2 forall a. Num a => a -> a -> a
(+) forall a. Num a => a -> a -> a
(+)
   (-) = forall a b c.
(T -> T -> T)
-> (a -> b -> c)
-> TrackedNumber a
-> TrackedNumber b
-> TrackedNumber c
tn2 (-) (-)
   * :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a
(*) = forall a b c.
(T -> T -> T)
-> (a -> b -> c)
-> TrackedNumber a
-> TrackedNumber b
-> TrackedNumber c
tn2 forall a. Num a => a -> a -> a
(*) forall a. Num a => a -> a -> a
(*)
   abs :: TrackedNumber a -> TrackedNumber a
abs = forall a b.
(T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b
tn1 forall a. Num a => a -> a
abs forall a. Num a => a -> a
abs
   signum :: TrackedNumber a -> TrackedNumber a
signum = forall a b.
(T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b
tn1 forall a. Num a => a -> a
signum forall a. Num a => a -> a
signum

instance Fractional a => Fractional (TrackedNumber a) where
   fromRational :: Rational -> TrackedNumber a
fromRational Rational
n = forall a. T -> a -> TrackedNumber a
TrackedNumber (forall a. Fractional a => Rational -> a
fromRational Rational
n) (forall a. Fractional a => Rational -> a
fromRational Rational
n)
   / :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a
(/) = forall a b c.
(T -> T -> T)
-> (a -> b -> c)
-> TrackedNumber a
-> TrackedNumber b
-> TrackedNumber c
tn2 forall a. Fractional a => a -> a -> a
(/) forall a. Fractional a => a -> a -> a
(/)

instance Eq a => Duplicate.C (TrackedNumber a) where
   accept :: TrackedNumber a -> TrackedNumber a -> Bool
accept (TrackedNumber T
_ a
x) (TrackedNumber T
_ a
y)  =  a
xforall a. Eq a => a -> a -> Bool
==a
y


instance (Monad m) => Functor (Track m) where
   fmap :: forall a b. (a -> b) -> Track m a -> Track m b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance (Monad m) => Applicative (Track m) where
   pure :: forall a. a -> Track m a
pure = forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(C t, Monad m) =>
a -> t m a
UMT.point
   <*> :: forall a b. Track m (a -> b) -> Track m a -> Track m b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Monad m) => Monad (Track m) where
   return :: forall a. a -> Track m a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
   Track m a
x >>= :: forall a b. Track m a -> (a -> Track m b) -> Track m b
>>= a -> Track m b
k  =  forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(C t, Monad m) =>
t m a -> (a -> t m b) -> t m b
UMT.bind (forall (m :: * -> *) a.
Track m a -> ExceptionalT Exception (WriterT [Assign] m) a
runTrack Track m a
x) (forall (m :: * -> *) a.
Track m a -> ExceptionalT Exception (WriterT [Assign] m) a
runTrack forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Track m b
k)


instance MT.MonadTrans Track where
   lift :: forall (m :: * -> *) a. Monad m => m a -> Track m a
lift = forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift

instance UMT.C Track where
   point :: forall (m :: * -> *) a. Monad m => a -> Track m a
point = forall (m :: * -> *) a. Monad m => a -> m a
return
   bind :: forall (m :: * -> *) a b.
Monad m =>
Track m a -> (a -> Track m b) -> Track m b
bind = forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(>>=)

instance Sys.C Track where
   doUpdate :: forall a s. C a => Updater Track s a
doUpdate =
      forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
(a -> a -> Wrap w (ST s) ()) -> Updater w s a
Sys.updateAndCheck forall a b. (a -> b) -> a -> b
$ \a
_ a
_ ->
         forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
t m a -> Wrap t m a
UMT.wrap forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a. Monad m => e -> ExceptionalT e m a
ME.throwT Exception
AnonymousException


newtype
   Track m a =
      Track {forall (m :: * -> *) a.
Track m a -> ExceptionalT Exception (WriterT [Assign] m) a
runTrack :: ME.ExceptionalT Exception (MW.WriterT Assigns m) a}

data
   Exception =
        Exception Term.Name (TrackedNumber Rational) (TrackedNumber Rational)
      | AnonymousException
   deriving (Int -> Exception -> ShowS
[Exception] -> ShowS
Exception -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exception] -> ShowS
$cshowList :: [Exception] -> ShowS
show :: Exception -> String
$cshow :: Exception -> String
showsPrec :: Int -> Exception -> ShowS
$cshowsPrec :: Int -> Exception -> ShowS
Show)

type Variable s = Sys.Variable Track s (TrackedNumber Rational)

globalVariable :: Term.Name -> ST s (Variable s)
globalVariable :: forall s. String -> ST s (Variable s)
globalVariable String
name =
   forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
SimpleUpdater w s a -> ST s (Variable w s a)
Sys.globalVariable
      (\STRef s [Update Track s]
al STRef s (Maybe (TrackedNumber Rational))
av -> forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
(a -> a -> Wrap w (ST s) ()) -> Updater w s a
Sys.updateAndCheck (forall (m :: * -> *).
Monad m =>
String
-> TrackedNumber Rational
-> TrackedNumber Rational
-> Wrap Track m ()
inconsistency String
name) STRef s [Update Track s]
al STRef s (Maybe (TrackedNumber Rational))
av forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a.
String
-> MaybeT (ST s) (TrackedNumber a)
-> MaybeT (Wrap Track (ST s)) (TrackedNumber a)
update String
name)

inconsistency ::
   Monad m =>
   Term.Name ->
   TrackedNumber Rational ->
   TrackedNumber Rational ->
   UMT.Wrap Track m ()
inconsistency :: forall (m :: * -> *).
Monad m =>
String
-> TrackedNumber Rational
-> TrackedNumber Rational
-> Wrap Track m ()
inconsistency String
name TrackedNumber Rational
old TrackedNumber Rational
new =
   forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
t m a -> Wrap t m a
UMT.wrap forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a. Monad m => e -> ExceptionalT e m a
ME.throwT forall a b. (a -> b) -> a -> b
$ String
-> TrackedNumber Rational -> TrackedNumber Rational -> Exception
Exception String
name TrackedNumber Rational
old TrackedNumber Rational
new

update ::
   Term.Name ->
   MaybeT (ST s) (TrackedNumber a) ->
   MaybeT (UMT.Wrap Track (ST s)) (TrackedNumber a)
update :: forall s a.
String
-> MaybeT (ST s) (TrackedNumber a)
-> MaybeT (Wrap Track (ST s)) (TrackedNumber a)
update String
name MaybeT (ST s) (TrackedNumber a)
act = do
   (TrackedNumber T
t a
x) <- forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b
mapMaybeT forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(C t, Monad m) =>
m a -> Wrap t m a
UMT.lift MaybeT (ST s) (TrackedNumber a)
act
   forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
t m a -> Wrap t m a
UMT.wrap forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
ExceptionalT Exception (WriterT [Assign] m) a -> Track m a
Track forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
MT.lift forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a w. Monad m => (a, w) -> WriterT w m a
writer (forall a. T -> a -> TrackedNumber a
TrackedNumber (String -> T
Term.Var String
name) a
x, [String -> T -> Assign
Assign String
name T
t])


example ::
   (ME.Exceptional Exception
       (Maybe (TrackedNumber Rational),
        Maybe (TrackedNumber Rational)),
    Assigns)
example :: (Exceptional
   Exception
   (Maybe (TrackedNumber Rational), Maybe (TrackedNumber Rational)),
 [Assign])
example =
   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
$ forall e (m :: * -> *) a. ExceptionalT e m a -> m (Exceptional e a)
ME.runExceptionalT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Track m a -> ExceptionalT Exception (WriterT [Assign] m) a
runTrack 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 Track s (TrackedNumber Rational)
x = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a
Expr.fromVariable Variable s
xv
                y :: T Track s (TrackedNumber Rational)
y = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a
Expr.fromVariable Variable s
yv
            T Track s (TrackedNumber Rational)
xforall a. Num a => a -> a -> a
*T Track s (TrackedNumber Rational)
3 forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s ()
=:= T Track s (TrackedNumber Rational)
yforall a. Fractional a => a -> a -> a
/T Track s (TrackedNumber Rational)
2
            T Track s (TrackedNumber Rational)
5 forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s ()
=:= T Track s (TrackedNumber Rational)
2forall a. Num a => a -> a -> a
+T Track s (TrackedNumber Rational)
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 a -> ST s (Maybe a)
Sys.query Variable s
xv)
            (forall (w :: (* -> *) -> * -> *) s a.
Variable w s a -> ST s (Maybe a)
Sys.query Variable s
yv))