Changeset 2656 for src/ASM/ASMCosts.ma
- Timestamp:
- Feb 11, 2013, 6:58:13 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r2593 r2656 216 216 [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status 217 217 | 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 219 220 | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 220 221 _ _ _ call_trace _ final_trace ⇒ … … 229 230 in 230 231 current_instruction_cost + tail_trace_cost 231 | _ ⇒ ? (* XXX Paolo ??? *) 232 ]. 233 cases daemon 234 qed. 232 ]. 235 233 236 234 definition compute_paid_trace_label_label ≝ … … 293 291 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 294 292 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 @⊥ 297 298 |5: 298 299 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call … … 444 445 #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl 445 446 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 @⊥ 448 452 |5: 449 453 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call … … 545 549 ] 546 550 ] 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 @⊥ 549 556 |5: 550 557 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
Note: See TracChangeset
for help on using the changeset viewer.