author | oheimb |
Mon, 05 Feb 2001 20:14:15 +0100 | |
changeset 11070 | cc421547e744 |
parent 11026 | a50365d21144 |
child 12517 | 360e3215f029 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Term.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
11070 | 7 |
header "Expressions and Statements" |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
9 |
theory Term = Value: |
8011 | 10 |
|
10069 | 11 |
datatype binop = Eq | Add (* function codes for binary operation *) |
9240 | 12 |
|
8011 | 13 |
datatype expr |
10069 | 14 |
= NewC cname (* class instance creation *) |
15 |
| Cast cname expr (* type cast *) |
|
16 |
| Lit val (* literal value, also references *) |
|
17 |
| BinOp binop expr expr (* binary operation *) |
|
18 |
| LAcc vname (* local (incl. parameter) access *) |
|
19 |
| LAss vname expr (* local assign *) ("_::=_" [ 90,90]90) |
|
20 |
| FAcc cname expr vname (* field access *) ("{_}_.._" [10,90,99 ]90) |
|
21 |
| FAss cname expr vname |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
22 |
expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90) |
10763 | 23 |
| Call cname expr mname |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
24 |
"ty list" "expr list" (* method call*) ("{_}_.._'( {_}_')" |
10763 | 25 |
[10,90,99,10,10] 90) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
26 |
|
10119 | 27 |
datatype stmt |
10069 | 28 |
= Skip (* empty statement *) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
29 |
| Expr expr (* expression statement *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
30 |
| Comp stmt stmt ("_;; _" [61,60]60) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
31 |
| Cond expr stmt stmt ("If '(_') _ Else _" [80,79,79]70) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
32 |
| Loop expr stmt ("While '(_') _" [80,79]70) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
33 |
|
8011 | 34 |
end |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
35 |