42 text \<open> |
42 text \<open> |
43 References and arrays are developed in parallel, |
43 References and arrays are developed in parallel, |
44 but keeping them separate makes some later proofs simpler. |
44 but keeping them separate makes some later proofs simpler. |
45 \<close> |
45 \<close> |
46 |
46 |
47 type_synonym addr = nat \<comment> "untyped heap references" |
47 type_synonym addr = nat \<comment> \<open>untyped heap references\<close> |
48 type_synonym heap_rep = nat \<comment> "representable values" |
48 type_synonym heap_rep = nat \<comment> \<open>representable values\<close> |
49 |
49 |
50 record heap = |
50 record heap = |
51 arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" |
51 arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" |
52 refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" |
52 refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" |
53 lim :: addr |
53 lim :: addr |
54 |
54 |
55 definition empty :: heap where |
55 definition empty :: heap where |
56 "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" |
56 "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" |
57 |
57 |
58 datatype 'a array = Array addr \<comment> "note the phantom type 'a" |
58 datatype 'a array = Array addr \<comment> \<open>note the phantom type 'a\<close> |
59 datatype 'a ref = Ref addr \<comment> "note the phantom type 'a" |
59 datatype 'a ref = Ref addr \<comment> \<open>note the phantom type 'a\<close> |
60 |
60 |
61 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
61 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
62 "addr_of_array (Array x) = x" |
62 "addr_of_array (Array x) = x" |
63 |
63 |
64 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |
64 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |