Changeset 2417 for src/common


Ignore:
Timestamp:
Oct 25, 2012, 4:36:07 PM (7 years ago)
Author:
boender
Message:
  • reverted changes to StructuredTraces? (shouldn't have been committed yet)
  • updated _jaap files to remove function identifier from cl_call and add an as_call predicate
Location:
src/common
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2413 r2417  
    1010  | cl_return: status_class
    1111  | cl_jump: status_class
    12   | cl_call: ident → status_class
     12  | cl_call: status_class
    1313  | cl_other: status_class.
    1414
     
    2121  ; as_classifier : as_status → status_class → Prop
    2222  ; as_label_of_pc : as_pc → option costlabel
    23   ; as_after_return : (Σs:as_status. ∃f.as_classifier s (cl_call f)) → as_status → Prop
     23  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    2424  ; as_final: as_status → Prop
    2525}.
     
    9090      ∀status_final: S.
    9191        as_execute S status_pre_fun_call status_start_fun_call →
    92         ∀f.∀H:as_classifier S status_pre_fun_call (cl_call f).
    93           as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H)) status_final →
     92        ∀H:as_classifier S status_pre_fun_call cl_call.
     93          as_after_return S «status_pre_fun_call, H» status_final →
    9494          trace_label_return S status_start_fun_call status_final →
    9595          as_costed S status_final →
     
    103103      ∀status_final: S.
    104104        as_execute S status_pre_fun_call status_start_fun_call →
    105         ∀f.∀H:as_classifier S status_pre_fun_call (cl_call f).
    106           as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H)) status_after_fun_call →
     105        ∀H:as_classifier S status_pre_fun_call cl_call.
     106          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
    107107          trace_label_return S status_start_fun_call status_after_fun_call →
    108108          ¬ as_costed S status_after_fun_call →
     
    123123  on tal : list (as_pc S) ≝
    124124 match tal with
    125  [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
     125 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
    126126 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
    127127 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
    128128 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
    129  | tal_base_call pre _ _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
     129 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    130130 ].
    131131
     
    155155and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
    156156  match tal with
    157   [ tal_step_call fl st1 st2 st3 st4 _ _ _ _ tlr _ tl ⇒
     157  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
    158158    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    159159    tal_unrepeating … tl ∧
     
    162162    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    163163    tal_unrepeating … tl
    164   | tal_base_call pre _ _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
     164  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
    165165  | _ ⇒ True
    166166  ].
     
    182182cases tal //
    183183#fl' #st1' [#st_fun] #st2' #st3' #H
    184 [ #f #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
     184[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
    185185#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
    186186qed.
     
    198198[ #s1 #s2 #EX #CL #CS
    199199| #s1 #s2 #EX #CL
    200 | #s1 #s2 #s3 #EX #f #CL #AF #tlr #CS
    201 | #fl #s1 #s2 #s3 #s4 #EX #f #CL #AF #tlr #CS #tal
     200| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     201| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
    202202| #fl #s1 #s2 #s3 #EX #tal #CL #CS
    203203] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     
    210210[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
    211211| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
    212 | #pre #start #final #EX #f #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
    213 | #fl' #pre #start #after #final #EX #f #CL #AF #tlr #CS #tal' #CS'
     212| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     213| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
    214214  cases (tal_pc_list_start … tal')
    215215  #hd #E >E
     
    225225  | tac_base:
    226226      ∀status: S.
    227         (∃f.as_classifier S status (cl_call f))
     227        as_classifier S status cl_call
    228228          trace_any_call S status status
    229229  | tac_step_call:
     
    233233      ∀status_start_fun_call: S.
    234234        as_execute S status_pre_fun_call status_start_fun_call →
    235         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     235        ∀H:as_classifier S status_pre_fun_call cl_call.
    236236          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    237237          trace_label_return S status_start_fun_call status_after_fun_call →
     
    278278        trace_label_call S status_initial status_pre_fun_call →
    279279        as_execute S status_pre_fun_call status_start_fun_call →
    280         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     280        ∀H:as_classifier S status_pre_fun_call cl_call.
    281281          trace_label_diverges S status_start_fun_call →
    282282            trace_label_diverges S status_initial.
     
    303303        trace_label_call S status_initial status_pre_fun_call →
    304304        as_execute S status_pre_fun_call status_start_fun_call →
    305         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     305        ∀H:as_classifier S status_pre_fun_call cl_call.
    306306          trace_label_diverges_exists S status_start_fun_call →
    307307            trace_label_diverges_exists S status_initial.
     
    312312      ∀status_start_fun: S.
    313313      ∀status_final: S.
    314         (∃f.as_classifier S status_initial (cl_call f))
     314        as_classifier S status_initial cl_call
    315315        as_execute S status_initial status_start_fun →
    316316        trace_label_return S status_start_fun status_final →
     
    320320      ∀status_initial: S.
    321321      ∀status_start_fun: S.
    322         (∃f.as_classifier S status_initial (cl_call f))
     322        as_classifier S status_initial cl_call
    323323        as_execute S status_initial status_start_fun →
    324324        trace_label_diverges S status_start_fun →
     
    331331      ∀status_start_fun: S.
    332332      ∀status_final: S.
    333         (∃f.as_classifier S status_initial (cl_call f))
     333        as_classifier S status_initial cl_call
    334334        as_execute S status_initial status_start_fun →
    335335        trace_label_return S status_start_fun status_final →
     
    339339      ∀status_initial: S.
    340340      ∀status_start_fun: S.
    341         (∃f.as_classifier S status_initial (cl_call f))
     341        as_classifier S status_initial cl_call
    342342        as_execute S status_initial status_start_fun →
    343343        trace_label_diverges_exists S status_start_fun →
     
    350350[ tal_base_not_return start final _ _ C ⇒ C
    351351| tal_base_return _ _  _ _ ⇒ I
    352 | tal_base_call _ _ _ _ _ _ _ _ C ⇒ C
    353 | tal_step_call f pre start after final X f C RET LR C' tr' ⇒ trace_any_label_label … tr'
     352| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     353| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    354354| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    355355].
     
    371371
    372372lemma trace_any_call_call : ∀S,s,s'.
    373   trace_any_call S s s' → ∃f.as_classifier S s' (cl_call f).
     373  trace_any_call S s s' → as_classifier S s' cl_call.
    374374#S #s #s' #T elim T [1,3: //]
    375375#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
     
    517517    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    518518      (tal_base_return ? st2mid st2' H G)
    519   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒
     519  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
    520520    fl2 = doesnt_end_with_ret ∧
    521521    ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     
    524524      we cannot use trace_any_any as it disallows labels in the end as soon
    525525      as it is non-empty) *)
    526     (∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    527       tal2 ≃ taa @ (tal_base_call … H f G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
    528     ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     526    (∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     527      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
     528    ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    529529    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
    530       tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧
     530      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    531531      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
    532   | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒
     532  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
    533533    ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    534     (fl2 = doesnt_end_with_ret ∧ ∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    535       tal2 ≃ taa @ tal_base_call … H f G K tlr2 L ∧
     534    (fl2 = doesnt_end_with_ret ∧ ∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     535      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
    536536      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
    537     ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     537    ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    538538    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
    539       tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧
     539      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    540540      tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
    541541  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
     
    552552cases tal1 -fl1 -s1 -s1' //
    553553[ #s1 #s1' #H #I *
    554 | #s1 #s1' #s1'' #s1''' #s1'''' #H #f #I #J #tlr #K #tl *
     554| #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl *
    555555| #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl)
    556556]
     
    563563  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
    564564  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    565   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
    566   | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
     565  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     566  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    567567  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    568568  ].
     
    570570[1,2,3: -tal_rel_eq_fl #tal2 * //
    571571| #tal2 * #s2_mid * #taa2 * #s2' *#H2 *
    572   [ * #EQ1 *#f *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
    573   | * #s2_mid' *#f *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
     572  [ * #EQ1 *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
     573  | * #s2_mid' *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
    574574     @(tal_rel_eq_fl … step)
    575575  ]
     
    603603  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
    604604  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    605   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
    606   | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
     605  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     606  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    607607  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    608608  ].
     
    637637  match the_trace with
    638638  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    639   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒
     639  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    640640      flatten_trace_label_return … call_trace
    641641  | tal_base_return the_status _ _ _ ⇒ [ ]
    642642  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    643     _ _ _ _ call_trace _ final_trace ⇒
     643    _ _ _ call_trace _ final_trace ⇒
    644644    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
    645645    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
     
    730730  [ tal_base_not_return st1 st1' H G K ⇒ ?
    731731  | tal_base_return st1 st1' H G ⇒ ?
    732   | tal_base_call st1 st1' st1'' H f G K tlr1 L ⇒ ?
    733   | tal_step_call fl1 st1 st1' st1'' st1''' H f G K tlr1 L tl1 ⇒ ?
     732  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
     733  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
    734734  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
    735735  ]
     
    760760    [ *#H' *#G' *#K' #EQ
    761761    | *#H' *#G' #EQ
    762     | *#st_mid' *#H' * [|*#st2_mid''] *#f' *#G' *#K' *#tlr2 *#L'
     762    | *#st_mid' *#H' * [|*#st2_mid''] *#G' *#K' *#tlr2 *#L'
    763763      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
    764764    | *#st_fun *#H' *
    765       [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#f' *#G' *#K' *#tlr2 *#L'
     765      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#G' *#K' *#tlr2 *#L'
    766766      [| *#tl2] ** #EQ #H_tl #H_tlr
    767767    ] >EQ >taa_append_tal_same_flatten
Note: See TracChangeset for help on using the changeset viewer.