99 open Hints_declaration
132 Joint.params -> AST.ident List.list -> Graphs.label
133 Monad.smax_def__o__monad
136 Joint.params -> AST.ident List.list -> Registers.register
137 Monad.smax_def__o__monad
140 Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
141 Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
142 Monad.smax_def__o__monad
144 val adds_graph_post :
145 Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
146 Graphs.label -> Graphs.label Monad.smax_def__o__monad
149 Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
150 Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
151 Joint.joint_internal_function
154 Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
155 Graphs.label -> Joint.joint_internal_function ->
156 Joint.joint_internal_function
159 Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
160 Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
161 Joint.joint_internal_function
163 val b_fin_adds_graph :
164 Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
165 Graphs.label -> Joint.joint_internal_function ->
166 Joint.joint_internal_function
169 Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
170 Registers.register List.list
172 val fin_step_registers :
173 Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list
175 type b_graph_translate_data = { init_ret : __; init_params : __;
176 init_stack_size : Nat.nat;
177 added_prologue : Joint.joint_seq List.list;
178 new_regs : Registers.register List.list;
179 f_step : (Graphs.label -> Joint.joint_step ->
180 Blocks.bind_step_block);
181 f_fin : (Graphs.label -> Joint.joint_fin_step
182 -> Blocks.bind_fin_block) }
184 val b_graph_translate_data_rect_Type4 :
185 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
186 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
187 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
188 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
189 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
191 val b_graph_translate_data_rect_Type5 :
192 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
193 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
194 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
195 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
196 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
198 val b_graph_translate_data_rect_Type3 :
199 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
200 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
201 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
202 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
203 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
205 val b_graph_translate_data_rect_Type2 :
206 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
207 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
208 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
209 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
210 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
212 val b_graph_translate_data_rect_Type1 :
213 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
214 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
215 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
216 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
217 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
219 val b_graph_translate_data_rect_Type0 :
220 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
221 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
222 -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
223 (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
224 -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
227 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
228 b_graph_translate_data -> __
231 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
232 b_graph_translate_data -> __
234 val init_stack_size :
235 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
236 b_graph_translate_data -> Nat.nat
239 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
240 b_graph_translate_data -> Joint.joint_seq List.list
243 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
244 b_graph_translate_data -> Registers.register List.list
247 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
248 b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
249 Blocks.bind_step_block
252 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
253 b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
254 Blocks.bind_fin_block
256 val b_graph_translate_data_inv_rect_Type4 :
257 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
258 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
259 -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
260 Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
261 Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
263 val b_graph_translate_data_inv_rect_Type3 :
264 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
265 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
266 -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
267 Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
268 Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
270 val b_graph_translate_data_inv_rect_Type2 :
271 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
272 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
273 -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
274 Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
275 Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
277 val b_graph_translate_data_inv_rect_Type1 :
278 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
279 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
280 -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
281 Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
282 Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
284 val b_graph_translate_data_inv_rect_Type0 :
285 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
286 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
287 -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
288 Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
289 Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
291 val b_graph_translate_data_jmdiscr :
292 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
293 b_graph_translate_data -> b_graph_translate_data -> __
295 type bound_b_graph_translate_data =
296 (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
298 val get_first_costlabel_next :
299 Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
300 -> (CostLabel.costlabel, __) Types.prod
302 val get_first_costlabel :
303 Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
304 -> CostLabel.costlabel
306 val not_emptyb : 'a1 List.list -> Bool.bool
308 val b_graph_translate_props_rect_Type4 :
309 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
310 b_graph_translate_data -> Joint.joint_closed_internal_function ->
311 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
312 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
313 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
315 val b_graph_translate_props_rect_Type5 :
316 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
317 b_graph_translate_data -> Joint.joint_closed_internal_function ->
318 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
319 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
320 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
322 val b_graph_translate_props_rect_Type3 :
323 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
324 b_graph_translate_data -> Joint.joint_closed_internal_function ->
325 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
326 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
327 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
329 val b_graph_translate_props_rect_Type2 :
330 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
331 b_graph_translate_data -> Joint.joint_closed_internal_function ->
332 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
333 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
334 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
336 val b_graph_translate_props_rect_Type1 :
337 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
338 b_graph_translate_data -> Joint.joint_closed_internal_function ->
339 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
340 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
341 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
343 val b_graph_translate_props_rect_Type0 :
344 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
345 b_graph_translate_data -> Joint.joint_closed_internal_function ->
346 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
347 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
348 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
350 val b_graph_translate_props_inv_rect_Type4 :
351 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
352 b_graph_translate_data -> Joint.joint_closed_internal_function ->
353 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
354 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
355 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
357 val b_graph_translate_props_inv_rect_Type3 :
358 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
359 b_graph_translate_data -> Joint.joint_closed_internal_function ->
360 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
361 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
362 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
364 val b_graph_translate_props_inv_rect_Type2 :
365 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
366 b_graph_translate_data -> Joint.joint_closed_internal_function ->
367 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
368 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
369 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
371 val b_graph_translate_props_inv_rect_Type1 :
372 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
373 b_graph_translate_data -> Joint.joint_closed_internal_function ->
374 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
375 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
376 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
378 val b_graph_translate_props_inv_rect_Type0 :
379 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
380 b_graph_translate_data -> Joint.joint_closed_internal_function ->
381 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
382 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
383 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
385 val b_graph_translate_props_jmdiscr :
386 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
387 b_graph_translate_data -> Joint.joint_closed_internal_function ->
388 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
389 List.list) -> (Graphs.label -> Registers.register List.list) -> __
391 val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
394 AST.ident List.list -> Joint.params -> Joint.joint_internal_function -> __
395 -> Joint.joint_internal_function
397 val b_graph_translate :
398 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
399 bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
400 Joint.joint_closed_internal_function Types.sig0
402 val b_graph_transform_program :
403 Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
404 Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
405 Joint.joint_program -> Joint.joint_program
407 val added_registers :
408 Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
409 -> (Graphs.label -> Registers.register List.list) -> Registers.register