Changeset 1808 for src/RTLabs/Traces.ma


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/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.
Note: See TracChangeset for help on using the changeset viewer.