7 header "Types, class Declarations, and whole programs" |
7 header "Types, class Declarations, and whole programs" |
8 |
8 |
9 theory Decl = Term: |
9 theory Decl = Term: |
10 |
10 |
11 datatype ty |
11 datatype ty |
12 = NT (* null type *) |
12 = NT --{* null type *} |
13 | Class cname (* class type *) |
13 | Class cname --{* class type *} |
14 |
14 |
15 types fdecl (* field declaration *) |
15 text{* field declaration *} |
16 = "vnam \<times> ty" |
16 types fdecl |
|
17 = "fname \<times> ty" |
17 |
18 |
18 record methd (* method declaration *) |
19 record methd |
19 = par :: ty |
20 = par :: ty |
20 res :: ty |
21 res :: ty |
21 lcl ::"(vname \<times> ty) list" |
22 lcl ::"(vname \<times> ty) list" |
22 bdy :: stmt |
23 bdy :: stmt |
23 |
24 |
24 types mdecl (* method declaration *) |
25 text{* method declaration *} |
|
26 types mdecl |
25 = "mname \<times> methd" |
27 = "mname \<times> methd" |
26 |
28 |
27 record class (* class *) |
29 record class |
28 = super :: cname |
30 = super :: cname |
29 fields ::"fdecl list" |
31 fields ::"fdecl list" |
30 methods ::"mdecl list" |
32 methods ::"mdecl list" |
31 |
33 |
32 types cdecl (* class declaration *) |
34 text{* class declaration *} |
|
35 types cdecl |
33 = "cname \<times> class" |
36 = "cname \<times> class" |
34 |
37 |
35 types prog |
38 types prog |
36 = "cdecl list" |
39 = "cdecl list" |
37 |
40 |
38 translations |
41 translations |
39 "fdecl" \<leftharpoondown> (type)"vname \<times> ty" |
42 "fdecl" \<leftharpoondown> (type)"fname \<times> ty" |
40 "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt" |
43 "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt" |
41 "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list" |
44 "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list" |
42 "cdecl" \<leftharpoondown> (type)"cname \<times> class" |
45 "cdecl" \<leftharpoondown> (type)"cname \<times> class" |
43 "prog " \<leftharpoondown> (type)"cdecl list" |
46 "prog " \<leftharpoondown> (type)"cdecl list" |
44 |
47 |
45 consts |
48 consts |
46 |
49 |
47 Prog :: prog (* program as a global value *) |
50 Prog :: prog --{* program as a global value *} |
48 Object :: cname (* name of root class *) |
51 Object :: cname --{* name of root class *} |
49 |
52 |
50 |
53 |
51 constdefs |
54 constdefs |
52 class :: "cname \<leadsto> class" |
55 class :: "cname \<leadsto> class" |
53 "class \<equiv> map_of Prog" |
56 "class \<equiv> map_of Prog" |