Changeset 2717 for extracted/costLabel.mli

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/costLabel.mli (modified) (2 diffs)

extracted/costLabel.mli

@@ -26 +26 @@
 
 open Identifiers
+
+open Exp
 
 open Arithmetic
@@ -67 +69 @@
 open AST
 
+open BitVectorTrie
+
 type costlabel = PreIdentifiers.identifier
 
 val costlabel_of_nat : Nat.nat -> costlabel
 
+type costlabel_map = costlabel BitVectorTrie.bitVectorTrie
+
+val costlabel_map0 : costlabel_map
+