{-# OPTIONS_GHC -fno-warn-missing-fields #-}

module Lava.Model where



import Control.Applicative
import Control.Arrow ((***))
import Control.Monad.Writer
import Control.Monad.State
import Data.Char
import Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map

import Data.Hardware.Internal

import qualified "chalmers-lava2000" Lava as L



-- | Identifies a driver in the circuit. A driver is either a primary input or
-- an output pin of a cell.
data Signal
       = PrimInpSig PrimInpId
       | CellSig CellId OutPin
     deriving (Eq, Show, Ord)

data Declaration lib
       = PrimInput PrimInpId
       | Cell CellId lib [Signal]
       | Label Tag Signal
     deriving (Eq, Show)

data DesignDB lib = DesignDB
       { cellDB   :: Map CellId (lib,[Signal])
       , fanoutDB :: Map Signal [(CellId,InPin)]
       , sigTagDB :: Map Signal [Tag]
       , tagSigDB :: Map Tag [Signal]
       , primIns  :: [Signal]
       }
     deriving (Eq, Show)
  -- sigTagDB and tagSigDB need only be defined for non-empty values. Use
  -- together with totalLookup. fanoutDB should be defined for all signals (even
  -- ones with no fanout), so that it can be used to list all signals. A
  -- database is valid if the corresponding list of declarations is (*** it
  -- should be possible to reconstruct a list of declarations from a database to
  -- make this well-defined).



class CellLibrary lib
  where
    numIns  :: lib -> InPin
    numOuts :: lib -> OutPin
      -- Number of inputs/outputs of the given cell

    inPinName :: lib -> InPin -> Name
    inPinId   :: lib -> Name  -> InPin

    outPinName :: lib -> OutPin -> Name
    outPinId   :: lib -> Name   -> OutPin

    isFlop :: lib -> Bool
      -- Tells whether or not the given cell is a flipflop.

    lava2000Interp :: Interpretation lib (L.Signal Bool)

  -- Requirements:
  --
  --   * The domain of (inPinName  c) is [0 .. numIns  c - 1]
  --   * The domain of (outPinName c) is [0 .. numOuts c - 1]
  --
  --   * (inPinName  c) is one-to-one, and its inverse is (inPinId  c).
  --   * (outPinName c) is one-to-one, and its inverse is (outPinId c).
  --
  --   * lava2000Interp is a valid interpretation (see definition of
  --     Interpretation). Moreover, the propagator method should constrain all
  --     and only all outputs of each cell.



cellInputs :: CellLibrary lib => CellId -> lib -> [(CellId,InPin)]
cellInputs cid ct = zip (repeat cid) [0 .. numIns ct-1]

cellOutputs :: CellLibrary lib => CellId -> lib -> [Signal]
cellOutputs cid ct = map (CellSig cid) [0 .. numOuts ct-1]



prop_uniquePrimInputs decls = iids == nub iids
  where
    iids = [iid | PrimInput iid <- decls]
  -- Each PrimInput has a uniqe PrimInpId.

prop_uniqueCells decls = cids == nub cids
  where
    cids = [cid | Cell cid _ _ <- decls]
  -- Each Cell has a uniqe CellId.

prop_correctCellInputs decls =
    and [numIns ct == genericLength ss | Cell _ ct ss <- decls]
  -- Each Cell has the correct number of inputs.



prop_validSignals :: CellLibrary lib => [Declaration lib] -> Bool
prop_validSignals decls = all (`elem` validSigs) referred
  where
    primInps  = [PrimInpSig iid | PrimInput iid <- decls]
    cellOuts  = [s | Cell cid ct _ <- decls, s <- cellOutputs cid ct]
    validSigs = primInps ++ cellOuts

    referred
        = concat [ss | Cell _ _ ss <- decls]
              ++ [s  | Label _ s   <- decls]
      -- All signals referred to in the declarations

  -- Checks that all signals referred to by a Cell or Label are valid. The valid
  -- signals are the declared primary inputs and the outputs of declared cells.



prop_validDecls :: CellLibrary lib => [Declaration lib] -> Bool
prop_validDecls decls
     = prop_uniquePrimInputs  decls
    && prop_uniqueCells       decls
    && prop_correctCellInputs decls  -- Correct number of inputs for each cell
    && prop_validSignals      decls  -- No reference to invalid signals

  -- A circuit is always defined in the presence of a cell library. This
  -- property defines what it means for a list of declarations to be valid with
  -- respect to a cell library.
  --
  -- The properties should be fulfilled as long as the requirements of the
  -- CellLibrary class are met and all signals are created using the methods:
  -- input, cell and label.
  --
  -- The only thing that can go wrong is if the number of inputs/outputs
  -- demanded by the type of a cell is different from what is specified by
  -- numIns/numOuts. Difference in the inputs won't be checked at all (and the
  -- only place where it might matter is in the propagator method of an
  -- interpretation). However, difference in the outputs is checked for by
  -- fromListFP (but the error is non-informative).



