Changeset 1058 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jul 6, 2011, 1:29:58 PM (8 years ago)
Author:
campbell
Message:

Evict CompCert? Maps interface in favour of BitVectorTries?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r964 r1058  
    2525include "common/Globalenvs.ma".
    2626include "Clight/Csyntax.ma".
    27 include "common/Maps.ma".
    2827(*include "Events.ma".*)
    2928include "common/Smallstep.ma".
     
    482481  block. *)
    483482
    484 definition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    485 
    486 definition empty_env: env ≝ (empty …).
     483definition env ≝ identifier_map SymbolTag block. (* map variable -> location *)
     484
     485definition empty_env: env ≝ (empty_map …).
    487486
    488487(* * [load_value_of_type ty m b ofs] computes the value of a datum
     
    535534      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    536535      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    537       alloc_variables (set … id b1 e) m1 vars e2 m2 →
     536      alloc_variables (add … e id b1) m1 vars e2 m2 →
    538537      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    539538
     
    551550  | bind_parameters_cons:
    552551      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    553       get ??? id e = Some ? b →
     552      lookup ?? e id = Some ? b →
    554553      store_value_of_type ty m b zero_offset v1 = Some ? m1 →
    555554      bind_parameters e m1 params vl m2 →
     
    559558
    560559definition blocks_of_env : env → list block ≝ λe.
    561   map ?? (λx. snd ?? x) (elements ??? e).
     560  map ?? (λx. snd ?? x) (elements ?? e).
    562561
    563562(* * Selection of the appropriate case of a [switch], given the value [n]
     
    666665with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝
    667666  | eval_Evar_local:   ∀id,l,ty.
    668       (* XXX notation? e!id*) get ??? id e = Some ? l →
     667      (* XXX notation? e!id*) lookup ?? e id = Some ? l →
    669668      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    670669  | eval_Evar_global: ∀id,l,ty.
    671       (* XXX e!id *) get ??? id e = None ? →
     670      (* XXX e!id *) lookup ?? e id = None ? →
    672671      find_symbol ?? ge id = Some ? l →
    673672      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
Note: See TracChangeset for help on using the changeset viewer.