module Lava.Table
  ( table
  , tableProp
  )
 where

import Lava.Signal
import Lava.Netlist
import Lava.Generic
import Lava.Sequent
import Lava.Property
import Lava.MyST

{-

Example use:

Suppose we have a circuit:

  f :: (Signal Bool, Signal Bool) -> Signal Bool
  f (x,y) = and2 (y,x)

Then we can look at its internal structure as follows:

  table (struct (f (var "i")))

will evaluate to

  ([(1,And 2 3),(3,Var "i_1"),(2,Var "i_2")],Object 1)

For circuits taking more complicated structures as arguments
(such as lists), one has to instantiate the list size first
of course.

If you do not like the "Object 1" output, you can just use
the function `flatten' to get a list of identifiers.

-}

----------------------------------------------------------------
-- table

tableProp :: Checkable a => a -> IO ([(Int,S Int)], [Int])
tableProp :: a -> IO ([(Int, S Int)], [Int])
tableProp a :: a
a =
  do (props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
     let (tab :: [(Int, S Int)]
tab, ps :: Struct Int
ps) = Struct Symbol -> ([(Int, S Int)], Struct Int)
forall (f :: * -> *).
Sequent f =>
f Symbol -> ([(Int, S Int)], f Int)
table ([Signal Bool] -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct [Signal Bool]
props)
     ([(Int, S Int)], [Int]) -> IO ([(Int, S Int)], [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, S Int)]
tab, Struct Int -> [Int]
forall a. Struct a -> [a]
flatten Struct Int
ps)

table :: Sequent f => f Symbol -> ([(Int,S Int)], f Int)
table :: f Symbol -> ([(Int, S Int)], f Int)
table str :: f Symbol
str =
  (forall s. ST s ([(Int, S Int)], f Int)) -> ([(Int, S Int)], f Int)
forall a. (forall s. ST s a) -> a
runST
  ( do STRef s Int
ref   <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef 0
       STRef s [(Int, S Int)]
table <- [(Int, S Int)] -> ST s (STRef s [(Int, S Int)])
forall a s. a -> ST s (STRef s a)
newSTRef []

       let new :: ST s Int
new =
             do Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
ref
                let n' :: Int
n' = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1
                STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
ref Int
n'
                Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n'

           define :: Int -> S Int -> ST s ()
define v :: Int
v def :: S Int
def =
             do [(Int, S Int)]
tab <- STRef s [(Int, S Int)] -> ST s [(Int, S Int)]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S Int)]
table
                STRef s [(Int, S Int)] -> [(Int, S Int)] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [(Int, S Int)]
table ((Int
v,S Int
def)(Int, S Int) -> [(Int, S Int)] -> [(Int, S Int)]
forall a. a -> [a] -> [a]
:[(Int, S Int)]
tab)

       f Int
str' <- ST s Int -> (Int -> S Int -> ST s ()) -> f Symbol -> ST s (f Int)
forall (f :: * -> *) s v.
Sequent f =>
ST s v -> (v -> S v -> ST s ()) -> f Symbol -> ST s (f v)
netlistST ST s Int
new Int -> S Int -> ST s ()
define f Symbol
str
       [(Int, S Int)]
tab  <- STRef s [(Int, S Int)] -> ST s [(Int, S Int)]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S Int)]
table
       ([(Int, S Int)], f Int) -> ST s ([(Int, S Int)], f Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, S Int)]
tab, f Int
str')
  )

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