Changeset 2398


Ignore:
Timestamp:
Oct 17, 2012, 3:35:08 PM (7 years ago)
Author:
boender
Message:
  • committed start of stacksize
Location:
src
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2299 r2398  
    1010  | cl_return: status_class
    1111  | cl_jump: status_class
    12   | cl_call: status_class
     12  | cl_call: ident → 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. as_classifier s cl_call) → as_status → Prop
     23  ; as_after_return : (Σs:as_status. ∃f.as_classifier s (cl_call f)) → 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         ∀H:as_classifier S status_pre_fun_call cl_call.
    93           as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
     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 →
    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         ∀H:as_classifier S status_pre_fun_call cl_call.
    106           as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_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 →
    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 [ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
     184[ #f #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 #CL #AF #tlr #CS
    201 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
     200| #s1 #s2 #s3 #EX #f #CL #AF #tlr #CS
     201| #fl #s1 #s2 #s3 #s4 #EX #f #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 #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
    213 | #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #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'
    214214  cases (tal_pc_list_start … tal')
    215215  #hd #E >E
     
    225225  | tac_base:
    226226      ∀status: S.
    227         as_classifier S status cl_call
     227        (∃f.as_classifier S status (cl_call f))
    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:as_classifier S status_pre_fun_call cl_call.
     235        ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
    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:as_classifier S status_pre_fun_call cl_call.
     280        ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
    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:as_classifier S status_pre_fun_call cl_call.
     305        ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
    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         as_classifier S status_initial cl_call
     314        (∃f.as_classifier S status_initial (cl_call f))
    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         as_classifier S status_initial cl_call
     322        (∃f.as_classifier S status_initial (cl_call f))
    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         as_classifier S status_initial cl_call
     333        (∃f.as_classifier S status_initial (cl_call f))
    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         as_classifier S status_initial cl_call
     341        (∃f.as_classifier S status_initial (cl_call f))
    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 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 f 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' → as_classifier S s' cl_call.
    374 #S #s #s' #T elim T //
     373  trace_any_call S s s' → ∃f.as_classifier S s' (cl_call f).
     374#S #s #s' #T elim T [1,3: //]
     375#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
    375376qed.
    376377
     
    509510    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    510511      (tal_base_return ? st2mid st2' H G)
    511   | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
     512  | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒
    512513    fl2 = doesnt_end_with_ret ∧
    513     ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
     514    ∃st2mid,taa,st2mid',H,f,G,K,tlr2,L.
    514515    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    515       (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
     516      (tal_base_call ? st2mid st2mid' st2' H f G K tlr2 L) ∧
    516517      tlr_rel … tlr1 tlr2
    517   | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
    518     ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
     518  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒
     519    ∃st2mid,taa,st2_fun,st2_after_fun,H,f,G,K,tlr2,L,tl2.
    519520    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    520       (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
     521      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H f G K tlr2 L tl2) ∧
    521522      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
    522523  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
     
    566567  [ tal_base_not_return st1' st1'' H G K ⇒ ?
    567568  | tal_base_return st1' st1'' H G ⇒ ?
    568   | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ?
    569   | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
     569  | tal_base_call st1' st1'' st1''' H f G K tlr1 L ⇒ ?
     570  | tal_step_call fl1' st1' st1'' st1''' st1'''' H f G L tlr1 K tl1 ⇒ ?
    570571  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
    571572  ].
     
    588589  [ *#H2 *#G2 *#K2 #R12
    589590  | *#H2 *#G2 #R12
    590   | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
    591   | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
     591  | *#st2' *#H2 *#f2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
     592  | *#st2' *#st2'' *#H2 *#f2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
    592593  ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct]
    593594  *#st3mid *#taa3
    594   [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
    595     %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3}
     595  [ *#st3' *#H3 *#f3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
     596    %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{f3} %{G3} %{K3} %{tlr3} %{L3}
    596597    %{R23} @(tlr_rel_transitive … R12' R23')
    597   | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
    598     %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
     598  | *#st3' *#st3'' *#H3 *#f3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
     599    %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{f3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
    599600    %{(tal_rel_transitive … R12'' R23'')}
    600601    %{R23} @(tlr_rel_transitive … R12' R23')
     
    625626  match the_trace with
    626627  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    627   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     628  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒
    628629      flatten_trace_label_return … call_trace
    629630  | tal_base_return the_status _ _ _ ⇒ [ ]
    630631  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    631     _ _ _ call_trace _ final_trace ⇒
     632    _ _ _ _ call_trace _ final_trace ⇒
    632633    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
    633634    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
     
    706707  [ tal_base_not_return st1 st1' H G K ⇒ ?
    707708  | tal_base_return st1 st1' H G ⇒ ?
    708   | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
    709   | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
     709  | tal_base_call st1 st1' st1'' H f G K tlr1 L ⇒ ?
     710  | tal_step_call fl1 st1 st1' st1'' st1''' H f G K tlr1 L tl1 ⇒ ?
    710711  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
    711712  ]
     
    736737    [ *#H' *#G' *#K' #EQ
    737738    | *#H' *#G' #EQ
    738     | *#st_mid' *#H' *#G' *#K' *#tlr2 *#L' * #EQ #H_tlr
    739     | *#st_fun *#st_after *#H' *#G' *#K' *#tlr2 *#L' *#tl2 ** #EQ #H_tlr #H_tal
     739    | *#st_mid' *#H' *#f' *#G' *#K' *#tlr2 *#L' * #EQ #H_tlr
     740    | *#st_fun *#st_after *#H' *#f' *#G' *#K' *#tlr2 *#L' *#tl2 ** #EQ #H_tlr #H_tal
    740741    ] >EQ >taa_append_tal_same_flatten
    741742  | whd in ⊢ (%→??(????%)?);
Note: See TracChangeset for help on using the changeset viewer.