Changeset 1993 for src/common


Ignore:
Timestamp:
May 24, 2012, 5:10:05 PM (8 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.

Location:
src/common
Files:
1 added
1 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1881 r1993  
    9595fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
    9696
    97 include "common/Mem.ma".
     97include "common/GenMem.ma".
    9898
    9999(* Hide the representation of memory to make displaying the results easier. *)
  • 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)).
  • src/common/Globalenvs.ma

    r1988 r1993  
    3737include "common/AST.ma".
    3838(*include "Values.ma".*)
    39 include "common/Mem.ma".
     39include "common/FrontEndMem.ma".
    4040
    4141   (* * The type of global environments.  The parameter [F] is the type
Note: See TracChangeset for help on using the changeset viewer.