Changeset 1927 for src/common

Timestamp:

May 9, 2012, 1:05:21 PM (8 years ago)

Author:

mulligan

Message:

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.

File:

• src/common/StructuredTraces.ma (modified) (4 diffs)

src/common/StructuredTraces.ma

@@ -14 +14 @@
 
 record abstract_status : Type[1] ≝
-  { as_status :> Type[0]
+{ 
+    as_status :> Type[0]
   ; as_execute : as_status → as_status → Prop
   ; as_pc : DeqSet
@@ -122 +123 @@
  ].
 
+definition as_trace_any_label_length':
+    ∀S: abstract_status.
+    ∀trace_ends_flag: trace_ends_with_ret.
+    ∀start_status: S.
+    ∀final_status: S.
+    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
+      nat ≝
+  λS: abstract_status.
+  λtrace_ends_flag: trace_ends_with_ret.
+  λstart_status: S.
+  λfinal_status: S.
+  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
+    |tal_pc_list … the_trace|.
+
 let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
   match tlr with
@@ -140 +155 @@
     bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
     tal_unrepeating … tl
+  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
   | _ ⇒ True
   ].
@@ -204 +220 @@
   λS,st1,st2,tr.match tr with
   [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
-  ].       
-
+  ].
+   
 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
   | tld_step: