source: driver/extracted/events.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 4.9 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 CostLabel
84
85type eventval =
86| EVint of AST.intsize * AST.bvint
87
88val eventval_rect_Type4 :
89  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
90
91val eventval_rect_Type5 :
92  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
93
94val eventval_rect_Type3 :
95  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
96
97val eventval_rect_Type2 :
98  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
99
100val eventval_rect_Type1 :
101  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
102
103val eventval_rect_Type0 :
104  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
105
106val eventval_inv_rect_Type4 :
107  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
108
109val eventval_inv_rect_Type3 :
110  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
111
112val eventval_inv_rect_Type2 :
113  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
114
115val eventval_inv_rect_Type1 :
116  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
117
118val eventval_inv_rect_Type0 :
119  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
120
121val eventval_discr : eventval -> eventval -> __
122
123val eventval_jmdiscr : eventval -> eventval -> __
124
125type event =
126| EVcost of CostLabel.costlabel
127| EVextcall of AST.ident * eventval List.list * eventval
128
129val event_rect_Type4 :
130  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
131  eventval -> 'a1) -> event -> 'a1
132
133val event_rect_Type5 :
134  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
135  eventval -> 'a1) -> event -> 'a1
136
137val event_rect_Type3 :
138  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
139  eventval -> 'a1) -> event -> 'a1
140
141val event_rect_Type2 :
142  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
143  eventval -> 'a1) -> event -> 'a1
144
145val event_rect_Type1 :
146  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
147  eventval -> 'a1) -> event -> 'a1
148
149val event_rect_Type0 :
150  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
151  eventval -> 'a1) -> event -> 'a1
152
153val event_inv_rect_Type4 :
154  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
155  List.list -> eventval -> __ -> 'a1) -> 'a1
156
157val event_inv_rect_Type3 :
158  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
159  List.list -> eventval -> __ -> 'a1) -> 'a1
160
161val event_inv_rect_Type2 :
162  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
163  List.list -> eventval -> __ -> 'a1) -> 'a1
164
165val event_inv_rect_Type1 :
166  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
167  List.list -> eventval -> __ -> 'a1) -> 'a1
168
169val event_inv_rect_Type0 :
170  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
171  List.list -> eventval -> __ -> 'a1) -> 'a1
172
173val event_discr : event -> event -> __
174
175val event_jmdiscr : event -> event -> __
176
177type trace = event List.list
178
179val e0 : trace
180
181val echarge : CostLabel.costlabel -> trace
182
183val eextcall : AST.ident -> eventval List.list -> eventval -> trace
184
185val eapp : trace -> trace -> trace
186
187type traceinf = __traceinf Lazy.t
188and __traceinf =
189| Econsinf of event * traceinf
190
191val traceinf_inv_rect_Type4 :
192  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
193
194val traceinf_inv_rect_Type3 :
195  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
196
197val traceinf_inv_rect_Type2 :
198  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
199
200val traceinf_inv_rect_Type1 :
201  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
202
203val traceinf_inv_rect_Type0 :
204  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
205
206val traceinf_discr : traceinf -> traceinf -> __
207
208val traceinf_jmdiscr : traceinf -> traceinf -> __
209
210val eappinf : trace -> traceinf -> traceinf
211
212val remove_costs : trace -> trace
213
214type traceinf' = __traceinf' Lazy.t
215and __traceinf' =
216| Econsinf' of trace * traceinf'
217
218val traceinf'_inv_rect_Type4 :
219  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
220
221val traceinf'_inv_rect_Type3 :
222  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
223
224val traceinf'_inv_rect_Type2 :
225  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
226
227val traceinf'_inv_rect_Type1 :
228  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
229
230val traceinf'_inv_rect_Type0 :
231  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
232
233val traceinf'_discr : traceinf' -> traceinf' -> __
234
235val traceinf'_jmdiscr : traceinf' -> traceinf' -> __
236
237val split_traceinf' : trace -> traceinf' -> (event, traceinf') Types.prod
238
239val traceinf_of_traceinf' : traceinf' -> traceinf
240
Note: See TracBrowser for help on using the repository browser.