equal
deleted
inserted
replaced
21 = "(fname \<rightharpoonup> val)" |
21 = "(fname \<rightharpoonup> val)" |
22 |
22 |
23 obj = "cname \<times> fields" |
23 obj = "cname \<times> fields" |
24 |
24 |
25 translations |
25 translations |
26 |
26 (type) "fields" \<leftharpoondown> (type) "fname => val option" |
27 "fields" \<leftharpoondown> (type)"fname => val option" |
27 (type) "obj" \<leftharpoondown> (type) "cname \<times> fields" |
28 "obj" \<leftharpoondown> (type)"cname \<times> fields" |
|
29 |
28 |
30 definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where |
29 definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where |
31 "init_vars m == Option.map (\<lambda>T. Null) o m" |
30 "init_vars m == Option.map (\<lambda>T. Null) o m" |
32 |
31 |
33 text {* private: *} |
32 text {* private: *} |
38 record state |
37 record state |
39 = heap :: heap |
38 = heap :: heap |
40 locals :: locals |
39 locals :: locals |
41 |
40 |
42 translations |
41 translations |
43 |
42 (type) "heap" \<leftharpoondown> (type) "loc => obj option" |
44 "heap" \<leftharpoondown> (type)"loc => obj option" |
43 (type) "locals" \<leftharpoondown> (type) "vname => val option" |
45 "locals" \<leftharpoondown> (type)"vname => val option" |
44 (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)" |
46 "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
|
47 |
45 |
48 definition del_locs :: "state => state" where |
46 definition del_locs :: "state => state" where |
49 "del_locs s \<equiv> s (| locals := empty |)" |
47 "del_locs s \<equiv> s (| locals := empty |)" |
50 |
48 |
51 definition init_locs :: "cname => mname => state => state" where |
49 definition init_locs :: "cname => mname => state => state" where |