|
1 (* Title: HOL/BCV/JType.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 The type system of the JVM |
|
7 *) |
|
8 |
|
9 JType = Err + |
|
10 |
|
11 types cname |
|
12 arities cname :: term |
|
13 |
|
14 types subclass = "(cname*cname)set" |
|
15 |
|
16 datatype ty = Void | Integer | NullT | Class cname |
|
17 |
|
18 constdefs |
|
19 is_Class :: ty => bool |
|
20 "is_Class T == case T of Void => False | Integer => False | NullT => False |
|
21 | Class C => True" |
|
22 |
|
23 is_ref :: ty => bool |
|
24 "is_ref T == T=NullT | is_Class T" |
|
25 |
|
26 subtype :: subclass => ty ord |
|
27 "subtype S T1 T2 == |
|
28 (T1=T2) | T1=NullT & is_Class T2 | |
|
29 (? C D. T1 = Class C & T2 = Class D & (C,D) : S^*)" |
|
30 |
|
31 sup :: "subclass => ty => ty => ty err" |
|
32 "sup S T1 T2 == |
|
33 case T1 of Void => (case T2 of Void => OK Void |
|
34 | Integer => Err |
|
35 | NullT => Err |
|
36 | Class D => Err) |
|
37 | Integer => (case T2 of Void => Err |
|
38 | Integer => OK Integer |
|
39 | NullT => Err |
|
40 | Class D => Err) |
|
41 | NullT => (case T2 of Void => Err |
|
42 | Integer => Err |
|
43 | NullT => OK NullT |
|
44 | Class D => OK(Class D)) |
|
45 | Class C => (case T2 of Void => Err |
|
46 | Integer => Err |
|
47 | NullT => OK(Class C) |
|
48 | Class D => OK(Class(some_lub (S^*) C D)))" |
|
49 |
|
50 Object :: cname |
|
51 "Object == arbitrary" |
|
52 |
|
53 is_type :: subclass => ty => bool |
|
54 "is_type S T == case T of Void => True | Integer => True | NullT => True |
|
55 | Class C => (C,Object):S^*" |
|
56 |
|
57 syntax |
|
58 "types" :: subclass => ty set |
|
59 "@subty" :: ty => subclass => ty => bool ("(_ /[='__ _)" [50, 1000, 51] 50) |
|
60 translations |
|
61 "types S" == "Collect(is_type S)" |
|
62 "x [=_S y" == "x <=_(subtype S) y" |
|
63 |
|
64 constdefs |
|
65 esl :: "subclass => ty esl" |
|
66 "esl S == (types S, subtype S, sup S)" |
|
67 |
|
68 end |