8011
|
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
|