src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Sat Dec 02 02:52:02 2006 +0100 (2006-12-02)
changeset 21624 6f79647cf536
parent 17309 c43ed29bd197
child 36866 426d5781bb25
permissions -rw-r--r--
TLA: converted legacy ML scripts;
     1 (*
     2     File:        MemClerkParameters.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1997 University of Munich
     6 *)
     7 
     8 header {* RPC-Memory example: Parameters of the memory clerk *}
     9 
    10 theory MemClerkParameters
    11 imports RPCParameters
    12 begin
    13 
    14 datatype mClkState = clkA | clkB
    15 
    16 types
    17   (* types sent on the clerk's send and receive channels are argument types
    18      of the memory and the RPC, respectively *)
    19   mClkSndArgType   = "memOp"
    20   mClkRcvArgType   = "rpcOp"
    21 
    22 constdefs
    23   (* translate a memory call to an RPC call *)
    24   MClkRelayArg     :: "memOp => rpcOp"
    25     "MClkRelayArg marg == memcall marg"
    26   (* translate RPC failures to memory failures *)
    27   MClkReplyVal     :: "Vals => Vals"
    28     "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    29 
    30 end