src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309 c43ed29bd197
parent 11703 6e5de8d4290a
child 21624 6f79647cf536
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MemClerkParameters.thy
wenzelm@17309
     3
    ID:          $Id$
wenzelm@3807
     4
    Author:      Stephan Merz
wenzelm@3807
     5
    Copyright:   1997 University of Munich
wenzelm@3807
     6
wenzelm@3807
     7
    Theory Name: MemClerkParameters
wenzelm@3807
     8
    Logic Image: TLA
wenzelm@3807
     9
wenzelm@3807
    10
    RPC-Memory example: Parameters of the memory clerk.
wenzelm@3807
    11
*)
wenzelm@3807
    12
wenzelm@17309
    13
theory MemClerkParameters
wenzelm@17309
    14
imports RPCParameters
wenzelm@17309
    15
begin
wenzelm@3807
    16
wenzelm@17309
    17
datatype mClkState = clkA | clkB
wenzelm@3807
    18
wenzelm@3807
    19
types
wenzelm@3807
    20
  (* types sent on the clerk's send and receive channels are argument types
wenzelm@3807
    21
     of the memory and the RPC, respectively *)
wenzelm@6255
    22
  mClkSndArgType   = "memOp"
wenzelm@6255
    23
  mClkRcvArgType   = "rpcOp"
wenzelm@3807
    24
wenzelm@6255
    25
constdefs
wenzelm@3807
    26
  (* translate a memory call to an RPC call *)
wenzelm@6255
    27
  MClkRelayArg     :: "memOp => rpcOp"
wenzelm@6255
    28
    "MClkRelayArg marg == memcall marg"
wenzelm@3807
    29
  (* translate RPC failures to memory failures *)
wenzelm@3807
    30
  MClkReplyVal     :: "Vals => Vals"
wenzelm@6255
    31
    "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
wenzelm@3807
    32
wenzelm@17309
    33
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17309
    34
wenzelm@3807
    35
end