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/aSMCostsSplit.ml

    r2649 r2717  
    1515open Interpret
    1616
    17 open BitVectorTrie
    18 
    1917open Fetch
    2018
     
    2220
    2321open LabelledObjects
     22
     23open BitVectorTrie
     24
     25open Exp
    2426
    2527open Arithmetic
     
    142144        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    143145        Nat.O)))))))))))))))))
    144       (Util.exponential (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
     146      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    145147        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    146         (Nat.S (Nat.S Nat.O))))))))))))))))))
     148        (Nat.S Nat.O))))))))))))))))))
    147149
    148150(** val compute_costs :
Note: See TracChangeset for help on using the changeset viewer.