Changeset 3589


Ignore:
Timestamp:
Jul 20, 2015, 3:48:33 PM (4 years ago)
Author:
piccolo
Message:

closed second daemon

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3588 r3589  
    458458frame_assign_var st v val = return new_st →
    459459var_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
     462inversion(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;
     466normalize nodelta #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct
     467whd <(append_nil … [?]) >divide_continuation_on_frame_app
     468>EQdivide normalize nodelta % // % // <(len_update … y … EQnew_frm) //
     469qed.
     470
    482471
    483472lemma var_instr_bond_seq_ok : ∀st.
Note: See TracChangeset for help on using the changeset viewer.