Changeset 3525


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

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3483 r3525  
    645645       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]).
    646646
    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 cont2
    654  (λx,y,z.
    655    let 〈cond,abs_top',abs_tail'〉 ≝ x in
    656    match call_post_clean p (\snd z) m keep abs_top' with
    657    [ None ⇒ 〈False,nil ?,nil ?〉
    658    | Some w ⇒
    659       match \fst z with
    660        [ ret_act opt_x ⇒
    661            match ret_costed_abs keep opt_x with
    662            [ 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 with
    669            [ 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 ?〉]]). *)
    673647(* in input :
    674648     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
    675651     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
    676654   in output :
    677655     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 non-call 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*)       
    680662       
    681663
Note: See TracChangeset for help on using the changeset viewer.