source: extracted/cminor_syntax.mli @ 2746

Last change on this file since 2746 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: 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 BitVectorTrie
96
97open CostLabel
98
99type expr =
100| Id of AST.typ * AST.ident
101| Cst of AST.typ * FrontEndOps.constant
102| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
103| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
104   expr * expr
105| Mem of AST.typ * expr
106| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
107| Ecost of AST.typ * CostLabel.costlabel * expr
108
109val expr_rect_Type4 :
110  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
111  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
112  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
113  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
114  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
115  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
116  'a1) -> AST.typ -> expr -> 'a1
117
118val expr_rect_Type3 :
119  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
120  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
121  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
122  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
123  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
124  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
125  'a1) -> AST.typ -> expr -> 'a1
126
127val expr_rect_Type2 :
128  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
129  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
130  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
131  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
132  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
133  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
134  'a1) -> AST.typ -> expr -> 'a1
135
136val expr_rect_Type1 :
137  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
138  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
139  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
140  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
141  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
142  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
143  'a1) -> AST.typ -> expr -> 'a1
144
145val expr_rect_Type0 :
146  (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
147  -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
148  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
149  expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
150  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
151  'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
152  'a1) -> AST.typ -> expr -> 'a1
153
154val expr_inv_rect_Type4 :
155  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
156  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
157  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
158  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
159  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
160  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
161  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
162  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
163  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
164  'a1) -> 'a1
165
166val expr_inv_rect_Type3 :
167  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
168  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
169  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
170  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
171  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
172  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
173  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
174  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
175  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
176  'a1) -> 'a1
177
178val expr_inv_rect_Type2 :
179  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
180  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
181  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
182  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
183  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
184  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
185  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
186  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
187  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
188  'a1) -> 'a1
189
190val expr_inv_rect_Type1 :
191  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
192  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
193  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
194  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
195  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
196  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
197  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
198  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
199  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
200  'a1) -> 'a1
201
202val expr_inv_rect_Type0 :
203  AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
204  FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
205  FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
206  'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
207  expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
208  -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
209  (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
210  __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
211  (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
212  'a1) -> 'a1
213
214val expr_jmdiscr : AST.typ -> expr -> expr -> __
215
216type expr_vars = __
217
218type stmt =
219| St_skip
220| St_assign of AST.typ * AST.ident * expr
221| St_store of AST.typ * expr * expr
222| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
223   * (AST.typ, expr) Types.dPair List.list
224| St_seq of stmt * stmt
225| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
226| St_return of (AST.typ, expr) Types.dPair Types.option
227| St_label of PreIdentifiers.identifier * stmt
228| St_goto of PreIdentifiers.identifier
229| St_cost of CostLabel.costlabel * stmt
230
231val stmt_rect_Type4 :
232  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
233  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
234  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
235  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
236  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
237  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
238  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
239  -> 'a1) -> stmt -> 'a1
240
241val stmt_rect_Type3 :
242  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
243  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
244  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
245  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
246  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
247  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
248  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
249  -> 'a1) -> stmt -> 'a1
250
251val stmt_rect_Type2 :
252  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
253  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
254  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
255  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
256  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
257  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
258  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
259  -> 'a1) -> stmt -> 'a1
260
261val stmt_rect_Type1 :
262  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
263  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
264  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
265  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
266  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
267  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
268  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
269  -> 'a1) -> stmt -> 'a1
270
271val stmt_rect_Type0 :
272  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
273  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
274  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
275  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
276  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
277  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
278  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
279  -> 'a1) -> stmt -> 'a1
280
281val stmt_inv_rect_Type4 :
282  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
283  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
284  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
285  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
286  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
287  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
288  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
289  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
290  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
291
292val stmt_inv_rect_Type3 :
293  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
294  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
295  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
296  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
297  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
298  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
299  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
300  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
301  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
302
303val stmt_inv_rect_Type2 :
304  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
305  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
306  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
307  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
308  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
309  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
310  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
311  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
312  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
313
314val stmt_inv_rect_Type1 :
315  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
316  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
317  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
318  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
319  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
320  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
321  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
322  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
323  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
324
325val stmt_inv_rect_Type0 :
326  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
327  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
328  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
329  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
330  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
331  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
332  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
333  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
334  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
335
336val stmt_discr : stmt -> stmt -> __
337
338val stmt_jmdiscr : stmt -> stmt -> __
339
340type stmt_P = __
341
342val labels_of : stmt -> PreIdentifiers.identifier List.list
343
344val cminor_stmt_inv_rect_Type4 :
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_Type5 :
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_Type3 :
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_Type2 :
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_Type1 :
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_rect_Type0 :
365  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
366  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
367
368val cminor_stmt_inv_inv_rect_Type4 :
369  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
370  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
371  -> 'a1
372
373val cminor_stmt_inv_inv_rect_Type3 :
374  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
375  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
376  -> 'a1
377
378val cminor_stmt_inv_inv_rect_Type2 :
379  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
380  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
381  -> 'a1
382
383val cminor_stmt_inv_inv_rect_Type1 :
384  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
385  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
386  -> 'a1
387
388val cminor_stmt_inv_inv_rect_Type0 :
389  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
390  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
391  -> 'a1
392
393val cminor_stmt_inv_discr :
394  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
395  List.list -> AST.typ Types.option -> stmt -> __
396
397val cminor_stmt_inv_jmdiscr :
398  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
399  List.list -> AST.typ Types.option -> stmt -> __
400
401type internal_function = { f_return : AST.typ Types.option;
402                           f_params : (AST.ident, AST.typ) Types.prod
403                                      List.list;
404                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
405                           f_stacksize : Nat.nat; f_body : stmt }
406
407val internal_function_rect_Type4 :
408  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
409  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
410  'a1) -> internal_function -> 'a1
411
412val internal_function_rect_Type5 :
413  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
414  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
415  'a1) -> internal_function -> 'a1
416
417val internal_function_rect_Type3 :
418  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
419  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
420  'a1) -> internal_function -> 'a1
421
422val internal_function_rect_Type2 :
423  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
424  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
425  'a1) -> internal_function -> 'a1
426
427val internal_function_rect_Type1 :
428  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
429  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
430  'a1) -> internal_function -> 'a1
431
432val internal_function_rect_Type0 :
433  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
434  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
435  'a1) -> internal_function -> 'a1
436
437val f_return : internal_function -> AST.typ Types.option
438
439val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
440
441val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
442
443val f_stacksize : internal_function -> Nat.nat
444
445val f_body : internal_function -> stmt
446
447val internal_function_inv_rect_Type4 :
448  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
449  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
450  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
451
452val internal_function_inv_rect_Type3 :
453  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
454  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
455  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
456
457val internal_function_inv_rect_Type2 :
458  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
459  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
460  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
461
462val internal_function_inv_rect_Type1 :
463  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
464  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
465  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
466
467val internal_function_inv_rect_Type0 :
468  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
469  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
470  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
471
472val internal_function_jmdiscr : internal_function -> internal_function -> __
473
474type cminor_program =
475  (internal_function AST.fundef, AST.init_data List.list) AST.program
476
477type cminor_noinit_program =
478  (internal_function AST.fundef, Nat.nat) AST.program
479
Note: See TracBrowser for help on using the repository browser.