source: extracted/smallstep.mli @ 2773

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