{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE Rank2Types            #-}

module Language.Embedded.Hardware.Interface.AXI (axi_light, AXIPred, FreePrim(..)) where

import Language.Embedded.VHDL (Mode(..))
import Language.Embedded.Hardware.Command.CMD
import Language.Embedded.Hardware.Command.Frontend
import Language.Embedded.Hardware.Interface
import Language.Embedded.Hardware.Expression.Frontend
import Language.Embedded.Hardware.Expression.Represent
import Language.Embedded.Hardware.Expression.Represent.Bit (Bits, Bit, bitFromInteger, ni)

-- hmm...
import Language.Embedded.Hardware.Expression.Syntax (HExp, HType)
import Language.Embedded.Hardware.Expression.Backend.VHDL ()

import Control.Monad.Identity (Identity)
import Control.Monad.Operational.Higher hiding (when)
import Data.Constraint (Constraint)
import Data.Typeable
import Data.Int
import Data.Word
import Data.Bits ()
import Data.Ix (Ix)

import Data.Constraint

import GHC.TypeLits
import qualified GHC.Exts as GHC (Constraint)

import Prelude hiding (not, and, or, div, null)
import qualified Prelude as P

--------------------------------------------------------------------------------
-- * AXI-light Controller.
--------------------------------------------------------------------------------

-- | Make sure that `pred a` implies `PredicateExp exp a`.
class FreeExp exp => FreePrim exp pred
  where
    witPred :: PrimType a => Proxy exp -> Dict (pred a) -> Dict (PredicateExp exp a)

instance FreePrim HExp HType
  where
    witPred _ _ = Dict

litP :: forall exp pred a . (FreePrim exp pred, PrimType a, pred a)
  => Proxy pred -> a -> exp a
litP _ a = case witPred (Proxy :: Proxy exp) (Dict :: Dict (pred a)) of
  Dict -> litE a

--------------------------------------------------------------------------------

-- | Short-hand for programs.
type Prog instr exp pred = Program instr (Param2 exp pred)

-- | Short-hand for constraints.
type AXIPred instr exp pred = (
     -- Instructions.
       SignalCMD      :<: instr
     , ArrayCMD       :<: instr
     , VariableCMD    :<: instr
     , ConditionalCMD :<: instr
     , ProcessCMD     :<: instr
     , LoopCMD        :<: instr
     , ComponentCMD   :<: instr
     , VHDLCMD        :<: instr
     -- Expressions.
     , Expr    exp
     , Rel     exp
     , Factor  exp
     , Primary exp
     -- 
     , FreeExp  exp
     , FreePrim exp pred
     --
     , PredicateExp exp (Bit)
     , PredicateExp exp (Bits 2)
     , PredicateExp exp (Bits 3)
     , PredicateExp exp (Bits 4)
     , PredicateExp exp (Bits 32)
     , PredicateExp exp (Integer)
     --
     , pred (Bit)
     , pred (Bits 2)
     , pred (Bits 3)
     , pred (Bits 4)
     , pred (Bits 32)
     , pred (Integer)
     --
     , Num (exp Integer)
     )

--------------------------------------------------------------------------------
-- ** Signature.
--------------------------------------------------------------------------------

axi_light
  :: forall instr exp pred sig . AXIPred instr exp pred
  => Comp instr exp pred Identity sig
  -> Sig  instr exp pred Identity (
          Signal (Bits 32) -- ^ Write address.
       -> Signal (Bits 3)  -- ^ Write channel protection type.
       -> Signal Bit       -- ^ Write address valid.
       -> Signal Bit       -- ^ Write address ready.
       -> Signal (Bits 32) -- ^ Write data.
       -> Signal (Bits 4)  -- ^ Write strobes.
       -> Signal Bit       -- ^ Write valid.
       -> Signal Bit       -- ^ Write ready.
       -> Signal (Bits 2)  -- ^ Write response.
       -> Signal Bit       -- ^ Write response valid.
       -> Signal Bit       -- ^ Response ready.
       -> Signal (Bits 32) -- ^ Read address.
       -> Signal (Bits 3)  -- ^ Protection type.
       -> Signal Bit       -- ^ Read address valid.
       -> Signal Bit       -- ^ Read address ready.
       -> Signal (Bits 32) -- ^ Read data.
       -> Signal (Bits 2)  -- ^ Read response.
       -> Signal Bit       -- ^ Read valid.
       -> Signal Bit       -- ^ Read ready.    
       -> ()
     )
axi_light comp =
  exactInput  "S_AXI_AWADDR"  $ \s_axi_awaddr  ->
  exactInput  "S_AXI_AWPROT"  $ \s_axi_awprot  ->
  exactInput  "S_AXI_AWVALID" $ \s_axi_awvalid ->
  exactOutput "S_AXI_AWREADY" $ \s_axi_awready ->
  exactInput  "S_AXI_WDATA"   $ \s_axi_wdata   ->
  exactInput  "S_AXI_WSTRB"   $ \s_axi_wstrb   ->
  exactInput  "S_AXI_WVALID"  $ \s_axi_wvalid  ->
  exactOutput "S_AXI_WREADY"  $ \s_axi_wready  ->
  exactOutput "S_AXI_BRESP"   $ \s_axi_bresp   ->
  exactOutput "S_AXI_BVALID"  $ \s_axi_bvalid  ->
  exactInput  "S_AXI_BREADY"  $ \s_axi_bready  ->
  exactInput  "S_AXI_ARADDR"  $ \s_axi_araddr  ->
  exactInput  "S_AXI_ARPROT"  $ \s_axi_arprot  ->
  exactInput  "S_AXI_ARVALID" $ \s_axi_arvalid ->
  exactOutput "S_AXI_ARREADY" $ \s_axi_arready ->
  exactOutput "S_AXI_RDATA"   $ \s_axi_rdata   ->
  exactOutput "S_AXI_RRESP"   $ \s_axi_rresp   ->
  exactOutput "S_AXI_RVALID"  $ \s_axi_rvalid  ->
  exactInput  "S_AXI_RREADY"  $ \s_axi_rready  ->
  ret $ axi_light_impl comp
    s_axi_awaddr s_axi_awprot s_axi_awvalid s_axi_awready
    s_axi_wdata  s_axi_wstrb  s_axi_wvalid  s_axi_wready
    s_axi_bresp  s_axi_bvalid s_axi_bready
    s_axi_araddr s_axi_arprot s_axi_arvalid s_axi_arready s_axi_rdata
    s_axi_rresp  s_axi_rvalid s_axi_rready

--------------------------------------------------------------------------------
-- ** Implementation.
--------------------------------------------------------------------------------

axi_light_impl
  :: forall instr exp pred sig . AXIPred instr exp pred
  -- Component to connect:
  => Comp instr exp pred Identity sig
  -- AXI signals:
  -> Signal (Bits 32) -- ^ Write address.
  -> Signal (Bits 3)  -- ^ Write channel protection type.
  -> Signal Bit       -- ^ Write address valid.
  -> Signal Bit       -- ^ Write address ready.
  -> Signal (Bits 32) -- ^ Write data.
  -> Signal (Bits 4)  -- ^ Write strobes.
  -> Signal Bit       -- ^ Write valid.
  -> Signal Bit       -- ^ Write ready.
  -> Signal (Bits 2)  -- ^ Write response.
  -> Signal Bit       -- ^ Write response valid.
  -> Signal Bit       -- ^ Response ready.
  -> Signal (Bits 32) -- ^ Read address.
  -> Signal (Bits 3)  -- ^ Protection type.
  -> Signal Bit       -- ^ Read address valid.
  -> Signal Bit       -- ^ Read address ready.
  -> Signal (Bits 32) -- ^ Read data.
  -> Signal (Bits 2)  -- ^ Read response.
  -> Signal Bit       -- ^ Read valid.
  -> Signal Bit       -- ^ Read ready.    
  -> Prog instr exp pred ()
axi_light_impl comp
    s_axi_awaddr s_axi_awprot s_axi_awvalid s_axi_awready
    s_axi_wdata  s_axi_wstrb  s_axi_wvalid  s_axi_wready
    s_axi_bresp  s_axi_bvalid s_axi_bready
    s_axi_araddr s_axi_arprot s_axi_arvalid s_axi_arready s_axi_rdata
    s_axi_rresp  s_axi_rvalid s_axi_rready
  = do
       ----------------------------------------
       -- AXI Light signals.
       --
       awaddr  :: Signal (Bits 32) <- newNamedSignal "axi_awaddr"
       awready :: Signal (Bit)     <- newNamedSignal "axi_awready"
       wready  :: Signal (Bit)     <- newNamedSignal "axi_wready"
       bresp   :: Signal (Bits 2)  <- newNamedSignal "axi_bresp"
       bvalid  :: Signal (Bit)     <- newNamedSignal "axi_bvalid"
       araddr  :: Signal (Bits 32) <- newNamedSignal "axi_araddr"
       arready :: Signal (Bit)     <- newNamedSignal "axi_arready"
       rdata   :: Signal (Bits 32) <- newNamedSignal "axi_rdata"
       rresp   :: Signal (Bits 2)  <- newNamedSignal "axi_rresp"
       rvalid  :: Signal (Bit)     <- newNamedSignal "axi_rvalid"

       ----------------------------------------
       -- Signals for user logic registers.
       --
       reg_rden  :: Signal (Bit)     <- newNamedSignal "slv_reg_rden"
       reg_wren  :: Signal (Bit)     <- newNamedSignal "slv_reg_wren"
       reg_out   :: Signal (Bits 32) <- newNamedSignal "reg_data_out"
       reg_index :: Signal (Integer) <- newNamedSignal "byte_index"
       registers <- declareRegisters (signatureOf comp)

       ----------------------------------------
       -- Short-hands for ...
       --
       -- > reset all input registers.
       let mReset  = resetInputs  (signatureOf comp) registers
       -- > reload all input registers.
       let mReload = reloadInputs (signatureOf comp) registers
       -- > fetch the names of all input registers.
       let mInputs = identInputs  (signatureOf comp) registers
       -- > fetch the names of all output registers.
       let mOutputs = identOutputs (signatureOf comp) registers
       -- > write to output.
       let mWrite :: Prog instr exp pred ()
           mWrite = loadOutputs araddr reg_out
             (addr_lsb) (addr_bits)         -- sizes.
             (signatureOf comp) (registers) -- sig and args.
       -- > read from input.
       let mRead :: Prog instr exp pred ()
           mRead = loadInputs awaddr reg_wren s_axi_wdata s_axi_wstrb
             (addr_lsb) (addr_bits)         -- sizes.
             (signatureOf comp) (registers) -- sig and args.
       
       ----------------------------------------
       -- I/O Connections.
       --
       s_axi_awready <=- awready
       s_axi_wready  <=- wready
       s_axi_bresp   <=- bresp
       s_axi_bvalid  <=- bvalid
       s_axi_arready <=- arready
       s_axi_rdata   <=- rdata
       s_axi_rresp   <=- rresp
       s_axi_rvalid  <=- rvalid

       ----------------------------------------
       -- Mem. mapped register select and write
       -- logic generation.
       --
       u_wr  <- unsafeFreezeSignal wready
       u_wv  <- unsafeFreezeSignal s_axi_wvalid
       u_awr <- unsafeFreezeSignal awready
       u_awv <- unsafeFreezeSignal s_axi_awvalid
       setSignal reg_wren
         (u_wr `and` u_wv `and` u_awr `and` u_awv)

       ----------------------------------------
       -- Mem. mapped register select and read
       -- logic generation.
       --
       u_arr <- unsafeFreezeSignal arready
       u_arv <- unsafeFreezeSignal s_axi_arvalid
       u_rv  <- unsafeFreezeSignal rvalid
       setSignal reg_rden
         (u_arr `and` u_arv `and` not u_rv)

       ----------------------------------------
       -- AXI_AWREADY generation.
       --
       -- processR s_axi_aclk s_axi_aresetn []
       processR []
         (do awready <== low)
         (do rdy <- unsafeFreezeSignal awready
             awv <- unsafeFreezeSignal s_axi_awvalid
             wv  <- unsafeFreezeSignal s_axi_wvalid
             iff (isLow rdy `and` isHigh awv `and` isHigh wv)
               (do awready <== high)
               (do awready <== low))
       
       ----------------------------------------
       -- AXI_AWADDR latching.
       --
       processR []
         (do awaddr <== zeroes)
         (do rdy <- unsafeFreezeSignal awready
             awv <- unsafeFreezeSignal s_axi_awvalid
             wv  <- unsafeFreezeSignal s_axi_wvalid
             when (isLow  rdy `and` isHigh awv `and` isHigh wv)
               (do awaddr <=- s_axi_awaddr))

       ----------------------------------------
       -- AXI_WREADY generation.
       --
       processR []
         (do wready <== low)
         (do rdy <- unsafeFreezeSignal awready
             awv <- unsafeFreezeSignal s_axi_awvalid
             wv  <- unsafeFreezeSignal s_axi_wvalid
             iff (isLow  rdy `and` isHigh wv `and` isHigh awv)
               (do wready <== high)
               (do wready <== low))

       ----------------------------------------
       -- Slave register logic.
       --
       processR [] (mReset) (mRead)
       
       ----------------------------------------
       -- Write response logic.
       --
       processR []
         (do bvalid <== low
             bresp  <== zeroes)
         (do awr <- unsafeFreezeSignal awready
             awv <- unsafeFreezeSignal s_axi_awvalid
             wr  <- unsafeFreezeSignal wready
             wv  <- unsafeFreezeSignal s_axi_wvalid
             bv  <- unsafeFreezeSignal bvalid
             br  <- unsafeFreezeSignal s_axi_bready
             ifE ( isHigh awr `and`
                   isHigh awv `and`
                   isHigh wr  `and`
                   isHigh wv  `and`
                   isLow bv
                 , do bvalid <== high
                      bresp  <== zeroes)
                 ( isHigh br  `and`
                   isHigh bv
                 , do bvalid <== low))

       ----------------------------------------
       -- AXI_AWREADY generation.
       --
       processR []
         (do arready <== low
             araddr  <== ones)
         (do arr <- unsafeFreezeSignal arready
             arv <- unsafeFreezeSignal s_axi_arvalid
             iff (isLow arr `and` isHigh arv)
               (do arready <== high
                   araddr  <=- s_axi_araddr)
               (do arready <== low))

       ----------------------------------------
       -- AXI_ARVALID generation.
       --
       processR []
         (do rvalid <== low
             rresp  <== zeroes)
         (do arr <- unsafeFreezeSignal arready
             arv <- unsafeFreezeSignal s_axi_arvalid
             rv  <- unsafeFreezeSignal rvalid
             rr  <- unsafeFreezeSignal s_axi_rready
             ifE ( isHigh arr `and` isHigh arv `and` isLow rv
                 , do rvalid <== high
                      rresp  <== zeroes)
                 ( isHigh rv `and` isHigh rr
                 , do rvalid <== low))

       ----------------------------------------
       -- Memory mapped rigister select and
       -- read logic generaiton.
       --
       process (araddr .: mOutputs) (mWrite)

       ----------------------------------------
       -- Output register of memory read data.
       --
       processR []
         (do rdata <== zeroes)
         (do rden <- unsafeFreezeSignal reg_rden
             when (isHigh rden)
               (do rdata <=- reg_out))

       ----------------------------------------
       -- User logic.
       --
       portmap comp registers
       --
       -- The end.
       ----------------------------------------
  where
    -- Application-specific design signals. The first depends on the bus width,
    -- the second on the number of bits needed to store an address. There's no
    -- '+ 1' on 'addr_bits' since the ranges add that by default (i.e. '0 to 0'
    -- contains one element).
    addr_lsb, addr_bits :: Integer
    addr_lsb  = 2 -- always '2' for a 32-bit bus.
    addr_bits = bits (widthOf comp) - 1
      where
        bits :: Integer -> Integer
        bits 0 = 1
        bits 1 = 1
        bits x = floor $ (1+) $ logBase 2.0 $ fromIntegral x

    -- AXI-lite constants.
    axi_data_width, axi_addr_width :: Integer
    axi_data_width = 32 -- always use 32-bit wide busses for AXI-lite.
    axi_addr_width = addr_lsb + addr_bits + 1 -- added one for consistency.

--------------------------------------------------------------------------------
-- ** Helpers.
--------------------------------------------------------------------------------

-- | Declare the registers which will be used by our AXI-lite slave to store
--   values received from the master and, once filled, as input for the comp.
declareRegisters :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred
  => Sig  instr exp pred Identity a
  -> Prog instr exp pred (Argument pred a)
declareRegisters (Ret _) = return Nil
declareRegisters (SSig _ _ sf) =
  do s <- newSignal
     a <- declareRegisters (sf s)
     return (ASig s a)
declareRegisters (SArr _ _ l af) =
  do s <- newArray (litP (Proxy :: Proxy pred) l)
     a <- declareRegisters (af s)
     return (AArr s a)

--------------------------------------------------------------------------------

-- | Reset the input registers.
resetInputs :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred
  => Sig  instr exp pred Identity a
  -> Argument pred a
  -> Prog instr exp pred ()
resetInputs (Ret _)           (Nil)        = return ()
resetInputs (SSig _ Out   sf) (ASig s arg) = resetInputs (sf s) arg
resetInputs (SArr _ Out _ af) (AArr a arg) = resetInputs (af a) arg
resetInputs (SSig _ In    sf) (ASig s arg) =
  do setSignal s (litP (Proxy :: Proxy pred) reset)
     resetInputs (sf s) arg
resetInputs (SArr _ In  _ af) (AArr a arg) =
  do resetArray a (litP (Proxy :: Proxy pred) reset)
     resetInputs (af a) arg

--------------------------------------------------------------------------------

-- | Reset the input registers to their previous values.
reloadInputs :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred
  => Sig  instr exp pred Identity a
  -> Argument pred a
  -> Prog instr exp pred ()
reloadInputs (Ret _)           (Nil)        = return ()
reloadInputs (SSig _ Out   sf) (ASig s arg) = reloadInputs (sf s) arg
reloadInputs (SArr _ Out _ af) (AArr a arg) = reloadInputs (af a) arg
reloadInputs (SSig _ In    sf) (ASig (s :: Signal b) arg) =
  case witPred (Proxy :: Proxy exp) (Dict :: Dict (pred b)) of
    Dict -> do
      sv <- unsafeFreezeSignal s
      setSignal s sv
      reloadInputs (sf s) arg
reloadInputs (SArr _ In  l af) (AArr a arg) =
  do copyArray (a, lit 0) (a, lit 0) (lit $ l - 1)
     reloadInputs (af a) arg
  where
    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

--------------------------------------------------------------------------------

-- | ...
loadInputs :: forall instr (exp :: * -> *) pred a . AXIPred instr exp pred
  => Signal   (Bits 32) -- ^ Address.
  -> Signal   (Bit)     -- ^ Ready.
  -> Signal   (Bits 32) -- ^ Input.
  -> Signal   (Bits 4)  -- ^ Protected bits.
  -> Integer            -- ^ Address lsb.
  -> Integer            -- ^ Address width.
  -> Sig instr exp pred Identity a
  -> Argument pred a
  -> Prog instr exp pred ()
loadInputs waddr rwren wdata wren addr_lsb addr_bits sig arg =
  do loc   <- getBits waddr (lit addr_lsb) (lit $ addr_bits - 1)
     ready <- unsafeFreezeSignal rwren
     when (isHigh ready) $
       switched loc
         (cases 0 sig arg)
         (reloadInputs sig arg)
  where
    cases :: Integer
          -> Sig instr exp pred Identity b
          -> Argument pred b
          -> [When Integer (Prog instr exp pred)]
    cases ix (Ret _)         (Nil)        = []
    cases ix (SSig _ Out   sf) (ASig s arg) = cases (ix + 1)             (sf s) arg
    cases ix (SArr _ Out l af) (AArr a arg) = cases (ix + P.toInteger l) (af a) arg
    cases ix (SSig _ In    sf) (ASig s arg) =
      let new = is (ix) (loadInputSignal wdata wren s)
       in new : cases (ix + 1) (sf s) arg
    cases ix (SArr _ In  l af) (AArr a arg) =
      let len = P.toInteger l
          new = map (\(i, j) -> is i (loadInputArray wdata wren a j)) $ zip [ix..ix+len-1] [0..]
       in new ++ cases (ix + len) (af a) arg

    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

loadInputSignal :: forall instr (exp :: * -> *) pred a .
     (AXIPred instr exp pred, pred a, Sized a)
  => Signal (Bits 32)
  -> Signal (Bits 4)
  -> Signal a
  -> Prog instr exp pred ()
loadInputSignal wdata wren reg = for 0 size $ \byte_index ->
  do bit <- getBit wren byte_index
     when (isHigh bit) $
       copyBits (reg, byte_index*8) (wdata, byte_index*8) (lit 7)
  where
    size :: exp Integer
    size = lit $ (P.div (bits reg) 8) - 1
    -- todo: I assume that `a` has a type \width\ that is some multiple of eight.

    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

loadInputArray :: forall instr (exp :: * -> * ) pred i a .
     (AXIPred instr exp pred, pred a, Sized a)
  => Signal (Bits 32)
  -> Signal (Bits 4)
  -> Array a
  -> Integer
  -> Prog instr exp pred ()
loadInputArray wdata wren arr ix = for 0 size $ \byte_index ->
  do bit <- getBit wren byte_index
     when (isHigh bit) $
       copyABits (arr, byte_index*8, lit ix) (wdata, byte_index*8) (lit 7)
  where
    size :: exp Integer
    size = lit $ (P.div (bits arr) 8) - 1
    -- todo: I assume that `a` has a type \width\ that is some multiple of eight.

    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

--------------------------------------------------------------------------------

-- | ...
loadOutputs :: forall instr (exp :: * -> *) pred a . AXIPred instr exp pred
  => Signal (Bits 32) -- ^ Address.
  -> Signal (Bits 32) -- ^ Output.
  -> Integer          -- ^ Address lsb.
  -> Integer          -- ^ Address width.
  -> Sig instr exp pred Identity a
  -> Argument pred a
  -> Prog instr exp pred ()
loadOutputs araddr rout addr_lsb addr_bits sig arg =
  do loc <- getBits araddr (lit addr_lsb) (lit $ addr_bits - 1)
     switched loc
       (cases 0 sig arg)
       (resetOut)
  where
    cases :: Integer
          -> Sig instr exp pred Identity b
          -> Argument pred b
          -> [When Integer (Prog instr exp pred)]
-- todo: due to a bug in the Xilinx tools I use (Vivado 2015.4), we cannot skip
-- any cases. So even if a signal is tagged as an input singal, it must be
-- part of the generated case statement to avoid holes. That is, we can't have:
--    cases ix (Ret _) (Nil) = []
--    cases ix (SSig _ In    sf) (ASig s arg) = cases (ix + 1)             (sf s) arg
--    cases ix (SArr _ In  l af) (AArr a arg) = cases (ix + P.toInteger l) (af a) arg
    cases ix (Ret _) (Nil)
      | ix < addr_max = to ix addr_max (resetOut) : []
      | otherwise     = []
    cases ix (SSig _ In    sf) (ASig s arg) =
      is ix (resetOut) : cases (ix + 1) (sf s) arg
    cases ix (SArr _ In  l af) (AArr a arg) = let len = P.toInteger l in
      to ix (ix + len - 1) (resetOut) : cases (ix + len) (af a) arg
    cases ix (SSig _ Out   sf) (ASig s arg) =
      let new = is ix (loadOutputSignal rout s)
       in new : cases (ix + 1) (sf s) arg
    cases ix (SArr _ Out l af) (AArr a arg) =
      let len = P.toInteger l
          new = map (\(i, j) -> is i (loadOutputArray rout a j)) $ zip [ix..ix+len-1] [0..]
       in new ++ cases (ix + len) (af a) arg

    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

    addr_max :: Integer
    addr_max = addr_bits ^ 2 - 1

    resetOut :: Prog instr exp pred ()
    resetOut = setSignal rout (lit reset)

loadOutputSignal :: forall instr (exp :: * -> *) pred a .
     (AXIPred instr exp pred, pred a, PrimType a, Integral a)
  => Signal (Bits 32)
  -> Signal a
  -> Prog instr exp pred ()
loadOutputSignal rout reg =
  case witPred (Proxy :: Proxy exp) (Dict :: Dict (pred a)) of
    Dict -> do
      r <- unsafeFreezeSignal reg
      setSignal rout (toBits r :: exp (Bits 32))

loadOutputArray :: forall instr (exp :: * -> *) pred a .
     ( AXIPred instr exp pred, pred a, PrimType a, Integral a)
  => Signal (Bits 32)
  -> Array a
  -> Integer
  -> Prog instr exp pred ()
loadOutputArray rout arr ix =
  case witPred (Proxy :: Proxy exp) (Dict :: Dict (pred a)) of
    Dict -> do
      r <- getArray arr (lit $ P.fromInteger ix)
      setSignal rout (toBits r :: exp (Bits 32))
  where
    lit :: (FreePrim exp pred, PrimType b, pred b) => b -> exp b
    lit = litP (Proxy :: Proxy pred)

--------------------------------------------------------------------------------

identInputs :: forall instr (exp :: * -> *) pred m a .
     Sig instr exp pred m a
  -> Argument pred a
  -> [Ident]
identInputs (Ret _)          (Nil)        = []
identInputs (SSig _ In sf)   (ASig s arg) = toIdent s : identInputs (sf s) arg
identInputs (SSig _ _  sf)   (ASig s arg) = identInputs (sf s) arg
identInputs (SArr _ In _ af) (AArr a arg) = toIdent a : identInputs (af a) arg
identInputs (SArr _ _  _ af) (AArr a arg) = identInputs (af a) arg

identOutputs :: forall instr (exp :: * -> *) pred m a .
     Sig instr exp pred m a
  -> Argument pred a
  -> [Ident]
identOutputs (Ret _) (Nil) = []
identOutputs (SSig _ Out sf)   (ASig s arg) = toIdent s : identOutputs (sf s) arg
identOutputs (SSig _ _   sf)   (ASig s arg) = identOutputs (sf s) arg
identOutputs (SArr _ Out _ af) (AArr a arg) = toIdent a : identOutputs (af a) arg
identOutputs (SArr _ _   _ af) (AArr a arg) = identOutputs (af a) arg

--------------------------------------------------------------------------------

signatureOf
  :: Comp instr exp pred m sig
  -> Sig  instr exp pred m sig
signatureOf (Component _ _ sig) = sig

widthOf
  :: Comp instr exp pred m sig
  -> Integer
widthOf comp = go (signatureOf comp)
  where
    go :: Sig instr exp pred m b -> Integer
    go (Ret _)        = 0
    go (SSig _ _ f)   = 1             + go (f dummy)
    go (SArr _ _ l g) = P.toInteger l + go (g dummy)

dummy :: a
dummy = error "todo: evaluated dummy"

high, low :: Expr exp => exp Bit
high = true
low  = false

isHigh, isLow :: (Expr exp, Rel exp) => exp Bit -> exp Bit
isHigh e = e `eq` high
isLow  e = e `eq` low

zeroes :: (Primary exp, Typeable n, KnownNat n) => exp (Bits n)
zeroes = value 0

ones :: forall exp n. (Primary exp, Typeable n, KnownNat n) => exp (Bits n)
ones = value $ bitFromInteger (2 ^ size - 1)
  where size = fromIntegral (ni (Proxy::Proxy n))

--------------------------------------------------------------------------------