source: driver/extracted/cminor_syntax.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: 19.3 KB
Line 
1open Preamble
2
3open FrontEndVal
4
5open Hide
6
7open ByteValues
8
9open GenMem
10
11open FrontEndMem
12
13open Proper
14
15open PositiveMap
16
17open Deqsets
18
19open Extralib
20
21open Lists
22
23open Identifiers
24
25open Integers
26
27open AST
28
29open Division
30
31open Exp
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
49open ErrorMessages
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open PreIdentifiers
60
61open Errors
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open CostLabel
96
97type expr =
98| Id of AST.typ * AST.ident
99| Cst of AST.typ * FrontEndOps.constant
100| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
101| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
102   expr * expr
103| Mem of AST.typ * expr
104| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
105| Ecost of AST.typ * CostLabel.costlabel * expr
106
107val expr_rect_Type4 :
108  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
109  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
110  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
111  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
112  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
113  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
114  'a1) -> AST.typ -> expr -> 'a1
115
116val expr_rect_Type3 :
117  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
118  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
119  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
120  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
121  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
122  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
123  'a1) -> AST.typ -> expr -> 'a1
124
125val expr_rect_Type2 :
126  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
127  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
128  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
129  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
130  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
131  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
132  'a1) -> AST.typ -> expr -> 'a1
133
134val expr_rect_Type1 :
135  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
136  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
137  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
138  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
139  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
140  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
141  'a1) -> AST.typ -> expr -> 'a1
142
143val expr_rect_Type0 :
144  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
145  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
146  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
147  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
148  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
149  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
150  'a1) -> AST.typ -> expr -> 'a1
151
152val expr_inv_rect_Type4 :
153  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
154  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
155  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
156  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
157  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
158  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
159  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
160  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
161  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
162  'a1) -> 'a1
163
164val expr_inv_rect_Type3 :
165  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
166  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
167  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
168  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
169  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
170  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
171  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
172  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
173  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
174  'a1) -> 'a1
175
176val expr_inv_rect_Type2 :
177  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
178  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
179  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
180  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
181  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
182  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
183  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
184  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
185  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
186  'a1) -> 'a1
187
188val expr_inv_rect_Type1 :
189  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
190  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
191  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
192  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
193  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
194  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
195  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
196  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
197  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
198  'a1) -> 'a1
199
200val expr_inv_rect_Type0 :
201  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
202  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
203  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
204  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
205  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
206  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
207  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
208  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
209  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
210  'a1) -> 'a1
211
212val expr_jmdiscr : AST.typ -> expr -> expr -> __
213
214type stmt =
215| St_skip
216| St_assign of AST.typ * AST.ident * expr
217| St_store of AST.typ * expr * expr
218| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
219   * (AST.typ, expr) Types.dPair List.list
220| St_seq of stmt * stmt
221| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
222| St_return of (AST.typ, expr) Types.dPair Types.option
223| St_label of PreIdentifiers.identifier * stmt
224| St_goto of PreIdentifiers.identifier
225| St_cost of CostLabel.costlabel * stmt
226
227val stmt_rect_Type4 :
228  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
229  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
230  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
231  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
232  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
233  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
234  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
235  -> 'a1) -> stmt -> 'a1
236
237val stmt_rect_Type3 :
238  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
239  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
240  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
241  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
242  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
243  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
244  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
245  -> 'a1) -> stmt -> 'a1
246
247val stmt_rect_Type2 :
248  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
249  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
250  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
251  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
252  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
253  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
254  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
255  -> 'a1) -> stmt -> 'a1
256
257val stmt_rect_Type1 :
258  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
259  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
260  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
261  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
262  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
263  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
264  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
265  -> 'a1) -> stmt -> 'a1
266
267val stmt_rect_Type0 :
268  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
269  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
270  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
271  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
272  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
273  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
274  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
275  -> 'a1) -> stmt -> 'a1
276
277val stmt_inv_rect_Type4 :
278  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
279  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
280  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
281  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
282  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
283  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
284  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
285  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
286  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
287
288val stmt_inv_rect_Type3 :
289  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
290  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
291  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
292  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
293  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
294  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
295  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
296  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
297  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
298
299val stmt_inv_rect_Type2 :
300  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
301  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
302  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
303  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
304  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
305  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
306  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
307  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
308  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
309
310val stmt_inv_rect_Type1 :
311  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
312  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
313  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
314  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
315  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
316  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
317  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
318  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
319  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
320
321val stmt_inv_rect_Type0 :
322  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
323  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
324  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
325  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
326  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
327  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
328  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
329  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
330  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
331
332val stmt_discr : stmt -> stmt -> __
333
334val stmt_jmdiscr : stmt -> stmt -> __
335
336val labels_of : stmt -> PreIdentifiers.identifier List.list
337
338val cminor_stmt_inv_rect_Type4 :
339  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
340  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
341
342val cminor_stmt_inv_rect_Type5 :
343  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
344  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
345
346val cminor_stmt_inv_rect_Type3 :
347  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
348  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
349
350val cminor_stmt_inv_rect_Type2 :
351  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
352  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
353
354val cminor_stmt_inv_rect_Type1 :
355  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
356  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
357
358val cminor_stmt_inv_rect_Type0 :
359  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
360  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
361
362val cminor_stmt_inv_inv_rect_Type4 :
363  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
364  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
365  -> 'a1
366
367val cminor_stmt_inv_inv_rect_Type3 :
368  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
369  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
370  -> 'a1
371
372val cminor_stmt_inv_inv_rect_Type2 :
373  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
374  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
375  -> 'a1
376
377val cminor_stmt_inv_inv_rect_Type1 :
378  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
379  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
380  -> 'a1
381
382val cminor_stmt_inv_inv_rect_Type0 :
383  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
384  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
385  -> 'a1
386
387val cminor_stmt_inv_discr :
388  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
389  List.list -> AST.typ Types.option -> stmt -> __
390
391val cminor_stmt_inv_jmdiscr :
392  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
393  List.list -> AST.typ Types.option -> stmt -> __
394
395type internal_function = { f_return : AST.typ Types.option;
396                           f_params : (AST.ident, AST.typ) Types.prod
397                                      List.list;
398                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
399                           f_stacksize : Nat.nat; f_body : stmt }
400
401val internal_function_rect_Type4 :
402  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
403  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
404  'a1) -> internal_function -> 'a1
405
406val internal_function_rect_Type5 :
407  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
408  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
409  'a1) -> internal_function -> 'a1
410
411val internal_function_rect_Type3 :
412  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
413  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
414  'a1) -> internal_function -> 'a1
415
416val internal_function_rect_Type2 :
417  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
418  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
419  'a1) -> internal_function -> 'a1
420
421val internal_function_rect_Type1 :
422  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
423  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
424  'a1) -> internal_function -> 'a1
425
426val internal_function_rect_Type0 :
427  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
428  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
429  'a1) -> internal_function -> 'a1
430
431val f_return : internal_function -> AST.typ Types.option
432
433val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
434
435val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
436
437val f_stacksize : internal_function -> Nat.nat
438
439val f_body : internal_function -> stmt
440
441val internal_function_inv_rect_Type4 :
442  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
443  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
444  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
445
446val internal_function_inv_rect_Type3 :
447  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
448  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
449  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
450
451val internal_function_inv_rect_Type2 :
452  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
453  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
454  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
455
456val internal_function_inv_rect_Type1 :
457  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
458  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
459  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
460
461val internal_function_inv_rect_Type0 :
462  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
463  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
464  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
465
466val internal_function_jmdiscr : internal_function -> internal_function -> __
467
468type cminor_program =
469  (internal_function AST.fundef, AST.init_data List.list) AST.program
470
471type cminor_noinit_program =
472  (internal_function AST.fundef, Nat.nat) AST.program
473
Note: See TracBrowser for help on using the repository browser.