author | wenzelm |
Thu, 09 Aug 2001 23:42:45 +0200 | |
changeset 11499 | 7a7bb59a05db |
parent 11497 | 0e66e0114d9a |
child 11507 | 4b32a46ffd29 |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/Term.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 2001 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
7 |
header "Statements and expression emulations" |
|
8 |
||
9 |
theory Term = Main: |
|
10 |
||
11 |
typedecl cname (* class name *) |
|
12 |
typedecl vnam (* variable or field name *) |
|
13 |
typedecl mname (* method name *) |
|
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset
|
14 |
types imname = "cname \<times> mname" |
11376 | 15 |
|
16 |
datatype vname (* variable for special names *) |
|
17 |
= This (* This pointer *) |
|
18 |
| Param (* method parameter *) |
|
19 |
| Res (* method result *) |
|
20 |
| VName vnam |
|
21 |
||
22 |
datatype stmt |
|
23 |
= Skip (* empty statement *) |
|
11476 | 24 |
| Comp stmt stmt ("_;; _" [91,90 ] 90) |
25 |
| Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91) |
|
11376 | 26 |
| Loop vname stmt ("While '(_') _" [99,91 ] 91) |
11476 | 27 |
| LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *) |
28 |
| FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *) |
|
11376 | 29 |
| Meth cname mname (* virtual method *) |
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset
|
30 |
| Impl imname (* method implementation *) |
11476 | 31 |
and expr |
32 |
= NewC cname ("new _" [ 99] 95) (* object creation *) |
|
33 |
| Cast cname expr (* type cast *) |
|
34 |
| LAcc vname (* local access *) |
|
35 |
| FAcc expr vnam ("_.._" [95,99] 95) (* field access *) |
|
36 |
| Call cname expr mname expr (* method call *) |
|
37 |
("{_}_.._'(_')" [99,95,99,95] 95) |
|
11376 | 38 |
|
39 |
end |
|
40 |