17 |
17 |
18 'c mdecl (* method declaration in a class *) |
18 'c mdecl (* method declaration in a class *) |
19 = "sig \\<times> ty \\<times> 'c" |
19 = "sig \\<times> ty \\<times> 'c" |
20 |
20 |
21 types 'c class (* class *) |
21 types 'c class (* class *) |
22 = "cname option \\<times> fdecl list \\<times> 'c mdecl list" |
22 = "cname \\<times> fdecl list \\<times> 'c mdecl list" |
23 (* superclass, fields, methods*) |
23 (* superclass, fields, methods*) |
24 |
24 |
25 'c cdecl (* class declaration, cf. 8.1 *) |
25 'c cdecl (* class declaration, cf. 8.1 *) |
26 = "cname \\<times> 'c class" |
26 = "cname \\<times> 'c class" |
27 |
27 |
30 Object :: cname (* name of root class *) |
30 Object :: cname (* name of root class *) |
31 ObjectC :: 'c cdecl (* decl of root class *) |
31 ObjectC :: 'c cdecl (* decl of root class *) |
32 |
32 |
33 defs |
33 defs |
34 |
34 |
35 ObjectC_def "ObjectC == (Object, (None, [], []))" |
35 ObjectC_def "ObjectC == (Object, (arbitrary, [], []))" |
36 |
36 |
37 |
37 |
38 types 'c prog = "'c cdecl list" |
38 types 'c prog = "'c cdecl list" |
39 |
39 |
|
40 |
|
41 translations |
|
42 "fdecl" <= (type) "vname \\<times> ty" |
|
43 "sig" <= (type) "mname \\<times> ty list" |
|
44 "mdecl c" <= (type) "sig \\<times> ty \\<times> c" |
|
45 "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list" |
|
46 "cdecl c" <= (type) "cname \\<times> (c class)" |
|
47 "prog c" <= (type) "(c cdecl) list" |
|
48 |
40 consts |
49 consts |
41 |
50 |
42 class :: "'c prog => (cname \\<leadsto> 'c class)" |
51 class :: "'c prog => (cname \\<leadsto> 'c class)" |
|
52 is_class :: "'c prog => cname => bool" |
43 |
53 |
44 is_class :: "'c prog => cname => bool" |
54 translations |
|
55 |
|
56 "class" => "map_of" |
|
57 "is_class G C" == "class G C \\<noteq> None" |
|
58 |
|
59 consts |
|
60 |
45 is_type :: "'c prog => ty => bool" |
61 is_type :: "'c prog => ty => bool" |
46 |
|
47 defs |
|
48 |
|
49 class_def "class == map_of" |
|
50 |
|
51 is_class_def "is_class G C == class G C \\<noteq> None" |
|
52 |
62 |
53 primrec |
63 primrec |
54 "is_type G (PrimT pt) = True" |
64 "is_type G (PrimT pt) = True" |
55 "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
65 "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
56 |
66 |