import Lava
import Libs.Simple130nm.Lava

import qualified Lava2000 as L

import Control.Monad.Trans
import Data.Logical.Let
  -- Only used in circLoop2.



circ1 :: (Signal,Signal) -> Lava Simple130nm Signal
circ1 = and2 ->- inv

circ1' (a,b) = do
    c <- and2 (a,b)
    inv c
  -- Same as circ1.

circ2 = halfAdd ->- and2 ->- inv

circLoop = mdo
    a <- label "a" =<< and2 (b,b)
    b <- label "b" =<< inv c
    c <- label "c" =<< and2 (b,a)
    return b
  -- Labels are not needed for definition.

circLoop2 = runLetT $ do
    b  <- free
    c  <- free
    a  <- lift $ label "a" =<< and2 (val b, val b)
    b' <- lift $ label "b" =<< inv (val c)
    c' <- lift $ label "c" =<< and2 (val b, a)
    b === b'
    c === c'
    return b'
  -- Alternative definition using logical variables

circInput :: Signal -> Lava Simple130nm Signal
circInput a = do
    b <- input "b"
    and2 (a,b)



test1 = L.simulateSeq (toLava2000 circ2) L.domain
  -- Simulation using Lava2000.

test2 = simulateSeq circ2 [(0,0),(1,1)]
  -- Simulation in Lava (uses Lava2000 internally).

test3 = verify circ2
  -- Check that output is always high.

test4 = fst $ depth $ circ1 (low,low)
  -- Find logcial depth of circ1.

test5 = fst $ depth circLoop
  -- Error because of combinational loop.

test6 = lookupTag "b" $ fanout circLoop
  -- Find the fanout at node "b". It is perfectly fine to have multiple labels
  -- on the same node, and even to use the same label on multiple places (try).

test7 = lookupTag "b" $ fanout circLoop2
  -- Just to test

test8 = size circLoop
  -- Find number of gates in circLoop.

test9 = simulate circInput 0
  -- Inputs can be defined, but they cause error in simulation.