15 |
15 |
16 syntax |
16 syntax |
17 subcls1 :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70) |
17 subcls1 :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70) |
18 subcls :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70) |
18 subcls :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70) |
19 widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70) |
19 widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70) |
20 cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70) |
20 cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70) |
21 |
21 |
22 translations |
22 translations |
23 "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
23 "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
24 "G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*" |
24 "G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*" |
25 "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
25 "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
26 "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G" |
26 "G\\<turnstile>S \\<preceq>? T" == "(S,T) \\<in> cast G" |
27 |
27 |
28 defs |
28 defs |
29 |
29 |
30 (* direct subclass, cf. 8.1.3 *) |
30 (* direct subclass, cf. 8.1.3 *) |
31 subcls1_def "subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}" |
31 subcls1_def "subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}" |
67 i.e. sort of syntactic subtyping *) |
67 i.e. sort of syntactic subtyping *) |
68 refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *) |
68 refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *) |
69 subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D" |
69 subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D" |
70 null "G\\<turnstile> NT \\<preceq> RefT R" |
70 null "G\\<turnstile> NT \\<preceq> RefT R" |
71 |
71 |
72 inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *) |
72 inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *) |
73 widen "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> G\\<turnstile> S \\<Rightarrow>? T" |
73 widen "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> G\\<turnstile> S \\<preceq>? T" |
74 subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C" |
74 subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C" |
75 |
75 |
76 end |
76 end |