source: extracted/events.mli @ 2716

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

...

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