Changeset 1917


Ignore:
Timestamp:
May 4, 2012, 2:21:38 PM (7 years ago)
Author:
tranquil
Message:

predicate for unrepeating traces, fused final_abstract_status with abstract_status (with an alias for backward compatibility)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1902 r1917  
    1010
    1111record abstract_status : Type[1] ≝
    12 {
    13   as_status :> Type[0];
    14   as_execute : as_status → as_status → Prop;
    15   as_classifier : as_status → status_class → Prop;
    16   as_costed : as_status → Prop;
    17   as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
     12  { as_status :> Type[0]
     13  ; as_execute : as_status → as_status → Prop
     14  ; as_different_points : as_status → as_status → Prop
     15  ; as_classifier : as_status → status_class → Prop
     16  ; as_costed : as_status → Prop
     17  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
     18  ; as_final: as_status → Prop
    1819}.
     20
     21(* temporary alias for backward compatibility *)
     22definition final_abstract_status ≝ abstract_status.
    1923
    2024inductive trace_ends_with_ret: Type[0] ≝
     
    9599        ¬ (as_costed S status_init) →
    96100          trace_any_label S end_flag status_pre status_end.
     101
     102include "basics/lists/list.ma".
     103
     104let rec tal_status_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : list S ≝
     105 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]
     111 ].
     112
     113let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
     114  match tlr with
     115  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
     116  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
     117  ]
     118and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
     119  match tll with
     120  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
     121  ]
     122and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
     123  match tal with
     124  [ 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
     128  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
     129   All ? (as_different_points S st1) (tal_status_list … tl) ∧
     130   tal_unrepeating … tl
     131  | _ ⇒ True
     132  ].
    97133
    98134inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
     
    130166        as_costed S start_status →
    131167        trace_label_call S start_status end_status
    132 .       
     168.
    133169
    134170coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
     
    167203            trace_label_diverges_exists S status_initial.
    168204
    169 record final_abstract_status : Type[1] ≝ {
    170   as_as :> abstract_status;
    171   as_final:as_status as_as → Prop
    172 }.
    173 
    174 
    175 inductive trace_whole_program (S:final_abstract_status) : S → Type[0] ≝
     205inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
    176206  | twp_terminating:
    177207      ∀status_initial: S.
     
    192222
    193223(* Again, an identical version in Prop for existence proofs. *)
    194 inductive trace_whole_program_exists (S:final_abstract_status) : S → Prop ≝
     224inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
    195225  | twp_terminating:
    196226      ∀status_initial: S.
     
    232262#S #s #s' #T elim T //
    233263qed.
     264
     265(* an uncalling, unreturning and *unjumping*,
     266  as well as unlabelled (but possibly for the first and last statuses)
     267  possibly empty trace segment *)
     268inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
     269  | taa_base :
     270      ∀start_status: S.
     271        trace_any_any S start_status start_status
     272  | taa_step :
     273      ∀status_pre: S.
     274      ∀status_init: S.
     275      ∀status_end: S.
     276        as_execute S status_pre status_init →
     277        trace_any_any S status_init status_end →
     278        as_classifier S status_pre cl_other →
     279        ¬as_costed … status_init →
     280          trace_any_any S status_pre status_end.
     281
     282let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
     283  match taa with
     284  [ taa_base st1' ⇒ [st1']
     285  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
     286  ].
     287
     288let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
     289  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
     290  match taa1
     291  return λst1,st2.λx : trace_any_any S st1 st2.
     292    trace_any_any S st2 st3 → trace_any_any S st1 st3
     293  with
     294  [ taa_base _ ⇒ λtaa2.taa2
     295  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
     296      taa_step … H (taa_append_taa … tl taa2) G K
     297  ].
     298
     299let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
     300  on taa :
     301  trace_any_label S fl st2 st3 →
     302  trace_any_label S fl st1 st3 ≝
     303  match taa
     304  return λst1,st2.λx : trace_any_any S st1 st2.
     305    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
     306  with
     307  [ taa_base _ ⇒ λtaa2.taa2
     308  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
     309      tal_step_default … H (taa_append_tal … tl taa2) G K
     310  ].
     311
     312(* TODO: use as_label for forcing same labels *)
     313let rec tlr_rel S1 st1 st1' S2 st2 st2'
     314  (tlr1 : trace_label_return S1 st1 st1')
     315  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
     316match tlr1 with
     317  [ tlr_base st1 st1' tll1 ⇒
     318    match tlr2 with
     319    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
     320    | _ ⇒ False
     321    ]
     322  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
     323    match tlr2 with
     324    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
     325      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
     326    | _ ⇒ False
     327    ]
     328  ]
     329and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
     330 (tll1 : trace_label_label S1 fl1 st1 st1')
     331 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
     332  match tll1 with
     333  [ tll_base fl1 st1 st1' tal1 _ ⇒
     334    match tll2 with
     335    [ tll_base fl2 st2 st2 tal2 _ ⇒ tal_rel … tal1 tal2
     336    ]
     337  ]
     338and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
     339 (tal1 : trace_any_label S1 fl1 st1 st1')
     340 (tal2 : trace_any_label S2 fl2 st2 st2')
     341   on tal1 : Prop ≝
     342  match tal1 with
     343  [ tal_base_not_return st1 st1' _ _ _ ⇒
     344    ∃st2mid,taa,H,G,K.
     345    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     346      (tal_base_not_return ? st2mid st2' H G K)
     347  | tal_base_return st1 st1' _ _ ⇒
     348    ∃st2mid,taa,H,G.
     349    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     350      (tal_base_return ? st2mid st2' H G)
     351  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
     352    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
     353    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     354      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
     355      tlr_rel … tlr1 tlr2
     356  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
     357    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
     358    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     359      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
     360      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
     361  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
     362    tal_rel … tl1 tal2 (* <- this makes it many to many *)
     363  ].
Note: See TracChangeset for help on using the changeset viewer.