Changeset 3525

Timestamp:

Mar 11, 2015, 5:20:05 PM (5 years ago)

Author:

sacerdot

Message:

• dead code removed + improved (?) comment

File:

• LTS/Language.ma (modified) (1 diff)

LTS/Language.ma

@@ -645 +645 @@
        | _ ⇒ (* 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 
+*)