module Lava.Signal where

import Lava.Ref
import Lava.Sequent
import Lava.Error

import Data.List
  ( transpose
  )

----------------------------------------------------------------
-- Signal, Symbol, S

newtype Signal a
  = Signal Symbol

newtype Symbol
  = Symbol (Ref (S Symbol))

data S s
  = Bool      Bool
  | Inv       s
  | And       [s]
  | Or        [s]
  | Xor       [s]
  | VarBool   String
  | DelayBool s s

  | Int      Int
  | Neg      s
  | Div      s s
  | Mod      s s
  | Plus     [s]
  | Times    [s]
  | Gte      s s
  | Equal    [s]
  | If       s s s
  | VarInt   String
  | DelayInt s s

symbol :: S Symbol -> Symbol
symbol :: S Symbol -> Symbol
symbol = Ref (S Symbol) -> Symbol
Symbol (Ref (S Symbol) -> Symbol)
-> (S Symbol -> Ref (S Symbol)) -> S Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S Symbol -> Ref (S Symbol)
forall a. a -> Ref a
ref

unsymbol :: Symbol -> S Symbol
unsymbol :: Symbol -> S Symbol
unsymbol (Symbol r :: Ref (S Symbol)
r) = Ref (S Symbol) -> S Symbol
forall a. Ref a -> a
deref Ref (S Symbol)
r

instance Eq (Signal a) where
  Signal (Symbol r1 :: Ref (S Symbol)
r1) == :: Signal a -> Signal a -> Bool
== Signal (Symbol r2 :: Ref (S Symbol)
r2) = Ref (S Symbol)
r1 Ref (S Symbol) -> Ref (S Symbol) -> Bool
forall a. Eq a => a -> a -> Bool
== Ref (S Symbol)
r2

----------------------------------------------------------------
-- operations

-- on bits

bool :: Bool -> Signal Bool
bool :: Bool -> Signal Bool
bool b :: Bool
b = S Symbol -> Signal Bool
forall a. S Symbol -> Signal a
lift0 (Bool -> S Symbol
forall s. Bool -> S s
Bool Bool
b)

low, high :: Signal Bool
low :: Signal Bool
low  = Bool -> Signal Bool
bool Bool
False
high :: Signal Bool
high = Bool -> Signal Bool
bool Bool
True

inv :: Signal Bool -> Signal Bool
inv :: Signal Bool -> Signal Bool
inv = (Symbol -> S Symbol) -> Signal Bool -> Signal Bool
forall a b. (Symbol -> S Symbol) -> Signal a -> Signal b
lift1 Symbol -> S Symbol
forall s. s -> S s
Inv

andl, orl, xorl :: [Signal Bool] -> Signal Bool
andl :: [Signal Bool] -> Signal Bool
andl = ([Symbol] -> S Symbol) -> [Signal Bool] -> Signal Bool
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
And
orl :: [Signal Bool] -> Signal Bool
orl  = ([Symbol] -> S Symbol) -> [Signal Bool] -> Signal Bool
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
Or
xorl :: [Signal Bool] -> Signal Bool
xorl = ([Symbol] -> S Symbol) -> [Signal Bool] -> Signal Bool
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
Xor

equalBool :: Signal Bool -> Signal Bool -> Signal Bool
equalBool :: Signal Bool -> Signal Bool -> Signal Bool
equalBool x :: Signal Bool
x y :: Signal Bool
y = Signal Bool -> Signal Bool
inv ([Signal Bool] -> Signal Bool
xorl [Signal Bool
x,Signal Bool
y])

ifBool :: Signal Bool -> (Signal Bool, Signal Bool) -> Signal Bool
ifBool :: Signal Bool -> (Signal Bool, Signal Bool) -> Signal Bool
ifBool c :: Signal Bool
c (x :: Signal Bool
x,y :: Signal Bool
y) = [Signal Bool] -> Signal Bool
orl[[Signal Bool] -> Signal Bool
andl[Signal Bool
c,Signal Bool
x],[Signal Bool] -> Signal Bool
andl[Signal Bool -> Signal Bool
inv Signal Bool
c,Signal Bool
y]]

