Changeset 1901 for src/common


Ignore:
Timestamp:
Apr 26, 2012, 3:35:01 PM (8 years ago)
Author:
mulligan
Message:

Slight changes to StructuredTraces?: should not change too much

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1880 r1901  
    99| cl_other : status_class.
    1010
    11 record abstract_status : Type[1] ≝ {
     11record abstract_status : Type[1] ≝
     12{
    1213  as_status :> Type[0];
    1314  as_execute : as_status → as_status → Prop;
    1415  as_classifier : as_status → status_class → Prop;
    1516  as_costed : as_status → Prop;
    16   as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
     17  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop;
     18  as_program_counters_properly_related: as_status → as_status → Prop
    1719}.
    1820
     
    6971          trace_label_return S status_start_fun_call status_final →
    7072          as_costed S status_final →
     73          as_program_counters_properly_related S status_pre_fun_call status_final →
    7174            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
    7275  (* A call followed by a non-empty trace. *)
     
    8285          trace_label_return S status_start_fun_call status_after_fun_call →
    8386          ¬ as_costed S status_after_fun_call →
     87          as_program_counters_properly_related S status_pre_fun_call status_after_fun_call →
    8488          trace_any_label S end_flag status_after_fun_call status_final →
    8589            trace_any_label S end_flag status_pre_fun_call status_final
     
    121125        ¬ (as_costed S status_init) →
    122126          trace_any_call S status_pre status_end.
    123 
    124127             
    125128inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
     
    216219[ tal_base_not_return start final _ _ C ⇒ C
    217220| tal_base_return _ _  _ _ ⇒ I
    218 | tal_base_call _ _ _ _ _ _ _ C ⇒ C
    219 | tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
     221| tal_base_call _ _ _ _ _ _ _ C _ ⇒ C
     222| tal_step_call f pre start after final X C RET PROPER LR C' tr' ⇒ trace_any_label_label … tr'
    220223| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    221224].
Note: See TracChangeset for help on using the changeset viewer.