Changeset 1926 for src/common


Ignore:
Timestamp:
May 8, 2012, 6:09:02 PM (8 years 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1921 r1926  
    22include "basics/bool.ma".
    33include "basics/jmeq.ma".
     4include "common/CostLabel.ma".
     5include "utilities/option.ma".
    46include "basics/lists/listb.ma".
    57include "ASM/Util.ma".
     
    1214
    1315record abstract_status : Type[1] ≝
    14 {   
    15     as_status :> Type[0]
     16  { as_status :> Type[0]
    1617  ; as_execute : as_status → as_status → Prop
    1718  ; as_pc : DeqSet
    1819  ; as_pc_of : as_status → as_pc
    1920  ; as_classifier : as_status → status_class → Prop
    20   ; as_costed : as_status → Prop
     21  ; as_label : as_status → option costlabel
    2122  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    2223  ; as_final: as_status → Prop
     
    2526(* temporary alias for backward compatibility *)
    2627definition final_abstract_status ≝ abstract_status.
     28
     29definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
     30  λa_s,st.as_label ? st ≠ None ?.
     31
     32definition as_label_safe : ∀a_s : abstract_status.
     33  (Σs : a_s.as_costed ? s) → costlabel ≝
     34  λa_s,st_sig.opt_safe … (pi2 … st_sig).
    2735
    2836inductive trace_ends_with_ret: Type[0] ≝
     
    113121 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    114122 ].
    115  
    116 definition as_trace_any_label_length':
    117     ∀S: abstract_status.
    118     ∀trace_ends_flag: trace_ends_with_ret.
    119     ∀start_status: S.
    120     ∀final_status: S.
    121     ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
    122       nat ≝
    123   λS: abstract_status.
    124   λtrace_ends_flag: trace_ends_with_ret.
    125   λstart_status: S.
    126   λfinal_status: S.
    127   λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
    128     |tal_pc_list … the_trace|.
    129123
    130124let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
     
    146140    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    147141    tal_unrepeating … tl
    148   | tal_base_call status_pre_fun_call status_start_fun_call status_final _ _ _
    149       fun_call_trace _ ⇒ tlr_unrepeating … fun_call_trace
    150142  | _ ⇒ True
     143  ].
     144
     145definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
     146  trace_label_label S fl st1 st2 → costlabel ≝
     147  λS,fl,st1,st2,tr.match tr with
     148  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
     149
     150definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
     151  trace_label_return S st1 st2 → costlabel ≝
     152  λS,st1,st2,tr.match tr with
     153  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
     154  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
    151155  ].
    152156
     
    196200.
    197201
     202definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
     203  trace_label_call S st1 st2 → costlabel ≝
     204  λS,st1,st2,tr.match tr with
     205  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
     206  ].       
     207
    198208coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
    199209  | tld_step:
     
    212222          trace_label_diverges S status_start_fun_call →
    213223            trace_label_diverges S status_initial.
     224
     225definition tld_hd_label : ∀S : abstract_status.∀st.
     226  trace_label_diverges S st → costlabel ≝
     227  λS,st,tr.match tr with
     228  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
     229  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
     230  ].       
    214231
    215232(* Version in Prop for showing existence. *)
     
    279296].
    280297
     298definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
     299  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
     300  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
     301
    281302lemma trace_label_label_label : ∀S,s,s',f.
    282303  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
     
    285306#f #start #end #tr' #C @(trace_any_label_label … tr')
    286307qed.
     308
     309definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
     310  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
     311  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
    287312
    288313lemma trace_any_call_call : ∀S,s,s'.
     
    338363  ].
    339364
    340 (* TODO: use as_label for forcing same labels *)
    341365let rec tlr_rel S1 st1 st1' S2 st2 st2'
    342366  (tlr1 : trace_label_return S1 st1 st1')
     
    359383 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
    360384  match tll1 with
    361   [ tll_base fl1 st1 st1' tal1 _
     385  [ tll_base fl1 st1 st1' tal1 H
    362386    match tll2 with
    363     [ tll_base fl2 st2 st2 tal2 _ ⇒ tal_rel … tal1 tal2
     387    [ tll_base fl2 st2 st2 tal2 G ⇒
     388      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
     389      tal_rel … tal1 tal2
    364390    ]
    365391  ]
     
    389415  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
    390416    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    391   ]. 
     417  ].
Note: See TracChangeset for help on using the changeset viewer.