source: extracted/costLabel.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

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 size: 710 bytes
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Exp
30
31open Arithmetic
32
33open Vector
34
35open Div_and_mod
36
37open Jmeq
38
39open Russell
40
41open List
42
43open Util
44
45open FoldStuff
46
47open BitVector
48
49open Extranat
50
51open Bool
52
53open Relations
54
55open Nat
56
57open Integers
58
59open Hints_declaration
60
61open Core_notation
62
63open Pts
64
65open Logic
66
67open Types
68
69open AST
70
71open BitVectorTrie
72
73type costlabel = PreIdentifiers.identifier
74
75val costlabel_of_nat : Nat.nat -> costlabel
76
77type costlabel_map = costlabel BitVectorTrie.bitVectorTrie
78
79val costlabel_map0 : costlabel_map
80
Note: See TracBrowser for help on using the repository browser.