source: extracted/smallstepExec.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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