11 memory implementation. |
11 memory implementation. |
12 *) |
12 *) |
13 |
13 |
14 RPCParameters = MemoryParameters + |
14 RPCParameters = MemoryParameters + |
15 |
15 |
16 datatype rpcOps = remoteCall |
16 datatype rpcOp = memcall memOp | othercall Vals |
17 datatype rpcState = rpcA | rpcB |
17 datatype rpcState = rpcA | rpcB |
18 |
18 |
|
19 (*** |
19 types |
20 types |
20 (* type of RPC arguments other than memory calls *) |
21 (* type of RPC arguments other than memory calls *) |
21 noMemArgType |
22 noMemArgType |
22 (* legal arguments for (our instance of) the RPC component *) |
23 (* legal arguments for (our instance of) the RPC component *) |
23 rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)" |
24 rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)" |
24 |
25 |
25 arities |
26 arities |
26 noMemArgType :: term |
27 noMemArgType :: term |
|
28 ***) |
27 |
29 |
28 consts |
30 consts |
29 (* some particular return values *) |
31 (* some particular return values *) |
30 RPCFailure :: "Vals" |
32 RPCFailure :: Vals |
31 BadCall :: "Vals" |
33 BadCall :: Vals |
32 |
34 |
33 (* Translate an rpc call to a memory call and test if the current argument |
35 (* Translate an rpc call to a memory call and test if the current argument |
34 is legal for the receiver (i.e., the memory). This can now be a little |
36 is legal for the receiver (i.e., the memory). This can now be a little |
35 simpler than for the generic RPC component. RelayArg returns an arbitrary |
37 simpler than for the generic RPC component. RelayArg returns an arbitrary |
36 memory call for illegal arguments. *) |
38 memory call for illegal arguments. *) |
37 IsLegalRcvArg :: "rpcArgType => bool" |
39 (*** |
38 RPCRelayArg :: "rpcArgType => memArgType" |
40 IsLegalRcvArg :: rpcArgType => bool |
|
41 RPCRelayArg :: rpcArgType => memArgType |
|
42 ***) |
|
43 IsLegalRcvArg :: rpcOp => bool |
|
44 RPCRelayArg :: rpcOp => memOp |
39 |
45 |
40 rules |
46 rules |
41 (* RPCFailure is different from MemVals and exceptions *) |
47 (* RPCFailure is different from MemVals and exceptions *) |
42 RFNoMemVal "~(MemVal RPCFailure)" |
48 RFNoMemVal "RPCFailure ~: MemVal" |
43 NotAResultNotRF "NotAResult ~= RPCFailure" |
49 NotAResultNotRF "NotAResult ~= RPCFailure" |
44 OKNotRF "OK ~= RPCFailure" |
50 OKNotRF "OK ~= RPCFailure" |
45 BANotRF "BadArg ~= RPCFailure" |
51 BANotRF "BadArg ~= RPCFailure" |
46 |
52 |
|
53 (*** |
47 IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)" |
54 IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)" |
48 RPCRelayArg_def "RPCRelayArg ra == |
55 RPCRelayArg_def "RPCRelayArg ra == |
49 case ra of Inl (rm) => (snd rm) |
56 case ra of Inl (rm) => (snd rm) |
50 | Inr (rn) => Inl (read, @ l. True)" |
57 | Inr (rn) => (read, @ l. True)" |
51 |
58 ***) |
|
59 defs |
|
60 IsLegalRcvArg_def "IsLegalRcvArg ra == |
|
61 case ra of (memcall m) => True |
|
62 | (othercall v) => False" |
|
63 RPCRelayArg_def "RPCRelayArg ra == |
|
64 case ra of (memcall m) => m |
|
65 | (othercall v) => arbitrary" |
52 end |
66 end |
53 |
67 |
54 |
68 |