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
Line 
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
21open Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
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
83open BitVectorTrie
84
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.