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 |
56 datatype_new 'a array = Array addr -- "note the phantom type 'a" |
57 datatype_new 'a ref = Ref addr -- "note the phantom type 'a " |
57 datatype_compat array |
|
58 |
|
59 datatype_new 'a ref = Ref addr -- "note the phantom type 'a" |
|
60 datatype_compat ref |
58 |
61 |
59 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
62 primrec addr_of_array :: "'a array \<Rightarrow> addr" where |
60 "addr_of_array (Array x) = x" |
63 "addr_of_array (Array x) = x" |
61 |
64 |
62 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |
65 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where |