source: extracted/smallstep.mli @ 2649

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

...

File size: 7.9 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Integers
18
19open AST
20
21open Division
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 Events
84
85type transrel =
86| Mk_transrel
87
88val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
89
90val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
91
92val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
93
94val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
95
96val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
97
98val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
99
100type genv
101
102type state
103
104type step = __
105
106val transrel_inv_rect_Type4 :
107  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
108
109val transrel_inv_rect_Type3 :
110  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
111
112val transrel_inv_rect_Type2 :
113  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
114
115val transrel_inv_rect_Type1 :
116  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
117
118val transrel_inv_rect_Type0 :
119  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
120
121val transrel_jmdiscr : transrel -> transrel -> __
122
123type program_behavior =
124| Terminates of Events.trace * Integers.int
125| Diverges of Events.trace
126| Reacts of Events.traceinf
127| Goes_wrong of Events.trace
128
129val program_behavior_rect_Type4 :
130  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
131  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
132  'a1
133
134val program_behavior_rect_Type5 :
135  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
136  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
137  'a1
138
139val program_behavior_rect_Type3 :
140  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
141  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
142  'a1
143
144val program_behavior_rect_Type2 :
145  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
146  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
147  'a1
148
149val program_behavior_rect_Type1 :
150  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
151  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
152  'a1
153
154val program_behavior_rect_Type0 :
155  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
156  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
157  'a1
158
159val program_behavior_inv_rect_Type4 :
160  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
161  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
162  (Events.trace -> __ -> 'a1) -> 'a1
163
164val program_behavior_inv_rect_Type3 :
165  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
166  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
167  (Events.trace -> __ -> 'a1) -> 'a1
168
169val program_behavior_inv_rect_Type2 :
170  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
171  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
172  (Events.trace -> __ -> 'a1) -> 'a1
173
174val program_behavior_inv_rect_Type1 :
175  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
176  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
177  (Events.trace -> __ -> 'a1) -> 'a1
178
179val program_behavior_inv_rect_Type0 :
180  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
181  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
182  (Events.trace -> __ -> 'a1) -> 'a1
183
184val program_behavior_discr : program_behavior -> program_behavior -> __
185
186val program_behavior_jmdiscr : program_behavior -> program_behavior -> __
187
188type semantics = { trans : transrel; ge : __ }
189
190val semantics_rect_Type4 :
191  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
192
193val semantics_rect_Type5 :
194  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
195
196val semantics_rect_Type3 :
197  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
198
199val semantics_rect_Type2 :
200  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
201
202val semantics_rect_Type1 :
203  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
204
205val semantics_rect_Type0 :
206  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
207
208val trans : semantics -> transrel
209
210type initial = __
211
212type final = __
213
214val ge : semantics -> __
215
216val semantics_inv_rect_Type4 :
217  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
218
219val semantics_inv_rect_Type3 :
220  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
221
222val semantics_inv_rect_Type2 :
223  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
224
225val semantics_inv_rect_Type1 :
226  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
227
228val semantics_inv_rect_Type0 :
229  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
230
231val semantics_jmdiscr : semantics -> semantics -> __
232
233type related_semantics = { sem1 : semantics; sem2 : semantics }
234
235val related_semantics_rect_Type4 :
236  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
237  'a1
238
239val related_semantics_rect_Type5 :
240  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
241  'a1
242
243val related_semantics_rect_Type3 :
244  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
245  'a1
246
247val related_semantics_rect_Type2 :
248  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
249  'a1
250
251val related_semantics_rect_Type1 :
252  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
253  'a1
254
255val related_semantics_rect_Type0 :
256  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
257  'a1
258
259val sem1 : related_semantics -> semantics
260
261val sem2 : related_semantics -> semantics
262
263type match_states = __
264
265val related_semantics_inv_rect_Type4 :
266  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
267  'a1) -> 'a1
268
269val related_semantics_inv_rect_Type3 :
270  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
271  'a1) -> 'a1
272
273val related_semantics_inv_rect_Type2 :
274  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
275  'a1) -> 'a1
276
277val related_semantics_inv_rect_Type1 :
278  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
279  'a1) -> 'a1
280
281val related_semantics_inv_rect_Type0 :
282  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
283  'a1) -> 'a1
284
285val related_semantics_jmdiscr : related_semantics -> related_semantics -> __
286
287type order_sim =
288  related_semantics
289  (* singleton inductive, whose constructor was mk_order_sim *)
290
291val order_sim_rect_Type4 :
292  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
293
294val order_sim_rect_Type5 :
295  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
296
297val order_sim_rect_Type3 :
298  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
299
300val order_sim_rect_Type2 :
301  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
302
303val order_sim_rect_Type1 :
304  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
305
306val order_sim_rect_Type0 :
307  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
308
309val sem : order_sim -> related_semantics
310
311type order = __
312
313val order_sim_inv_rect_Type4 :
314  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
315
316val order_sim_inv_rect_Type3 :
317  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
318
319val order_sim_inv_rect_Type2 :
320  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
321
322val order_sim_inv_rect_Type1 :
323  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
324
325val order_sim_inv_rect_Type0 :
326  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
327
328val order_sim_jmdiscr : order_sim -> order_sim -> __
329
Note: See TracBrowser for help on using the repository browser.