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 analysis

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#"

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