Changeset 1993 for src/common
- Timestamp:
- May 24, 2012, 5:10:05 PM (8 years ago)
- Location:
- src/common
- Files:
-
- 1 added
- 1 deleted
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Animation.ma
r1881 r1993 95 95 fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)). 96 96 97 include "common/ Mem.ma".97 include "common/GenMem.ma". 98 98 99 99 (* Hide the representation of memory to make displaying the results easier. *) -
src/common/GenMem.ma
r1988 r1993 180 180 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m). 181 181 //; qed. 182 183 184 (* This function should be moved to common/GenMem.ma and replaces in_bounds *) 185 definition do_if_in_bounds: 186 ∀A:Type[0]. mem → pointer → (block → block_contents → Z → A) → option A ≝ 187 λS,m,ptr,F. 188 let b ≝ pblock ptr in 189 if Zltb (block_id b) (nextblock … m) then 190 let content ≝ blocks … m b in 191 let off ≝ offv (poff ptr) in 192 if andb (Zleb (low … content) off) (Zleb off (high … content)) then 193 Some … (F b content off) 194 else 195 None ? 196 else 197 None ?. 198 199 definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝ 200 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off). 201 202 definition bestorev: ∀m:mem. ∀ptr:pointer. beval → option mem ≝ 203 λm,ptr,v. do_if_in_bounds … m ptr 204 (λb,content,off. 205 let contents ≝ update … off v (contents … content) in 206 let content ≝ mk_block_contents (low … content) (high … content) contents in 207 let blocks ≝ update_block … b content (blocks … m) in 208 mk_mem … blocks (nextblock … m) (nextblock_pos … m)). -
src/common/Globalenvs.ma
r1988 r1993 37 37 include "common/AST.ma". 38 38 (*include "Values.ma".*) 39 include "common/ Mem.ma".39 include "common/FrontEndMem.ma". 40 40 41 41 (* * The type of global environments. The parameter [F] is the type
Note: See TracChangeset
for help on using the changeset viewer.