Changeset 1058 for src/Clight/Csem.ma

Timestamp:

Jul 6, 2011, 1:29:58 PM (8 years ago)

Author:

campbell

Message:

Evict CompCert? Maps interface in favour of BitVectorTries?.

File:

• src/Clight/Csem.ma (modified) (6 diffs)

src/Clight/Csem.ma

@@ -25 +25 @@
 include "common/Globalenvs.ma".
 include "Clight/Csyntax.ma".
-include "common/Maps.ma".
 (*include "Events.ma".*)
 include "common/Smallstep.ma".
@@ -482 +481 @@
   block. *)
 
-definition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
-
-definition empty_env: env ≝ (empty …).
+definition env ≝ identifier_map SymbolTag block. (* map variable -> location *)
+
+definition empty_env: env ≝ (empty_map …).
 
 (* * [load_value_of_type ty m b ofs] computes the value of a datum
@@ -535 +534 @@
       ∀e,m,id,ty,vars,m1,b1,m2,e2.
       alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
-      alloc_variables (set … id b1 e) m1 vars e2 m2 →
+      alloc_variables (add … e id b1) m1 vars e2 m2 →
       alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
 
@@ -551 +550 @@
   | bind_parameters_cons:
       ∀e,m,id,ty,params,v1,vl,b,m1,m2.
-      get ??? id e = Some ? b →
+      lookup ?? e id = Some ? b →
       store_value_of_type ty m b zero_offset v1 = Some ? m1 →
       bind_parameters e m1 params vl m2 →
@@ -559 +558 @@
 
 definition blocks_of_env : env → list block ≝ λe.
-  map ?? (λx. snd ?? x) (elements ??? e).
+  map ?? (λx. snd ?? x) (elements ?? e).
 
 (* * Selection of the appropriate case of a [switch], given the value [n]
@@ -666 +665 @@
 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝
   | eval_Evar_local:   ∀id,l,ty.
-      (* XXX notation? e!id*) get ??? id e = Some ? l →
+      (* XXX notation? e!id*) lookup ?? e id = Some ? l →
       eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
   | eval_Evar_global: ∀id,l,ty.
-      (* XXX e!id *) get ??? id e = None ? →
+      (* XXX e!id *) lookup ?? e id = None ? →
       find_symbol ?? ge id = Some ? l →
       eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0