package Client(
    clientRouteRequest,
    clientArbitSubmission
) where

import Types
import BusTypes
import TagEngine
import Vector
import Util
import Arbiter
import FIFO
import FIFOF
import SpecialFIFOs
import Printf

busRequestToAddr :: BusRequest -> Addr
busRequestToAddr req = case req of
    BusReadRequest (ReadRequest addr _) -> addr
    BusWriteRequest (WriteRequest addr _) -> addr

clientRouteRequest :: (Add n (TLog numServers) (TLog (TAdd numServers 1)))
                  => Integer
                  -> FIFOF (TaggedBusRequest inFlightTransactions)
                  -> Vector numServers (Arbiter.Arbiter_IFC numClients)
                  -> Vector numClients (Arbiter.Arbiter_IFC (TAdd numServers 1))
                  -> (Addr -> Maybe (MkServerIdx numServers))
                  -> Rules
clientRouteRequest clientIdx clientReqQueue requestArbiterByServer responseArbiterByClient serverMap =
    rules
        (sprintf "client[%d] route request" clientIdx): when True ==> do
            let clientRequest :: TaggedBusRequest inFlightTransactions
                clientRequest = clientReqQueue.first

                targetAddr :: Addr
                targetAddr = busRequestToAddr |> clientRequest.busRequest

                targetServerIdx :: Maybe (MkServerIdx numServers)
                targetServerIdx = serverMap targetAddr
            case targetServerIdx of
                Just serverIdx -> do
                    let targetServerArbiter :: Arbiter.Arbiter_IFC numClients
                        targetServerArbiter = select requestArbiterByServer serverIdx

                        arbiterClientSlot :: Arbiter.ArbiterClient_IFC
                        arbiterClientSlot = select targetServerArbiter.clients clientIdx
                    arbiterClientSlot.request
                Nothing -> do
                    let targetClientResponseArbiter :: Arbiter.Arbiter_IFC (TAdd numServers 1)
                        targetClientResponseArbiter = select responseArbiterByClient clientIdx

                        -- arbiters 0 to n-1 where `n:=numServer` are reserved
                        -- for servers to make requests to. Arbiter n is reserved for
                        -- when this rule needs to skip making a request to a server
                        -- and should instead forward the `BusError UnMapped` response
                        -- back to the client. Vector.last selects arbiter `n`
                        clientResponseArbiterSlot :: Arbiter.ArbiterClient_IFC
                        clientResponseArbiterSlot = Vector.last targetClientResponseArbiter.clients

                        responseUnMapped :: BusResponse
                        responseUnMapped = case clientRequest.busRequest of
                            BusReadRequest _ -> BusReadResponse (Left UnMapped)
                            BusWriteRequest _ -> BusWriteResponse (Left UnMapped)

                        response :: TaggedBusResponse inFlightTransactions
                        response = TaggedBusResponse { tag = clientRequest.tag; busResponse = responseUnMapped }
                    clientResponseArbiterSlot.request

clientArbitSubmission :: (Add n (TLog numServers) (TLog (TAdd numServers 1)))
                     => Integer
                     -> FIFOF (TaggedBusRequest inFlightTransactions)
                     -> FIFOF (TaggedBusResponse inFlightTransactions)
                     -> Arbiter.Arbiter_IFC (TAdd numServers 1)
                     -> Vector numServers (FIFOF (MkClientTagType numClients, TaggedBusResponse inFlightTransactions))
                     -> Rules
clientArbitSubmission clientIdx clientReqQueue clientRespQueue clientRespArbiter submitRespQueues =
    rules
        (sprintf "client[%d] arbit submission" clientIdx): when True ==> do
            let grantedIdx :: UInt (TLog (TAdd numServers 1))
                grantedIdx = unpack clientRespArbiter.grant_id

                isClientRequest :: Bool
                isClientRequest = grantedIdx == fromInteger (valueOf numServers)
            if isClientRequest then do
                let clientRequest :: TaggedBusRequest inFlightTransactions
                    clientRequest = clientReqQueue.first

                    responseUnMapped :: BusResponse
                    responseUnMapped = case clientRequest.busRequest of
                        BusReadRequest _ -> BusReadResponse (Left UnMapped)
                        BusWriteRequest _ -> BusWriteResponse (Left UnMapped)

                    response :: TaggedBusResponse inFlightTransactions
                    response = TaggedBusResponse { tag = clientRequest.tag; busResponse = responseUnMapped }
                clientRespQueue.enq response
                clientReqQueue.deq
            else do
                let grantedServerIdx :: MkServerIdx numServers
                    grantedServerIdx = truncate grantedIdx

                    selectedSubmitRespQueue :: FIFOF (MkClientTagType numClients, TaggedBusResponse inFlightTransactions)
                    selectedSubmitRespQueue = select submitRespQueues grantedServerIdx

                    response :: (MkClientTagType numClients, TaggedBusResponse inFlightTransactions)
                    response = selectedSubmitRespQueue.first
                clientRespQueue.enq response.snd
                selectedSubmitRespQueue.deq