# Changeset 3525

Ignore:
Timestamp:
Mar 11, 2015, 5:20:05 PM (6 years ago)
Message:
• dead code removed + improved (?) comment
File:
1 edited

Unmodified
Added
Removed
• ## LTS/Language.ma

 r3483 | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). (* definition check_continuations : ∀p : instr_params. ∀l1,l2 : list (ActionLabel × (Instructions p)). associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) →  option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ λp,cont1,cont2,m,keep,abs_top,abs_tail. foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 (λx,y,z. let 〈cond,abs_top',abs_tail'〉 ≝ x in match call_post_clean p (\snd z) m keep abs_top' with [ None ⇒ 〈False,nil ?,nil ?〉 | Some w ⇒ match \fst z with [ ret_act opt_x ⇒ match ret_costed_abs keep opt_x with [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 | None ⇒ 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 ] | cost_act opt_x ⇒ match opt_x with [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *) (* in input : abs_top is the list of labels to be propageted to the deepest level of the call stack equivalently (?) is the list of labels I need to pay now abs_tail are the lists of labels to be propagated to the levels "below" the deepest level equivalently (?) is the list of labels I must have already payid in the code already executed; generated by the continuations below me in the stack in output : abs_top is the list of labels to be propageted from the current level of the call stack abs_tail are the lists of labels to be propagated from the levels "below" the current level *) non empty only in the case of non-call stack frames (whiles, ifs, etc; but in practice it is always nil!) abs_tail are the lists of labels to be propagated from the levels "below" the current level or equivalently (?) the list of labels I must have already paied in the code already executed; generated by this level of the stack *)
Note: See TracChangeset for help on using the changeset viewer.