module UniqueLogic.ST.Expression (
   T,
   -- * Construct primitive expressions
   constant, fromVariable,
   -- * Operators from rules with small numbers of arguments
   fromRule1, fromRule2, fromRule3,
   -- * Operators from rules with any number of arguments
   Apply, arg, runApply,
   -- * Predicates on expressions
   (=:=),
   -- * Common operators (see also 'Num' and 'Fractional' instances)
   (=!=),
   sqr, sqrt,
   max, maximum,
   pair,
   ) where

import qualified UniqueLogic.ST.Rule as Rule
import qualified UniqueLogic.ST.System as Sys
import qualified UniqueLogic.ST.Duplicate as Duplicate

import Control.Monad (ap, )
import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )

-- import Control.Category ((.))
-- import Data.Maybe (Maybe)

-- import Prelude (Double, Eq, Ord, (+), (*), (/))
import qualified Prelude as P
import Prelude hiding (max, maximum, sqrt)


{- |
An expression is defined by a set of equations
and the variable at the top-level.
The value of the expression equals the value of the top variable.
-}
newtype T w s a = Cons (Sys.T w s (Sys.Variable w s a))


{- |
Make a constant expression of a simple numeric value.
-}
constant :: (Sys.C w, Duplicate.C a) => a -> T w s a
constant :: forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => a -> T w s a
constant = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
a -> T w s (Variable w s a)
Sys.constant

fromVariable :: Sys.Variable w s a -> T w s a
fromVariable :: forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a
fromVariable = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return


fromRule1 ::
   (Sys.C w, Duplicate.C a) =>
   (Sys.Variable w s a -> Sys.T w s ()) ->
   (T w s a)
fromRule1 :: forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
(Variable w s a -> T w s ()) -> T w s a
fromRule1 Variable w s a -> T w s ()
rule = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall a b. (a -> b) -> a -> b
$ do
   Variable w s a
xv <- forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
T w s (Variable w s a)
Sys.localVariable
   Variable w s a -> T w s ()
rule Variable w s a
xv
   forall (m :: * -> *) a. Monad m => a -> m a
return Variable w s a
xv

fromRule2, _fromRule2 ::
   (Sys.C w, Duplicate.C b) =>
   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()) ->
   (T w s a -> T w s b)
fromRule2 :: forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
fromRule2 Variable w s a -> Variable w s b -> T w s ()
rule (Cons T w s (Variable w s a)
x) = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall a b. (a -> b) -> a -> b
$ do
   Variable w s a
xv <- T w s (Variable w s a)
x
   Variable w s b
yv <- forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
T w s (Variable w s a)
Sys.localVariable
   Variable w s a -> Variable w s b -> T w s ()
rule Variable w s a
xv Variable w s b
yv
   forall (m :: * -> *) a. Monad m => a -> m a
return Variable w s b
yv

fromRule3, _fromRule3 ::
   (Sys.C w, Duplicate.C c) =>
   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()) ->
   (T w s a -> T w s b -> T w s c)
fromRule3 :: forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 Variable w s a -> Variable w s b -> Variable w s c -> T w s ()
rule (Cons T w s (Variable w s a)
x) (Cons T w s (Variable w s b)
y) = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall a b. (a -> b) -> a -> b
$ do
   Variable w s a
xv <- T w s (Variable w s a)
x
   Variable w s b
yv <- T w s (Variable w s b)
y
   Variable w s c
zv <- forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
T w s (Variable w s a)
Sys.localVariable
   Variable w s a -> Variable w s b -> Variable w s c -> T w s ()
rule Variable w s a
xv Variable w s b
yv Variable w s c
zv
   forall (m :: * -> *) a. Monad m => a -> m a
return Variable w s c
zv


newtype Apply w s f = Apply (Sys.T w s f)

instance Functor (Apply w s) where
   fmap :: forall a b. (a -> b) -> Apply w s a -> Apply w s b
fmap a -> b
f (Apply T w s a
a) = forall (w :: (* -> *) -> * -> *) s f. T w s f -> Apply w s f
Apply forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f T w s a
a

instance Applicative (Apply w s) where
   pure :: forall a. a -> Apply w s a
pure a
a = forall (w :: (* -> *) -> * -> *) s f. T w s f -> Apply w s f
Apply forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return a
a
   Apply T w s (a -> b)
