module UniqueLogic.ST.Expression (
T,
constant, fromVariable,
fromRule1, fromRule2, fromRule3,
Apply, arg, runApply,
(=:=),
(=!=),
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 qualified Prelude as P
import Prelude hiding (max, maximum, sqrt)
newtype T w s a = Cons (Sys.T w s (Sys.Variable w s a))
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
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
_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
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
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