equal
deleted
inserted
replaced
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 = "memOp" |
19 mClkSndArgType = "memOp" |
20 mClkRcvArgType = "rpcOp" |
20 mClkRcvArgType = "rpcOp" |
21 |
21 |
22 constdefs |
22 definition |
23 (* translate a memory call to an RPC call *) |
23 (* translate a memory call to an RPC call *) |
24 MClkRelayArg :: "memOp => rpcOp" |
24 MClkRelayArg :: "memOp => rpcOp" |
25 "MClkRelayArg marg == memcall marg" |
25 where "MClkRelayArg marg = memcall marg" |
|
26 |
|
27 definition |
26 (* translate RPC failures to memory failures *) |
28 (* translate RPC failures to memory failures *) |
27 MClkReplyVal :: "Vals => Vals" |
29 MClkReplyVal :: "Vals => Vals" |
28 "MClkReplyVal v == if v = RPCFailure then MemFailure else v" |
30 where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)" |
29 |
31 |
30 end |
32 end |