equal
deleted
inserted
replaced
51 lim :: addr |
51 lim :: addr |
52 |
52 |
53 definition empty :: heap where |
53 definition empty :: heap where |
54 "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" |
54 "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" |
55 |
55 |
56 datatype_new 'a array = Array addr -- "note the phantom type 'a" |
56 old_datatype 'a array = Array addr -- "note the phantom type 'a" |
57 datatype_compat array |
57 old_datatype 'a ref = Ref addr -- "note the phantom type 'a" |
58 |
|
59 datatype_new 'a ref = Ref addr -- "note the phantom type 'a" |
|
60 datatype_compat ref |
|
61 |
58 |
62 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
59 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
63 "addr_of_array (Array x) = x" |
60 "addr_of_array (Array x) = x" |
64 |
61 |
65 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |
62 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |