|
8011
|
1 |
(* Title: HOL/MicroJava/J/Decl.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb
|
|
|
4 |
Copyright 1997 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
Class declarations
|
|
|
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 |
|
|
|
35 |
ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
|
|
|
36 |
|
|
|
37 |
end
|