Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
{-# 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