Changeset 2010


Ignore:
Timestamp:
May 31, 2012, 3:10:30 PM (5 years ago)
Author:
campbell
Message:

Make globalenvs use proper maps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1999 r2010  
    4343(* Functions are given negative block numbers *)
    4444record genv_t (F:Type[0]) : Type[0] ≝ {
    45   functions: block → option F;
    46   nextfunction: Z;
    47   symbols: ident → option block
     45  functions: positive_map F;
     46  nextfunction: Pos;
     47  symbols: identifier_map SymbolTag block
    4848}.
    4949
     
    5151λF,name_fun,g.
    5252  let blk_id ≝ nextfunction ? g in
    53   let b ≝ mk_block Code blk_id in
    54   mk_genv_t F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
    55               (Zpred blk_id)
    56               ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? g i) ]).
     53  let b ≝ mk_block Code (neg blk_id) in
     54  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g))
     55              (succ blk_id)
     56              (add ?? (symbols … g) (\fst name_fun) b).
    5757
    5858definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
    5959λF,name,b,g.
    60   mk_genv_t F (functions ? g)
    61               (nextfunction ? g)
    62               ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b | inr _ ⇒ symbols ? g i ]).
     60  mk_genv_t F (functions g)
     61              (nextfunction g)
     62              (add ?? (symbols … g) name b).
    6363
    6464(* Construct environment and initial memory store *)
    6565definition empty_mem ≝ empty. (* XXX*)
    6666definition empty : ∀F. genv_t F ≝
    67   λF. mk_genv_t F (λ_. None ?) (-2) (λ_. None ?).
    68 (*  mkgenv (ZMap.init None) (-2) (PTree.empty block).*)
     67  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??).
    6968
    7069definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
    7170λF,init,fns.
    7271  foldr ?? (add_funct F) init fns.
     72
     73(* Return the address of the given global symbol, if any. *)
     74definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
     75λF,ge. lookup ?? (symbols … ge).
    7376
    7477(* init *)
     
    8790  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
    8891  | Init_addrof r' symb ofs ⇒
    89       match (*find_symbol ge symb*) symbols ? ge symb with
     92      match find_symbol … ge symb with
    9093      [ None ⇒ None ?
    9194      | Some b' ⇒
     
    179182      let init ≝ extract_init init_info in
    180183        do st ← st;
    181         match symbols ? g id with
     184        match find_symbol … g id with
    182185        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
    183186        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
     
    215218(* Return the function description associated with the given address, if any. *)
    216219definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝
    217 λF,ge. functions ? ge.
     220λF,ge,b. match block_region b with [ Code ⇒
     221           match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge)
     222         | _ ⇒ None ? ] | _ ⇒ None ? ].
    218223
    219224(* Same as [find_funct_ptr] but the function address is given as
    220225   a value, which must be a pointer with offset 0. *)
    221226definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝
    222 λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then functions ? ge (pblock ptr) else None ? | _ ⇒ None ? ].
    223 
    224 (* Return the address of the given global symbol, if any. *)
    225 definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
    226 λF,ge. symbols ? ge.
     227λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then find_funct_ptr … ge (pblock ptr) else None ? | _ ⇒ None ? ].
    227228
    228229
     
    235236| #f #fn #E normalize in E; destruct
    236237| #r #f #E normalize in E; destruct
    237 | * #pty #b #c * #off #f #E normalize in E;
     238| * #pty #b #c * #off #f #E whd in E:(??%?);
    238239  cases off in E ⊢ %; [ 2,3: #x ]
    239   #E normalize in E; destruct
     240  #E whd in E:(??%?); destruct
    240241  %{pty} %{b} %{c} % // @E
    241242] qed.
Note: See TracChangeset for help on using the changeset viewer.