|
1 (* Title: HOL/MicroJava/J/TypeRel.thy |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 The relations between Java types |
|
7 *) |
|
8 |
|
9 TypeRel = Prog + |
|
10 |
|
11 consts |
|
12 subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *) |
|
13 widen, (* widening *) |
|
14 cast :: "'c prog \\<Rightarrow> (ty \\<times> ty) set" (* casting *) |
|
15 |
|
16 syntax |
|
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>_\\<prec>C _" [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) |
|
21 |
|
22 translations |
|
23 "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
|
24 "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^+" |
|
25 "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
|
26 "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G" |
|
27 |
|
28 defs |
|
29 |
|
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}" |
|
32 |
|
33 consts |
|
34 |
|
35 cmethd :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)" |
|
36 cfield :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)" |
|
37 fields :: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times> ty) list" |
|
38 |
|
39 constdefs (* auxiliary relations for recursive definitions below *) |
|
40 |
|
41 subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set" |
|
42 "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}" |
|
43 |
|
44 (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) |
|
45 recdef cmethd "subcls1_rel" |
|
46 "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty |
|
47 | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> |
|
48 if is_class G D then cmethd (G,D) |
|
49 else arbitrary) \\<oplus> |
|
50 map_of (map (\\<lambda>(s, m ). |
|
51 (s,(C,m))) ms)) |
|
52 else arbitrary)" |
|
53 |
|
54 (* list of fields of a class, including inherited and hidden ones *) |
|
55 recdef fields "subcls1_rel" |
|
56 "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary |
|
57 | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@ |
|
58 (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> |
|
59 if is_class G D then fields (G,D) |
|
60 else arbitrary)) |
|
61 else arbitrary)" |
|
62 defs |
|
63 |
|
64 cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields" |
|
65 |
|
66 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3 |
|
67 i.e. sort of syntactic subtyping *) |
|
68 refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *) |
|
69 subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D" |
|
70 null "G\\<turnstile> NT \\<preceq> RefT R" |
|
71 |
|
72 inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *) |
|
73 widen "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> G\\<turnstile> S \\<Rightarrow>? T" |
|
74 subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C" |
|
75 |
|
76 end |