source: extracted/smallstep.mli @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 8 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: 7.9 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open Extralib
14
15open Lists
16
17open Identifiers
18
19open Integers
20
21open AST
22
23open Division
24
25open Exp
26
27open Arithmetic
28
29open Extranat
30
31open Vector
32
33open FoldStuff
34
35open BitVector
36
37open Z
38
39open BitVectorZ
40
41open Pointers
42
43open ErrorMessages
44
45open Option
46
47open Setoids
48
49open Monad
50
51open Positive
52
53open PreIdentifiers
54
55open Errors
56
57open Div_and_mod
58
59open Jmeq
60
61open Russell
62
63open Util
64
65open Bool
66
67open Relations
68
69open Nat
70
71open List
72
73open Hints_declaration
74
75open Core_notation
76
77open Pts
78
79open Logic
80
81open Types
82
83open Coqlib
84
85open Values
86
87open Events
88
89type transrel =
90| Mk_transrel
91
92val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
93
94val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
95
96val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
97
98val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
99
100val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
101
102val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
103
104type genv
105
106type state
107
108type step = __
109
110val transrel_inv_rect_Type4 :
111  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
112
113val transrel_inv_rect_Type3 :
114  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
115
116val transrel_inv_rect_Type2 :
117  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
118
119val transrel_inv_rect_Type1 :
120  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
121
122val transrel_inv_rect_Type0 :
123  transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
124
125val transrel_jmdiscr : transrel -> transrel -> __
126
127type program_behavior =
128| Terminates of Events.trace * Integers.int
129| Diverges of Events.trace
130| Reacts of Events.traceinf
131| Goes_wrong of Events.trace
132
133val program_behavior_rect_Type4 :
134  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
135  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
136  'a1
137
138val program_behavior_rect_Type5 :
139  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
140  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
141  'a1
142
143val program_behavior_rect_Type3 :
144  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
145  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
146  'a1
147
148val program_behavior_rect_Type2 :
149  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
150  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
151  'a1
152
153val program_behavior_rect_Type1 :
154  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
155  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
156  'a1
157
158val program_behavior_rect_Type0 :
159  (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
160  (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
161  'a1
162
163val program_behavior_inv_rect_Type4 :
164  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
165  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
166  (Events.trace -> __ -> 'a1) -> 'a1
167
168val program_behavior_inv_rect_Type3 :
169  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
170  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
171  (Events.trace -> __ -> 'a1) -> 'a1
172
173val program_behavior_inv_rect_Type2 :
174  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
175  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
176  (Events.trace -> __ -> 'a1) -> 'a1
177
178val program_behavior_inv_rect_Type1 :
179  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
180  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
181  (Events.trace -> __ -> 'a1) -> 'a1
182
183val program_behavior_inv_rect_Type0 :
184  program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
185  (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
186  (Events.trace -> __ -> 'a1) -> 'a1
187
188val program_behavior_discr : program_behavior -> program_behavior -> __
189
190val program_behavior_jmdiscr : program_behavior -> program_behavior -> __
191
192type semantics = { trans : transrel; ge : __ }
193
194val semantics_rect_Type4 :
195  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
196
197val semantics_rect_Type5 :
198  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
199
200val semantics_rect_Type3 :
201  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
202
203val semantics_rect_Type2 :
204  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
205
206val semantics_rect_Type1 :
207  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
208
209val semantics_rect_Type0 :
210  (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
211
212val trans : semantics -> transrel
213
214type initial = __
215
216type final = __
217
218val ge : semantics -> __
219
220val semantics_inv_rect_Type4 :
221  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
222
223val semantics_inv_rect_Type3 :
224  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
225
226val semantics_inv_rect_Type2 :
227  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
228
229val semantics_inv_rect_Type1 :
230  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
231
232val semantics_inv_rect_Type0 :
233  semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
234
235val semantics_jmdiscr : semantics -> semantics -> __
236
237type related_semantics = { sem1 : semantics; sem2 : semantics }
238
239val related_semantics_rect_Type4 :
240  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
241  'a1
242
243val related_semantics_rect_Type5 :
244  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
245  'a1
246
247val related_semantics_rect_Type3 :
248  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
249  'a1
250
251val related_semantics_rect_Type2 :
252  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
253  'a1
254
255val related_semantics_rect_Type1 :
256  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
257  'a1
258
259val related_semantics_rect_Type0 :
260  (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
261  'a1
262
263val sem1 : related_semantics -> semantics
264
265val sem2 : related_semantics -> semantics
266
267type match_states = __
268
269val related_semantics_inv_rect_Type4 :
270  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
271  'a1) -> 'a1
272
273val related_semantics_inv_rect_Type3 :
274  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
275  'a1) -> 'a1
276
277val related_semantics_inv_rect_Type2 :
278  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
279  'a1) -> 'a1
280
281val related_semantics_inv_rect_Type1 :
282  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
283  'a1) -> 'a1
284
285val related_semantics_inv_rect_Type0 :
286  related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
287  'a1) -> 'a1
288
289val related_semantics_jmdiscr : related_semantics -> related_semantics -> __
290
291type order_sim =
292  related_semantics
293  (* singleton inductive, whose constructor was mk_order_sim *)
294
295val order_sim_rect_Type4 :
296  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
297
298val order_sim_rect_Type5 :
299  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
300
301val order_sim_rect_Type3 :
302  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
303
304val order_sim_rect_Type2 :
305  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
306
307val order_sim_rect_Type1 :
308  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
309
310val order_sim_rect_Type0 :
311  (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
312
313val sem : order_sim -> related_semantics
314
315type order = __
316
317val order_sim_inv_rect_Type4 :
318  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
319
320val order_sim_inv_rect_Type3 :
321  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
322
323val order_sim_inv_rect_Type2 :
324  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
325
326val order_sim_inv_rect_Type1 :
327  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
328
329val order_sim_inv_rect_Type0 :
330  order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
331
332val order_sim_jmdiscr : order_sim -> order_sim -> __
333
Note: See TracBrowser for help on using the repository browser.