Changeset 1536 for src/common


Ignore:
Timestamp:
Nov 23, 2011, 12:07:03 PM (8 years ago)
Author:
campbell
Message:

Use predicates throughout the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1532 r1536  
    1212  as_status :> Type[0];
    1313  as_execute : as_status → as_status → Prop;
    14   as_classifier : as_status → status_class;
    15   as_after_return : (Σs:as_status. as_classifier s = cl_call) → as_status → bool
     14  as_classifier : as_status → status_class → Prop;
     15  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    1616}.
    1717
     
    3939      ∀end_status: S.
    4040        trace_any_label S ends_flag start_status end_status →
    41         as_classifier S start_status = cl_cost →
     41        as_classifier S start_status cl_cost →
    4242          trace_label_label S ends_flag start_status end_status
    4343with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
     
    4646      ∀final_status: S.
    4747        as_execute S start_status final_status →
    48         as_classifier S start_status ≠ cl_return →
    49         as_classifier S final_status = cl_cost →
     48        ¬ as_classifier S start_status cl_return →
     49        as_classifier S final_status cl_cost →
    5050          trace_any_label S doesnt_end_with_ret start_status final_status
    5151  | tal_base_return:
     
    5353      ∀final_status: S.
    5454        as_execute S start_status final_status →
    55         as_classifier S start_status = cl_return →
     55        as_classifier S start_status cl_return →
    5656          trace_any_label S ends_with_ret start_status final_status
    5757  | tal_step_call:
     
    6262      ∀status_start_fun_call: S.
    6363        as_execute S status_pre_fun_call status_start_fun_call →
    64         ∀H:as_classifier S status_pre_fun_call = cl_call.
    65           as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call = true
     64        ∀H:as_classifier S status_pre_fun_call cl_call.
     65          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call
    6666          trace_label_return S status_start_fun_call status_after_fun_call →
    6767          trace_any_label S end_flag status_after_fun_call status_final →
     
    7474        as_execute S status_pre status_init →
    7575        trace_any_label S end_flag status_init status_end →
    76         as_classifier S status_pre = cl_nocost →
     76        as_classifier S status_pre cl_nocost →
    7777          trace_any_label S end_flag status_pre status_end.
    7878
     
    9292        trace_label_call S status_initial status_pre_fun_call →
    9393        as_execute S status_pre_fun_call status_start_fun_call →
    94         ∀H:as_classifier S status_pre_fun_call = cl_call.
     94        ∀H:as_classifier S status_pre_fun_call cl_call.
    9595          trace_label_diverges S status_start_fun_call →
    9696            trace_label_diverges S status_initial
     
    101101      ∀end_status: S.
    102102        trace_any_call S start_status end_status →
    103         as_classifier S start_status = cl_cost →
     103        as_classifier S start_status cl_cost →
    104104        trace_label_call S start_status end_status
    105105       
     
    107107  | tac_base:
    108108      ∀status: S.
    109         as_classifier S status = cl_call →
     109        as_classifier S status cl_call →
    110110          trace_any_call S status status
    111111  | tac_step_call:
     
    115115      ∀status_start_fun_call: S.
    116116        as_execute S status_pre_fun_call status_start_fun_call →
    117         ∀H:as_classifier S status_pre_fun_call = cl_call.
    118           as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call = true
     117        ∀H:as_classifier S status_pre_fun_call cl_call.
     118          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call
    119119          trace_label_return S status_start_fun_call status_after_fun_call →
    120120          trace_any_call S status_after_fun_call status_final →
     
    126126        as_execute S status_pre status_init →
    127127        trace_any_call S status_init status_end →
    128         as_classifier S status_pre = cl_nocost →
     128        as_classifier S status_pre cl_nocost →
    129129          trace_any_call S status_pre status_end.
    130130
Note: See TracChangeset for help on using the changeset viewer.