Changeset 2553 for src/common


Ignore:
Timestamp:
Dec 12, 2012, 2:43:03 PM (7 years ago)
Author:
tranquil
Message:

as_classify changed to a partial function
added a status for tailcalls

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2540 r2553  
    8282    sim_status_rel st1 st2 →
    8383    match as_classify … st1 with
    84     [ cl_call ⇒ ∀prf.
    85       (*
    86            st1' ------------S----------\
    87             ↑ \                         \
    88            st1 \--L--\                   \
    89             | \       \                   \
    90             S  \-C-\  st2_after_call →taa→ st2'
    91             |       \     ↑
    92            st2 →taa→ st2_pre_call
    93       *)
    94       ∃st2_pre_call.
    95       as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
    96       call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    97       ∃st2_after_call,st2'.
    98       ∃taa2 : trace_any_any … st2 st2_pre_call.
    99       ∃taa2' : trace_any_any … st2_after_call st2'.
    100       as_execute … st2_pre_call st2_after_call ∧
    101       sim_status_rel st1' st2' ∧
    102       label_rel … st1' st2_after_call
    103     | cl_return ⇒
    104       (*
    105            st1
    106           / ↓
    107          | st1'----------S,L------------\
    108          S   \                           \
    109           \   \-----R-------\            |     
    110            \                 |           |
    111            st2 →taa→ st2_ret |           |
    112                         ↓   /            |
    113                    st2_after_ret →taaf→ st2'
    114 
    115          we also ask that st2_after_ret be not labelled if the taaf tail is
    116          not empty
    117       *)
    118       ∃st2_ret,st2_after_ret,st2'.
    119       ∃taa2 : trace_any_any … st2 st2_ret.
    120       ∃taa2' : trace_any_any_free … st2_after_ret st2'.
    121       (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
    122       as_classifier … st2_ret cl_return ∧
    123       as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
    124       ret_rel … sim_status_rel st1' st2_after_ret ∧
    125       label_rel … st1' st2'
    126     | cl_other ⇒
    127         (*         
    128         st1 → st1'
    129           |      \
    130           S      S,L
    131           |        \
    132          st2 →taaf→ st2'
    133          
    134          the taaf can be empty (e.g. tunneling) but we ask it must not be the
    135          case when both st1 and st1' are labelled (we would be able to collapse
    136          labels otherwise)
    137        *)
    138       ∃st2'.
    139       ∃taa2 : trace_any_any_free … st2 st2'.
    140       (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    141       sim_status_rel st1' st2' ∧
    142       label_rel … st1' st2'
    143     | cl_jump ⇒
    144       (* just like cl_other, but with a hypothesis more *)
    145       as_costed … st1' →
    146       ∃st2'.
    147       ∃taa2 : trace_any_any_free … st2 st2'.
    148       (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    149       sim_status_rel st1' st2' ∧
    150       label_rel … st1' st2'
     84    [ None ⇒ True
     85    | Some cl ⇒
     86      match cl with
     87      [ cl_call ⇒ ∀prf.
     88        (*
     89             st1' ------------S----------\
     90              ↑ \                         \
     91             st1 \--L--\                   \
     92              | \       \                   \
     93              S  \-C-\  st2_after_call →taa→ st2'
     94              |       \     ↑
     95             st2 →taa→ st2_pre_call
     96        *)
     97        ∃st2_pre_call.
     98        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
     99        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
     100        ∃st2_after_call,st2'.
     101        ∃taa2 : trace_any_any … st2 st2_pre_call.
     102        ∃taa2' : trace_any_any … st2_after_call st2'.
     103        as_execute … st2_pre_call st2_after_call ∧
     104        sim_status_rel st1' st2' ∧
     105        label_rel … st1' st2_after_call
     106      | cl_tailcall ⇒ ∀prf.
     107        (*
     108             st1' ------------S----------\
     109              ↑ \                         \
     110             st1 \--L--\                   \
     111              |         \                   \
     112              S         st2_after_call →taa→ st2'
     113              |             ↑
     114             st2 →taa→ st2_pre_call
     115        *)
     116        ∃st2_pre_call.
     117        as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
     118        ∃st2_after_call,st2'.
     119        ∃taa2 : trace_any_any … st2 st2_pre_call.
     120        ∃taa2' : trace_any_any … st2_after_call st2'.
     121        as_execute … st2_pre_call st2_after_call ∧
     122        sim_status_rel st1' st2' ∧
     123        label_rel … st1' st2_after_call
     124      | cl_return ⇒
     125        (*
     126             st1
     127            / ↓
     128           | st1'----------S,L------------\
     129           S   \                           \
     130            \   \-----R-------\            |     
     131             \                 |           |
     132             st2 →taa→ st2_ret |           |
     133                          ↓   /            |
     134                     st2_after_ret →taaf→ st2'
     135
     136           we also ask that st2_after_ret be not labelled if the taaf tail is
     137           not empty
     138        *)
     139        ∃st2_ret,st2_after_ret,st2'.
     140        ∃taa2 : trace_any_any … st2 st2_ret.
     141        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
     142        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
     143        as_classifier … st2_ret cl_return ∧
     144        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
     145        ret_rel … sim_status_rel st1' st2_after_ret ∧
     146        label_rel … st1' st2'
     147      | cl_other ⇒
     148          (*         
     149          st1 → st1'
     150            |      \
     151            S      S,L
     152            |        \
     153           st2 →taaf→ st2'
     154           
     155           the taaf can be empty (e.g. tunneling) but we ask it must not be the
     156           case when both st1 and st1' are labelled (we would be able to collapse
     157           labels otherwise)
     158         *)
     159        ∃st2'.
     160        ∃taa2 : trace_any_any_free … st2 st2'.
     161        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     162        sim_status_rel st1' st2' ∧
     163        label_rel … st1' st2'
     164      | cl_jump ⇒
     165        (* just like cl_other, but with a hypothesis more *)
     166        as_costed … st1' →
     167        ∃st2'.
     168        ∃taa2 : trace_any_any_free … st2 st2'.
     169        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     170        sim_status_rel st1' st2' ∧
     171        label_rel … st1' st2'
     172      ]
    151173    ].
    152174
     
    202224  | tal_base_return st1 st1' _ _ ⇒ ?
    203225  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
     226  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
    204227  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
    205228  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
     
    211234  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
    212235  ]
     236| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
    213237| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    214238  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
     
    219243destruct
    220244<associative_taa_append_tal
    221   [1,2,3,4:%{(refl …)}] %{st2mid}
     245  [1,2,3,4,5:%{(refl …)}] %{st2mid}
    222246  [1,2:|*: %{G2} %{EQcall} ]
    223247  %{(taa_append_taa … taa2 taa2')}
    224248  [1,2: %{H2} %{G2} [%{K2}] %
     249  |5: %{st2mid'} %{H2} %{tlr2} % //
    225250  |*: %{st2mid'} %{H2}
    226251    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
     
    229254qed.
    230255
     256(*
     257check trace_any_label_label
    231258let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
    232259  on tal : as_costed … st2 ≝
     
    242269]
    243270qed.
     271*)
    244272
    245273lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
     
    451479  | tal_base_return st1' st1'' H G ⇒ ?
    452480  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
     481  | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ?
    453482  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
    454483  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
     
    485514  lapply (sim_execute … H st1_R_st2)
    486515  (* without try it fails... why? *)
    487   try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     516  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
    488517  [ #H lapply (H K) -H ] *
    489518  #st2' ** -st2 -st2'
     
    502531| (* tal_base_return *) whd
    503532  lapply (sim_execute … H st1_R_st2)
    504   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     533  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    505534  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    506535  ***** #ncost #J2 #K2
     
    511540| (* tal_base_call *) whd
    512541  lapply (sim_execute … H st1_R_st2)
    513   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     542  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
    514543  #H elim (H G) -H
    515544  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    538567  |*: whd <st1_L_st2' assumption
    539568  ]
     569| (* tal_base_tailcall *) whd
     570  lapply (sim_execute … H st1_R_st2)
     571  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     572  #H elim (H G) -H
     573  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     574  #st1_R_st2_mid #st1_L_st2_after_call
     575  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     576  #st2_after_ret * #st2' * #tlr2 * #taa2''
     577  * #props #S
     578  %{st2_after_ret} %{st2'}
     579  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
     580  %{taa2''}
     581  %{props}
     582  % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
    540583| (* tal_step_call *)
    541584  lapply (sim_execute … H st1_R_st2)
    542   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     585  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
    543586  #H elim (H G) -H
    544587  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    585628    ]
    586629  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
    587   |*: whd <st1_L_st2'' @(tal_end_costed … tl1)
     630  |*: whd <st1_L_st2'' @(trace_any_label_label … tl1)
    588631  ]
    589632| (* step_default *)
    590633  lapply (sim_execute … H st1_R_st2)
    591   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     634  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    592635  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    593636  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     
    603646  | (* can't happen *)
    604647    *** #_ #L' elim (absurd ?? K)
    605     whd >st1_L_st2_mid <L' @(tal_end_costed … tl1)
     648    whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1)
    606649  ]
    607650  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
     
    622665  ∀prf : as_classifier ? st1 cl_call.
    623666  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
     667| ft_advance_tailcall :
     668  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     669  ∀prf : as_classifier ? st1 cl_tailcall.
     670  flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
    624671| ft_advance_ret :
    625672  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     
    664711| IEVcost : costlabel → intensional_event
    665712| IEVcall : ident → intensional_event
     713| IEVtailcall : ident → ident → intensional_event
    666714| IEVret : ident → intensional_event.
    667715
     
    677725  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
    678726  ft_observables_aux (add @ acc) … pre1
     727| ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
     728  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     729  let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
     730  ft_observables_aux (add @ acc) … pre1
    679731| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
    680732  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     
    689741#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
    690742[ // ]
    691 #st2 #st3 #stack [3: #f ] #pre #H #G #IH #acc
     743#st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
    692744whd in ⊢ (??%(??%?));
    693745>IH >IH >append_nil //
     
    718770  [IEVcall (as_call_ident … «st3, G»)].
    719771#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
     772whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     773>ft_extend_taa_obs
     774lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
     775[ #st2 * #ft #H #G >append_nil %
     776| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
     777  >(not_costed_no_label … K)
     778  normalize nodelta //
     779]
     780qed.
     781
     782lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
     783  ∀ft : flat_trace S st1 st2 (f :: stack).
     784  ∀taa : trace_any_any S st2 st3.
     785  ∀H : as_execute S st3 st4.∀G.
     786  ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
     787  ft_observables … ft @
     788  option_to_list … (!l←as_label … st2;return IEVcost l) @
     789  [IEVtailcall f (as_tailcall_ident … «st3, G»)].
     790#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    720791whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    721792>ft_extend_taa_obs
     
    805876#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    806877[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    807 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: * [*]] #cl [#ncost_st1']
     878|*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
    808879  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    809880  [1,2: (* other/jump *)
    810881    lapply (sim_execute … ex G')
    811     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     882    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
    812883    [ #H lapply (H ncost_st1') -H ] *
    813884    #st2' *#taaf ** #ncost #G'' #H''
     
    838909      >S >L' %
    839910    ]
    840   |3: (* ret *)
     911  |3: (* tailcall *)
    841912    lapply (sim_execute … ex G')
    842     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     913    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     914    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
     915    * #taa2 * #taa2' ** #ex' #G'' #H''
     916    lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
     917    generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
     918    <EQcall in ⊢ (%→???%%→%);
     919    #ft1' #EQft1'
     920    %{st2_after_call} %{st2'}
     921    %[@(ft_advance_tailcall … f … ex' cl')
     922      @(ft_extend_taa … (taa_append_taa … taa taa2))
     923      assumption]
     924    %{taa2'}
     925    % [ %{H'' G''} ]
     926    >ft_extend_taa_advance_tailcall_obs
     927    lapply EQft1' lapply ft1' -ft1'
     928    >EQcall in ⊢ (%→???%%→%);
     929    #ft1' #EQft1' destruct (EQft1')
     930    whd in ⊢ (??%?);
     931    >ft_observables_aux_def >append_nil
     932    >S >L' %
     933  |4: (* ret *)
     934    lapply (sim_execute … ex G')
     935    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    843936    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    844937    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    860953    ]
    861954    >S >L' %
    862   |4: (* call *)
     955  |5: (* call *)
    863956    lapply (sim_execute … ex G')
    864     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     957    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
    865958    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    866959    * #taa2 * #taa2' ** #ex' #G'' #H''
  • src/common/StructuredTraces.ma

    r2531 r2553  
    1111  | cl_jump: status_class
    1212  | cl_call: status_class
     13  | cl_tailcall: status_class
    1314  | cl_other: status_class.
    1415
     
    1819  ; as_pc : DeqSet
    1920  ; as_pc_of : as_status → as_pc
    20   ; as_classify : as_status → status_class
     21  ; as_classify : as_status → option status_class
    2122  ; as_label_of_pc : as_pc → option costlabel
    22   ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
     23  ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
    2324  ; as_final: as_status → Prop
    24   ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     25  ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
     26  ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
    2527  }.
    2628
    27 definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
     29definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
    2830definition as_call ≝ λS,s,f.as_call_ident S s = f.
    2931
     
    187189          as_costed S status_final →
    188190            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
     191  (* A tailcall, which ends the trace like a return. *)
     192  | tal_base_tailcall:
     193      ∀status_pre_fun_call: S.
     194      ∀status_start_fun_call: S.
     195      ∀status_final: S.
     196        as_execute S status_pre_fun_call status_start_fun_call →
     197        as_classifier S status_pre_fun_call cl_tailcall →
     198          trace_label_return S status_start_fun_call status_final →
     199            trace_any_label S ends_with_ret status_pre_fun_call status_final
    189200  (* A call followed by a non-empty trace. *)
    190201  | tal_step_call:
     
    220231 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
    221232 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
     233 | tal_base_tailcall pre _ _ _ _ _ ⇒ [as_pc_of … pre]
    222234 ].
    223235
     
    255267    tal_unrepeating … tl
    256268  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
     269  | tal_base_tailcall pre _ _ _ _ trace ⇒ tlr_unrepeating … trace
    257270  | _ ⇒ True
    258271  ].
     
    284297| #s1 #s2 #EX #CL
    285298| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     299| #s1 #s2 #s3 #EX #CL #tlr
    286300| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
    287301| #fl #s1 #s2 #s3 #EX #tal #CL #CS
    288 ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     302] whd in ⊢ (??(λ_.??%?)); % [2,4,6,8,10,12: % | *: skip ]
    289303qed.
    290304
     
    296310| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
    297311| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     312| #pre #start #final #EX #CL #tlr #CS' % // @(not_costed_no_label ?? CS')
    298313| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
    299314  cases (tal_pc_list_start … tal')
     
    310325  | tac_base:
    311326      ∀status: S.
    312         as_classifier S status cl_call
     327        as_classifier S status cl_call ∨ as_classifier S status cl_tailcall
    313328          trace_any_call S status status
    314329  | tac_step_call:
     
    436451| tal_base_return _ _  _ _ ⇒ I
    437452| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     453| tal_base_tailcall _ _ _ _ _ _ ⇒ I
    438454| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    439455| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
     
    456472
    457473lemma trace_any_call_call : ∀S,s,s'.
    458   trace_any_call S s s' → as_classifier S s' cl_call.
     474  trace_any_call S s s' → as_classifier S s' cl_call ∨ as_classifier S s' cl_tailcall.
    459475#S #s #s' #T elim T [1,3: //]
    460476#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
     
    616632      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    617633      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
     634  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒
     635    fl2 = ends_with_ret ∧
     636    ∃st2mid,G.as_tailcall_ident S2 («st2mid, G») = as_tailcall_ident ? «st1, prf» ∧
     637    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     638    ∃tlr2 : trace_label_return ? st2mid' st2'.
     639      tal2 ≃ taa @ (tal_base_tailcall … H G tlr2) ∧ tlr_rel … tlr1 tlr2
    618640  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
    619641    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     
    636658let rec tal_collapsable_eq_fl S1 fl1 s1 s1'
    637659  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
    638   tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝ ?.
    639 cases tal1 -fl1 -s1 -s1' //
    640 [ #s1 #s1' #H #I *
    641 | #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl *
    642 | #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl)
    643 ]
    644 qed.
     660  tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝
     661match tal1 return λfl1,s1,s1',tal1.
     662  tal_collapsable S1 fl1 s1 s1' tal1 → fl1 = doesnt_end_with_ret with
     663[ tal_base_not_return _ _ _ _ _ ⇒ λ_.refl …
     664| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable_eq_fl … tl1
     665| _ ⇒ Ⓧ
     666].
    645667
    646668let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2'
     
    651673  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    652674  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     675  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
    653676  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    654677  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    655678  ].
    656679-fl1 -s1 -s1'
    657 [1,2,3: -tal_rel_eq_fl #tal2 * //
     680[1,2,3,4: -tal_rel_eq_fl #tal2 * //
    658681| #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 *
    659682  [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
     
    691714  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    692715  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     716  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
    693717  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    694718  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    695719  ].
    696720-fl1 -s1 -s1'
    697 [1,2,3: -tal_rel_collapsable #tal2 * *
     721[1,2,3,4: -tal_rel_collapsable #tal2 * *
    698722  #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable %
    699723| #tal2 *
     
    725749  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    726750  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     751      flatten_trace_label_return … call_trace
     752  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    727753      flatten_trace_label_return … call_trace
    728754  | tal_base_return the_status _ _ _ ⇒ [ ]
     
    819845  | tal_base_return st1 st1' H G ⇒ ?
    820846  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
     847  | tal_base_tailcall st1 st1' st1'' H G tlr1 ⇒ ?
    821848  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
    822849  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
     
    843870  >EQ1 >EQ2 normalize nodelta #_ #_
    844871  >(tal_rel_to_traces_same_flatten … H_tal) @refl
    845 |2,3,4,5,6:
    846   [1,2,3: * #EQ destruct(EQ)]
    847   [1,2,3,4: * #st_mid [1,2:|*: * #G' * #call ] * #taa
     872|2,3,4,5,6,7:
     873  [1,2,3,4: * #EQ destruct(EQ)]
     874  [1,2,3,4,5: * #st_mid [1,2:|*: * #G' * #call ] * #taa
    848875    [ *#H' *#G' *#K' #EQ
    849876    | *#H' *#G' #EQ
    850877    | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L'
    851878      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
     879    | *#st_mid' *#H' *#tlr2 * #EQ #H_tlr
    852880    | *#st_fun *#H' *
    853881      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
     
    858886  ]
    859887  [1,2: %
    860   |3: @(tlr_rel_to_traces_same_flatten … H_tlr)
    861   |4,5: <map_append
     888  |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
     889  |4,6: <map_append
    862890    >(tal_collapsable_flatten … H_tl) >append_nil
    863891    >(tlr_rel_to_traces_same_flatten … H_tlr) %
    864   |6: <map_append
     892  |7: <map_append
    865893    >(tlr_rel_to_traces_same_flatten … H_tlr)
    866894    >(tal_rel_to_traces_same_flatten … H_tl)
Note: See TracChangeset for help on using the changeset viewer.