Changeset 1808 for src/RTLabs/Traces.ma
- Timestamp:
- Mar 6, 2012, 6:06:48 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1806 r1808 1707 1707 ] qed. 1708 1708 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. 1716 1713 *) 1717 1714 … … 1724 1721 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s) 1725 1722 (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 ≝ 1727 1724 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with 1728 1725 [ ex_intro n B ⇒ 1729 1726 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. True1727 return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s 1731 1728 with 1732 1729 [ 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 (* 1733 1733 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1734 1734 [ ex_intro T' _ ⇒ 1735 1735 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1736 ] 1736 ]*) 1737 1737 | 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 (* 1738 1741 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1739 1742 [ ex_intro T' _ ⇒ 1740 1743 ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? 1741 ] 1744 ]*) 1742 1745 ] STATEMENT_COSTLABEL 1743 1746 ]. 1744 1747 [ /2/ 1745 1748 | @(trace_any_label_label … T) 1749 | %{tr} @EV 1746 1750 | @(trace_any_call_call … T) 1747 | %{tr} @EV1748 | @I1749 1751 | /2/ 1750 1752 | @(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.