Theory MemClerkParameters

(*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
    Author:     Stephan Merz, University of Munich

section ‹RPC-Memory example: Parameters of the memory clerk›

theory MemClerkParameters
imports RPCParameters

datatype mClkState = clkA | clkB

(* types sent on the clerk's send and receive channels are argument types
   of the memory and the RPC, respectively *)
type_synonym mClkSndArgType = "memOp"
type_synonym mClkRcvArgType = "rpcOp"

  (* translate a memory call to an RPC call *)
  MClkRelayArg     :: "memOp  rpcOp"
  where "MClkRelayArg marg = memcall marg"

  (* translate RPC failures to memory failures *)
  MClkReplyVal     :: "Vals  Vals"
  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"