Changeset 1993 for src/common/GenMem.ma


Ignore:
Timestamp:
May 24, 2012, 5:10:05 PM (7 years ago)
Author:
campbell
Message:

Make front-end memory model only depend on the general definitions by
moving a few definitions from the back-end one. Give the front-end
model a more descriptive name.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r1988 r1993  
    180180lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m).
    181181//; qed.
     182
     183
     184(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
     185definition 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
     199definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝
     200 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
     201
     202definition 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)).
Note: See TracChangeset for help on using the changeset viewer.