source: extracted/smallstepExec.mli @ 2649

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

...

File size: 9.8 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Proper
32
33open ErrorMessages
34
35open Option
36
37open Setoids
38
39open Monad
40
41open Positive
42
43open PreIdentifiers
44
45open Errors
46
47open IOMonad
48
49open Arithmetic
50
51open Vector
52
53open FoldStuff
54
55open BitVector
56
57open Extranat
58
59open Integers
60
61open CostLabel
62
63open PositiveMap
64
65open Deqsets
66
67open Lists
68
69open Identifiers
70
71open AST
72
73open Division
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open Coqlib
82
83open Values
84
85open Events
86
87type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
88                                                 Types.option);
89                                      step : (__ -> __ -> ('outty, 'inty,
90                                             (Events.trace, __) Types.prod)
91                                             IOMonad.iO) }
92
93val trans_system_rect_Type4 :
94  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
95  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
96  trans_system -> 'a3
97
98val trans_system_rect_Type5 :
99  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
100  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
101  trans_system -> 'a3
102
103val trans_system_rect_Type3 :
104  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
105  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
106  trans_system -> 'a3
107
108val trans_system_rect_Type2 :
109  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
110  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
111  trans_system -> 'a3
112
113val trans_system_rect_Type1 :
114  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
115  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
116  trans_system -> 'a3
117
118val trans_system_rect_Type0 :
119  (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
120  'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
121  trans_system -> 'a3
122
123type ('outty, 'inty) global
124
125type ('outty, 'inty) state
126
127val is_final :
128  ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option
129
130val step :
131  ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
132  Types.prod) IOMonad.iO
133
134val trans_system_inv_rect_Type4 :
135  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
136  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
137  IOMonad.iO) -> __ -> 'a3) -> 'a3
138
139val trans_system_inv_rect_Type3 :
140  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
141  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
142  IOMonad.iO) -> __ -> 'a3) -> 'a3
143
144val trans_system_inv_rect_Type2 :
145  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
146  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
147  IOMonad.iO) -> __ -> 'a3) -> 'a3
148
149val trans_system_inv_rect_Type1 :
150  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
151  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
152  IOMonad.iO) -> __ -> 'a3) -> 'a3
153
154val trans_system_inv_rect_Type0 :
155  ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
156  Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
157  IOMonad.iO) -> __ -> 'a3) -> 'a3
158
159val repeat :
160  Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace,
161  __) Types.prod) IOMonad.iO
162
163val trace_map :
164  ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
165  (Events.trace, 'a2 List.list) Types.prod Errors.res
166
167type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g : 
168                           __; avs_inv : (__ -> Bool.bool) }
169
170val await_value_stuff_rect_Type4 :
171  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
172  await_value_stuff -> 'a1
173
174val await_value_stuff_rect_Type5 :
175  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
176  await_value_stuff -> 'a1
177
178val await_value_stuff_rect_Type3 :
179  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
180  await_value_stuff -> 'a1
181
182val await_value_stuff_rect_Type2 :
183  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
184  await_value_stuff -> 'a1
185
186val await_value_stuff_rect_Type1 :
187  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
188  await_value_stuff -> 'a1
189
190val await_value_stuff_rect_Type0 :
191  (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
192  await_value_stuff -> 'a1
193
194type avs_O
195
196type avs_I
197
198val avs_exec : await_value_stuff -> (__, __) trans_system
199
200val avs_g : await_value_stuff -> __
201
202val avs_inv : await_value_stuff -> __ -> Bool.bool
203
204val await_value_stuff_inv_rect_Type4 :
205  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
206  Bool.bool) -> __ -> 'a1) -> 'a1
207
208val await_value_stuff_inv_rect_Type3 :
209  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
210  Bool.bool) -> __ -> 'a1) -> 'a1
211
212val await_value_stuff_inv_rect_Type2 :
213  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
214  Bool.bool) -> __ -> 'a1) -> 'a1
215
216val await_value_stuff_inv_rect_Type1 :
217  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
218  Bool.bool) -> __ -> 'a1) -> 'a1
219
220val await_value_stuff_inv_rect_Type0 :
221  await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
222  Bool.bool) -> __ -> 'a1) -> 'a1
223
224type await_value = __
225
226type assert0 = __
227
228type after_aux = __
229
230type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
231and ('state, 'output, 'input) __execution =
232| E_stop of Events.trace * Integers.int * 'state
233| E_step of Events.trace * 'state * ('state, 'output, 'input) execution
234| E_wrong of Errors.errmsg
235| E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
236
237val execution_inv_rect_Type4 :
238  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
239  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
240  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
241  -> __ -> 'a4) -> 'a4
242
243val execution_inv_rect_Type3 :
244  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
245  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
246  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
247  -> __ -> 'a4) -> 'a4
248
249val execution_inv_rect_Type2 :
250  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
251  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
252  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
253  -> __ -> 'a4) -> 'a4
254
255val execution_inv_rect_Type1 :
256  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
257  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
258  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
259  -> __ -> 'a4) -> 'a4
260
261val execution_inv_rect_Type0 :
262  ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
263  'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
264  (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
265  -> __ -> 'a4) -> 'a4
266
267val execution_discr :
268  ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
269
270val execution_jmdiscr :
271  ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
272
273val exec_inf_aux :
274  ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
275  IOMonad.iO -> (__, 'a1, 'a2) execution
276
277type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
278                                  make_global : (__ -> __);
279                                  make_initial_state : (__ -> __ Errors.res) }
280
281val fullexec_rect_Type4 :
282  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
283  'a3) -> ('a1, 'a2) fullexec -> 'a3
284
285val fullexec_rect_Type5 :
286  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
287  'a3) -> ('a1, 'a2) fullexec -> 'a3
288
289val fullexec_rect_Type3 :
290  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
291  'a3) -> ('a1, 'a2) fullexec -> 'a3
292
293val fullexec_rect_Type2 :
294  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
295  'a3) -> ('a1, 'a2) fullexec -> 'a3
296
297val fullexec_rect_Type1 :
298  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
299  'a3) -> ('a1, 'a2) fullexec -> 'a3
300
301val fullexec_rect_Type0 :
302  (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
303  'a3) -> ('a1, 'a2) fullexec -> 'a3
304
305type ('outty, 'inty) program0
306
307val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system
308
309val make_global : ('a1, 'a2) fullexec -> __ -> __
310
311val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res
312
313val fullexec_inv_rect_Type4 :
314  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
315  -> __ Errors.res) -> __ -> 'a3) -> 'a3
316
317val fullexec_inv_rect_Type3 :
318  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
319  -> __ Errors.res) -> __ -> 'a3) -> 'a3
320
321val fullexec_inv_rect_Type2 :
322  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
323  -> __ Errors.res) -> __ -> 'a3) -> 'a3
324
325val fullexec_inv_rect_Type1 :
326  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
327  -> __ Errors.res) -> __ -> 'a3) -> 'a3
328
329val fullexec_inv_rect_Type0 :
330  ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
331  -> __ Errors.res) -> __ -> 'a3) -> 'a3
332
333val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution
334
335type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
336
337val split_trace :
338  ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
339  'a2) execution) Types.prod Types.option
340
Note: See TracBrowser for help on using the repository browser.