equal
deleted
inserted
replaced
14 datatype mClkState = clkA | clkB |
14 datatype mClkState = clkA | clkB |
15 |
15 |
16 types |
16 types |
17 (* types sent on the clerk's send and receive channels are argument types |
17 (* types sent on the clerk's send and receive channels are argument types |
18 of the memory and the RPC, respectively *) |
18 of the memory and the RPC, respectively *) |
19 mClkSndArgType = "memArgType" |
19 mClkSndArgType = "memOp" |
20 mClkRcvArgType = "rpcArgType" |
20 mClkRcvArgType = "rpcOp" |
21 |
21 |
22 consts |
22 constdefs |
23 (* translate a memory call to an RPC call *) |
23 (* translate a memory call to an RPC call *) |
24 MClkRelayArg :: "memArgType => rpcArgType" |
24 MClkRelayArg :: "memOp => rpcOp" |
|
25 "MClkRelayArg marg == memcall marg" |
25 (* translate RPC failures to memory failures *) |
26 (* translate RPC failures to memory failures *) |
26 MClkReplyVal :: "Vals => Vals" |
27 MClkReplyVal :: "Vals => Vals" |
27 |
28 "MClkReplyVal v == if v = RPCFailure then MemFailure else v" |
28 rules |
|
29 MClkRelayArg_def "MClkRelayArg marg == Inl (remoteCall, marg)" |
|
30 MClkReplyVal_def "MClkReplyVal v == |
|
31 if v = RPCFailure then MemFailure else v" |
|
32 |
29 |
33 end |
30 end |
34 |
31 |