Changeset 3588 for LTS


Ignore:
Timestamp:
Jul 20, 2015, 2:52:13 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3587 r3588  
    458458frame_assign_var st v val = return new_st →
    459459var_instr_bond_ok (\fst new_st) i ct.
    460 ** [|#x #xs] #fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
     460** [(*empty list activation frame*)|(*non empty list activation frame*)#x #xs]
     461#fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
    461462inversion(divide_continuation_on_frames ct [i])
    462 [1,3:#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
     463[1,3:(* divide_continuation_on_frames ct [i] is nil*)
     464#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
    463465>IH whd in match (frame_assign_var ???); inversion(new_st)
    464466#l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN
    465467whd normalize in HN; destruct]
    466 |#lfi #llfi #IH0 #INV0 normalize nodelta #ABS cases ABS
    467 |#lfi #llfi #IH0 #INV0 normalize nodelta
    468 
     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
     473inversion(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]
    469479
    470480cases daemon
Note: See TracChangeset for help on using the changeset viewer.