Changeset 2688 for src/joint/Traces.ma


Ignore:
Timestamp:
Feb 21, 2013, 6:03:46 PM (7 years ago)
Author:
tranquil
Message:
  • in Arithmeticcs.ma: commented include that breaks script in latest matita
  • moved COST_LABEL out of joint_seq
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2681 r2688  
    102102  λp,stmt.
    103103  match stmt with
    104   [ step_seq _ ⇒ cl_other
    105   | CALL f args dest ⇒ cl_call
     104  [ CALL f args dest ⇒ cl_call
    106105  | COND _ _ ⇒ cl_jump
     106  | _ ⇒ cl_other
    107107  ].
    108108
     
    124124  | final s ⇒ Some ? (joint_classify_final p s)
    125125  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    126   ].
    127 
    128 definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
    129   λp,g,s.match s with
    130   [ COST_LABEL _ ⇒ False
    131   | _ ⇒ True
    132126  ].
    133127
     
    145139  >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
    146140]
    147 * [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
     141* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    148142normalize in ⊢ (%→?); #EQ destruct
    149143%[|%[|%[|%[|%[| %]]]]]
     
    266260  [ sequential s _ ⇒
    267261    match s with
    268     [ step_seq s ⇒
    269       match s with
    270       [ COST_LABEL lbl ⇒ Some ? lbl
    271       | _ ⇒ None ?
    272       ]
     262    [  COST_LABEL lbl ⇒ Some ? lbl
    273263    | _ ⇒ None ?
    274264    ]
    275265  | _ ⇒ None ?
    276266  ].
    277 
    278 
    279 lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
    280 no_cost_label p (globals p) s →
    281 cost_label_of_stmt … (sequential … s nxt) = None ?.
    282 #p * // #lbl #next *
    283 qed.
    284267
    285268definition joint_abstract_status :
Note: See TracChangeset for help on using the changeset viewer.