import Lava
import Lava.Patterns
import Libs.Nangate45.Lava
import Analysis.Timing

import qualified Lava2000 as L

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



circ1 :: (Signal,Signal) -> Lava Nangate45 Signal
circ1 = and2_x1 ->- inv_x1

circ1' (a,b) = do
    c <- and2_x1 (a,b)
    inv_x1 c
  -- Same as circ1.

circ2 :: (Signal,Signal) -> Lava Nangate45 Signal
circ2 = ha_x1 ->- and2_x1 ->- inv_x1

circLoop :: Lava Nangate45 Signal
circLoop = mdo
    a <- label "a" =<< and2_x1 (b,b)
    b <- label "b" =<< inv_x1 c
    c <- label "c" =<< and2_x1 (b,a)
    return b
  -- Labels are not needed for definition.

circLoop2 :: Lava Nangate45 Signal
circLoop2 = runLetT $ do
    b  <- free
    c  <- free
    a  <- lift $ label "a" =<< and2_x1 (val b, val b)
    b' <- lift $ label "b" =<< inv_x1 (val c)
    c' <- lift $ label "c" =<< and2_x1 (val b, a)
    b === b'
    c === c'
    return b'
  -- Alternative definition using logical variables

circInput :: Signal -> Lava Nangate45 Signal
circInput a = do
    b <- input
    and2_x1 (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 =<< input
  -- 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.

test10 = fst $ analyzeTiming $ circ1 =<< input
  -- Timing analysis without wires.