delayBool :: Signal Bool -> Signal Bool -> Signal Bool
delayBool :: Signal Bool -> Signal Bool -> Signal Bool
delayBool = (Symbol -> Symbol -> S Symbol)
-> Signal Bool -> Signal Bool -> Signal Bool
forall a b c.
(Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 Symbol -> Symbol -> S Symbol
forall s. s -> s -> S s
DelayBool

varBool :: String -> Signal Bool
varBool :: String -> Signal Bool
varBool s :: String
s = S Symbol -> Signal Bool
forall a. S Symbol -> Signal a
lift0 (String -> S Symbol
forall s. String -> S s
VarBool String
s)

-- on ints

int :: Int -> Signal Int
int :: Int -> Signal Int
int n :: Int
n = S Symbol -> Signal Int
forall a. S Symbol -> Signal a
lift0 (Int -> S Symbol
forall s. Int -> S s
Int Int
n)

neg :: Signal Int -> Signal Int
neg :: Signal Int -> Signal Int
neg = (Symbol -> S Symbol) -> Signal Int -> Signal Int
forall a b. (Symbol -> S Symbol) -> Signal a -> Signal b
lift1 Symbol -> S Symbol
forall s. s -> S s
Neg

divide, modulo :: Signal Int -> Signal Int -> Signal Int
divide :: Signal Int -> Signal Int -> Signal Int
divide = (Symbol -> Symbol -> S Symbol)
-> Signal Int -> Signal Int -> Signal Int
forall a b c.
(Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 Symbol -> Symbol -> S Symbol
forall s. s -> s -> S s
Div
modulo :: Signal Int -> Signal Int -> Signal Int
modulo = (Symbol -> Symbol -> S Symbol)
-> Signal Int -> Signal Int -> Signal Int
forall a b c.
(Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 Symbol -> Symbol -> S Symbol
forall s. s -> s -> S s
Mod

plusl, timesl :: [Signal Int] -> Signal Int
plusl :: [Signal Int] -> Signal Int
plusl  = ([Symbol] -> S Symbol) -> [Signal Int] -> Signal Int
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
Plus
timesl :: [Signal Int] -> Signal Int
timesl = ([Symbol] -> S Symbol) -> [Signal Int] -> Signal Int
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
Times

equall :: [Signal Int] -> Signal Bool
equall :: [Signal Int] -> Signal Bool
equall = ([Symbol] -> S Symbol) -> [Signal Int] -> Signal Bool
forall a c. ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl [Symbol] -> S Symbol
forall s. [s] -> S s
Equal

gteInt :: Signal Int -> Signal Int -> Signal Bool
gteInt :: Signal Int -> Signal Int -> Signal Bool
gteInt = (Symbol -> Symbol -> S Symbol)
-> Signal Int -> Signal Int -> Signal Bool
forall a b c.
(Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 Symbol -> Symbol -> S Symbol
forall s. s -> s -> S s
Gte

equalInt :: Signal Int -> Signal Int -> Signal Bool
equalInt :: Signal Int -> Signal Int -> Signal Bool
equalInt x :: Signal Int
x y :: Signal Int
y = [Signal Int] -> Signal Bool
equall [Signal Int
x,Signal Int
y]

ifInt :: Signal Bool -> (Signal Int, Signal Int) -> Signal a
ifInt :: Signal Bool -> (Signal Int, Signal Int) -> Signal a
ifInt c :: Signal Bool
c (x :: Signal Int
x,y :: Signal Int
y) = (Symbol -> Symbol -> Symbol -> S Symbol)
-> Signal Bool -> Signal Int -> Signal Int -> Signal a
forall a b c d.
(Symbol -> Symbol -> Symbol -> S Symbol)
-> Signal a -> Signal b -> Signal c -> Signal d
lift3 Symbol -> Symbol -> Symbol -> S Symbol
forall s. s -> s -> s -> S s
If Signal Bool
c Signal Int
x Signal Int
y

delayInt :: Signal Int -> Signal Int -> Signal Int
delayInt :: Signal Int -> Signal Int -> Signal Int
delayInt = (Symbol -> Symbol -> S Symbol)
-> Signal Int -> Signal Int -> Signal Int
forall a b c.
(Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 Symbol -> Symbol -> S Symbol
forall s. s -> s -> S s
DelayInt

varInt :: String -> Signal Int
varInt :: String -> Signal Int
varInt s :: String
s = S Symbol -> Signal Int
forall a. S Symbol -> Signal a
lift0 (String -> S Symbol
forall s. String -> S s
VarInt String
s)

-- liftings

lift0 :: S Symbol -> Signal a
lift0 :: S Symbol -> Signal a
lift0 oper :: S Symbol
oper = Symbol -> Signal a
forall a. Symbol -> Signal a
Signal (S Symbol -> Symbol
symbol S Symbol
oper)

lift1 :: (Symbol -> S Symbol) -> Signal a -> Signal b
lift1 :: (Symbol -> S Symbol) -> Signal a -> Signal b
lift1 oper :: Symbol -> S Symbol
oper (Signal a :: Symbol
a) = Symbol -> Signal b
forall a. Symbol -> Signal a
Signal (S Symbol -> Symbol
symbol (Symbol -> S Symbol
oper Symbol
a))

lift2 :: (Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 :: (Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift2 oper :: Symbol -> Symbol -> S Symbol
oper (Signal a :: Symbol
a) (Signal b :: Symbol
b) = Symbol -> Signal c
forall a. Symbol -> Signal a
Signal (S Symbol -> Symbol
symbol (Symbol -> Symbol -> S Symbol
oper Symbol
a Symbol
b))

lift3 :: (Symbol -> Symbol -> Symbol -> S Symbol)
      -> Signal a -> Signal b -> Signal c -> Signal d
lift3 :: (Symbol -> Symbol -> Symbol -> S Symbol)
-> Signal a -> Signal b -> Signal c -> Signal d
lift3 oper :: Symbol -> Symbol -> Symbol -> S Symbol
oper (Signal a :: Symbol
a) (Signal b :: Symbol
b) (Signal c :: Symbol
c) = Symbol -> Signal d
forall a. Symbol -> Signal a
Signal (S Symbol -> Symbol
symbol (Symbol -> Symbol -> Symbol -> S Symbol
oper Symbol
a Symbol
b Symbol
c))

liftl :: ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl :: ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
liftl oper :: [Symbol] -> S Symbol
oper sigas :: [Signal a]
sigas = Symbol -> Signal c
forall a. Symbol -> Signal a
Signal (S Symbol -> Symbol
symbol ([Symbol] -> S Symbol
oper ((Signal a -> Symbol) -> [Signal a] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\(Signal a :: Symbol
a) -> Symbol
a) [Signal a]
sigas)))

----------------------------------------------------------------
-- evaluate

eval :: S (S a) -> S a
eval :: S (S a) -> S a
eval s :: S (S a)
s =
  case S (S a)
s of
    Bool b :: Bool
b       -> Bool -> S a
forall s. Bool -> S s
Bool Bool
b
    Inv (Bool b :: Bool
b) -> Bool -> S a
forall s. Bool -> S s
Bool (Bool -> Bool
not Bool
b)
    And xs :: [S a]
xs       -> Bool -> S a
forall s. Bool -> S s
Bool (Bool -> S a) -> ([S a] -> Bool) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Bool) -> [S a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all S a -> Bool
forall s. S s -> Bool
bval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs
    Or xs :: [S a]
xs        -> Bool -> S a
forall s. Bool -> S s
Bool (Bool -> S a) -> ([S a] -> Bool) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Bool) -> [S a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any S a -> Bool
forall s. S s -> Bool
bval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs
    Xor xs :: [S a]
xs       -> Bool -> S a
forall s. Bool -> S s
Bool (Bool -> S a) -> ([S a] -> Bool) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> ([S a] -> Int) -> [S a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [S a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([S a] -> Int) -> ([S a] -> [S a]) -> [S a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Bool) -> [S a] -> [S a]
forall a. (a -> Bool) -> [a] -> [a]
filter S a -> Bool
forall s. S s -> Bool
bval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs

    Int n :: Int
n                 -> Int -> S a
forall s. Int -> S s
Int Int
n
    Neg (Int n :: Int
n)           -> Int -> S a
forall s. Int -> S s
Int (-Int
n)
    Div (Int n1 :: Int
n1) (Int n2 :: Int
n2) -> Int -> S a
forall s. Int -> S s
Int (Int
n1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n2)
    Mod (Int n1 :: Int
n1) (Int n2 :: Int
n2) -> Int -> S a
forall s. Int -> S s
Int (Int
n1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n2)
    Plus xs :: [S a]
xs               -> Int -> S a
forall s. Int -> S s
Int  (Int -> S a) -> ([S a] -> Int) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum     ([Int] -> Int) -> ([S a] -> [Int]) -> [S a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Int) -> [S a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map S a -> Int
forall s. S s -> Int
nval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs
    Times xs :: [S a]
xs              -> Int -> S a
forall s. Int -> S s
Int  (Int -> S a) -> ([S a] -> Int) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([Int] -> Int) -> ([S a] -> [Int]) -> [S a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Int) -> [S a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map S a -> Int
forall s. S s -> Int
nval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs
    Gte (Int n1 :: Int
n1) (Int n2 :: Int
n2) -> Bool -> S a
forall s. Bool -> S s
Bool (Int
n1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n2)
    Equal xs :: [S a]
xs              -> Bool -> S a
forall s. Bool -> S s
Bool (Bool -> S a) -> ([S a] -> Bool) -> [S a] -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall a. Eq a => [a] -> Bool
equal   ([Int] -> Bool) -> ([S a] -> [Int]) -> [S a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S a -> Int) -> [S a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map S a -> Int
forall s. S s -> Int
nval ([S a] -> S a) -> [S a] -> S a
forall a b. (a -> b) -> a -> b
$ [S a]
xs
    If (Bool c :: Bool
c) x :: S a
x y :: S a
y       -> if Bool
c then S a
x else S a
y

    DelayBool s :: S a
s s' :: S a
s' -> Error -> S a
forall a. Error -> a
wrong Error
Lava.Error.DelayEval
    DelayInt  s :: S a
s s' :: S a
s' -> Error -> S a
forall a. Error -> a
wrong Error
Lava.Error.DelayEval
    VarBool   s :: String
s    -> Error -> S a
forall a. Error -> a
wrong Error
Lava.Error.VarEval
    VarInt    s :: String
s    -> Error -> S a
forall a. Error -> a
wrong Error
Lava.Error.VarEval
 where
  bval :: S s -> Bool
bval (Bool b :: Bool
b) = Bool
b
  nval :: S s -> Int
nval (Int n :: Int
n)  = Int
n

  equal :: [a] -> Bool
equal (x :: a
x:y :: a
y:xs :: [a]
xs) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Bool
&& [a] -> Bool
equal (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
  equal _        = Bool
True

evalLazy :: S (Maybe (S a)) -> Maybe (S a)
evalLazy :: S (Maybe (S a)) -> Maybe (S a)
evalLazy s :: S (Maybe (S a))
s =
  case S (Maybe (S a))
s of
    -- lazy
    And xs :: [Maybe (S a)]
xs
      | (Maybe (S a) -> Bool) -> [Maybe (S a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (S a) -> Bool -> Bool
forall s. Maybe (S s) -> Bool -> Bool
`bval` Bool
False) [Maybe (S a)]
xs        -> Bool -> Maybe (S a)
forall s. Bool -> Maybe (S s)
bans Bool
False

    Or xs :: [Maybe (S a)]
xs
      | (Maybe (S a) -> Bool) -> [Maybe (S a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (S a) -> Bool -> Bool
forall s. Maybe (S s) -> Bool -> Bool
`bval` Bool
True) [Maybe (S a)]
xs         -> Bool -> Maybe (S a)
forall s. Bool -> Maybe (S s)
bans Bool
True

    Xor xs :: [Maybe (S a)]
xs
      | (Maybe (S a) -> Bool) -> [Maybe (S a)] -> Int
forall a. (a -> Bool) -> [a] -> Int
number (Maybe (S a) -> Bool -> Bool
forall s. Maybe (S s) -> Bool -> Bool
`bval` Bool
True) [Maybe (S a)]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 -> Bool -> Maybe (S a)
forall s. Bool -> Maybe (S s)
bans Bool
False

    -- strict
    _ -> S (S a) -> S a
forall a. S (S a) -> S a
eval (S (S a) -> S a) -> Maybe (S (S a)) -> Maybe (S a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` S (Maybe (S a)) -> Maybe (S (S a))
forall (s :: * -> *) (m :: * -> *) a.
(Sequent s, Monad m) =>
s (m a) -> m (s a)
sequent S (Maybe (S a))
s

 where
  bans :: Bool -> Maybe (S s)
bans = S s -> Maybe (S s)
forall a. a -> Maybe a
Just (S s -> Maybe (S s)) -> (Bool -> S s) -> Bool -> Maybe (S s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> S s
forall s. Bool -> S s
Bool

  bval :: Maybe (S s) -> Bool -> Bool
bval (Just (Bool b :: Bool
b)) b' :: Bool
b' = Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b'
  bval _               _  = Bool
False

  number :: (a -> Bool) -> [a] -> Int
number p :: a -> Bool
p = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> Int) -> ([a] -> [a]) -> [a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p

arguments :: S a -> [a]
arguments :: S a -> [a]
arguments s :: S a
s =
  case S a
s of
    Bool b :: Bool
b     -> []
    Inv s :: a
s      -> [a
s]
    And xs :: [a]
xs     -> [a]
xs
    Or xs :: [a]
xs      -> [a]
xs
    Xor xs :: [a]
xs     -> [a]
xs

    Int n :: Int
n      -> []
    Neg s :: a
s      -> [a
s]
    Div s1 :: a
s1 s2 :: a
s2  -> [a
s1,a
s2]
    Mod s1 :: a
s1 s2 :: a
s2  -> [a
s1,a
s2]
    Plus xs :: [a]
xs    -> [a]
xs
    Times xs :: [a]
xs   -> [a]
xs
    Gte x :: a
x y :: a
y    -> [a
x,a
y]
    Equal xs :: [a]
xs   -> [a]
xs
    If x :: a
x y :: a
y z :: a
z   -> [a
x,a
y,a
z]

    DelayBool s :: a
s s' :: a
s' -> [a
s,a
s']
    DelayInt  s :: a
s s' :: a
s' -> [a
s,a
s']
    VarBool s :: String
s      -> []
    VarInt  s :: String
s      -> []

zips :: S [a] -> [S a]
zips :: S [a] -> [S a]
zips s :: S [a]
s =
  case S [a]
s of
    Bool b :: Bool
b     -> [Bool -> S a
forall s. Bool -> S s
Bool Bool
b]
    Inv s :: [a]
s      -> (a -> S a) -> [a] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map a -> S a
forall s. s -> S s
Inv [a]
s
    And xs :: [[a]]
xs     -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
And ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)
    Or xs :: [[a]]
xs      -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
Or  ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)
    Xor xs :: [[a]]
xs     -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
Xor ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)

    Int n :: Int
n      -> [Int -> S a
forall s. Int -> S s
Int Int
n]
    Neg s :: [a]
s      -> (a -> S a) -> [a] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map a -> S a
forall s. s -> S s
Neg [a]
s
    Div s1 :: [a]
s1 s2 :: [a]
s2  -> (a -> a -> S a) -> [a] -> [a] -> [S a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> S a
forall s. s -> s -> S s
Div [a]
s1 [a]
s2
    Mod s1 :: [a]
s1 s2 :: [a]
s2  -> (a -> a -> S a) -> [a] -> [a] -> [S a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> S a
forall s. s -> s -> S s
Mod [a]
s1 [a]
s2
    Plus xs :: [[a]]
xs    -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
Plus  ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)
    Times xs :: [[a]]
xs   -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
Times ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)
    Gte x :: [a]
x y :: [a]
y    -> (a -> a -> S a) -> [a] -> [a] -> [S a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> S a
forall s. s -> s -> S s
Gte [a]
x [a]
y
    Equal xs :: [[a]]
xs   -> ([a] -> S a) -> [[a]] -> [S a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> S a
forall s. [s] -> S s
Equal ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xs)
    If x :: [a]
x y :: [a]
y z :: [a]
z   -> (a -> a -> a -> S a) -> [a] -> [a] -> [a] -> [S a]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 a -> a -> a -> S a
forall s. s -> s -> s -> S s
If [a]
x [a]
y [a]
z

    DelayBool s :: [a]
s s' :: [a]
s' -> (a -> a -> S a) -> [a] -> [a] -> [S a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> S a
forall s. s -> s -> S s
DelayBool [a]
s [a]
s'
    DelayInt  s :: [a]
s s' :: [a]
s' -> (a -> a -> S a) -> [a] -> [a] -> [S a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> S a
forall s. s -> s -> S s
DelayInt [a]
s [a]
s'
    VarBool s :: String
s      -> [String -> S a
forall s. String -> S s
VarBool String
s]
    VarInt  s :: String
s      -> [String -> S a
forall s. String -> S s
VarInt  String
s]

----------------------------------------------------------------
-- properties of S

instance Functor S where
  fmap :: (a -> b) -> S a -> S b
fmap f :: a -> b
f s :: S a
s =
    case S a
s of
      Bool b :: Bool
b    -> Bool -> S b
forall s. Bool -> S s
Bool Bool
b
      Inv x :: a
x     -> b -> S b
forall s. s -> S s
Inv (a -> b
f a
x)
      And xs :: [a]
xs    -> [b] -> S b
forall s. [s] -> S s
And ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
      Or  xs :: [a]
xs    -> [b] -> S b
forall s. [s] -> S s
Or  ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
      Xor xs :: [a]
xs    -> [b] -> S b
forall s. [s] -> S s
Xor ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)

      Int   n :: Int
n   -> Int -> S b
forall s. Int -> S s
Int Int
n
      Neg   x :: a
x   -> b -> S b
forall s. s -> S s
Neg   (a -> b
f a
x)
      Div   x :: a
x y :: a
y -> b -> b -> S b
forall s. s -> s -> S s
Div   (a -> b
f a
x) (a -> b
f a
y)
      Mod   x :: a
x y :: a
y -> b -> b -> S b
forall s. s -> s -> S s
Mod   (a -> b
f a
x) (a -> b
f a
y)
      Plus  xs :: [a]
xs  -> [b] -> S b
forall s. [s] -> S s
Plus  ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
      Times xs :: [a]
xs  -> [b] -> S b
forall s. [s] -> S s
Times ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
      Gte   x :: a
x y :: a
y -> b -> b -> S b
forall s. s -> s -> S s
Gte (a -> b
f a
x) (a -> b
f a
y)
      Equal xs :: [a]
xs  -> [b] -> S b
forall s. [s] -> S s
Equal ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
      If x :: a
x y :: a
y z :: a
z  -> b -> b -> b -> S b
forall s. s -> s -> s -> S s
If (a -> b
f a
x) (a -> b
f a
y) (a -> b
f a
z)

      DelayBool x :: a
x y :: a
y -> b -> b -> S b
forall s. s -> s -> S s
DelayBool (a -> b
f a
x) (a -> b
f a
y)
      DelayInt  x :: a
x y :: a
y -> b -> b -> S b
forall s. s -> s -> S s
DelayInt  (a -> b
f a
x) (a -> b
f a
y)
      VarBool   v :: String
v   -> String -> S b
forall s. String -> S s
VarBool String
v
      VarInt    v :: String
v   -> String -> S b
forall s. String -> S s
VarInt  String
v

instance Sequent S where
  sequent :: S (m a) -> m (S a)
sequent s :: S (m a)
s =
    case S (m a)
s of
      Bool b :: Bool
b    -> S a -> m (S a)
forall (m :: * -> *) a. Monad m => a -> m a
lift0 (Bool -> S a
forall s. Bool -> S s
Bool Bool
b)
      Inv x :: m a
x     -> (a -> S a) -> m a -> m (S a)
forall (m :: * -> *) t b. Monad m => (t -> b) -> m t -> m b
lift1 a -> S a
forall s. s -> S s
Inv m a
x
      And xs :: [m a]
xs    -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
And [m a]
xs
      Or  xs :: [m a]
xs    -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
Or  [m a]
xs
      Xor xs :: [m a]
xs    -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
Xor [m a]
xs

      Int   n :: Int
n   -> S a -> m (S a)
forall (m :: * -> *) a. Monad m => a -> m a
lift0 (Int -> S a
forall s. Int -> S s
Int Int
n)
      Neg   x :: m a
x   -> (a -> S a) -> m a -> m (S a)
forall (m :: * -> *) t b. Monad m => (t -> b) -> m t -> m b
lift1 a -> S a
forall s. s -> S s
Neg   m a
x
      Div   x :: m a
x y :: m a
y -> (a -> a -> S a) -> m a -> m a -> m (S a)
forall (m :: * -> *) t t b.
Monad m =>
(t -> t -> b) -> m t -> m t -> m b
lift2 a -> a -> S a
forall s. s -> s -> S s
Div   m a
x m a
y
      Mod   x :: m a
x y :: m a
y -> (a -> a -> S a) -> m a -> m a -> m (S a)
forall (m :: * -> *) t t b.
Monad m =>
(t -> t -> b) -> m t -> m t -> m b
lift2 a -> a -> S a
forall s. s -> s -> S s
Mod   m a
x m a
y
      Plus  xs :: [m a]
xs  -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
Plus  [m a]
xs
      Times xs :: [m a]
xs  -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
Times [m a]
xs
      Gte   x :: m a
x y :: m a
y -> (a -> a -> S a) -> m a -> m a -> m (S a)
forall (m :: * -> *) t t b.
Monad m =>
(t -> t -> b) -> m t -> m t -> m b
lift2 a -> a -> S a
forall s. s -> s -> S s
Gte   m a
x m a
y
      Equal xs :: [m a]
xs  -> ([a] -> S a) -> [m a] -> m (S a)
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(t a -> b) -> t (m a) -> m b
liftl [a] -> S a
forall s. [s] -> S s
Equal [m a]
xs
      If x :: m a
x y :: m a
y z :: m a
z  -> (a -> a -> a -> S a) -> m a -> m a -> m a -> m (S a)
forall (m :: * -> *) t t t b.
Monad m =>
(t -> t -> t -> b) -> m t -> m t -> m t -> m b
lift3 a -> a -> a -> S a
forall s. s -> s -> s -> S s
If m a
x m a
y m a
z

      DelayBool x :: m a
x y :: m a
y -> (a -> a -> S a) -> m a -> m a -> m (S a)
forall (m :: * -> *) t t b.
Monad m =>
(t -> t -> b) -> m t -> m t -> m b
lift2 a -> a -> S a
forall s. s -> s -> S s
DelayBool m a
x m a
y
      DelayInt  x :: m a
x y :: m a
y -> (a -> a -> S a) -> m a -> m a -> m (S a)
forall (m :: * -> *) t t b.
Monad m =>
(t -> t -> b) -> m t -> m t -> m b
lift2 a -> a -> S a
forall s. s -> s -> S s
DelayInt m a
x m a
y
      VarBool  v :: String
v    -> S a -> m (S a)
forall (m :: * -> *) a. Monad m => a -> m a
lift0 (String -> S a
forall s. String -> S s
VarBool String
v)
      VarInt   v :: String
v    -> S a -> m (S a)
forall (m :: * -> *) a. Monad m => a -> m a
lift0 (String -> S a
forall s. String -> S s
VarInt String
v)
   where
    lift0 :: a -> m a
lift0 op :: a
op =
      do a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
op

    lift1 :: (t -> b) -> m t -> m b
lift1 op :: t -> b
op x :: m t
x =
      do t
x' <- m t
x
         b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> b
op t
x')

    lift2 :: (t -> t -> b) -> m t -> m t -> m b
lift2 op :: t -> t -> b
op x :: m t
x y :: m t
y =
      do t
x' <- m t
x
         t
y' <- m t
y
         b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> t -> b
op t
x' t
y')

    lift3 :: (t -> t -> t -> b) -> m t -> m t -> m t -> m b
lift3 op :: t -> t -> t -> b
op x :: m t
x y :: m t
y z :: m t
z =
      do t
x' <- m t
x
         t
y' <- m t
y
         t
z' <- m t
z
         b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> t -> t -> b
op t
x' t
y' t
z')

    liftl :: (t a -> b) -> t (m a) -> m b
liftl op :: t a -> b
op xs :: t (m a)
xs =
      do t a
xs' <- t (m a) -> m (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence t (m a)
xs
         b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t a -> b
op t a
xs')

instance Show (Signal a) where
  showsPrec :: Int -> Signal a -> ShowS
showsPrec n :: Int
n (Signal s :: Symbol
s) =
    Int -> Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
n Symbol
s

instance Show Symbol where
  showsPrec :: Int -> Symbol -> ShowS
showsPrec n :: Int
n sym :: Symbol
sym =
    Int -> S Symbol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (Symbol -> S Symbol
unsymbol Symbol
sym)

instance Show a => Show (S a) where
  showsPrec :: Int -> S a -> ShowS
showsPrec n :: Int
n s :: S a
s =
    case S a
s of
      Bool True  -> String -> ShowS
showString "high"
      Bool False -> String -> ShowS
showString "low"

      Inv x :: a
x      -> String -> ShowS
showString "inv"  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x]
      And xs :: [a]
xs     -> String -> ShowS
showString "andl" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs
      Or  xs :: [a]
xs     -> String -> ShowS
showString "orl"  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs
      Xor xs :: [a]
xs     -> String -> ShowS
showString "xorl" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs

      Int   i :: Int
i    -> Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
n Int
i
      Neg   x :: a
x    -> String -> ShowS
showString "-" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
n a
x
      Div   x :: a
x y :: a
y  -> String -> ShowS
showString "idiv" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y]
      Mod   x :: a
x y :: a
y  -> String -> ShowS
showString "imod" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y]
      Plus  xs :: [a]
xs   -> String -> ShowS
showString "plusl" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs
      Times xs :: [a]
xs   -> String -> ShowS
showString "timesl" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs
      Gte   x :: a
x y :: a
y  -> String -> ShowS
showString "gte" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y]
      Equal xs :: [a]
xs   -> String -> ShowS
showString "equall" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a]
xs
      If x :: a
x y :: a
y z :: a
z   -> String -> ShowS
showString "ifThenElse" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y,a
z]

      DelayBool x :: a
x y :: a
y -> String -> ShowS
showString "delay" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y]
      DelayInt  x :: a
x y :: a
y -> String -> ShowS
showString "delay" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
forall a. Show a => [a] -> ShowS
showList [a
x,a
y]

      VarBool s :: String
s     -> String -> ShowS
showString String
s
      VarInt  s :: String
s     -> String -> ShowS
showString String
s
      _             -> String -> ShowS
showString "<<symbol>>"

----------------------------------------------------------------
-- the end.