module Lava.ConstructiveAnalysis where
import Lava.Signal
import Lava.Operators
import Lava.Error
import Lava.Generic
import Lava.Sequent
import Lava.Ref
import Lava.MyST
( STRef
, newSTRef
, readSTRef
, writeSTRef
, runST
, fixST
, unsafeInterleaveST
)
import Data.List
( isPrefixOf
)
constructive :: (Generic a, Generic b) => (a -> b) -> (a -> Signal Bool)
constructive :: (a -> b) -> a -> Signal Bool
constructive circ :: a -> b
circ inp :: a
inp =
(forall s. ST s (Signal Bool)) -> Signal Bool
forall a. (forall s. ST s a) -> a
runST
( do STRef s [Signal Bool]
defined <- [Signal Bool] -> ST s (STRef s [Signal Bool])
forall a s. a -> ST s (STRef s a)
newSTRef []
TableST s (S Symbol) (Signal Bool, Signal Bool)
table <- ST s (TableST s (S Symbol) (Signal Bool, Signal Bool))
forall s a b. ST s (TableST s a b)
tableST
let gather :: Symbol -> ST s (Signal Bool, Signal Bool)
gather (Symbol sym :: Ref (S Symbol)
sym) =
do Maybe (Signal Bool, Signal Bool)
ms <- TableST s (S Symbol) (Signal Bool, Signal Bool)
-> Ref (S Symbol) -> ST s (Maybe (Signal Bool, Signal Bool))
forall s a b. TableST s a b -> Ref a -> ST s (Maybe b)
findST TableST s (S Symbol) (Signal Bool, Signal Bool)
table Ref (S Symbol)
sym
case Maybe (Signal Bool, Signal Bool)
ms of
Just s :: (Signal Bool, Signal Bool)
s -> do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signal Bool, Signal Bool)
s
Nothing -> ((Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool))
-> ST s (Signal Bool, Signal Bool)
forall a s. (a -> ST s a) -> ST s a
fixST (\s :: (Signal Bool, Signal Bool)
s ->
do TableST s (S Symbol) (Signal Bool, Signal Bool)
-> Ref (S Symbol) -> (Signal Bool, Signal Bool) -> ST s ()
forall s a b. TableST s a b -> Ref a -> b -> ST s ()
extendST TableST s (S Symbol) (Signal Bool, Signal Bool)
table Ref (S Symbol)
sym (Signal Bool, Signal Bool)
s
S (Signal Bool, Signal Bool)
ss <- (Symbol -> ST s (Signal Bool, Signal Bool))
-> S Symbol -> ST s (S (Signal Bool, Signal Bool))
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap (ST s (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s (Signal Bool, Signal Bool)
-> ST s (Signal Bool, Signal Bool))
-> (Symbol -> ST s (Signal Bool, Signal Bool))
-> Symbol
-> ST s (Signal Bool, Signal Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> ST s (Signal Bool, Signal Bool)
gather) (Ref (S Symbol) -> S Symbol
forall a. Ref a -> a
deref Ref (S Symbol)
sym)
S (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
define S (Signal Bool, Signal Bool)
ss
)
define :: S (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
define (Bool b :: Bool
b) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Signal Bool
bool Bool
b, Bool -> Signal Bool
bool (Bool -> Bool
not Bool
b))
define (DelayBool ~(inipos :: Signal Bool
inipos,inineg :: Signal Bool
inineg) ~(nextpos :: Signal Bool
nextpos,nextneg :: Signal Bool
nextneg)) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signal Bool
respos, Signal Bool -> Signal Bool
inv Signal Bool
respos)
where
respos :: Signal Bool
respos = Signal Bool -> Signal Bool -> Signal Bool
forall a. Generic a => a -> a -> a
delay Signal Bool
inipos Signal Bool
nextpos
define (VarBool s :: String
s) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signal Bool
respos, Signal Bool -> Signal Bool
inv Signal Bool
respos)
where
respos :: Signal Bool
respos
| String
tag String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s = Symbol -> Signal Bool
forall a. Symbol -> Signal a
Signal (String -> a -> Symbol
forall a. Generic a => String -> a -> Symbol
pickSymbol (Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
tag) String
s) a
inp)
| Bool
otherwise = String -> Signal Bool
forall a. Constructive a => String -> a
var String
s
define (Inv ~(xpos :: Signal Bool
xpos,xneg :: Signal Bool
xneg)) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
result ( [Signal Bool] -> Signal Bool
andl [Signal Bool
xneg]
, [Signal Bool] -> Signal Bool
orl [Signal Bool
xpos]
)
define (And xs :: [(Signal Bool, Signal Bool)]
xs) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
result ( [Signal Bool] -> Signal Bool
andl [ Signal Bool
xpos | (xpos :: Signal Bool
xpos,_) <- [(Signal Bool, Signal Bool)]
xs ]
, [Signal Bool] -> Signal Bool
orl [ Signal Bool
xneg | (_,xneg :: Signal Bool
xneg) <- [(Signal Bool, Signal Bool)]
xs ]
)
define (Or xs :: [(Signal Bool, Signal Bool)]
xs) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
result ( [Signal Bool] -> Signal Bool
orl [ Signal Bool
xpos | (xpos :: Signal Bool
xpos,_) <- [(Signal Bool, Signal Bool)]
xs ]
, [Signal Bool] -> Signal Bool
andl [ Signal Bool
xneg | (_,xneg :: Signal Bool
xneg) <- [(Signal Bool, Signal Bool)]
xs ]
)
define (Xor xs :: [(Signal Bool, Signal Bool)]
xs) =
do (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
result ( [(Signal Bool, Signal Bool)] -> Signal Bool
xorpos [(Signal Bool, Signal Bool)]
xs
, [(Signal Bool, Signal Bool)] -> Signal Bool
forall a. [(a, Signal Bool)] -> Signal Bool
xorneg [(Signal Bool, Signal Bool)]
xs
)
where
xorpos :: [(Signal Bool, Signal Bool)] -> Signal Bool
xorpos [] = Signal Bool
low
xorpos [(xpos :: Signal Bool
xpos,xneg :: Signal Bool
xneg)] = Signal Bool
xpos
xorpos ((xpos :: Signal Bool
xpos,xneg :: Signal Bool
xneg):xs :: [(Signal Bool, Signal Bool)]
xs) =
(Signal Bool, Signal Bool) -> Signal Bool
or2 ( [Signal Bool] -> Signal Bool
andl (Signal Bool
xpos Signal Bool -> [Signal Bool] -> [Signal Bool]
forall a. a -> [a] -> [a]
: [ Signal Bool
xneg | (_,xneg :: Signal Bool
xneg) <- [(Signal Bool, Signal Bool)]
xs ])
, [Signal Bool] -> Signal Bool
andl [ Signal Bool
xneg, [(Signal Bool, Signal Bool)] -> Signal Bool
xorpos [(Signal Bool, Signal Bool)]
xs ]
)
xorneg :: [(a, Signal Bool)] -> Signal Bool
xorneg xs :: [(a, Signal Bool)]
xs =
(Signal Bool, Signal Bool) -> Signal Bool
or2 ( [Signal Bool] -> Signal Bool
andl [ Signal Bool
xneg | (_,xneg :: Signal Bool
xneg) <- [(a, Signal Bool)]
xs ]
, [Signal Bool] -> Signal Bool
orl [ (Signal Bool, Signal Bool) -> Signal Bool
and2 (Signal Bool
xpos,Signal Bool
ypos)
| (xpos :: Signal Bool
xpos,ypos :: Signal Bool
ypos) <- [Signal Bool] -> [(Signal Bool, Signal Bool)]
forall b. [b] -> [(b, b)]
pairs [ Signal Bool
xpos | (_,xpos :: Signal Bool
xpos) <- [(a, Signal Bool)]
xs ]
]
)
pairs :: [b] -> [(b, b)]
pairs [] = []
pairs (x :: b
x:xs :: [b]
xs) = [ (b
x,b
y) | b
y <- [b]
xs ] [(b, b)] -> [(b, b)] -> [(b, b)]
forall a. [a] -> [a] -> [a]
++ [b] -> [(b, b)]
pairs [b]
xs
define s :: S (Signal Bool, Signal Bool)
s =
do Error -> ST s (Signal Bool, Signal Bool)
forall a. Error -> a
wrong Error
NoArithmetic
result :: (Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
result (xpos :: Signal Bool
xpos,xneg :: Signal Bool
xneg) =
do [Signal Bool]
defs <- STRef s [Signal Bool] -> ST s [Signal Bool]
forall s a. STRef s a -> ST s a
readSTRef STRef s [Signal Bool]
defined
STRef s [Signal Bool] -> [Signal Bool] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [Signal Bool]
defined ((Signal Bool
xpos Signal Bool -> Signal Bool -> Signal Bool
<#> Signal Bool
xneg) Signal Bool -> [Signal Bool] -> [Signal Bool]
forall a. a -> [a] -> [a]
: [Signal Bool]
defs)
(Signal Bool, Signal Bool) -> ST s (Signal Bool, Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signal Bool
xpos,Signal Bool
xneg)
in (Symbol -> ST s (Signal Bool, Signal Bool))
-> Struct Symbol -> ST s (Struct (Signal Bool, Signal Bool))
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap Symbol -> ST s (Signal Bool, Signal Bool)
gather (b -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct (a -> b
circ (String -> a -> a
forall a. Generic a => String -> a -> a
symbolize String
tag a
inp)))
[Signal Bool]
defs <- STRef s [Signal Bool] -> ST s [Signal Bool]
forall s a. STRef s a -> ST s a
readSTRef STRef s [Signal Bool]
defined
Signal Bool -> ST s (Signal Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Signal Bool] -> Signal Bool
andl [Signal Bool]
defs)
)
where
tag :: String
tag = "#constr#"