newtype Lava lib a = Lava
          { unLava :: WriterT [Declaration lib] (State (PrimInpId,CellId)) a }
        deriving (Functor, Applicative, Monad, MonadFix)



runLava :: CellLibrary lib => Lava lib a -> (a, DesignDB lib)
runLava (Lava lava) = (a, DesignDB cDB fDB stDB tsDB ins)
  where
    ((a,decls),_) = runState (runWriterT lava) (0,0)

    cDB  = Map.fromList [ (cid,(ct,ins)) | Cell cid ct ins <- decls ]
    stDB = fmap nub $ Map.fromListWith (++) [ (s,[t]) | Label t s <- decls ]
    tsDB = fmap nub $ Map.fromListWith (++) [ (t,[s]) | Label t s <- decls ]

    fDB = Map.fromListWith (++) $ concat
      [ zip ins (map return $ cellInputs cid ct)
          ++
        zip (cellOutputs cid ct) (repeat [])
          -- Just to make all outputs appear in the map.
        | Cell cid ct ins <- decls
      ]

    ins = [PrimInpSig iid | PrimInput iid <- decls]



class (Monad m, CellLibrary lib) => MonadLava lib m | m -> lib
  where
    newPrimInpId :: m PrimInpId
    newCellId    :: m CellId

    declare :: Declaration lib -> m ()

    listenDecls :: m a -> m (a, [Declaration lib])

    toLava :: m a -> Lava lib a

instance CellLibrary lib => MonadLava lib (Lava lib)
  where
    newPrimInpId = Lava $ do
        (iid,cid) <- get
        put (succ iid, cid)
        return iid

    newCellId = Lava $ do
        (iid,cid) <- get
        put (iid, succ cid)
        return cid

    declare = Lava . tell . return

    listenDecls = Lava . listen . unLava

    toLava = id



inputSig :: MonadLava lib m => m Signal
inputSig = do
    iid <- newPrimInpId
    declare (PrimInput iid)
    return (PrimInpSig iid)
  -- Declare a primary input

cellList :: MonadLava lib m => lib -> [Signal] -> m [Signal]
cellList ct ins = do
    cid <- newCellId
    declare $ Cell cid ct ins
    return (cellOutputs cid ct)
  -- Declare a cell

labelSig :: MonadLava lib m => Tag -> Signal -> m Signal
labelSig tag sig
    | not $ all isAlphaNum tag = error msg
    | otherwise                = declare (Label tag sig) >> return sig
  where
    msg =
      "label: Only alphanumeric characters allowed\n\
      \Offending label: " ++ tag

  -- Declare a label; only side-effect important



data Interpretation lib x = Interp
       { defaultVal  :: x
       , accumulator :: x -> x -> x
       , propagator  :: lib -> ([x] -> [Maybe x])
           -- The lists contain all outputs in pin order and then all inputs in
           -- pin order (pin 0 first).
       }

  -- The number of elements accepted/returned by the propagator should be
  -- (numOuts cell + numIns cell).



type InterpDesignDB lib x = (DesignDB lib, Map Signal x)



lookupTag :: Tag -> InterpDesignDB lib x -> [x]
lookupTag tag (db,sigMap) = map (sigMap Map.!) (tag `totalLookup` tagSigDB db)

depthInterp :: CellLibrary lib => Interpretation lib Int
depthInterp = Interp
    { defaultVal = 0  -- Inputs
    , propagator = prop
    }
  where
    prop ct vals
        | isFlop ct = genericReplicate no (Just 0)     ++ ins
        | otherwise = genericReplicate no (Just (d+1)) ++ ins
      where
        ni  = numIns  ct
        no  = numOuts ct
        ins = genericReplicate ni Nothing
        d   = maximum (0 : genericDrop no vals)
          -- Cells with no inputs will have depth 0+1.