Changeset 3525
 Timestamp:
 Mar 11, 2015, 5:20:05 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3483 r3525 645 645  _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). 646 646 647 (*648 definition check_continuations : ∀p : instr_params.649 ∀l1,l2 : list (ActionLabel × (Instructions p)).650 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →651 list (list CostLabel) → option (Prop × (list CostLabel) × (list (list CostLabel))) ≝652 λp,cont1,cont2,m,keep,abs_top,abs_tail.653 foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2654 (λx,y,z.655 let 〈cond,abs_top',abs_tail'〉 ≝ x in656 match call_post_clean p (\snd z) m keep abs_top' with657 [ None ⇒ 〈False,nil ?,nil ?〉658  Some w ⇒659 match \fst z with660 [ ret_act opt_x ⇒661 match ret_costed_abs keep opt_x with662 [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧663 get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉664  None ⇒665 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉666 ]667  cost_act opt_x ⇒668 match opt_x with669 [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉670  Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧671 get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]672  _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *)673 647 (* in input : 674 648 abs_top is the list of labels to be propageted to the deepest level of the call stack 649 equivalently (?) is the list of labels I need to pay now 650 675 651 abs_tail are the lists of labels to be propagated to the levels "below" the deepest level 652 equivalently (?) is the list of labels I must have already payid in the 653 code already executed; generated by the continuations below me in the stack 676 654 in output : 677 655 abs_top is the list of labels to be propageted from the current level of the call stack 678 abs_tail are the lists of labels to be propagated from the levels "below" the current level 679 *) 656 non empty only in the case of noncall stack frames (whiles, ifs, etc; but in 657 practice it is always nil!) 658 abs_tail are the lists of labels to be propagated from the levels "below" the current level 659 or equivalently (?) the list of labels I must have already paied in the code 660 already executed; generated by this level of the stack 661 *) 680 662 681 663
Note: See TracChangeset
for help on using the changeset viewer.