source: extracted/cminor_syntax.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 Floats
26
27open Integers
28
29open AST
30
31open Division
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 Option
50
51open Setoids
52
53open Monad
54
55open Positive
56
57open Char
58
59open String
60
61open PreIdentifiers
62
63open Errors
64
65open Div_and_mod
66
67open Jmeq
68
69open Russell
70
71open Util
72
73open Bool
74
75open Relations
76
77open Nat
78
79open List
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Types
90
91open Coqlib
92
93open Values
94
95open FrontEndOps
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
218val label : String.string
219
220type stmt =
221| St_skip
222| St_assign of AST.typ * AST.ident * expr
223| St_store of AST.typ * expr * expr
224| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
225   * (AST.typ, expr) Types.dPair List.list
226| St_seq of stmt * stmt
227| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
228| St_return of (AST.typ, expr) Types.dPair Types.option
229| St_label of PreIdentifiers.identifier * stmt
230| St_goto of PreIdentifiers.identifier
231| St_cost of CostLabel.costlabel * stmt
232
233val stmt_rect_Type4 :
234  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
235  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
236  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
237  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
238  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
239  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
240  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
241  -> 'a1) -> stmt -> 'a1
242
243val stmt_rect_Type3 :
244  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
245  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
246  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
247  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
248  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
249  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
250  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
251  -> 'a1) -> stmt -> 'a1
252
253val stmt_rect_Type2 :
254  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
255  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
256  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
257  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
258  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
259  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
260  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
261  -> 'a1) -> stmt -> 'a1
262
263val stmt_rect_Type1 :
264  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
265  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
266  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
267  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
268  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
269  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
270  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
271  -> 'a1) -> stmt -> 'a1
272
273val stmt_rect_Type0 :
274  'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
275  'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
276  expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
277  -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
278  'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
279  (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
280  (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
281  -> 'a1) -> stmt -> 'a1
282
283val stmt_inv_rect_Type4 :
284  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
285  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
286  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
287  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
288  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
289  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
290  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
291  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
292  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
293
294val stmt_inv_rect_Type3 :
295  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
296  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
297  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
298  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
299  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
300  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
301  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
302  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
303  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
304
305val stmt_inv_rect_Type2 :
306  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
307  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
308  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
309  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
310  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
311  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
312  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
313  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
314  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
315
316val stmt_inv_rect_Type1 :
317  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
318  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
319  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
320  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
321  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
322  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
323  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
324  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
325  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
326
327val stmt_inv_rect_Type0 :
328  stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
329  (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
330  Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
331  -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
332  (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
333  (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
334  __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
335  'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
336  stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
337
338val stmt_discr : stmt -> stmt -> __
339
340val stmt_jmdiscr : stmt -> stmt -> __
341
342type stmt_P = __
343
344val labels_of : stmt -> PreIdentifiers.identifier List.list
345
346val cminor_stmt_inv_rect_Type4 :
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_Type5 :
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_Type3 :
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_Type2 :
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_rect_Type1 :
363  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
364  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
365
366val cminor_stmt_inv_rect_Type0 :
367  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
368  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
369
370val cminor_stmt_inv_inv_rect_Type4 :
371  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
372  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
373  -> 'a1
374
375val cminor_stmt_inv_inv_rect_Type3 :
376  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
377  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
378  -> 'a1
379
380val cminor_stmt_inv_inv_rect_Type2 :
381  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
382  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
383  -> 'a1
384
385val cminor_stmt_inv_inv_rect_Type1 :
386  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
387  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
388  -> 'a1
389
390val cminor_stmt_inv_inv_rect_Type0 :
391  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
392  List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
393  -> 'a1
394
395val cminor_stmt_inv_discr :
396  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
397  List.list -> AST.typ Types.option -> stmt -> __
398
399val cminor_stmt_inv_jmdiscr :
400  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
401  List.list -> AST.typ Types.option -> stmt -> __
402
403type internal_function = { f_return : AST.typ Types.option;
404                           f_params : (AST.ident, AST.typ) Types.prod
405                                      List.list;
406                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
407                           f_stacksize : Nat.nat; f_body : stmt }
408
409val internal_function_rect_Type4 :
410  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
411  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
412  'a1) -> internal_function -> 'a1
413
414val internal_function_rect_Type5 :
415  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
416  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
417  'a1) -> internal_function -> 'a1
418
419val internal_function_rect_Type3 :
420  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
421  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
422  'a1) -> internal_function -> 'a1
423
424val internal_function_rect_Type2 :
425  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
426  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
427  'a1) -> internal_function -> 'a1
428
429val internal_function_rect_Type1 :
430  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
431  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
432  'a1) -> internal_function -> 'a1
433
434val internal_function_rect_Type0 :
435  (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
436  (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
437  'a1) -> internal_function -> 'a1
438
439val f_return : internal_function -> AST.typ Types.option
440
441val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
442
443val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
444
445val f_stacksize : internal_function -> Nat.nat
446
447val f_body : internal_function -> stmt
448
449val internal_function_inv_rect_Type4 :
450  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
451  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
452  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
453
454val internal_function_inv_rect_Type3 :
455  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
456  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
457  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
458
459val internal_function_inv_rect_Type2 :
460  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
461  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
462  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
463
464val internal_function_inv_rect_Type1 :
465  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
466  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
467  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
468
469val internal_function_inv_rect_Type0 :
470  internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
471  Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
472  Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
473
474val internal_function_jmdiscr : internal_function -> internal_function -> __
475
476type cminor_program =
477  (internal_function AST.fundef, AST.init_data List.list) AST.program
478
479type cminor_noinit_program =
480  (internal_function AST.fundef, Nat.nat) AST.program
481
Note: See TracBrowser for help on using the repository browser.