author  schirmer 
Thu, 11 Jul 2002 09:36:41 +0200  
changeset 13345  bd611943cbc2 
parent 13337  f75dfc606ac7 
child 13358  c837ba4cfb62 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Term.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 

7 
header {* Java expressions and statements *} 

8 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

9 
theory Term = Value + Table: 
12854  10 

11 
text {* 

12 
design issues: 

13 
\begin{itemize} 

14 
\item invocation frames for local variables could be reduced to special static 

15 
objects (one per method). This would reduce redundancy, but yield a rather 

16 
nonstandard execution model more difficult to understand. 

17 
\item method bodies separated from calls to handle assumptions in axiomat. 

18 
semantics 

19 
NB: Body is intended to be in the environment of the called method. 

20 
\item class initialization is regarded as (auxiliary) statement 

21 
(required for AxSem) 

22 
\item result expression of method return is handled by a special result variable 

23 
result variable is treated uniformly with local variables 

24 
\begin{itemize} 

25 
\item[+] welltypedness and existence of the result/return expression is 

26 
ensured without extra efford 

27 
\end{itemize} 

28 
\end{itemize} 

29 

30 
simplifications: 

31 
\begin{itemize} 

32 
\item expression statement allowed for any expression 

33 
\item no unary, binary, etc, operators 

34 
\item This is modeled as a special nonassignable local variable 

35 
\item Super is modeled as a general expression with the same value as This 

36 
\item access to field x in current class via This.x 

37 
\item NewA creates only onedimensional arrays; 

38 
initialization of further subarrays may be simulated with nested NewAs 

39 
\item The 'Lit' constructor is allowed to contain a reference value. 

40 
But this is assumed to be prohibited in the input language, which is enforced 

41 
by the typechecking rules. 

42 
\item a call of a static method via a type name may be simulated by a dummy 

43 
variable 

44 
\item no nested blocks with inner local variables 

45 
\item no synchronized statements 

46 
\item no secondary forms of if, while (e.g. no for) (may be easily simulated) 

47 
\item no switch (may be simulated with if) 

48 
\item the @{text try_catch_finally} statement is divided into the 

49 
@{text try_catch} statement 

50 
and a finally statement, which may be considered as try..finally with 

51 
empty catch 

52 
\item the @{text try_catch} statement has exactly one catch clause; 

53 
multiple ones can be 

54 
simulated with instanceof 

55 
\item the compiler is supposed to add the annotations {@{text _}} during 

56 
typechecking. This 

57 
transformation is left out as its result is checked by the type rules anyway 

58 
\end{itemize} 

59 
*} 

60 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

61 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

62 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

