source: extracted/events.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: 5.0 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
[2717]21open Exp
22
[2601]23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
[2649]39open ErrorMessages
40
[2601]41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
[2717]83open BitVectorTrie
84
[2601]85open CostLabel
86
87type eventval =
88| EVint of AST.intsize * AST.bvint
89
90val eventval_rect_Type4 :
91  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
92
93val eventval_rect_Type5 :
94  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
95
96val eventval_rect_Type3 :
97  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
98
99val eventval_rect_Type2 :
100  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
101
102val eventval_rect_Type1 :
103  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
104
105val eventval_rect_Type0 :
106  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
107
108val eventval_inv_rect_Type4 :
109  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
110
111val eventval_inv_rect_Type3 :
112  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
113
114val eventval_inv_rect_Type2 :
115  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
116
117val eventval_inv_rect_Type1 :
118  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
119
120val eventval_inv_rect_Type0 :
121  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
122
123val eventval_discr : eventval -> eventval -> __
124
125val eventval_jmdiscr : eventval -> eventval -> __
126
127type event =
128| EVcost of CostLabel.costlabel
129| EVextcall of AST.ident * eventval List.list * eventval
130
131val event_rect_Type4 :
132  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
133  eventval -> 'a1) -> event -> 'a1
134
135val event_rect_Type5 :
136  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
137  eventval -> 'a1) -> event -> 'a1
138
139val event_rect_Type3 :
140  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
141  eventval -> 'a1) -> event -> 'a1
142
143val event_rect_Type2 :
144  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
145  eventval -> 'a1) -> event -> 'a1
146
147val event_rect_Type1 :
148  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
149  eventval -> 'a1) -> event -> 'a1
150
151val event_rect_Type0 :
152  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
153  eventval -> 'a1) -> event -> 'a1
154
155val event_inv_rect_Type4 :
156  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
157  List.list -> eventval -> __ -> 'a1) -> 'a1
158
159val event_inv_rect_Type3 :
160  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
161  List.list -> eventval -> __ -> 'a1) -> 'a1
162
163val event_inv_rect_Type2 :
164  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
165  List.list -> eventval -> __ -> 'a1) -> 'a1
166
167val event_inv_rect_Type1 :
168  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
169  List.list -> eventval -> __ -> 'a1) -> 'a1
170
171val event_inv_rect_Type0 :
172  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
173  List.list -> eventval -> __ -> 'a1) -> 'a1
174
175val event_discr : event -> event -> __
176
177val event_jmdiscr : event -> event -> __
178
179type trace = event List.list
180
181val e0 : trace
182
183val echarge : CostLabel.costlabel -> trace
184
185val eextcall : AST.ident -> eventval List.list -> eventval -> trace
186
187val eapp : trace -> trace -> trace
188
189type traceinf = __traceinf Lazy.t
190and __traceinf =
191| Econsinf of event * traceinf
192
193val traceinf_inv_rect_Type4 :
194  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
195
196val traceinf_inv_rect_Type3 :
197  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
198
199val traceinf_inv_rect_Type2 :
200  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
201
202val traceinf_inv_rect_Type1 :
203  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
204
205val traceinf_inv_rect_Type0 :
206  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
207
208val traceinf_discr : traceinf -> traceinf -> __
209
210val traceinf_jmdiscr : traceinf -> traceinf -> __
211
212val eappinf : trace -> traceinf -> traceinf
213
214val remove_costs : trace -> trace
215
216type traceinf' = __traceinf' Lazy.t
217and __traceinf' =
218| Econsinf' of trace * traceinf'
219
220val traceinf'_inv_rect_Type4 :
221  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
222
223val traceinf'_inv_rect_Type3 :
224  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
225
226val traceinf'_inv_rect_Type2 :
227  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
228
229val traceinf'_inv_rect_Type1 :
230  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
231
232val traceinf'_inv_rect_Type0 :
233  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
234
235val traceinf'_discr : traceinf' -> traceinf' -> __
236
237val traceinf'_jmdiscr : traceinf' -> traceinf' -> __
238
239val split_traceinf' : trace -> traceinf' -> (event, traceinf') Types.prod
240
241val traceinf_of_traceinf' : traceinf' -> traceinf
242
Note: See TracBrowser for help on using the repository browser.