f <*> :: forall a b. Apply w s (a -> b) -> Apply w s a -> Apply w s b
<*> Apply T w s a
a = forall (w :: (* -> *) -> * -> *) s f. T w s f -> Apply w s f
Apply forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap T w s (a -> b)
f T w s a
a


{- |
This function allows to generalize 'fromRule2' and 'fromRule3' to more arguments
using 'Applicative' combinators.

Example:

> fromRule3 rule x y
>    = runApply $ liftA2 rule (arg x) (arg y)
>    = runApply $ pure rule <*> arg x <*> arg y

Building rules with 'arg' provides more granularity
than using auxiliary 'pair' rules!
-}
arg ::
   T w s a -> Apply w s (Sys.Variable w s a)
arg :: forall (w :: (* -> *) -> * -> *) s a.
T w s a -> Apply w s (Variable w s a)
arg (Cons T w s (Variable w s a)
x) = forall (w :: (* -> *) -> * -> *) s f. T w s f -> Apply w s f
Apply T w s (Variable w s a)
x

runApply ::
   (Sys.C w, Duplicate.C a) =>
   Apply w s (Sys.Variable w s a -> Sys.T w s ()) ->
   T w s a
runApply :: forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
Apply w s (Variable w s a -> T w s ()) -> T w s a
runApply (Apply T w s (Variable w s a -> T w s ())
rule) = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall a b. (a -> b) -> a -> b
$ do
   Variable w s a -> T w s ()
f <- T w s (Variable w s a -> T w s ())
rule
   Variable w s a
xv <- forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
T w s (Variable w s a)
Sys.localVariable
   Variable w s a -> T w s ()
f Variable w s a
xv
   forall (m :: * -> *) a. Monad m => a -> m a
return Variable w s a
xv

{-
examples of how to use 'arg' and 'runApply'
-}
_fromRule2 :: forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
_fromRule2 Variable w s a -> Variable w s b -> T w s ()
rule T w s a
x = forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
Apply w s (Variable w s a -> T w s ()) -> T w s a
runApply forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA Variable w s a -> Variable w s b -> T w s ()
rule forall a b. (a -> b) -> a -> b
$ forall (w :: (* -> *) -> * -> *) s a.
T w s a -> Apply w s (Variable w s a)
arg T w s a
x
_fromRule3 :: forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
_fromRule3 Variable w s a -> Variable w s b -> Variable w s c -> T w s ()
rule T w s a
x T w s b
y = forall (w :: (* -> *) -> * -> *) a s.
(C w, C a) =>
Apply w s (Variable w s a -> T w s ()) -> T w s a
runApply forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Variable w s a -> Variable w s b -> Variable w s c -> T w s ()
rule (forall (w :: (* -> *) -> * -> *) s a.
T w s a -> Apply w s (Variable w s a)
arg T w s a
x) (forall (w :: (* -> *) -> * -> *) s a.
T w s a -> Apply w s (Variable w s a)
arg T w s b
y)


instance (Sys.C w, Duplicate.C a, P.Fractional a) => P.Num (T w s a) where
   fromInteger :: Integer -> T w s a
fromInteger = forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => a -> T w s a
constant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger
   + :: T w s a -> T w s a -> T w s a
(+) = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 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
   (-) = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 (\Variable w s a
z Variable w s a
x Variable w s a
y -> 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 w s a
x Variable w s a
y Variable w s a
z)
   * :: T w s a -> T w s a -> T w s a
(*) = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 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
   abs :: T w s a -> T w s a
abs = forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
fromRule2 (forall (w :: (* -> *) -> * -> *) a b s.
C w =>
(a -> b) -> Variable w s a -> Variable w s b -> T w s ()
Sys.assignment2 forall a. Num a => a -> a
abs)
   signum :: T w s a -> T w s a
signum = forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
fromRule2 (forall (w :: (* -> *) -> * -> *) a b s.
C w =>
(a -> b) -> Variable w s a -> Variable w s b -> T w s ()
Sys.assignment2 forall a. Num a => a -> a
signum)

instance (Sys.C w, Duplicate.C a, P.Fractional a) => P.Fractional (T w s a) where
   fromRational :: Rational -> T w s a
fromRational = forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => a -> T w s a
constant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational
   / :: T w s a -> T w s a -> T w s a
