Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/costLabel.ml

    r2649 r2717  
    2626
    2727open Identifiers
     28
     29open Exp
    2830
    2931open Arithmetic
     
    6769open AST
    6870
     71open BitVectorTrie
     72
    6973type costlabel = PreIdentifiers.identifier
    7074
     
    7377  Identifiers.identifier_of_nat PreIdentifiers.CostTag
    7478
     79type costlabel_map = costlabel BitVectorTrie.bitVectorTrie
     80
     81(** val costlabel_map0 : costlabel_map **)
     82let costlabel_map0 =
     83  BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     84    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     85    Nat.O))))))))))))))))
     86
Note: See TracChangeset for help on using the changeset viewer.