{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module Arbiter where

import qualified Prelude
import qualified Bank
import qualified Commands
import qualified Datatypes
import qualified Requests
import qualified Trace
import qualified Eqtype
import qualified Seq
import qualified Ssrnat

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

type Arrival_function_t =
  Prelude.Int -> Requests.Requests_t
  -- singleton inductive, whose constructor was mkArrivalFunction
  
coq_Arrival_at :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Arrival_function_t ->
                  Prelude.Int -> Requests.Requests_t
coq_Arrival_at _ _ arrival_function_t =
  arrival_function_t

data Arbiter_state_t = Coq_mkArbiterState {
  cmds :: Commands.Commands_t,
  time :: Prelude.Int,
  internal_state :: Bank.State_t
}

coq_Arbiter_Commands :: Bank.Requestor_configuration -> Bank.Arbiter_configuration ->
                        Bank.Bank_configuration -> Arbiter_state_t -> Commands.Commands_t
coq_Arbiter_Commands _ _ _ a =
  case a of {
   Coq_mkArbiterState arbiter_Commands _ _ -> arbiter_Commands}

coq_Arbiter_Time :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration
                    -> Arbiter_state_t -> Prelude.Int
coq_Arbiter_Time _ _ _ a =
  case a of {
   Coq_mkArbiterState _ arbiter_Time _ -> arbiter_Time}

coq_Arbiter_State :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration
                     -> Arbiter_state_t -> Bank.State_t
coq_Arbiter_State _ _ _ a =
  case a of {
   Coq_mkArbiterState _ _ arbiter_State -> arbiter_State}

data Arbiter_trace_t =
   Coq_mkArbiterTrace (Requests.Requests_t -> Arbiter_state_t) (Requests.Requests_t -> Arbiter_state_t ->
                                                               Arbiter_state_t)

coq_Init :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration ->
            Arbiter_trace_t -> Requests.Requests_t -> Arbiter_state_t
coq_Init _ _ _ arbiter_trace_t =
  case arbiter_trace_t of {
   Coq_mkArbiterTrace init _ -> init}

coq_Next :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration ->
            Arbiter_trace_t -> Requests.Requests_t -> Arbiter_state_t -> Arbiter_state_t
coq_Next _ _ _ arbiter_trace_t =
  case arbiter_trace_t of {
   Coq_mkArbiterTrace _ next -> next}

type Arbiter_t = Prelude.Int -> Trace.Trace_t
  -- singleton inductive, whose constructor was mkArbiter
  
coq_Default_arrival_at :: Bank.Requestor_configuration -> Bank.Bank_configuration -> (Datatypes.Coq_list
                          Requests.Request_t) -> Eqtype.Equality__Coq_sort -> Datatypes.Coq_list
                          Requests.Request_t
coq_Default_arrival_at rEQESTOR_CFG bANK_CFG input t =
  Seq.filter (\x ->
    Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce Requests.coq_Date rEQESTOR_CFG bANK_CFG x) t) input

coq_Default_arrival_function_t :: Bank.Requestor_configuration -> Bank.Bank_configuration ->
                                  Requests.Requests_t -> Arrival_function_t
coq_Default_arrival_function_t rEQESTOR_CFG bANK_CFG r =
  unsafeCoerce coq_Default_arrival_at rEQESTOR_CFG bANK_CFG r

coq_Default_arbitrate :: Bank.Requestor_configuration -> Bank.Arbiter_configuration ->
                         Bank.Bank_configuration -> Arrival_function_t -> Arbiter_trace_t -> Prelude.Int
                         -> Arbiter_state_t
coq_Default_arbitrate rEQESTOR_CFG aRBITER_CFG bANK_CFG aF aT t =
  let {r = coq_Arrival_at rEQESTOR_CFG bANK_CFG aF t} in
  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
    (\_ -> coq_Init rEQESTOR_CFG aRBITER_CFG bANK_CFG aT r)
    (\t' ->
    coq_Next rEQESTOR_CFG aRBITER_CFG bANK_CFG aT r
      (coq_Default_arbitrate rEQESTOR_CFG aRBITER_CFG bANK_CFG aF aT t'))
    t