Changeset 2656 for src/ASM/ASMCosts.ma

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:

• src/ASM/ASMCosts.ma (modified) (5 diffs)

src/ASM/ASMCosts.ma

@@ -216 +216 @@
   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
-  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
+  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call
+  | tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call
   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
      _ _ _ call_trace _ final_trace ⇒
@@ -229 +230 @@
       in
         current_instruction_cost + tail_trace_cost
-  | _ ⇒ ? (* XXX Paolo ??? *)
-  ]. 
-  cases daemon
-  qed.
+  ].
 
 definition compute_paid_trace_label_label ≝
@@ -293 +291 @@
       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
       destruct @⊥
-    |4: (* XXX *)
-      cases daemon 
+    |4: 
+      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
+      #classifier_assm #trace_label_return
+      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
+      destruct @⊥
     |5:
       #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
     destruct @⊥
-  |4: (* XXX *)
-    cases daemon 
+  |4:
+    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
+    #classifier_assm #trace_label_return
+    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
+    destruct @⊥
   |5:
     #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
@@ -545 +549 @@
       ]
     ]
-  |4: (* XXX *)
-    cases daemon 
+  |4:
+    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
+    #classifier_assm #trace_label_return
+    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
+    destruct @⊥
   |5:
     #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call