source: extracted/smallstepExec.mli @ 2731

Last change on this file since 2731 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
RevLine 
[2601]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
[2649]33open ErrorMessages
34
[2601]35open Option
36
37open Setoids
38
39open Monad
40
41open Positive
42
43open PreIdentifiers
44
45open Errors
46
47open IOMonad
48
[2717]49open Exp
50
[2601]51open Arithmetic
52
53open Vector
54
55open FoldStuff
56
57open BitVector
58
59open Extranat
60
61open Integers
62
[2717]63open BitVectorTrie
64
[2601]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
[2717]232type assert_nz = __
233
[2601]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
[2649]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
[2717]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.