Changeset 1993 for src/common

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:

• Animation.ma (modified) (1 diff)
• FrontEndMem.ma (added)
• GenMem.ma (modified) (1 diff)
• Globalenvs.ma (modified) (1 diff)
• Mem.ma (deleted)

src/common/Animation.ma

@@ -95 +95 @@
 fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
 
-include "common/Mem.ma".
+include "common/GenMem.ma".
 
 (* Hide the representation of memory to make displaying the results easier. *)

src/common/GenMem.ma

@@ -180 +180 @@
 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m).
 //; qed.
+
+
+(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
+definition do_if_in_bounds:
+ ∀A:Type[0]. mem → pointer → (block → block_contents → Z → A) → option A ≝
+ λS,m,ptr,F.
+  let b ≝ pblock ptr in
+  if Zltb (block_id b) (nextblock … m) then
+   let content ≝ blocks … m b in
+   let off ≝ offv (poff ptr) in
+   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
+    Some … (F b content off)
+   else
+    None ?
+  else
+   None ?.
+
+definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝
+ λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
+
+definition bestorev: ∀m:mem. ∀ptr:pointer. beval → option mem ≝
+ λm,ptr,v. do_if_in_bounds … m ptr
+  (λb,content,off.
+    let contents ≝ update … off v (contents … content) in
+    let content ≝ mk_block_contents (low … content) (high … content) contents in
+    let blocks ≝ update_block … b content (blocks … m) in
+     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).

src/common/Globalenvs.ma

@@ -37 +37 @@
 include "common/AST.ma".
 (*include "Values.ma".*)
-include "common/Mem.ma".
+include "common/FrontEndMem.ma".
 
    (* * The type of global environments.  The parameter [F] is the type