Changeset 1918 for src/common


Ignore:
Timestamp:
May 4, 2012, 3:40:36 PM (8 years ago)
Author:
tranquil
Message:

using listb.ma now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1917 r1918  
    22include "basics/bool.ma".
    33include "basics/jmeq.ma".
     4include "basics/lists/listb.ma".
     5include "ASM/Util.ma".
    46
    57inductive status_class : Type[0] ≝
     
    1214  { as_status :> Type[0]
    1315  ; as_execute : as_status → as_status → Prop
    14   ; as_different_points : as_status → as_status → Prop
     16  ; as_pc : DeqSet
     17  ; as_pc_of : as_status → as_pc
    1518  ; as_classifier : as_status → status_class → Prop
    1619  ; as_costed : as_status → Prop
     
    100103          trace_any_label S end_flag status_pre status_end.
    101104
    102 include "basics/lists/list.ma".
    103 
    104 let rec tal_status_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : list S ≝
     105let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
     106  on tal : list (as_pc S) ≝
    105107 match tal with
    106  [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ pre :: tal_status_list … tl
    107  | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  pre :: tal_status_list … tl
    108  | tal_base_not_return pre _ _ _ _ ⇒ [pre]
    109  | tal_base_return pre _ _ _ ⇒ [pre]
    110  | tal_base_call pre _ _ _ _ _ _ _ ⇒ [pre]
     108 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
     109 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
     110 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
     111 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
     112 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    111113 ].
    112114
     
    123125  match tal with
    124126  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
    125    All ? (as_different_points S st1) (tal_status_list … tl) ∧
    126    tal_unrepeating … tl ∧
    127    tlr_unrepeating … tlr
     127    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
     128    tal_unrepeating … tl ∧
     129    tlr_unrepeating … tlr
    128130  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
    129    All ? (as_different_points S st1) (tal_status_list … tl) ∧
    130    tal_unrepeating … tl
     131    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
     132    tal_unrepeating … tl
    131133  | _ ⇒ True
    132134  ].
     135
     136let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
     137  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
     138cases tal //
     139#fl' #st1' [#st_fun] #st2' #st3' #H
     140[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
     141#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
     142qed.
    133143
    134144inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
     
    158168        ¬ (as_costed S status_init) →
    159169          trace_any_call S status_pre status_end.
     170
    160171             
    161172inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.