99 open Hints_declaration
131 (** val fresh_label :
132 Joint.params -> AST.ident List.list -> Graphs.label
133 Monad.smax_def__o__monad **)
134 let fresh_label g_pars globals =
135 Obj.magic (fun def ->
136 let { Types.fst = r; Types.snd = luniverse } =
137 Identifiers.fresh PreIdentifiers.LabelTag def.Joint.joint_if_luniverse
139 { Types.fst = (Joint.set_luniverse g_pars globals def luniverse);
142 (** val fresh_register :
143 Joint.params -> AST.ident List.list -> Registers.register
144 Monad.smax_def__o__monad **)
145 let fresh_register g_pars globals =
146 Obj.magic (fun def ->
147 let { Types.fst = r; Types.snd = runiverse } =
148 Identifiers.fresh PreIdentifiers.RegisterTag
149 def.Joint.joint_if_runiverse
151 { Types.fst = (Joint.set_runiverse g_pars globals def runiverse);
154 (** val adds_graph_pre :
155 Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
156 Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
157 Monad.smax_def__o__monad **)
158 let rec adds_graph_pre g_pars globals pre_process insts src =
160 | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) src
161 | List.Cons (i, rest) ->
162 Monad.m_bind0 (Monad.smax_def State.state_monad)
163 (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun mid ->
164 Monad.m_bind0 (Monad.smax_def State.state_monad)
165 (adds_graph_pre g_pars globals pre_process rest mid) (fun dst ->
166 Monad.m_bind0 (Monad.smax_def State.state_monad)
168 (Joint.add_graph g_pars globals src (Joint.Sequential
169 ((Joint.Step_seq (pre_process dst i)), (Obj.magic mid)))))
170 (fun x -> Monad.m_return0 (Monad.smax_def State.state_monad) dst)))
172 (** val adds_graph_post :
173 Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
174 Graphs.label -> Graphs.label Monad.smax_def__o__monad **)
175 let rec adds_graph_post g_pars globals insts dst =
177 | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) dst
178 | List.Cons (i, rest) ->
179 Monad.m_bind0 (Monad.smax_def State.state_monad)
180 (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun src ->
181 Monad.m_bind0 (Monad.smax_def State.state_monad)
182 (adds_graph_post g_pars globals rest dst) (fun mid ->
183 Monad.m_bind0 (Monad.smax_def State.state_monad)
185 (Joint.add_graph g_pars globals src (Joint.Sequential
186 ((Joint.Step_seq i), mid)))) (fun x ->
187 Monad.m_return0 (Monad.smax_def State.state_monad) src)))
190 Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
191 Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
192 Joint.joint_internal_function **)
193 let adds_graph g_pars globals insts src dst def =
194 let pref = insts.Types.fst.Types.fst in
195 let op = insts.Types.fst.Types.snd in
196 let post = insts.Types.snd in
197 let { Types.fst = def0; Types.snd = mid } =
198 Obj.magic adds_graph_pre g_pars globals (fun lbl inst -> inst lbl)
199 (Obj.magic pref) src def
201 let { Types.fst = def1; Types.snd = mid' } =
202 Obj.magic adds_graph_post g_pars globals post dst def0
204 Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
207 (** val fin_adds_graph :
208 Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
209 Graphs.label -> Joint.joint_internal_function ->
210 Joint.joint_internal_function **)
211 let fin_adds_graph g_pars globals insts src def =
212 let pref = insts.Types.fst in
213 let last = insts.Types.snd in
214 let { Types.fst = def0; Types.snd = mid } =
215 Obj.magic adds_graph_pre g_pars globals (fun x i -> i) pref src def
217 Joint.add_graph g_pars globals mid (Joint.Final last) def0
219 (** val b_adds_graph :
220 Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
221 Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
222 Joint.joint_internal_function **)
223 let b_adds_graph g_pars globals insts src dst def =
224 let { Types.fst = def0; Types.snd = stmts } =
225 Obj.magic Bind_new.bcompile
226 (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
229 adds_graph g_pars globals stmts src dst def0
231 (** val b_fin_adds_graph :
232 Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
233 Graphs.label -> Joint.joint_internal_function ->
234 Joint.joint_internal_function **)
235 let b_fin_adds_graph g_pars globals insts src def =
236 let { Types.fst = def0; Types.snd = stmts } =
237 Obj.magic Bind_new.bcompile
238 (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
241 fin_adds_graph g_pars globals stmts src def0
243 (** val step_registers :
244 Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
245 Registers.register List.list **)
246 let step_registers p globals s =
247 Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s
249 (** val fin_step_registers :
250 Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
251 let fin_step_registers p = function
252 | Joint.GOTO x -> List.Nil
253 | Joint.RETURN -> List.Nil
254 | Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r
256 type b_graph_translate_data = { init_ret : __; init_params : __;
257 init_stack_size : Nat.nat;
258 added_prologue : Joint.joint_seq List.list;
259 new_regs : Registers.register List.list;
260 f_step : (Graphs.label -> Joint.joint_step ->
261 Blocks.bind_step_block);
262 f_fin : (Graphs.label -> Joint.joint_fin_step
263 -> Blocks.bind_fin_block) }
265 (** val b_graph_translate_data_rect_Type4 :
266 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
267 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
268 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
269 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
270 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
271 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18277 =
272 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
273 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
274 f_step = f_step0; f_fin = f_fin0 } = x_18277
276 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
277 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
279 (** val b_graph_translate_data_rect_Type5 :
280 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
281 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
282 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
283 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
284 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
285 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18279 =
286 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
287 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
288 f_step = f_step0; f_fin = f_fin0 } = x_18279
290 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
291 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
293 (** val b_graph_translate_data_rect_Type3 :
294 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
295 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
296 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
297 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
298 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
299 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18281 =
300 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
301 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
302 f_step = f_step0; f_fin = f_fin0 } = x_18281
304 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
305 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
307 (** val b_graph_translate_data_rect_Type2 :
308 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
309 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
310 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
311 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
312 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
313 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18283 =
314 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
315 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
316 f_step = f_step0; f_fin = f_fin0 } = x_18283
318 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
319 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
321 (** val b_graph_translate_data_rect_Type1 :
322 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
323 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
324 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
325 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
326 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
327 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18285 =
328 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
329 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
330 f_step = f_step0; f_fin = f_fin0 } = x_18285
332 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
333 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
335 (** val b_graph_translate_data_rect_Type0 :
336 Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
337 __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
338 List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
339 -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
340 -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
341 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18287 =
342 let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
343 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
344 f_step = f_step0; f_fin = f_fin0 } = x_18287
346 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
347 added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __
350 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
351 b_graph_translate_data -> __ **)
352 let rec init_ret src dst globals xxx =
355 (** val init_params :
356 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
357 b_graph_translate_data -> __ **)
358 let rec init_params src dst globals xxx =
361 (** val init_stack_size :
362 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
363 b_graph_translate_data -> Nat.nat **)
364 let rec init_stack_size src dst globals xxx =
367 (** val added_prologue :
368 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
369 b_graph_translate_data -> Joint.joint_seq List.list **)
370 let rec added_prologue src dst globals xxx =
374 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
375 b_graph_translate_data -> Registers.register List.list **)
376 let rec new_regs src dst globals xxx =
380 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
381 b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
382 Blocks.bind_step_block **)
383 let rec f_step src dst globals xxx =
387 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
388 b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
389 Blocks.bind_fin_block **)
390 let rec f_fin src dst globals xxx =
393 (** val b_graph_translate_data_inv_rect_Type4 :
394 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
395 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
396 List.list -> Registers.register List.list -> (Graphs.label ->
397 Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
398 Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
399 __ -> 'a1) -> 'a1 **)
400 let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
401 let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __
403 (** val b_graph_translate_data_inv_rect_Type3 :
404 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
405 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
406 List.list -> Registers.register List.list -> (Graphs.label ->
407 Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
408 Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
409 __ -> 'a1) -> 'a1 **)
410 let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
411 let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __
413 (** val b_graph_translate_data_inv_rect_Type2 :
414 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
415 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
416 List.list -> Registers.register List.list -> (Graphs.label ->
417 Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
418 Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
419 __ -> 'a1) -> 'a1 **)
420 let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
421 let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __
423 (** val b_graph_translate_data_inv_rect_Type1 :
424 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
425 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
426 List.list -> Registers.register List.list -> (Graphs.label ->
427 Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
428 Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
429 __ -> 'a1) -> 'a1 **)
430 let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
431 let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __
433 (** val b_graph_translate_data_inv_rect_Type0 :
434 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
435 b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
436 List.list -> Registers.register List.list -> (Graphs.label ->
437 Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
438 Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
439 __ -> 'a1) -> 'a1 **)
440 let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
441 let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __
443 (** val b_graph_translate_data_jmdiscr :
444 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
445 b_graph_translate_data -> b_graph_translate_data -> __ **)
446 let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
447 Logic.eq_rect_Type2 x
448 (let { init_ret = a0; init_params = a10; init_stack_size = a20;
449 added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
451 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
453 type bound_b_graph_translate_data =
454 (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
456 (** val get_first_costlabel_next :
457 Joint.params -> AST.ident List.list ->
458 Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
460 let get_first_costlabel_next p g def =
461 (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
462 (Types.pi1 def).Joint.joint_if_entry with
463 | Types.None -> (fun _ -> assert false (* absurd case *))
466 | Joint.Sequential (s', nxt) ->
468 | Joint.COST_LABEL c ->
469 (fun _ -> { Types.fst = c; Types.snd = nxt })
470 | Joint.CALL (x, x0, x1) ->
471 (fun _ -> assert false (* absurd case *))
472 | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
473 | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
474 | Joint.Final x -> (fun _ -> assert false (* absurd case *))
475 | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
478 (** val get_first_costlabel :
479 Joint.params -> AST.ident List.list ->
480 Joint.joint_closed_internal_function -> CostLabel.costlabel **)
481 let get_first_costlabel p g f =
482 (get_first_costlabel_next p g f).Types.fst
484 (** val not_emptyb : 'a1 List.list -> Bool.bool **)
485 let not_emptyb = function
486 | List.Nil -> Bool.False
487 | List.Cons (x, x0) -> Bool.True
489 (** val b_graph_translate_props_rect_Type4 :
490 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
491 b_graph_translate_data -> Joint.joint_closed_internal_function ->
492 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
493 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
494 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
495 let rec b_graph_translate_props_rect_Type4 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
496 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
498 (** val b_graph_translate_props_rect_Type5 :
499 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
500 b_graph_translate_data -> Joint.joint_closed_internal_function ->
501 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
502 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
503 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
504 let rec b_graph_translate_props_rect_Type5 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
505 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
507 (** val b_graph_translate_props_rect_Type3 :
508 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
509 b_graph_translate_data -> Joint.joint_closed_internal_function ->
510 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
511 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
512 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
513 let rec b_graph_translate_props_rect_Type3 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
514 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
516 (** val b_graph_translate_props_rect_Type2 :
517 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
518 b_graph_translate_data -> Joint.joint_closed_internal_function ->
519 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
520 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
521 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
522 let rec b_graph_translate_props_rect_Type2 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
523 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
525 (** val b_graph_translate_props_rect_Type1 :
526 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
527 b_graph_translate_data -> Joint.joint_closed_internal_function ->
528 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
529 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
530 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
531 let rec b_graph_translate_props_rect_Type1 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
532 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
534 (** val b_graph_translate_props_rect_Type0 :
535 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
536 b_graph_translate_data -> Joint.joint_closed_internal_function ->
537 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
538 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
539 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
540 let rec b_graph_translate_props_rect_Type0 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
541 h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __
543 (** val b_graph_translate_props_inv_rect_Type4 :
544 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
545 b_graph_translate_data -> Joint.joint_closed_internal_function ->
546 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
547 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
548 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
550 let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
551 let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
554 (** val b_graph_translate_props_inv_rect_Type3 :
555 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
556 b_graph_translate_data -> Joint.joint_closed_internal_function ->
557 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
558 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
559 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
561 let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
562 let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
565 (** val b_graph_translate_props_inv_rect_Type2 :
566 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
567 b_graph_translate_data -> Joint.joint_closed_internal_function ->
568 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
569 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
570 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
572 let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
573 let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
576 (** val b_graph_translate_props_inv_rect_Type1 :
577 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
578 b_graph_translate_data -> Joint.joint_closed_internal_function ->
579 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
580 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
581 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
583 let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
584 let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
587 (** val b_graph_translate_props_inv_rect_Type0 :
588 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
589 b_graph_translate_data -> Joint.joint_closed_internal_function ->
590 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
591 List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
592 -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
594 let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
595 let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
598 (** val b_graph_translate_props_jmdiscr :
599 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
600 b_graph_translate_data -> Joint.joint_closed_internal_function ->
601 Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
602 List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
603 let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
604 Logic.eq_rect_Type2 __
605 (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __
607 (** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
609 { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }
612 AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
613 __ -> Joint.joint_internal_function **)
614 let set_entry globals pars int_fun entry =
615 { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
616 Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
617 Joint.joint_if_result = int_fun.Joint.joint_if_result;
618 Joint.joint_if_params = int_fun.Joint.joint_if_params;
619 Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
620 Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
621 Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
624 (** val b_graph_translate :
625 Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
626 bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
627 Joint.joint_closed_internal_function Types.sig0 **)
628 let b_graph_translate src_g_pars dst_g_pars globals data def =
630 Obj.magic Bind_new.bcompile
632 (Relations.compose pair_swap
633 (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
634 (Types.pi1 def).Joint.joint_if_runiverse
636 let runiv = runiv_data.Types.fst in
637 let data0 = runiv_data.Types.snd in
638 let entry = (Types.pi1 def).Joint.joint_if_entry in
639 let init = { Joint.joint_if_luniverse =
640 (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
641 runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
642 data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
643 Joint.joint_if_local_stacksize =
644 (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
645 (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
646 Joint.joint_if_entry = entry }
648 let f = fun lbl stmt def0 ->
650 | Joint.Sequential (inst, next) ->
651 b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
652 (Obj.magic next) def0
653 | Joint.Final inst ->
654 b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
655 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
658 Identifiers.foldi PreIdentifiers.LabelTag f
659 (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
661 let prologue = data0.added_prologue in
663 match not_emptyb prologue with
665 let { Types.fst = init_c; Types.snd = nxt } =
666 get_first_costlabel_next (Joint.graph_params_to_params src_g_pars)
670 Joint.add_graph dst_g_pars globals (Obj.magic entry)
671 (Joint.Sequential ((Joint.Step_seq
673 (Joint.uns_pars__o__u_pars
674 (Joint.gp_to_p__o__stmt_pars dst_g_pars)) globals)), nxt))
677 let { Types.fst = def_out1; Types.snd = entry' } =
678 Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
682 adds_graph dst_g_pars globals { Types.fst = { Types.fst = List.Nil;
683 Types.snd = (fun x -> Joint.COST_LABEL init_c) }; Types.snd =
684 prologue } entry' (Obj.magic entry) def_out1
686 set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out2
688 | Bool.False -> def_out
692 (** val b_graph_transform_program :
693 Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
694 Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
695 Joint.joint_program -> Joint.joint_program **)
696 let b_graph_transform_program src dst init =
697 Joint.transform_joint_program (Joint.graph_params_to_params src)
698 (Joint.graph_params_to_params dst) (fun varnames def_in ->
700 (b_graph_translate src dst varnames (init varnames def_in) def_in))
702 (** val added_registers :
703 Joint.graph_params -> AST.ident List.list ->
704 Joint.joint_internal_function -> (Graphs.label -> Registers.register
705 List.list) -> Registers.register List.list **)
706 let added_registers p g def f_regs =
707 let f = fun lbl x acc -> List.append (f_regs lbl) acc in
708 Identifiers.foldi PreIdentifiers.LabelTag f
709 (Obj.magic def.Joint.joint_if_code) List.Nil