Changeset 3589
- Timestamp:
- Jul 20, 2015, 3:48:33 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/variable_stack_pass.ma
r3588 r3589 458 458 frame_assign_var st v val = return new_st → 459 459 var_instr_bond_ok (\fst new_st) i ct. 460 ** [(*empty list activation frame*)|(*non empty list activation frame*)#x #xs] 461 #fp #i #ct #v #val #new_st whd in ⊢(%→?→?); 462 inversion(divide_continuation_on_frames ct [i]) 463 [1,3:(* divide_continuation_on_frames ct [i] is nil*) 464 #IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS] 465 >IH whd in match (frame_assign_var ???); inversion(new_st) 466 #l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN 467 whd normalize in HN; destruct] 468 |(*divide_continuation_on_frames not nil *)2,4: 469 #lfi #llfi #IH0 #INV0 normalize nodelta] [#ABS cases ABS 470 |whd in match(frame_assign_var ???); inversion(new_st) #newl #newp 471 #_ normalize nodelta * #H1A #H1B 472 473 inversion(assign_frame x (to_shift+v) (\fst fp) val) 474 [2: #ll] #INVaf normalize nodelta 475 #Hrr elim newl whd >INV0 normalize nodelta 476 [2: #ln #lln #IHl] whd >INV0 normalize nodelta try(%) 477 478 ] 479 480 cases daemon 481 qed. 460 * #act_frm #fp #i #ct #v #val * #new_st #new_fp whd in ⊢ (% → ?); 461 <(append_nil … [?]) >divide_continuation_on_frame_app 462 inversion(divide_continuation_on_frames …) normalize nodelta 463 [|#x #xs #_] #EQdivide cases act_frm -act_frm [2,4: #y #ys] ** 464 #H1 #H2 #H3 change with (m_bind ?????) in ⊢ (??%? → ?); 465 #H cases(bind_inversion ????? H) -H #new_frm * whd in match assign_frame; 466 normalize nodelta #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct 467 whd <(append_nil … [?]) >divide_continuation_on_frame_app 468 >EQdivide normalize nodelta % // % // <(len_update … y … EQnew_frm) // 469 qed. 470 482 471 483 472 lemma var_instr_bond_seq_ok : ∀st.
Note: See TracChangeset
for help on using the changeset viewer.