Revision 63f10e14
Added by PierreLoïc Garoche about 5 years ago
src/machine_code.ml  

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 = 
Also available in: Unified diff
Removing silly warning message