source: extracted/cminor_syntax.mli @ 2649

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

...

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 Arithmetic
32
33open Extranat
34
35open Vector
36
37open FoldStuff
38
39open BitVector
40
41open Z
42
43open BitVectorZ
44
45open Pointers
46
47open ErrorMessages
48
49open Option
50
51open Setoids
52
53open Monad
54
55open Positive
56
57open PreIdentifiers
58
59open Errors
60
61open Div_and_mod
62
63open Jmeq
64
65open Russell
66
67open Util
68
69open Bool
70
71open Relations
72
73open Nat
74
75open List
76
77open Hints_declaration
78
79open Core_notation
80
81open Pts
82
83open Logic
84
85open Types
86
87open Coqlib
88
89open Values
90
91open FrontEndOps
92
93open CostLabel
94
95type expr =
96| Id of AST.typ * AST.ident
97| Cst of AST.typ * FrontEndOps.constant
98| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
99| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
100   expr * expr
101| Mem of AST.typ * expr
102| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
103| Ecost of AST.typ * CostLabel.costlabel * expr
104
105val expr_rect_Type4 :
106  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
107  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
108  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
109  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
110  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
111  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
112  'a1) -> AST.typ -> expr -> 'a1
113
114val expr_rect_Type3 :
115  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
116  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
117  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
118  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
119  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
120  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
121  'a1) -> AST.typ -> expr -> 'a1
122
123val expr_rect_Type2 :
124  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
125  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
126  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
127  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
128  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
129  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
130  'a1) -> AST.typ -> expr -> 'a1
131
132val expr_rect_Type1 :
133  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
134  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
135  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
136  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
137  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
138  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
139  'a1) -> AST.typ -> expr -> 'a1
140
141val expr_rect_Type0 :
142  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
143  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
144  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
145  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
146  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
147  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
148  'a1) -> AST.typ -> expr -> 'a1
149
150val expr_inv_rect_Type4 :
151  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
152  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
153  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
154  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
155  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
156  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
157  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
158  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
159  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
160  'a1) -> 'a1
161
162val expr_inv_rect_Type3 :
163  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
164  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
165  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
166  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
167  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
168  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
169  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
170  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
171  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
172  'a1) -> 'a1
173
174val expr_inv_rect_Type2 :
175  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
176  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
177  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
178  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
179  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
180  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
181  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
182  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
183  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
184  'a1) -> 'a1
185
186val expr_inv_rect_Type1 :
187  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
188  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
189  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
190  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
191  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
192  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
193  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
194  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
195  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
196  'a1) -> 'a1
197
198val expr_inv_rect_Type0 :
199  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
200  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
201  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
202  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
203  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
204  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
205  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
206  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
207  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
208  'a1) -> 'a1
209
210val expr_jmdiscr : AST.typ -> expr -> expr -> __
211
212type expr_vars = __
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
336type stmt_P = __
337
338val labels_of : stmt -> PreIdentifiers.identifier List.list
339
340val cminor_stmt_inv_rect_Type4 :
341  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
342  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
343
344val cminor_stmt_inv_rect_Type5 :
345  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
346  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
347
348val cminor_stmt_inv_rect_Type3 :
349  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
350  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
351
352val cminor_stmt_inv_rect_Type2 :
353  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
354  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
355
356val cminor_stmt_inv_rect_Type1 :
357  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
358  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
359
360val cminor_stmt_inv_rect_Type0 :
361  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
362  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
363
364val cminor_stmt_inv_inv_rect_Type4 :
365  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
366  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
367  -> 'a1
368
369val cminor_stmt_inv_inv_rect_Type3 :
370  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
371  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
372  -> 'a1
373
374val cminor_stmt_inv_inv_rect_Type2 :
375  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
376  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
377  -> 'a1
378
379val cminor_stmt_inv_inv_rect_Type1 :
380  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
381  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
382  -> 'a1
383
384val cminor_stmt_inv_inv_rect_Type0 :
385  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
386  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
387  -> 'a1
388
389val cminor_stmt_inv_discr :
390  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
391  List.list -> AST.typ Types.option -> stmt -> __
392
393val cminor_stmt_inv_jmdiscr :
394  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
395  List.list -> AST.typ Types.option -> stmt -> __
396
397type internal_function = { f_return : AST.typ Types.option;
398                           f_params : (AST.ident, AST.typ) Types.prod
399                                      List.list;
400                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
401                           f_stacksize : Nat.nat; f_body : stmt }
402
403val internal_function_rect_Type4 :
404  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
405  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
406  'a1) -> internal_function -> 'a1
407
408val internal_function_rect_Type5 :
409  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
410  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
411  'a1) -> internal_function -> 'a1
412
413val internal_function_rect_Type3 :
414  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
415  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
416  'a1) -> internal_function -> 'a1
417
418val internal_function_rect_Type2 :
419  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
420  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
421  'a1) -> internal_function -> 'a1
422
423val internal_function_rect_Type1 :
424  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
425  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
426  'a1) -> internal_function -> 'a1
427
428val internal_function_rect_Type0 :
429  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
430  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
431  'a1) -> internal_function -> 'a1
432
433val f_return : internal_function -> AST.typ Types.option
434
435val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
436
437val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
438
439val f_stacksize : internal_function -> Nat.nat
440
441val f_body : internal_function -> stmt
442
443val internal_function_inv_rect_Type4 :
444  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
445  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
446  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
447
448val internal_function_inv_rect_Type3 :
449  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
450  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
451  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
452
453val internal_function_inv_rect_Type2 :
454  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
455  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
456  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
457
458val internal_function_inv_rect_Type1 :
459  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
460  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
461  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
462
463val internal_function_inv_rect_Type0 :
464  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
465  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
466  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
467
468val internal_function_jmdiscr : internal_function -> internal_function -> __
469
470type cminor_program =
471  (internal_function AST.fundef, AST.init_data List.list) AST.program
472
473type cminor_noinit_program =
474  (internal_function AST.fundef, Nat.nat) AST.program
475
Note: See TracBrowser for help on using the repository browser.