Changeset 2717 for extracted/aSMCostsSplit.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/aSMCostsSplit.ml (modified) (3 diffs)

extracted/aSMCostsSplit.ml

@@ -15 +15 @@
 open Interpret
 
-open BitVectorTrie
-
 open Fetch
 
@@ -22 +20 @@
 
 open LabelledObjects
+
+open BitVectorTrie
+
+open Exp
 
 open Arithmetic
@@ -142 +144 @@
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O)))))))))))))))))
-      (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))))))))))))))))))
+        (Nat.S Nat.O))))))))))))))))))
 
 (** val compute_costs :