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