7 |
7 |
8 theory State |
8 theory State |
9 imports TypeRel Value |
9 imports TypeRel Value |
10 begin |
10 begin |
11 |
11 |
12 types |
12 type_synonym |
13 fields' = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value" |
13 fields' = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value" |
14 |
14 |
|
15 type_synonym |
15 obj = "cname \<times> fields'" -- "class instance with class name and fields" |
16 obj = "cname \<times> fields'" -- "class instance with class name and fields" |
16 |
17 |
17 definition obj_ty :: "obj => ty" where |
18 definition obj_ty :: "obj => ty" where |
18 "obj_ty obj == Class (fst obj)" |
19 "obj_ty obj == Class (fst obj)" |
19 |
20 |
20 definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where |
21 definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where |
21 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" |
22 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" |
22 |
23 |
23 types aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *} |
24 type_synonym aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *} |
24 locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents" |
25 type_synonym locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents" |
25 |
26 |
26 state = "aheap \<times> locals" -- "heap, local parameter including This" |
27 type_synonym state = "aheap \<times> locals" -- "heap, local parameter including This" |
27 xstate = "val option \<times> state" -- "state including exception information" |
28 type_synonym xstate = "val option \<times> state" -- "state including exception information" |
28 |
29 |
29 abbreviation (input) |
30 abbreviation (input) |
30 heap :: "state => aheap" |
31 heap :: "state => aheap" |
31 where "heap == fst" |
32 where "heap == fst" |
32 |
33 |