equal
deleted
inserted
replaced
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 \\<equiv> (Object, (None, [], []))" |
35 ObjectC_def "ObjectC == (Object, (None, [], []))" |
36 |
36 |
37 |
37 |
38 types 'c prog = "'c cdecl list" |
38 types 'c prog = "'c cdecl list" |
39 |
39 |
40 consts |
40 consts |
41 |
41 |
42 class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)" |
42 class :: "'c prog => (cname \\<leadsto> 'c class)" |
43 |
43 |
44 is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool" |
44 is_class :: "'c prog => cname => bool" |
45 is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool" |
45 is_type :: "'c prog => ty => bool" |
46 |
46 |
47 defs |
47 defs |
48 |
48 |
49 class_def "class \\<equiv> map_of" |
49 class_def "class == map_of" |
50 |
50 |
51 is_class_def "is_class G C \\<equiv> class G C \\<noteq> None" |
51 is_class_def "is_class G C == class G C \\<noteq> None" |
52 |
52 |
53 primrec |
53 primrec |
54 "is_type G (PrimT pt) = True" |
54 "is_type G (PrimT pt) = True" |
55 "is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)" |
55 "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
56 |
56 |
57 end |
57 end |