Changeset 2656 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Feb 11, 2013, 6:58:13 PM (8 years ago)
Author:
sacerdot
Message:

Ported to tailcalls (currently nothing is classified as a tailcall).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2516 r2656  
    3030  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost cm the_status
    3131  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     32      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     33      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     34        call_trace_cost + current_instruction_cost
     35  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    3236      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
    3337      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     
    104108      @execute_1_ok_clock
    105109    |4:
     110      #status_pre_fun_call #status_start_fun_call #status_final #is_next
     111      #classifier_assm #call_trace
     112      whd in match (compute_max_trace_any_label_cost … (tal_base_tailcall …));
     113      >(compute_max_trace_label_return_cost_is_ok … call_trace)
     114      >associative_plus @eq_f cases(is_next)
     115      @execute_1_ok_clock
     116    |5:
    106117      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    107118      #status_final #is_next #is_call #is_after_return #call_trace #not_costed #final_trace
     
    125136      @eq_f >commutative_plus in ⊢ (??%?); >associative_plus in ⊢ (??%?);
    126137      @eq_f @commutative_plus
    127     |5:
     138    |6:
    128139      #end_flag #status_pre #status_init #status_end #is_next
    129140      #trace_any_label #is_other #is_not_costed
     
    186197  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    187198      compute_trace_label_return_cost_using_paid … call_trace
     199  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
     200      compute_trace_label_return_cost_using_paid … call_trace
    188201  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    189202     _ _ _ call_trace _ final_trace ⇒
     
    241254  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
    242255  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
    243   |
    244     #sp #ss #sf #H1 #H2 #tr1 #tr2 #H3
     256  | #sp #ss #sf #H1 #H2 #tr1 #tr2 #H3
     257    whd in ⊢ (???%); whd in ⊢ (??(??%)?); whd in ⊢ (??(?%?)?);
     258    >compute_trace_label_return_cost_using_paid_ok in ⊢ (??%?);
     259    >commutative_plus in ⊢ (??%?); @eq_f %
     260  | #sp #ss #sf #H1 #H2 #tr1
    245261    whd in ⊢ (???%); whd in ⊢ (??(??%)?); whd in ⊢ (??(?%?)?);
    246262    >compute_trace_label_return_cost_using_paid_ok in ⊢ (??%?);
     
    571587      ]
    572588    ]
    573   |8:
     589  |9:
    574590    #end_flag #start_status #end_status #trace_any_label #costed_assm
    575591    #unrepeating_witness'
     
    585601        change with (? = lookup_present ? ? ? ? ?)
    586602        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    587         normalize in match (nth_safe ? ? ? ?);
     603        whd in ⊢ (∀p:????%.???(????%?));
    588604        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
    589605        inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
     
    616632    assumption
    617633  |6:
     634    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     635    #classifier_assm #trace_label_return #unrepeating_witness
     636    whd in ⊢ (??%?);
     637    @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     638    assumption
     639  |7:
    618640    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    619641    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     
    637659      * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
    638660    ]
    639   |7:
     661  |8:
    640662    #end_flag #status_pre_fun_call #status_start_fun_call #status_final
    641663    #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness
Note: See TracChangeset for help on using the changeset viewer.