source: extracted/label.mli @ 2649

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

...

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