Changeset 2499 for src/RTLabs/semantics.ma
- Timestamp:
- Nov 28, 2012, 12:52:12 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/semantics.ma
r2475 r2499 49 49 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m. 50 50 51 definition next_instruction : frame → statement ≝ 52 λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f). 53 51 54 definition init_locals : list (register × typ) → register_env val ≝ 52 55 foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??). … … 89 92 match st return λ_. IO ??? with 90 93 [ State f fs m ⇒ 91 let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f)in94 let s ≝ next_instruction f in 92 95 match s return λs. labels_present ? s → IO ??? with 93 96 [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉 … … 271 274 whd in ⊢ (??%? → ?); 272 275 generalize in ⊢ (??(?%)? → ?); 273 cases ( lookup_present LabelTag statement (f_graph func) next next_ok)276 cases (next_instruction ?) 274 277 [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % 275 278 | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % … … 314 317 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m' 315 318 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 316 cases ( lookup_present … nok)319 cases (next_instruction ?) 317 320 (* Function call cases. *) 318 321 [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
Note: See TracChangeset
for help on using the changeset viewer.