Changeset 2010
 Timestamp:
 May 31, 2012, 3:10:30 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r1999 r2010 43 43 (* Functions are given negative block numbers *) 44 44 record genv_t (F:Type[0]) : Type[0] ≝ { 45 functions: block → optionF;46 nextfunction: Z;47 symbols: ident → optionblock45 functions: positive_map F; 46 nextfunction: Pos; 47 symbols: identifier_map SymbolTag block 48 48 }. 49 49 … … 51 51 λF,name_fun,g. 52 52 let blk_id ≝ nextfunction ? g in 53 let b ≝ mk_block Code blk_idin54 mk_genv_t F ( (*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b'))55 ( Zpredblk_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). 57 57 58 58 definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝ 59 59 λ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). 63 63 64 64 (* Construct environment and initial memory store *) 65 65 definition empty_mem ≝ empty. (* XXX*) 66 66 definition 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 ??). 69 68 70 69 definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝ 71 70 λF,init,fns. 72 71 foldr ?? (add_funct F) init fns. 72 73 (* Return the address of the given global symbol, if any. *) 74 definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝ 75 λF,ge. lookup ?? (symbols … ge). 73 76 74 77 (* init *) … … 87 90  Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n) 88 91  Init_addrof r' symb ofs ⇒ 89 match (*find_symbol ge symb*) symbols ?ge symb with92 match find_symbol … ge symb with 90 93 [ None ⇒ None ? 91 94  Some b' ⇒ … … 179 182 let init ≝ extract_init init_info in 180 183 do st ← st; 181 match symbols ?g id with184 match find_symbol … g id with 182 185 [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init) 183 186  None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *) … … 215 218 (* Return the function description associated with the given address, if any. *) 216 219 definition 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 ? ]. 218 223 219 224 (* Same as [find_funct_ptr] but the function address is given as 220 225 a value, which must be a pointer with offset 0. *) 221 226 definition 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 ? ]. 227 228 228 229 … … 235 236  #f #fn #E normalize in E; destruct 236 237  #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:(??%?); 238 239 cases off in E ⊢ %; [ 2,3: #x ] 239 #E normalize in E; destruct240 #E whd in E:(??%?); destruct 240 241 %{pty} %{b} %{c} % // @E 241 242 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.