Changeset 1058


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

Evict CompCert? Maps interface in favour of BitVectorTries?.

Location:
src
Files:
1 deleted
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r964 r1058  
    276276  match e' with
    277277  [ Evar id ⇒
    278       match (get … id en) with
     278      match (lookup ?? en id) with
    279279      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
    280280      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
     
    330330  match h with [ pair id ty ⇒
    331331    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
    332       exec_alloc_variables (set … id b1 en) m1 vars
     332      exec_alloc_variables (add ?? en id b1) m1 vars
    333333]]].
    334334
     
    344344      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    345345      | cons v1 vl ⇒
    346           do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (get … id e);
     346          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
    347347          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
    348348          exec_bind_parameters e m1 params' vl
  • src/Clight/CexecComplete.ma

    r961 r1058  
    327327| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
    328328  < H3 whd in H1:(??%?) ⊢ (??%?)
    329     destruct (H1) @refl
     329  < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1)
     330  @refl
    330331] qed.
    331332
  • src/Clight/CexecSound.ma

    r961 r1058  
    206206| #v #ty
    207207    whd in ⊢ (???%);
    208     lapply (refl ? (get ident PTree block v en));
    209     cases (get ident PTree block v en) in ⊢ (???% → %);
     208    lapply (refl ? (lookup SymbolTag block en v))
     209    cases (lookup SymbolTag block en v) in ⊢ (???% → %)
    210210    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
    211211        whd; @(eval_Evar_global … eget efind)
  • 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
  • src/common/Identifiers.ma

    r1057 r1058  
    9191                                           (match m with [ an_id_map m' ⇒ m' ])).
    9292
     93(* Extract every identifier, value pair from the map. *)
     94definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
     95λtag,A,m.
     96  fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
     97           (match m with [ an_id_map m' ⇒ m' ]) [ ].
     98
    9399axiom MissingId : String.
    94100
Note: See TracChangeset for help on using the changeset viewer.