394 
394 
[control_on_clock node args c (conditional g [MReset i] [MNoReset i])]

395 
395 

396 
396 
let translate_eq node ((m, si, j, d, s) as args) eq =

397 

(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)


397 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)

398 
398 
match eq.eq_lhs, eq.eq_rhs.expr_desc with

399 
399 
 [x], Expr_arrow (e1, e2) >

400 

let var_x = get_node_var x node in

401 

let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in

402 

let c1 = translate_expr node args e1 in

403 

let c2 = translate_expr node args e2 in

404 

(m,

405 

MReset o :: si,

406 

Utils.IMap.add o (arrow_top_decl, []) j,

407 

d,

408 

(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)


400 
let var_x = get_node_var x node in


401 
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in


402 
let c1 = translate_expr node args e1 in


403 
let c2 = translate_expr node args e2 in


404 
(m,


405 
MReset o :: si,


406 
Utils.IMap.add o (arrow_top_decl, []) j,


407 
d,


408 
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)

409 
409 
 [x], Expr_pre e1 when ISet.mem (get_node_var x node) d >

410 

let var_x = get_node_var x node in

411 

(ISet.add var_x m,

412 

si,

413 

j,

414 

d,

415 

control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)


410 
let var_x = get_node_var x node in


411 
(ISet.add var_x m,


412 
si,


413 
j,


414 
d,


415 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)

416 
416 
 [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d >

417 

let var_x = get_node_var x node in

418 

(ISet.add var_x m,

419 

MStateAssign (var_x, translate_expr node args e1) :: si,

420 

j,

421 

d,

422 

control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)


417 
let var_x = get_node_var x node in


418 
(ISet.add var_x m,


419 
MStateAssign (var_x, translate_expr node args e1) :: si,


420 
j,


421 
d,


422 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)

423 
423 

424 
424 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

425 

let var_p = List.map (fun v > get_node_var v node) p in

426 

let el = expr_list_of_expr arg in

427 

let vl = List.map (translate_expr node args) el in

428 

let node_f = node_from_name f in

429 

let call_f =

430 

node_f,

431 

NodeDep.filter_static_inputs (node_inputs node_f) el in

432 

let o = new_instance node node_f eq.eq_rhs.expr_tag in

433 

let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in

434 

let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in

435 

(*Clocks.new_var true in

436 

Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;

437 

Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)

438 

(m,

439 

(if Stateless.check_node node_f then si else MReset o :: si),

440 

Utils.IMap.add o call_f j,

441 

d,

442 

(if Stateless.check_node node_f

443 

then []

444 

else reset_instance node args o r call_ck) @

445 

(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)

446 

(*

447 

(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)

448 

are preserved. While they are replaced as if g then x = t else x = e in C or Java

449 

backends. *)

450 

 [x], Expr_ite (c, t, e)


425 
let var_p = List.map (fun v > get_node_var v node) p in


426 
let el = expr_list_of_expr arg in


427 
let vl = List.map (translate_expr node args) el in


428 
let node_f = node_from_name f in


429 
let call_f =


430 
node_f,


431 
NodeDep.filter_static_inputs (node_inputs node_f) el in


432 
let o = new_instance node node_f eq.eq_rhs.expr_tag in


433 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in


434 
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in


435 
(*Clocks.new_var true in


436 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;


437 
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)


438 
(m,


439 
(if Stateless.check_node node_f then si else MReset o :: si),


440 
Utils.IMap.add o call_f j,


441 
d,


442 
(if Stateless.check_node node_f


443 
then []


444 
else reset_instance node args o r call_ck) @


445 
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)


446 
(*


447 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)


448 
are preserved. While they are replaced as if g then x = t else x = e in C or Java


449 
backends. *)


450 
 [x], Expr_ite (c, t, e)

451 
451 
when (match !Options.output with  "horn" > true  "C"  "java"  _ > false)

452 

>


452 
>

453 
453 
let var_x = get_node_var x node in

454 
454 
(m,

455 

si,

456 

j,

457 

d,

458 

(control_on_clock node args eq.eq_rhs.expr_clock

459 

(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)


455 
si,


456 
j,


457 
d,


458 
(control_on_clock node args eq.eq_rhs.expr_clock


459 
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)

460 
460 
)

461 
461 

462 

*)


462 
*)

463 
463 
 [x], _ > (

464 
464 
let var_x = get_node_var x node in

465 
465 
(m, si, j, d,

...  ...  
471 
471 
)

472 
472 
)

473 
473 
 _ >

474 

begin

475 

Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;

476 

assert false

477 

end


474 
begin


475 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;


476 
assert false


477 
end

478 
478 

479 
479 
let find_eq xl eqs =

480 
480 
let rec aux accu eqs =
