source: extracted/label.mli @ 2717

Last change on this file since 2717 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: 2.7 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list
80
81val labels_of_labeled_statements :
82  Csyntax.labeled_statements -> CostLabel.costlabel List.list
83
84val labels_of_statement : Csyntax.statement -> CostLabel.costlabel List.list
85
86val labels_of_clight_fundef :
87  (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
88  List.list
89
90val labels_of_clight :
91  Csyntax.clight_program -> CostLabel.costlabel List.list
92
93type in_clight_label = CostLabel.costlabel Types.sig0
94
95type clight_cost_map = in_clight_label -> Nat.nat
96
97val clight_label_free : Csyntax.clight_program -> Bool.bool
98
99val add_cost_before :
100  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
101  Identifiers.universe) Types.prod
102
103val add_cost_after :
104  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
105  Identifiers.universe) Types.prod
106
107val add_cost_expr :
108  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
109  Identifiers.universe) Types.prod
110
111val const_int : AST.intsize -> Nat.nat -> Csyntax.expr
112
113val label_expr_descr :
114  Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
115  (Csyntax.expr_descr, Identifiers.universe) Types.prod
116
117val label_expr :
118  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
119  Identifiers.universe) Types.prod
120
121val label_exprs :
122  Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr List.list,
123  Identifiers.universe) Types.prod
124
125val label_opt_expr :
126  Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
127  Types.option, Identifiers.universe) Types.prod
128
129val label_lstatements :
130  Csyntax.labeled_statements -> Identifiers.universe ->
131  (Csyntax.labeled_statements, Identifiers.universe) Types.prod
132
133val label_statement :
134  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
135  Identifiers.universe) Types.prod
136
137val label_function :
138  Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
139  Identifiers.universe) Types.prod
140
141val label_fundef :
142  Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
143  Identifiers.universe) Types.prod
144
145val clight_label :
146  Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
147  Types.prod
148
Note: See TracBrowser for help on using the repository browser.