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

module Lava.Model where



import Control.Monad.Writer
import Control.Monad.State
import Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map

import Data.Hardware.Internal

import qualified Lava2000 as L



data Signal
       = Constant   ConstId
       | PrimInpSig PrimInpId
       | CellSig    CellId Pin
           -- The pins of a cell are numbered consequtively from 0, starting
           -- with the outputs.
     deriving (Eq, Show, Ord)

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

data DesignDB lib = DesignDB
       { inputDB  :: Map PrimInpId Name
       , cellDB   :: Map CellId (lib,[Signal])
       , fanoutDB :: Map Signal [Signal]
       , tagDB    :: Map Tag [Signal]
       }
     deriving (Eq, Show)
  -- fanoutDB and tagDB need only be defined if the value is non-empty. Use
  -- together with totalLookup. 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
    numConsts :: TypeOf lib -> ConstId
      -- Only used for specifying valid circuits (see prop_validDecls).

    numIns  :: lib -> Int
    numOuts :: lib -> Int
      -- Number of inputs/outputs of the given cell

    pinName :: lib -> Pin  -> Name
    pinId   :: lib -> Name -> Pin

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

    lava2000Interp :: Interpretation lib (L.Signal Bool)

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



libraryConstants :: CellLibrary lib => TypeOf lib -> [Signal]
libraryConstants t = map Constant [0 .. numConsts t-1]

cellInputs :: CellLibrary lib => CellId -> lib -> [Signal]
cellInputs cid ct = map (CellSig cid) [no .. no+ni]
  where
    no = icast (numOuts ct)
    ni = icast (numIns  ct)

cellOutputs :: CellLibrary lib => CellId -> lib -> [Signal]
cellOutputs cid ct = map (CellSig cid) [0 .. icast (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 == length ss | Cell _ ct ss <- decls]
  -- Each Cell has the correct number of inputs.



prop_validSignals :: forall lib . 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 = libraryConstants (T::TypeOf lib) ++ 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 constants defined by the library, the declared primary
  -- inputs and the *outputs* of declared cells. It is not allowed to refer to
  -- cell inputs.



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:
  -- libraryConstants, 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 (Monad, MonadFix)



runLava :: CellLibrary lib => Lava lib a -> (a, DesignDB lib)
runLava (Lava lava) = (a, makeDesignDB decls)
  where
    ((a,decls),_) = runState (runWriterT lava) (0,0)

    fanouts decls = Map.fromListWith (++) $ concat
        [ zip ins (map return $ cellInputs cid ct) | Cell cid ct ins <- decls ]

    makeDesignDB decls = DesignDB iDB cDB (fanouts decls) tDB
      where
        iDB = Map.fromList          [(iid,nm)       | PrimInput iid nm <- decls]
        cDB = Map.fromList          [(cid,(ct,ins)) | Cell cid ct ins  <- decls]
        tDB = Map.fromListWith (++) [(tag,[sig])    | Label tag sig    <- 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])

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



inputSig :: MonadLava lib m => Name -> m Signal
inputSig nm = do
    iid <- newPrimInpId
    declare $ PrimInput iid nm
    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 = declare (Label tag sig) >> return sig
  -- Declare a label; only side-effect important



data Interpretation lib x = Interp
       { constants   :: [x]
       , defaultVal  :: x
       , accumulator :: x -> x -> x
       , propagator  :: lib -> ([x] -> [Maybe x])
           -- The value of pin p appears at position p in the lists (i.e.
           -- outputs first).
       }

  -- Requirements:
  --
  --   * The length of the constant list is (numConsts (T::TypeOf lib)).
  --
  --   * The number of elements accepted/returned by the propagator is
  --     (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` tagDB db)

depthInterp :: forall lib . CellLibrary lib => Interpretation lib Int
depthInterp = Interp
    { constants  = replicate (icast $ numConsts (T::TypeOf lib)) 0
    , propagator = prop
    }
  where
    prop ct vals
        | isFlop ct = replicate no (Just 0)     ++ ins
        | otherwise = replicate no (Just (d+1)) ++ ins
      where
        ni  = numIns  ct
        no  = numOuts ct
        ins = replicate ni Nothing
        d   = maximum (drop no vals)