author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9346 | 297dcbf64526 |
child 10613 | 78b1d6c3ee9c |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Decl.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
5 |
||
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
6 |
Class declarations and programs |
8011 | 7 |
*) |
8 |
||
9 |
Decl = Type + |
|
10 |
||
11 |
types fdecl (* field declaration, cf. 8.3 (, 9.3) *) |
|
12 |
= "vname \\<times> ty" |
|
13 |
||
14 |
||
15 |
types sig (* signature of a method, cf. 8.4.2 *) |
|
16 |
= "mname \\<times> ty list" |
|
17 |
||
18 |
'c mdecl (* method declaration in a class *) |
|
19 |
= "sig \\<times> ty \\<times> 'c" |
|
20 |
||
21 |
types 'c class (* class *) |
|
22 |
= "cname option \\<times> fdecl list \\<times> 'c mdecl list" |
|
23 |
(* superclass, fields, methods*) |
|
24 |
||
25 |
'c cdecl (* class declaration, cf. 8.1 *) |
|
26 |
= "cname \\<times> 'c class" |
|
27 |
||
28 |
consts |
|
29 |
||
30 |
Object :: cname (* name of root class *) |
|
31 |
ObjectC :: 'c cdecl (* decl of root class *) |
|
32 |
||
33 |
defs |
|
34 |
||
10042 | 35 |
ObjectC_def "ObjectC == (Object, (None, [], []))" |
8011 | 36 |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
37 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
38 |
types 'c prog = "'c cdecl list" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
39 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
40 |
consts |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
41 |
|
10042 | 42 |
class :: "'c prog => (cname \\<leadsto> 'c class)" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
43 |
|
10042 | 44 |
is_class :: "'c prog => cname => bool" |
45 |
is_type :: "'c prog => ty => bool" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
46 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
47 |
defs |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
48 |
|
10042 | 49 |
class_def "class == map_of" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
50 |
|
10042 | 51 |
is_class_def "is_class G C == class G C \\<noteq> None" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
52 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
53 |
primrec |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
54 |
"is_type G (PrimT pt) = True" |
10042 | 55 |
"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
56 |
|
8011 | 57 |
end |