Changeset 1808


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.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1806 r1808  
    17071707] qed.
    17081708
    1709 (* FIXME:
    1710 
    1711    This isn't going to work in this form: the existential isn't the coinductive
    1712    type, so this isn't technically a cofixpoint.  Try to return just the
    1713    structured trace won't either, because the termination oracle is in Prop.
    1714    
    1715    Not sure how to get out of this situation...
     1709(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
     1710       a trace_label_diverges value, but I only know how to construct those
     1711       using a cofixpoint in Type[0], which means I can't use the termination
     1712       oracle.
    17161713*)
    17171714
     
    17241721  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    17251722  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    1726   : ∃T:trace_label_diverges (RTLabs_status ge) s. True
     1723  : trace_label_diverges_exists (RTLabs_status ge) s
    17271724match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
    17281725[ ex_intro n B ⇒
    17291726    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B
    1730       return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True
     1727      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    17311728    with
    17321729    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
     1730        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1731            tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
     1732(*
    17331733        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
    17341734        [ ex_intro T' _ ⇒
    17351735            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    1736         ]
     1736        ]*)
    17371737    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
     1738        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1739            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
     1740(*
    17381741        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
    17391742        [ ex_intro T' _ ⇒
    17401743            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
    1741         ]
     1744        ]*)
    17421745    ] STATEMENT_COSTLABEL
    17431746].
    17441747[ /2/
    17451748| @(trace_any_label_label … T)
     1749| %{tr} @EV
    17461750| @(trace_any_call_call … T)
    1747 | %{tr} @EV
    1748 | @I
    17491751| /2/
    17501752| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
    1751 ] (* XXX fails, see above. *) qed.
     1753] qed.
  • 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.