author | kleing |
Thu, 21 Feb 2002 09:54:08 +0100 | |
changeset 12911 | 704713ca07ea |
parent 12517 | 360e3215f029 |
child 12951 | a9fdcb71d252 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Type.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* \isaheader{Java types} *} |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10069
diff
changeset
|
9 |
theory Type = JBasis: |
8011 | 10 |
|
12517 | 11 |
typedecl cnam |
12 |
||
13 |
-- "exceptions" |
|
14 |
datatype |
|
15 |
xcpt |
|
16 |
= NullPointer |
|
17 |
| ClassCast |
|
18 |
| OutOfMemory |
|
8011 | 19 |
|
12517 | 20 |
-- "class names" |
21 |
datatype cname |
|
22 |
= Object |
|
23 |
| Xcpt xcpt |
|
24 |
| Cname cname |
|
25 |
||
26 |
typedecl vnam -- "variable or field name" |
|
27 |
typedecl mname -- "method name" |
|
28 |
||
29 |
-- "names for @{text This} pointer and local/field variables" |
|
30 |
datatype vname |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
31 |
= This |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
32 |
| VName vnam |
8011 | 33 |
|
12517 | 34 |
-- "primitive type, cf. 4.2" |
35 |
datatype prim_ty |
|
36 |
= Void -- "'result type' of void methods" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
37 |
| Boolean |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
38 |
| Integer |
8011 | 39 |
|
12517 | 40 |
-- "reference type, cf. 4.3" |
41 |
datatype ref_ty |
|
42 |
= NullT -- "null type, cf. 4.1" |
|
43 |
| ClassT cname -- "class type" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
44 |
|
12517 | 45 |
-- "any type, cf. 4.1" |
46 |
datatype ty |
|
47 |
= PrimT prim_ty -- "primitive type" |
|
48 |
| RefT ref_ty -- "reference type" |
|
8011 | 49 |
|
50 |
syntax |
|
12517 | 51 |
NT :: "ty" |
10069 | 52 |
Class :: "cname => ty" |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
53 |
|
8011 | 54 |
translations |
10069 | 55 |
"NT" == "RefT NullT" |
56 |
"Class C" == "RefT (ClassT C)" |
|
8011 | 57 |
|
58 |
end |