Changeset 1574 for src/common


Ignore:
Timestamp:
Nov 28, 2011, 5:57:47 PM (8 years ago)
Author:
campbell
Message:

A little more progress on traces on RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1544 r1574  
    131131        ¬ (as_costed S status_pre) →
    132132          trace_any_call S status_pre status_end.
     133
     134let rec trace_any_label_label S s s' f
     135  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
     136match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
     137[ tal_base_not_return start final _ _ C ⇒ C
     138| tal_base_return _ _  _ _ ⇒ I
     139| tal_step_call f pre start after final X C RET LR tr' ⇒ trace_any_label_label … tr'
     140| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
     141].
     142
     143lemma trace_label_label_label : ∀S,s,s',f.
     144  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
     145#S #s #s' #f #tr
     146cases tr
     147#f #start #end #tr' #C @(trace_any_label_label … tr')
     148qed.
     149
Note: See TracChangeset for help on using the changeset viewer.