Changeset 3588
- Timestamp:
- Jul 20, 2015, 2:52:13 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/variable_stack_pass.ma
r3587 r3588 458 458 frame_assign_var st v val = return new_st → 459 459 var_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 ⊢(%→?→?); 461 462 inversion(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] 463 465 >IH whd in match (frame_assign_var ???); inversion(new_st) 464 466 #l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN 465 467 whd 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 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 ] 469 479 470 480 cases daemon
Note: See TracChangeset
for help on using the changeset viewer.