Ignore:
Timestamp:
Mar 6, 2012, 6:06:48 PM (8 years ago)
Author:
campbell
Message:

Create a Prop version of the non-terminating structured traces so that
I can at least show existence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1806 r1808  
    122122          trace_any_call S status_pre status_end.
    123123
     124             
     125inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
     126  | tlc_base:
     127      ∀start_status: S.
     128      ∀end_status: S.
     129        trace_any_call S start_status end_status →
     130        as_costed S start_status →
     131        trace_label_call S start_status end_status
     132.       
    124133
    125134coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
     
    138147        ∀H:as_classifier S status_pre_fun_call cl_call.
    139148          trace_label_diverges S status_start_fun_call →
    140             trace_label_diverges S status_initial
    141              
    142 with trace_label_call: S → S → Type[0] ≝
    143   | tlc_base:
    144       ∀start_status: S.
    145       ∀end_status: S.
    146         trace_any_call S start_status end_status →
    147         as_costed S start_status →
    148         trace_label_call S start_status end_status
    149 .       
     149            trace_label_diverges S status_initial.
     150
     151(* Version in Prop for showing existence. *)
     152coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
     153  | tld_step:
     154      ∀status_initial: S.
     155      ∀status_labelled: S.
     156          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
     157          trace_label_diverges_exists S status_labelled →
     158            trace_label_diverges_exists S status_initial
     159  | tld_base:
     160      ∀status_initial: S.
     161      ∀status_pre_fun_call: S.
     162      ∀status_start_fun_call: S.
     163        trace_label_call S status_initial status_pre_fun_call →
     164        as_execute S status_pre_fun_call status_start_fun_call →
     165        ∀H:as_classifier S status_pre_fun_call cl_call.
     166          trace_label_diverges_exists S status_start_fun_call →
     167            trace_label_diverges_exists S status_initial.
    150168
    151169let rec trace_any_label_label S s s' f
Note: See TracChangeset for help on using the changeset viewer.