-- exhibiting hdl failure under clash 1.8.1. (works fine under 1.6.4)
-- PTB Dec 2023

-- 1.6.4:
-- time clash -XCPP -fconstraint-solver-iterations=0 -package silently \
--   -fclash-no-render-enums -fclash-spec-limit=80 -fclash-inline-limit=80 \
--   -freduction-depth=400 -fclash-clear --verilog Test.hs
-- GHC: Setting up GHC took: 1.059s
-- GHC: Compiling and loading modules took: 1.801s
-- Clash: Parsing and compiling primitives took 0.305s
-- GHC+Clash: Loading modules cumulatively took 3.626s
-- Clash: Compiling Test.tacache_server32
-- Clash: Normalization took 0.507s
-- Clash: Netlist generation took 0.015s
-- Clash: Compiling Test.tacache_server32 took 0.653s
-- Clash: Total compilation took 4.280s
-- 3.458u 0.794s 0:04.57 92.7%     0+0k 528264+976io 677pf+0w

-- 1.8.1:
-- time clash -XCPP -fconstraint-solver-iterations=0 -package silently \
--   -fclash-no-render-enums -fclash-spec-limit=80 -fclash-inline-limit=80 \
--   -freduction-depth=400 -f clash-clear --verilog Test.hs
-- GHC: Setting up GHC took: 0.989s
-- GHC: Compiling and loading modules took: 1.895s
-- Clash: Parsing and compiling primitives took 0.318s
-- GHC+Clash: Loading modules cumulatively took 3.807s
-- Clash: Compiling Test.tacache_server32
-- Clash: Normalization took 0.368s
-- <no location info>: error:
-- Clash error call:
--  Clash.Netlist(1041): Under-applied constructor Product
--  "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe"
--  [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[
--  Product "GHC.Tuple.(,)" Nothing [Signed 126,SP "GHC.Maybe.Maybe"
--  [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Signed 32])]]])]),Signed 126]
--      
--  Applied args:
--  [Identifier (RawIdentifier "result_7" Nothing []) (Just (Indexed
--  (Product "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe"
--  [("GHC.Maybe.Nothing",[]), ("GHC.Maybe.Just",[Product "GHC.Tuple.(,)"
--  Nothing [Signed 126,SP "GHC.Maybe.Maybe" [("GHC.Maybe.Nothing",[]),
--  ("GHC.Maybe.Just",[Signed 32])]]])]),Sum "GHC.Maybe.Maybe"
--  ["GHC.Maybe.Nothing","GHC.Maybe.Just"]],0,0)))]
--                  
--  Function args:
--  (Product "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe"
--  [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Product
--  "GHC.Tuple.(,)" Nothing [Signed 126,SP "GHC.Maybe.Maybe"
--  [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Signed 32])]]])]),
--  Signed 126],Name {nameSort = User, nameOcc = "GHC.Tuple.(,)", ...
--  ...
--  CallStack (from HasCallStack):
--    error, called at src/Clash/Netlist.hs:1041:17 in
--    clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist
--    mkDcApplication, called at src/Clash/Netlist.hs:863:16 in
--    clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist
--    mkExpr, called at src/Clash/Netlist.hs:508:31 in
--    clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist
--    3.913u 0.599s 0:04.52 99.5%     0+0k 0+896io 0pf+0w

module Test
  where

import Clash.Prelude
import Control.Monad.State

-- frontend part of a memoizing cache for a TLB (translation lookaside buffer)
-- acting as three-way intermediate collating user and cache and TLB data
--
-- inputs
-- user  port A for translation requests accessing memoized data
-- user  port B for invalidate memoized translation commands
-- tlb   port  C for weak invalidate memoized translation commands from the TLB 
-- tlb   port  D for weak translation info to be memoized snooped from the TLB
-- cache port A for cacheline from cache holding translate data for req A
-- cache port B for cacheline from cache holding translate data for cmd B
-- cache port C for cacheline from cache holding translate data for cmd C
--
-- outputs
-- user  port A replying to translation requests A with translation data
-- cache port A1 for returning a modified cacheline
-- cache port A2 for returning a modified cacheline (may need 2 at once)
-- cache port B requesting cacheline containing invalid data B
-- cache port C requesting cacheline containing invalid data C
-- cache port D requesting cacheline to hold translated data D

{-# ANN tacache_server32
  (Synthesize { t_name   = "TACacheServer"
              , t_inputs = [ PortName "dr"        -- user A
                           , PortName "dx"        -- user B
                           , PortName "d_x"       -- tlb C
                           , PortName "dw"        -- tlb D
                           , PortName "outs1"     -- cache A
                           , PortName "outs2"     -- cache B
                           , PortName "outs3"     -- cache C
                           ]
              , t_output = PortProduct ""
                             [ PortName "dr_"     -- user A
                             , PortName "wins1"   -- cache A1
                             , PortName "wins2"   -- cache A2
                             , PortName "rins0"   -- cache B
                             , PortName "rins1"   -- cache C
                             , PortName "rins2"   -- cache D
                             ]
              }) #-}

-- for definiteness
type IDX  = Signed 6
type TAG  = Signed 126
-- 6+126 = 132
type Cxdr = Signed 132
type Addr = Signed 32

{-# NOINLINE tacache_server32 #-}
tacache_server32
  :: ( HiddenClockResetEnable System)
   => Signal System (Maybe Cxdr) -- input frnt rd addr req to server
   -> Signal System (Maybe Cxdr) -- input frnt inval addr rq to srvr
   -> Signal System (Maybe Cxdr) -- input back/weak inval rq to srvr
   -> Signal System (Maybe (Cxdr,Addr)) -- back/weak wr rq to srvr
   -> Signal System (Maybe (IDX,CacheLine 0 TAG Addr))
   -> Signal System (Maybe (IDX,CacheLine 0 TAG Addr))
   -> Signal System (Maybe (IDX,CacheLine 0 TAG Addr))
   -> ( Signal System (Maybe Addr) -- output from srvr (rd memoized)
      , Signal System (Maybe(IDX,CacheLine 0 TAG Addr))
      , Signal System (Maybe(IDX,CacheLine 0 TAG Addr))
      , Signal System (Maybe IDX)
      , Signal System (Maybe IDX)
      , Signal System (Maybe IDX)
      )
tacache_server32 = tacache_server'
  where 
  tacache_server'
   :: forall (dom::Domain) (m::Nat) (n::Nat) (p::Nat) (q::Nat)
            cxdr addr idx tag
   . ( HiddenClockResetEnable dom
     , KnownNat q, KnownNat n, KnownNat m, KnownNat p
     , n <= p
     , cxdr ~ Signed p
     , addr ~ Signed q
     , idx  ~ Signed n
     , tag  ~ Signed (p-n)
     , p ~ 132
     , q ~ 32
     , n ~ 6
     , m ~ 0
     )
   -- SNat n                         -- 2^n lines
   -- SNat m                         -- of 2^m entries each
   => Signal dom (Maybe cxdr)        -- input frnt read addr req to server
   -> Signal dom (Maybe cxdr)        -- input frnt invalidate addr req to server
   -> Signal dom (Maybe cxdr)        -- input back/weak invalidate req to server
   -> Signal dom (Maybe (cxdr,addr)) -- input back/weak write req to server
   -> Signal dom (Maybe (idx,CacheLine m tag addr))
   -> Signal dom (Maybe (idx,CacheLine m tag addr))
   -> Signal dom (Maybe (idx,CacheLine m tag addr))
   -> ( Signal dom (Maybe addr)        -- output from server (rd memoized)
      , Signal dom (Maybe(idx,CacheLine m tag addr))
      , Signal dom (Maybe(idx,CacheLine m tag addr))
      , Signal dom (Maybe idx)
      , Signal dom (Maybe idx)
      , Signal dom (Maybe idx)
      )
  tacache_server' = tacache_server n m
    where
    n = SNat :: SNat n -- 2^n (64) lines
    m = SNat :: SNat m -- 2^m (1) tags per line

-- idx cacheline entries are Just(tag,Just addr) to translate idx++tag->addr
--                       and Just(tag,Nothing) for invalidated idx++tag entry
--                       and Nothing for no entry there
type CacheLine m tag addr                    -- 2^m tags per line, 2^n lines
               = Vec (2^m) (Maybe(tag,Maybe addr))

{-# NOINLINE tacache_server #-}
tacache_server
   :: forall (dom::Domain) (m::Nat) (n::Nat) (p::Nat) (q::Nat)
            cxdr  -- cache key
            addr  -- cache data
            idx   -- cacheline index (which cacheline)
            tag   -- cacheline tag   (identifier for search in cacheline)
   . ( HiddenClockResetEnable dom
     , KnownNat q, KnownNat n, KnownNat m, KnownNat p
     , n <= p
     , cxdr ~ Signed p
     , addr ~ Signed q
     , idx  ~ Signed n
     , tag  ~ Signed (p-n)
--   , p ~ 132
--   , q ~ 32
     )
   => SNat n                         -- 2^n cachelines
   -> SNat m                         -- of 2^m entries each
   -> Signal dom (Maybe cxdr)        -- input frnt read addr req to server
   -> Signal dom (Maybe cxdr)        -- input frnt invalidate addr req to server
   -> Signal dom (Maybe cxdr)        -- input back/weak invalidate req to server
   -> Signal dom (Maybe (cxdr,addr)) -- input back/weak write req to server
   -> Signal dom (Maybe (idx,CacheLine m tag addr)) -- cacheline in from cache
   -> Signal dom (Maybe (idx,CacheLine m tag addr)) -- cacheline in from cache
   -> Signal dom (Maybe (idx,CacheLine m tag addr)) -- cacheline in from cache
   -> ( Signal dom (Maybe addr)      -- output read reply (memoized data)
      , Signal dom (Maybe(idx,CacheLine m tag addr)) -- cacheline out to cache
      , Signal dom (Maybe(idx,CacheLine m tag addr)) -- cacheline out to cache
      , Signal dom (Maybe idx)                       -- cacheline req to cache
      , Signal dom (Maybe idx)                       -- cacheline req to cache
      , Signal dom (Maybe idx)                       -- cacheline req to cache
      )
tacache_server n m dr dx d_x dw outs0 outs1 outs2 =
                        (dr',wins1,wins2,rins0,rins1,rins2)
  where
  (dr',wins1,wins2,rins0,rins1,rins2) =
    unbundle $ mealy (tacache_server_step n m) def
             $ bundle(dr,dx,d_x,dw,outs0,outs1,outs2)


tacache_server_step
   :: forall (m::Nat) (n::Nat) (p::Nat) (q::Nat)
            cxdr addr idx tag s
   . ( KnownNat q, KnownNat n, KnownNat m, KnownNat p
     , n <= p
     , cxdr ~ Signed p
     , addr ~ Signed q
     , idx  ~ Signed n
     , tag  ~ Signed (p-n)
     , s    ~ ()                     -- nonexistent state for fake mealy machine
--   , p ~ 132
--   , q ~ 32
     )
   => SNat n                         -- 2^n lines
   -> SNat m                         -- of 2^m entries each
   -> s
   -> ( Maybe cxdr        -- input frnt read addr req to server
      , Maybe cxdr        -- input frnt invalidate addr req to server
      , Maybe cxdr        -- input back/weak invalidate req to server
      , Maybe (cxdr,addr) -- input back/weak write req to server
      , Maybe (idx,CacheLine m tag addr)
      , Maybe (idx,CacheLine m tag addr)
      , Maybe (idx,CacheLine m tag addr)
      )
   -> ( s
      , ( Maybe addr        -- output from server (rd memoized)
        , Maybe(idx,CacheLine m tag addr)
        , Maybe(idx,CacheLine m tag addr)
        , Maybe idx
        , Maybe idx
        , Maybe idx
        )
      )
tacache_server_step n m s (dr,dx,d_x,dw,out0,out1,out2) =
     (s', (dr',win1,win2,rin0,rin1,rin2))

  where 
      s' :: ()
      s' = s

      dr' :: Maybe addr
      dr' = f (dr,out0) -- no delay dr as checks for match here
             where f :: (Maybe cxdr,Maybe(idx,CacheLine m tag addr))
                     -> Maybe addr
                   f (Just x,Just (idx',v)) = 
                     let (idx,tag) = tacache_split_cxdr x
                         (_,ma) = tazcache_line_read_step v tag -- send out idx
                     in if idx' == idx then ma else Nothing
                   f _ = Nothing

      rin0 :: Maybe idx
      rin0 = f dr
             where f :: Maybe cxdr -> Maybe idx
                   f (Just x)   = let (idx,tag) = tacache_split_cxdr x
                                  in Just idx
                   f _          = Nothing

      rin1 :: Maybe idx
      rin1 = f dx        -- choose line to read for invalidate
             where f :: Maybe cxdr -> Maybe idx
                   f (Just x)   = let (idx,tag) = tacache_split_cxdr x
                                  in Just idx
                   f _          = Nothing

      rin2 :: Maybe idx
      rin2 = f (d_x,dw) -- choose line to read for weak inval/write
             where f :: (Maybe cxdr,Maybe(cxdr,addr)) -> Maybe idx
                   f (Just x,Nothing)
                                = let (idx,tag) = tacache_split_cxdr x
                                  in Just idx
                   f (Nothing,Just(x,a))
                                = let (idx,tag) = tacache_split_cxdr x
                                  in Just idx
                   f _          = Nothing

      -- outs1 and outs2 are prev state
      -- may need to write two lines simultaneously, so ...
      win1,win2 :: Maybe(idx,CacheLine m tag addr)
      (win1,win2) = 
             case (dx, d_x, dw, out1, out2) of

  -- !!! FIX for HDL from here on, replace (v,_) = with v = fst $  !!! --

               (Just x,Nothing,Nothing,Just (idx,v),_) -> 
                 -- strong inval req 
                 let (v',_) = tazcache_line_inval_step v tag
                     (idx',tag) = tacache_split_cxdr x
                 in ( if idx == idx' then Just(idx',v') else Nothing
                    , Nothing
                    )

               (Just x1,Just x2,Nothing,Just (idx1,v1),Just (idx2,v2)) ->
                 -- strong inval, weak inval req
                 let (idx1',tag1) = tacache_split_cxdr x1
                     (idx2',tag2) = tacache_split_cxdr x2
                 in
                 if idx1' /= idx2' then
                   let (v1',_) = tazcache_line_inval_step v1 tag1
                       (v2',_) = tazcache_line_weak_inval_step v2 tag2
                   in ( if idx1 == idx1' then Just(idx1',v1') else Nothing
                      , if idx2 == idx2' then Just(idx2',v2') else Nothing
                      )
                 else
                   let (v1',_) = tazcache_line_inval_step v1 tag1
                       (v2',_) = tazcache_line_weak_inval_step v1' tag2
                   in ( if idx2 == idx2' then Just(idx2',v2') else Nothing
                      , Nothing
                      )

  -- !!! FIX for HDL from here, as above, and make cases top level fns !!! ---

               (Just x1,Nothing,Just(x2,a2),Just (idx1,v1),Just (idx2,v2)) -> 
                 -- strong inval, weak write req
                 let (idx1',tag1) = tacache_split_cxdr x1
                     (idx2',tag2) = tacache_split_cxdr x2
                 in
                 if idx1' /= idx2' then -- different cachelines
                   let (v1',_) = tazcache_line_inval_step v1 tag1
                       (v2',_) = tazcache_line_weak_write_step v2 tag2 a2
                   in ( Nothing
                      , if idx2 == idx2' then Just(idx2',v2') else Nothing
                      )
                 else                  -- same cacheline
                   let (v1',_) = tazcache_line_inval_step v1 tag1
                       (v2',_) = tazcache_line_weak_write_step v1' tag2 a2
                   in ( Nothing
                      , if idx2 == idx2' then Just(idx2',v2') else Nothing
                      )

               (Nothing,Just x,Nothing,_,Just (idx,v)) ->
                 -- weak inval req
                 let (v',_) = tazcache_line_weak_inval_step v tag
                     (idx',tag) = tacache_split_cxdr x
                 in ( Nothing
                    , if idx == idx' then Just(idx',v') else Nothing
                    )

               (Nothing,Nothing,Just(x,a),_,Just (idx,v)) -> 
                 -- weak write req
                 let (v',_) = tazcache_line_weak_write_step v tag a
                     (idx',tag) = tacache_split_cxdr x
                 in ( Nothing
                    , if idx == idx' then Just(idx',v') else Nothing
                    )

               _ -> (Nothing,Nothing)
 
   --------------------  support -----------------------

-- split incoming addr for translation into a cacheline index and tag
{-# NOINLINE tacache_split_cxdr #-}
tacache_split_cxdr
  :: forall (n::Nat) (p::Nat) tag cxdr idx f
   . ( KnownNat n, KnownNat p
     , Resize f  -- might as well be just Signed
     , n <= p, n + (p-n) ~ p, (p-n) + n ~ p
     , BitPack cxdr, p ~    BitSize cxdr, cxdr ~ f p
     , BitPack idx,  n ~    BitSize idx,  idx  ~ f n
     , BitPack tag, (p-n) ~ BitSize tag,  tag  ~ f (p-n)
     ) 
  => cxdr
  -> (idx,tag)
tacache_split_cxdr x =
    let (hibits,lobits) = split x
        idx = unpack hibits
        tag = unpack lobits
    in  (idx, tag)

-- remove ith entry from a vector, shrinking it by one
excise :: forall (n::Nat) x i . ( KnownNat n, Enum i, Default x )
       => Vec (n+1) x -> i -> Vec n x
excise v i = takeI (imap f (zip v (v <<+ def)))
             where f j (x,x') = if fromEnum j < fromEnum i then x else x'

   --------------------  cacheline ops -----------------------

-- locate entry with matching tag in cache line and report content
{-# NOINLINE tazcache_line_read_step #-}
tazcache_line_read_step ::
                   ( KnownNat m, KnownNat p_n, KnownNat q
                   , BitPack tag,  p_n ~ BitSize tag,  Eq tag
                   , BitPack addr, q ~   BitSize addr
                   ) 
                => CacheLine m tag addr
                -> tag
                -> (CacheLine m tag addr, Maybe addr)
tazcache_line_read_step v tag =
    let mi  = findIndex p v
              where p (Just (t,Just a)) = t==tag
                    p _                 = False
    in 
    case mi of
      Nothing -> (v,Nothing)
      Just i  -> let vi = v!!i -- move to front (de-age) if found
                     v' = vi +>> excise (v :< def) (fromEnum i)
                     ma = case vi of
                            Just (t,Just a)  -> Just a  -- matching entry
                            Just (t,Nothing) -> Nothing -- invalidated entry
                            Nothing          -> Nothing -- not there
                 in (v',ma)

-- remove element with matching tag from cacheline, report position
{-# NOINLINE tazcache_line_inval_step #-}
tazcache_line_inval_step ::
                   ( KnownNat m, KnownNat p_n, KnownNat q
                   , BitPack tag,  p_n ~ BitSize tag,  Eq tag
                   , BitPack addr, q ~   BitSize addr
                   ) 
                => CacheLine m tag addr
                -> tag
                -> (CacheLine m tag addr, Maybe(Index(2^m)))
tazcache_line_inval_step v tag =
    let mi  = findIndex p v
              where p (Just (t,Just _)) = t==tag -- known known
                    p _                 = False
    in
    case mi of
      Nothing -> (v, mi)
      -- tlb will have to confirm erase, remove ith from cacheline here
      Just i  -> let v' = excise (v :< def) (fromEnum i)
                 in (v', mi)

-- add placeholder invalidated entry to cacheline, replace entry if was there
{-# NOINLINE tazcache_line_weak_inval_step #-}
tazcache_line_weak_inval_step ::
                   ( KnownNat m, KnownNat p_n, KnownNat q
                   , BitPack tag,  p_n ~ BitSize tag,  Eq tag
                   , BitPack addr, q ~   BitSize addr
                   ) 
                => CacheLine m tag addr
                -> tag
                -> (CacheLine m tag addr, Maybe(Index(2^m)))
tazcache_line_weak_inval_step v tag =
    let mi  = findIndex p v
              where p (Just (t,_)) = t==tag -- known {known or unknown}
                    p _            = False
    in
    case mi of
      Nothing -> let v' = Just(tag,Nothing) +>> v
                 in (v', mi)
      Just i  -> let v' = Just(tag,Nothing) +>> excise (v :< def) (fromEnum i)
                 in (v', mi)

-- add entry to cacheline, replace if already there, move to front (de-age)
{-# NOINLINE tazcache_line_write_step #-}
tazcache_line_write_step ::
                   ( KnownNat m, KnownNat p_n, KnownNat q
                   , BitPack tag,  p_n ~ BitSize tag,  Eq tag
                   , BitPack addr, q ~   BitSize addr
                   ) 
                => CacheLine m tag addr
                -> tag
                -> addr
                -> CacheLine m tag addr
tazcache_line_write_step v tag a =
    let mi  = findIndex p v
              where p (Just (t,_)) = t==tag
                    p _            = False
    in
    case mi of
      Nothing -> let v' = Just(tag,Just a) +>> v
                 in v'
      Just i  -> let v' = Just(tag,Just a) +>> excise (v :< def) (fromEnum i)
                 in v'

-- add entry to cacheline if not already there, leave untouched if there
-- report Just maxBound if aged oldest entry out of cacheline, else Nothing
{-# NOINLINE tazcache_line_weak_write_step #-}
tazcache_line_weak_write_step :: 
                   ( KnownNat m, KnownNat p_n, KnownNat q
                   , BitPack tag,  p_n ~ BitSize tag,  Eq tag
                   , BitPack addr, q ~   BitSize addr
                   ) 
                => CacheLine m tag addr
                -> tag
                -> addr
                -> (CacheLine m tag addr, Maybe(Index(2^m)))
tazcache_line_weak_write_step v tag a =
    let -- i :: Index (2^m)
        mi  = findIndex p v
              where p (Just (t,_)) = t==tag
                    p _            = False
    in
    case mi of
      Nothing -> let v' = Just(tag,Just a) +>> (v :< def)
                 in case last v' of
                      Nothing           -> (takeI v',Nothing)
                      Just (t, Nothing) -> (takeI v',Nothing) -- invalid entry
                      _                 -> (takeI v',Just i)
                                          where i = maxBound
      Just i  -> (v,mi)