Changeset 2656


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

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

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2593 r2656  
    216216  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
    217217  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
    218   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
     218  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call
     219  | tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call
    219220  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    220221     _ _ _ call_trace _ final_trace ⇒
     
    229230      in
    230231        current_instruction_cost + tail_trace_cost
    231   | _ ⇒ ? (* XXX Paolo ??? *)
    232   ].
    233   cases daemon
    234   qed.
     232  ].
    235233
    236234definition compute_paid_trace_label_label ≝
     
    293291      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    294292      destruct @⊥
    295     |4: (* XXX *)
    296       cases daemon
     293    |4:
     294      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     295      #classifier_assm #trace_label_return
     296      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     297      destruct @⊥
    297298    |5:
    298299      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    444445    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    445446    destruct @⊥
    446   |4: (* XXX *)
    447     cases daemon
     447  |4:
     448    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     449    #classifier_assm #trace_label_return
     450    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     451    destruct @⊥
    448452  |5:
    449453    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    545549      ]
    546550    ]
    547   |4: (* XXX *)
    548     cases daemon
     551  |4:
     552    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     553    #classifier_assm #trace_label_return
     554    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     555    destruct @⊥
    549556  |5:
    550557    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
  • 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
  • src/BACKEND_BROKEN_FILES

    r2645 r2656  
    2525ASM/CostProofs.ma                 mancano tailcall
    2626
    27 ASM/Policy.ma                     zzzzzzzz
    28 
    2927========================================================
    3028
Note: See TracChangeset for help on using the changeset viewer.