Changeset 2717 for extracted/aSMCosts.ml

Timestamp:

Feb 23, 2013, 1:16:55 AM (7 years ago)

Author:

sacerdot

Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:

• extracted/aSMCosts.ml (modified) (7 diffs)

extracted/aSMCosts.ml

@@ -5 +5 @@
 open LabelledObjects
 
+open BitVectorTrie
+
+open Exp
+
 open Arithmetic
 
@@ -74 +78 @@
 
 open ASM
-
-open BitVectorTrie
 
 open Fetch
@@ -141 +143 @@
 | StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
   Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
-| StructuredTraces.Tal_base_tailcall (x, x0, x1, x4) ->
-  assert false (* absurd case *)
+| StructuredTraces.Tal_base_tailcall
+    (pre_fun_call, start_fun_call, final, x1) ->
+  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
 | StructuredTraces.Tal_step_call
     (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
@@ -184 +187 @@
    | Nat.S program_size' ->
      (fun _ ->
-       (let { Types.fst = eta24805; Types.snd = ticks } =
+       (let { Types.fst = eta31521; Types.snd = ticks } =
           Fetch.fetch code_memory' program_counter'
         in
        let { Types.fst = instruction0; Types.snd = program_counter'' } =
-         eta24805
+         eta31521
        in
        (fun _ ->
@@ -247 +250 @@
                           (block_cost' code_memory' jump_target program_size'
                             cost_labels Bool.False)))
-                  | ASM.JMP addr ->
-                    (fun _ ->
-                      Nat.plus ticks
-                        (Types.pi1
-                          (block_cost' code_memory' program_counter''
-                            program_size' cost_labels Bool.False)))
                   | ASM.MOVC (src, trgt) ->
                     (fun _ ->
@@ -428 +425 @@
                              (Types.pi1
                                (block_cost' code_memory' program_counter''
+                                 program_size' cost_labels Bool.False)))
+                       | ASM.JMP addr ->
+                         (fun _ ->
+                           Nat.plus ticks
+                             (Types.pi1
+                               (block_cost' code_memory' program_counter''
                                  program_size' cost_labels Bool.False)))) __))
                   __))
@@ -440 +443 @@
   let cost_of_block =
     block_cost' code_memory program_counter0
-      (Util.exponential (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
+      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-        (Nat.S (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
+        (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
   in
   cost_of_block