106 | St_skip of Graphs.label
107 | St_cost of CostLabel.costlabel * Graphs.label
108 | St_const of AST.typ * Registers.register * FrontEndOps.constant
110 | St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
111 * Registers.register * Registers.register * Graphs.label
112 | St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
113 * Registers.register * Registers.register * Registers.register
115 | St_load of AST.typ * Registers.register * Registers.register * Graphs.label
116 | St_store of AST.typ * Registers.register * Registers.register
118 | St_call_id of AST.ident * Registers.register List.list
119 * Registers.register Types.option * Graphs.label
120 | St_call_ptr of Registers.register * Registers.register List.list
121 * Registers.register Types.option * Graphs.label
122 | St_cond of Registers.register * Graphs.label * Graphs.label
125 val statement_rect_Type4 :
126 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
127 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
128 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
129 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
130 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
131 Registers.register -> Registers.register -> Registers.register ->
132 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
133 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
134 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
135 (AST.ident -> Registers.register List.list -> Registers.register
136 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
137 Registers.register List.list -> Registers.register Types.option ->
138 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
139 -> 'a1) -> 'a1 -> statement -> 'a1
141 val statement_rect_Type5 :
142 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
143 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
144 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
145 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
146 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
147 Registers.register -> Registers.register -> Registers.register ->
148 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
149 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
150 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
151 (AST.ident -> Registers.register List.list -> Registers.register
152 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
153 Registers.register List.list -> Registers.register Types.option ->
154 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
155 -> 'a1) -> 'a1 -> statement -> 'a1
157 val statement_rect_Type3 :
158 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
159 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
160 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
161 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
162 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
163 Registers.register -> Registers.register -> Registers.register ->
164 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
165 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
166 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
167 (AST.ident -> Registers.register List.list -> Registers.register
168 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
169 Registers.register List.list -> Registers.register Types.option ->
170 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
171 -> 'a1) -> 'a1 -> statement -> 'a1
173 val statement_rect_Type2 :
174 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
175 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
176 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
177 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
178 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
179 Registers.register -> Registers.register -> Registers.register ->
180 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
181 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
182 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
183 (AST.ident -> Registers.register List.list -> Registers.register
184 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
185 Registers.register List.list -> Registers.register Types.option ->
186 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
187 -> 'a1) -> 'a1 -> statement -> 'a1
189 val statement_rect_Type1 :
190 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
191 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
192 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
193 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
194 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
195 Registers.register -> Registers.register -> Registers.register ->
196 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
197 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
198 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
199 (AST.ident -> Registers.register List.list -> Registers.register
200 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
201 Registers.register List.list -> Registers.register Types.option ->
202 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
203 -> 'a1) -> 'a1 -> statement -> 'a1
205 val statement_rect_Type0 :
206 (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
207 (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
208 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
209 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
210 (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
211 Registers.register -> Registers.register -> Registers.register ->
212 Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
213 Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
214 Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
215 (AST.ident -> Registers.register List.list -> Registers.register
216 Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
217 Registers.register List.list -> Registers.register Types.option ->
218 Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
219 -> 'a1) -> 'a1 -> statement -> 'a1
221 val statement_inv_rect_Type4 :
222 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
223 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
224 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
225 -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
226 -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
227 FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
228 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
229 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
230 (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
231 -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
232 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
233 Registers.register List.list -> Registers.register Types.option ->
234 Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
235 Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
237 val statement_inv_rect_Type3 :
238 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
239 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
240 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
241 -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
242 -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
243 FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
244 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
245 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
246 (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
247 -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
248 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
249 Registers.register List.list -> Registers.register Types.option ->
250 Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
251 Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
253 val statement_inv_rect_Type2 :
254 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
255 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
256 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
257 -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
258 -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
259 FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
260 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
261 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
262 (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
263 -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
264 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
265 Registers.register List.list -> Registers.register Types.option ->
266 Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
267 Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
269 val statement_inv_rect_Type1 :
270 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
271 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
272 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
273 -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
274 -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
275 FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
276 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
277 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
278 (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
279 -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
280 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
281 Registers.register List.list -> Registers.register Types.option ->
282 Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
283 Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
285 val statement_inv_rect_Type0 :
286 statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
287 Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
288 FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
289 -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
290 -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
291 FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
292 Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
293 Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
294 (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
295 -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
296 Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
297 Registers.register List.list -> Registers.register Types.option ->
298 Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
299 Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
301 val statement_jmdiscr : statement -> statement -> __
303 type internal_function = { f_labgen : Identifiers.universe;
304 f_reggen : Identifiers.universe;
305 f_result : (Registers.register, AST.typ)
306 Types.prod Types.option;
307 f_params : (Registers.register, AST.typ)
308 Types.prod List.list;
309 f_locals : (Registers.register, AST.typ)
310 Types.prod List.list;
311 f_stacksize : Nat.nat;
312 f_graph : statement Graphs.graph;
313 f_entry : Graphs.label Types.sig0;
314 f_exit : Graphs.label Types.sig0 }
316 val internal_function_rect_Type4 :
317 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
318 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
319 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
320 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
321 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
323 val internal_function_rect_Type5 :
324 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
325 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
326 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
327 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
328 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
330 val internal_function_rect_Type3 :
331 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
332 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
333 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
334 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
335 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
337 val internal_function_rect_Type2 :
338 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
339 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
340 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
341 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
342 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
344 val internal_function_rect_Type1 :
345 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
346 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
347 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
348 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
349 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
351 val internal_function_rect_Type0 :
352 (Identifiers.universe -> Identifiers.universe -> (Registers.register,
353 AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
354 Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
355 -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
356 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1
358 val f_labgen : internal_function -> Identifiers.universe
360 val f_reggen : internal_function -> Identifiers.universe
363 internal_function -> (Registers.register, AST.typ) Types.prod Types.option
366 internal_function -> (Registers.register, AST.typ) Types.prod List.list
369 internal_function -> (Registers.register, AST.typ) Types.prod List.list
371 val f_stacksize : internal_function -> Nat.nat
373 val f_graph : internal_function -> statement Graphs.graph
375 val f_entry : internal_function -> Graphs.label Types.sig0
377 val f_exit : internal_function -> Graphs.label Types.sig0
379 val internal_function_inv_rect_Type4 :
380 internal_function -> (Identifiers.universe -> Identifiers.universe ->
381 (Registers.register, AST.typ) Types.prod Types.option ->
382 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
383 AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
384 __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
387 val internal_function_inv_rect_Type3 :
388 internal_function -> (Identifiers.universe -> Identifiers.universe ->
389 (Registers.register, AST.typ) Types.prod Types.option ->
390 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
391 AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
392 __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
395 val internal_function_inv_rect_Type2 :
396 internal_function -> (Identifiers.universe -> Identifiers.universe ->
397 (Registers.register, AST.typ) Types.prod Types.option ->
398 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
399 AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
400 __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
403 val internal_function_inv_rect_Type1 :
404 internal_function -> (Identifiers.universe -> Identifiers.universe ->
405 (Registers.register, AST.typ) Types.prod Types.option ->
406 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
407 AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
408 __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
411 val internal_function_inv_rect_Type0 :
412 internal_function -> (Identifiers.universe -> Identifiers.universe ->
413 (Registers.register, AST.typ) Types.prod Types.option ->
414 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
415 AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
416 __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ ->
419 val internal_function_jmdiscr : internal_function -> internal_function -> __
421 type rTLabs_program =
422 (internal_function AST.fundef, AST.init_data List.list) AST.program