Changeset 1926

Timestamp:

05/08/12 18:09:02 (13 months ago)

Author:

tranquil

Message:

* added as_label to abstract status, with as_costed defined with it. This temporarily breaks stuff around
* defined a relation on traces which tells that their shapes and labels are the same

Files:

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

src/common/StructuredTraces.ma

@@ -2 +2 @@
 include "basics/bool.ma".
 include "basics/jmeq.ma".
+include "common/CostLabel.ma".
+include "utilities/option.ma".
 include "basics/lists/listb.ma".
 include "ASM/Util.ma".
@@ -12 +14 @@
 
 record abstract_status : Type[1] ≝
-{   
-    as_status :> Type[0]
+  { as_status :> Type[0]
   ; as_execute : as_status → as_status → Prop
   ; as_pc : DeqSet
   ; as_pc_of : as_status → as_pc
   ; as_classifier : as_status → status_class → Prop
-  ; as_costed : as_status → Prop
+  ; as_label : as_status → option costlabel
   ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
   ; as_final: as_status → Prop
@@ -25 +26 @@
 (* temporary alias for backward compatibility *)
 definition final_abstract_status ≝ abstract_status.
+
+definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
+  λa_s,st.as_label ? st ≠ None ?.
+
+definition as_label_safe : ∀a_s : abstract_status.
+  (Σs : a_s.as_costed ? s) → costlabel ≝
+  λa_s,st_sig.opt_safe … (pi2 … st_sig).
 
 inductive trace_ends_with_ret: Type[0] ≝
@@ -113 +121 @@
  | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
  ].
- 
-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 ≝
@@ -146 +140 @@
     bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
     tal_unrepeating … tl
-  | tal_base_call status_pre_fun_call status_start_fun_call status_final _ _ _
-      fun_call_trace _ ⇒ tlr_unrepeating … fun_call_trace
   | _ ⇒ True
+  ].
+
+definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
+  trace_label_label S fl st1 st2 → costlabel ≝
+  λS,fl,st1,st2,tr.match tr with
+  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
+
+definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
+  trace_label_return S st1 st2 → costlabel ≝
+  λS,st1,st2,tr.match tr with
+  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
+  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
   ].
 
@@ -196 +200 @@
 .
 
+definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
+  trace_label_call S st1 st2 → costlabel ≝
+  λ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:
@@ -212 +222 @@
           trace_label_diverges S status_start_fun_call →
             trace_label_diverges S status_initial.
+
+definition tld_hd_label : ∀S : abstract_status.∀st.
+  trace_label_diverges S st → costlabel ≝
+  λS,st,tr.match tr with
+  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
+  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
+  ].       
 
 (* Version in Prop for showing existence. *)
@@ -279 +296 @@
 ].
 
+definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
+  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
+  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
+
 lemma trace_label_label_label : ∀S,s,s',f.
   ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
@@ -285 +306 @@
 #f #start #end #tr' #C @(trace_any_label_label … tr')
 qed.
+
+definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
+  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
+  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
 
 lemma trace_any_call_call : ∀S,s,s'.
@@ -338 +363 @@
   ].
 
-(* TODO: use as_label for forcing same labels *)
 let rec tlr_rel S1 st1 st1' S2 st2 st2'
   (tlr1 : trace_label_return S1 st1 st1')
@@ -359 +383 @@
  (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
   match tll1 with
-  [ tll_base fl1 st1 st1' tal1 _ ⇒
+  [ tll_base fl1 st1 st1' tal1 H ⇒
     match tll2 with
-    [ tll_base fl2 st2 st2 tal2 _ ⇒ tal_rel … tal1 tal2
+    [ tll_base fl2 st2 st2 tal2 G ⇒
+      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
+      tal_rel … tal1 tal2
     ]
   ]
@@ -389 +415 @@
   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
     tal_rel … tl1 tal2 (* <- this makes it many to many *)
-  ]. 
+  ].