63 
types locals = "(lname, val) table" (* local variables *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

64 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

65 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

66 
datatype jump 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

67 
= Break label (* break *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

68 
 Cont label (* continue *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

69 
 Ret (* return from method *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

70 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

71 
datatype xcpt (* exception *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

72 
= Loc loc (* location of allocated execption object *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

73 
 Std xname (* intermediate standard exception, see Eval.thy *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

74 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

75 
datatype error 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

76 
= AccessViolation (* Access to a member that isn't permitted *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

77 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

78 
datatype abrupt (* abrupt completion *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

79 
= Xcpt xcpt (* exception *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

80 
 Jump jump (* break, continue, return *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

81 
 Error error (* runtime errors, we wan't to detect and proof absent 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

82 
in welltyped programms *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

83 
types 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

84 
abopt = "abrupt option" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

85 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

86 
text {* Local variable store and exception. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

87 
Anticipation of State.thy used by smallstep semantics. For a method call, 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

88 
we save the local variables of the caller in the term Callee to restore them 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

89 
after method return. Also an exception must be restored after the finally 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

90 
statement *} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

91 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

92 
translations 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

93 
"locals" <= (type) "(lname, val) table" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

94 

12854  95 
datatype inv_mode (* invocation mode for method calls *) 
96 
= Static (* static *) 

97 
 SuperM (* super *) 

98 
 IntVir (* interface or virtual *) 

99 

100 
record sig = (* signature of a method, cf. 8.4.2 *) 

101 
name ::"mname" (* acutally belongs to Decl.thy *) 

102 
parTs::"ty list" 

103 

104 
translations 

105 
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>" 

106 
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>" 

107 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

108 
 "function codes for unary operations" 
13345  109 
datatype unop = UPlus  {*{\tt +} unary plus*} 
110 
 UMinus  {*{\tt } unary minus*} 

111 
 UBitNot  {*{\tt ~} bitwise NOT*} 

112 
 UNot  {*{\tt !} logical complement*} 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

113 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

114 
 "function codes for binary operations" 
13345  115 
datatype binop = Mul  {*{\tt * } multiplication*} 
116 
 Div  {*{\tt /} division*} 

117 
 Mod  {*{\tt %} remainder*} 

118 
 Plus  {*{\tt +} addition*} 

119 
 Minus  {*{\tt } subtraction*} 

120 
 LShift  {*{\tt <<} left shift*} 

121 
 RShift  {*{\tt >>} signed right shift*} 

122 
 RShiftU  {*{\tt >>>} unsigned right shift*} 

123 
 Less  {*{\tt <} less than*} 

124 
 Le  {*{\tt <=} less than or equal*} 

125 
 Greater  {*{\tt >} greater than*} 

126 
 Ge  {*{\tt >=} greater than or equal*} 

127 
 Eq  {*{\tt ==} equal*} 

128 
 Neq  {*{\tt !=} not equal*} 

129 
 BitAnd  {*{\tt &} bitwise AND*} 

130 
 And  {*{\tt &} boolean AND*} 

131 
 BitXor  {*{\tt ^} bitwise Xor*} 

132 
 Xor  {*{\tt ^} boolean Xor*} 

133 
 BitOr  {*{\tt } bitwise Or*} 

134 
 Or  {*{\tt } boolean Or*} 

135 
text{* The boolean operators {\tt &} and {\tt } strictly evaluate both 

136 
of their arguments. The lazy operators {\tt &&} and {\tt } are modeled 

137 
as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and 

138 
{\tt a  b = a?true:b} 

139 
*} 

12854  140 
datatype var 
141 
= LVar lname(* local variable (incl. parameters) *) 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

142 
 FVar qtname qtname bool expr vname 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

143 
(*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

144 
 AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

145 
 InsInitV stmt var (* insertion of initialization before 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

146 
evaluation of var (for smallstep sem.) *) 
12854  147 

148 
and expr 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

149 
= NewC qtname (* class instance creation *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

150 
 NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

151 
 Cast ty expr (* type cast *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

152 
 Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

153 
 Lit val (* literal value, references not allowed *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

154 
 UnOp unop expr (* unary operation *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

155 
 BinOp binop expr expr (* binary operation *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

156 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

157 
 Super (* special Super keyword *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

158 
 Acc var (* variable access *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

159 
 Ass var expr (* variable assign *) ("_:=_" [90,85 ]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

160 
 Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

161 
 Call qtname ref_ty inv_mode expr mname "(ty list)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

162 
"(expr list)" (* method call *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

163 
("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

164 
 Methd qtname sig (* (folded) method (see below) *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

165 
 Body qtname stmt (* (unfolded) method body *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

166 
 InsInitE stmt expr (* insertion of initialization before 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

167 
evaluation of expr (for smallstep sem.) *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

168 
 Callee locals expr (* save Callers locals in CalleeFrame 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

169 
(for smallstep semantics) *) 
12854  170 
and stmt 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

171 
= Skip (* empty statement *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

172 
 Expr expr (* expression statement *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

173 
 Lab jump stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

174 
(* handles break *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

175 
 Comp stmt stmt ("_;; _" [ 66,65]65) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

176 
 If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

177 
 Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

178 
 Do jump (* break, continue, return *) 
12854  179 
 Throw expr 
180 
 TryC stmt 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

181 
qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

182 
 Fin stmt stmt ("_ Finally _" [ 79,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

183 
 FinA abopt stmt (* Save abruption of first statement 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

184 
(for smallstep sem.) *) 
12854  185 
 Init qtname (* class initialization *) 
186 

187 

188 
text {* 

189 
The expressions Methd and Body are artificial program constructs, in the 

190 
sense that they are not used to define a concrete Bali program. In the 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

191 
operational semantic's they are "generated on the fly" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

192 
to decompose the task to define the behaviour of the Call expression. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

193 
They are crucial for the axiomatic semantics to give a syntactic hook to insert 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

194 
some assertions (cf. AxSem.thy, Eval.thy). 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

195 
The Init statement (to initialize a class on its first use) is 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

196 
inserted in various places by the semantics. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

197 
Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

198 
smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

199 
local variables of the caller for method return. So ve avoid modelling a 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

200 
frame stack. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

201 
The InsInitV/E terms are only used by the smallstep semantics to model the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

202 
intermediate steps of classinitialisation. 
12854  203 
*} 
204 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

205 
types "term" = "(expr+stmt,var,expr list) sum3" 
12854  206 
translations 
207 
"sig" <= (type) "mname \<times> ty list" 

208 
"var" <= (type) "Term.var" 

209 
"expr" <= (type) "Term.expr" 

210 
"stmt" <= (type) "Term.stmt" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

211 
"term" <= (type) "(expr+stmt,var,expr list) sum3" 
12854  212 

213 
syntax 

214 

215 
this :: expr 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

216 
LAcc :: "vname \<Rightarrow> expr" ("!!") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

217 
LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85) 
12854  218 
Return :: "expr \<Rightarrow> stmt" 
219 
StatRef :: "ref_ty \<Rightarrow> expr" 

220 

221 
translations 

222 

223 
"this" == "Acc (LVar This)" 

224 
"!!v" == "Acc (LVar (EName (VNam v)))" 

225 
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)" 

226 
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 

227 
(* Res := e;; Do Ret *) 

228 
"StatRef rt" == "Cast (RefT rt) (Lit Null)" 

229 

230 
constdefs 

231 

232 
is_stmt :: "term \<Rightarrow> bool" 

233 
"is_stmt t \<equiv> \<exists>c. t=In1r c" 

234 

235 
ML {* 

236 
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def")); 

237 
*} 

238 

239 
declare is_stmt_rews [simp] 

13345  240 

241 
axclass inj_term < "type" 

242 
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83) 

243 

244 
instance stmt::inj_term .. 

245 

246 
defs (overloaded) 

247 
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" 

248 

249 
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" 

250 
by (simp add: stmt_inj_term_def) 

251 

252 
instance expr::inj_term .. 

253 

254 
defs (overloaded) 

255 
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" 

256 

257 
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" 

258 
by (simp add: expr_inj_term_def) 

259 

260 
instance var::inj_term .. 

261 

262 
defs (overloaded) 

263 
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" 

264 

265 
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" 

266 
by (simp add: var_inj_term_def) 

267 

268 
instance "list":: (type) inj_term .. 

269 

270 
defs (overloaded) 

271 
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es" 

272 

273 
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" 

274 
by (simp add: expr_list_inj_term_def) 

275 

12854  276 
end 