79 open Hints_declaration
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 *
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
107 val 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
116 val 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
125 val 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
134 val 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
143 val 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
152 val 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) -> __ -> __ ->
164 val 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) -> __ -> __ ->
176 val 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) -> __ -> __ ->
188 val 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) -> __ -> __ ->
200 val 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) -> __ -> __ ->
212 val expr_jmdiscr : AST.typ -> expr -> expr -> __
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
227 val 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
237 val 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
247 val 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
257 val 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
267 val 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
277 val 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
288 val 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
299 val 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
310 val 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
321 val 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
332 val stmt_discr : stmt -> stmt -> __
334 val stmt_jmdiscr : stmt -> stmt -> __
336 val labels_of : stmt -> PreIdentifiers.identifier List.list
338 val 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
342 val 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
346 val 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
350 val 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
354 val 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
358 val 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
362 val 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)
367 val 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)
372 val 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)
377 val 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)
382 val 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)
387 val cminor_stmt_inv_discr :
388 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
389 List.list -> AST.typ Types.option -> stmt -> __
391 val cminor_stmt_inv_jmdiscr :
392 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
393 List.list -> AST.typ Types.option -> stmt -> __
395 type internal_function = { f_return : AST.typ Types.option;
396 f_params : (AST.ident, AST.typ) Types.prod
398 f_vars : (AST.ident, AST.typ) Types.prod List.list;
399 f_stacksize : Nat.nat; f_body : stmt }
401 val 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
406 val 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
411 val 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
416 val 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
421 val 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
426 val 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
431 val f_return : internal_function -> AST.typ Types.option
433 val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
435 val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
437 val f_stacksize : internal_function -> Nat.nat
439 val f_body : internal_function -> stmt
441 val 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
446 val 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
451 val 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
456 val 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
461 val 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
466 val internal_function_jmdiscr : internal_function -> internal_function -> __
468 type cminor_program =
469 (internal_function AST.fundef, AST.init_data List.list) AST.program
471 type cminor_noinit_program =
472 (internal_function AST.fundef, Nat.nat) AST.program