author | kleing |
Fri, 22 Sep 2000 16:28:53 +0200 | |
changeset 10061 | fe82134773dc |
parent 10042 | 7164dc0d24d8 |
child 10069 | c7226e6f9625 |
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 |
|
5 |
||
6 |
Java types |
|
7 |
*) |
|
8 |
||
9 |
Type = JBasis + |
|
10 |
||
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
11 |
types cname (* class name *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
12 |
vnam (* variable or field name *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
13 |
mname (* method name *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
14 |
|
8011 | 15 |
arities cname, vnam, mname :: term |
16 |
||
17 |
datatype vname (* names for This pointer and local/field variables *) |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
18 |
= This |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
19 |
| VName vnam |
8011 | 20 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
21 |
datatype prim_ty (* primitive type, cf. 4.2 *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
22 |
= Void (* 'result type' of void methods *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
23 |
| Boolean |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
24 |
| Integer |
8011 | 25 |
|
26 |
datatype ref_ty (* reference type, cf. 4.3 *) |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
27 |
= NullT (* null type, cf. 4.1 *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
28 |
| ClassT cname (* class type *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
29 |
|
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
30 |
datatype ty (* any type, cf. 4.1 *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
31 |
= PrimT prim_ty (* primitive type *) |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
32 |
| RefT ref_ty (* reference type *) |
8011 | 33 |
|
34 |
syntax |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
35 |
NT :: " ty" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
36 |
Class :: "cname => ty" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
37 |
|
8011 | 38 |
translations |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
39 |
"NT" == "RefT NullT" |
8011 | 40 |
"Class C" == "RefT (ClassT C)" |
41 |
||
42 |
end |