Changeset 1808 for src/RTLabs/Traces.ma

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:

• src/RTLabs/Traces.ma (modified) (2 diffs)

src/RTLabs/Traces.ma

@@ -1707 +1707 @@
 ] qed.
 
-(* FIXME:
-
-   This isn't going to work in this form: the existential isn't the coinductive
-   type, so this isn't technically a cofixpoint.  Try to return just the
-   structured trace won't either, because the termination oracle is in Prop.
-   
-   Not sure how to get out of this situation...
+(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
+       a trace_label_diverges value, but I only know how to construct those
+       using a cofixpoint in Type[0], which means I can't use the termination
+       oracle.
 *)
 
@@ -1724 +1721 @@
   (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
   (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
-  : ∃T:trace_label_diverges (RTLabs_status ge) s. True ≝
+  : trace_label_diverges_exists (RTLabs_status ge) s ≝
 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
 [ ex_intro n B ⇒
     match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B
-      return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True
+      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
     with
     [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
+        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
+            tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
+(*
         match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
         [ ex_intro T' _ ⇒
             ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
-        ]
+        ]*)
     | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
+        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
+            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
+(*
         match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
         [ ex_intro T' _ ⇒
             ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
-        ]
+        ]*)
     ] STATEMENT_COSTLABEL
 ].
 [ /2/ 
 | @(trace_any_label_label … T)
+| %{tr} @EV
 | @(trace_any_call_call … T)
-| %{tr} @EV
-| @I
 | /2/
 | @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
-] (* XXX fails, see above. *) qed.
+] qed.