equal
deleted
inserted
replaced
50 where "lookup_obj s a' == the (heap s (the_Addr a'))" |
50 where "lookup_obj s a' == the (heap s (the_Addr a'))" |
51 |
51 |
52 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where |
52 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where |
53 "raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo" |
53 "raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo" |
54 |
54 |
55 text {* Make new_Addr completely specified (at least for the code generator) *} |
55 text {* Make @{text new_Addr} completely specified (at least for the code generator) *} |
56 (* |
56 (* |
57 definition new_Addr :: "aheap => loc \<times> val option" where |
57 definition new_Addr :: "aheap => loc \<times> val option" where |
58 "new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))" |
58 "new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))" |
59 *) |
59 *) |
60 consts nat_to_loc' :: "nat => loc'" |
60 consts nat_to_loc' :: "nat => loc'" |