(/) = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 (\Variable w s a
z Variable w s a
x Variable w s a
y -> 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 w s a
x Variable w s a
y Variable w s a
z)

sqr :: (Sys.C w, Duplicate.C a, P.Floating a) => T w s a -> T w s a
sqr :: forall (w :: (* -> *) -> * -> *) a s.
(C w, C a, Floating a) =>
T w s a -> T w s a
sqr = forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
fromRule2 forall a (w :: (* -> *) -> * -> *) s.
(Floating a, C w) =>
Variable w s a -> Variable w s a -> T w s ()
Rule.square

sqrt :: (Sys.C w, Duplicate.C a, P.Floating a) => T w s a -> T w s a
sqrt :: forall (w :: (* -> *) -> * -> *) a s.
(C w, C a, Floating a) =>
T w s a -> T w s a
sqrt = forall (w :: (* -> *) -> * -> *) b s a.
(C w, C b) =>
(Variable w s a -> Variable w s b -> T w s ())
-> T w s a -> T w s b
fromRule2 (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a (w :: (* -> *) -> * -> *) s.
(Floating a, C w) =>
Variable w s a -> Variable w s a -> T w s ()
Rule.square)


infixl 4 =!=

(=!=) :: (Sys.C w) => T w s a -> T w s a -> T w s a
=!= :: forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s a
(=!=) (Cons T w s (Variable w s a)
x) (Cons T w s (Variable w s a)
y) = forall (w :: (* -> *) -> * -> *) s a.
T w s (Variable w s a) -> T w s a
Cons forall a b. (a -> b) -> a -> b
$ do
   Variable w s a
xv <- T w s (Variable w s a)
x
   Variable w s a
yv <- T w s (Variable w s a)
y
   forall (w :: (* -> *) -> * -> *) s a.
C w =>
Variable w s a -> Variable w s a -> T w s ()
Rule.equ Variable w s a
xv Variable w s a
yv
   forall (m :: * -> *) a. Monad m => a -> m a
return Variable w s a
xv

infix 0 =:=

(=:=) :: (Sys.C w) => T w s a -> T w s a -> Sys.T w s ()
=:= :: forall (w :: (* -> *) -> * -> *) s a.
C w =>
T w s a -> T w s a -> T w s ()
(=:=) (Cons T w s (Variable w s a)
x) (Cons T w s (Variable w s a)
y) = do
   Variable w s a
xv <- T w s (Variable w s a)
x
   Variable w s a
yv <- T w s (Variable w s a)
y
   forall (w :: (* -> *) -> * -> *) s a.
C w =>
Variable w s a -> Variable w s a -> T w s ()
Rule.equ Variable w s a
xv Variable w s a
yv


{- |
We are not able to implement a full Ord instance
including Eq superclass and comparisons,
but we need to compute maxima.
-}
max :: (Sys.C w, Ord a, Duplicate.C a) => T w s a -> T w s a -> T w s a
max :: forall (w :: (* -> *) -> * -> *) a s.
(C w, Ord a, C a) =>
T w s a -> T w s a -> T w s a
max = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 forall a (w :: (* -> *) -> * -> *) s.
(Ord a, C w) =>
Variable w s a -> Variable w s a -> Variable w s a -> T w s ()
Rule.max

maximum :: (Sys.C w, Ord a, Duplicate.C a) => [T w s a] -> T w s a
maximum :: forall (w :: (* -> *) -> * -> *) a s.
(C w, Ord a, C a) =>
[T w s a] -> T w s a
maximum = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 forall (w :: (* -> *) -> * -> *) a s.
(C w, Ord a, C a) =>
T w s a -> T w s a -> T w s a
max


{- |
Construct or decompose a pair.
-}
pair ::
   (Sys.C w, Duplicate.C a, Duplicate.C b) =>
   T w s a -> T w s b -> T w s (a,b)
pair :: forall (w :: (* -> *) -> * -> *) a b s.
(C w, C a, C b) =>
T w s a -> T w s b -> T w s (a, b)
pair = forall (w :: (* -> *) -> * -> *) c s a b.
(C w, C c) =>
(Variable w s a -> Variable w s b -> Variable w s c -> T w s ())
-> T w s a -> T w s b -> T w s c
fromRule3 forall (w :: (* -> *) -> * -> *) s a b.
C w =>
Variable w s a -> Variable w s b -> Variable w s (a, b) -> T w s ()
Rule.pair