Changeset 2656 for src/ASM/ASMCosts.ma


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

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

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.