369 
369 
let norm_eq = { eq with eq_rhs = norm_rhs } in

370 
370 
norm_eq::defs', vars'

371 
371 

372 

(** normalize_node node returns a normalized node,

373 

ie.


372 
let normalize_eq_split node defvars eq =


373 


374 
let defs, vars = normalize_eq node defvars eq in


375 
List.fold_right (fun eq (def, vars) >


376 
let eq_defs = Splitting.tuple_split_eq eq in


377 
if eq_defs = [eq] then


378 
eq::def, vars


379 
else


380 
List.fold_left (normalize_eq node) (def, vars) eq_defs


381 
) defs ([], vars)


382 


383 
let normalize_eexpr decls node vars ee =


384 
(* New output variable *)


385 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in


386 
let output_var =


387 
mkvar_decl


388 
ee.eexpr_loc


389 
(output_id,


390 
mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)


391 
mkclock ee.eexpr_loc Ckdec_any,


392 
false (* not a constant *),


393 
None,


394 
None


395 
)


396 
in


397 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in


398 
(* Calls are first inlined *)


399 
let nodes = get_nodes decls in


400 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in


401 
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes


402 
let calls = List.map


403 
(fun called_nd > List.find (fun nd2 > nd2.node_id = called_nd) nodes) calls


404 
in


405 
*)


406 
(*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd > pp_print_string fmt nd.node_id)) calls; *)


407 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in


408 
let locals = node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in


409 
let (new_locals, eqs) =


410 
if calls = [] && not (eq_has_arrows eq) then


411 
(locals, [eq])


412 
else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)


413 
(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in


414 
(*Format.eprintf "eqs %a@.@?"


415 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *)


416 
(new_locals, eqs)


417 
*)


418 
(locals, [eq])


419 


420 
) in


421 
(* Normalizing expr and eqs *)


422 
let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in


423 
let todefine = List.fold_left


424 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)


425 
(ISet.add output_id ISet.empty) vars in


426 
try


427 
let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in


428 
let env = Typing.type_var_decl [] env output_var in (* typing the variable *)


429 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)


430 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in


431 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)


432 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in


433 
(* check that table is empty *)


434 
if (not (ISet.is_empty undefined_vars)) then


435 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));


436 


437 
(*Format.eprintf "normalized eqs %a@.@?"


438 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)


439 
ee.eexpr_normalized < Some (output_var, defs, vars)


440 
with (Types.Error (loc,err)) as exc >


441 
eprintf "Typing error for eexpr %a: %a%a%a@."


442 
Printers.pp_eexpr ee


443 
Types.pp_error err


444 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs


445 
Location.pp_loc loc


446 


447 
;


448 
raise exc


449 


450 
let normalize_spec decls node vars s =


451 
let nee = normalize_eexpr decls node vars in


452 
List.iter nee s.requires;


453 
List.iter nee s.ensures;


454 
List.iter (fun (_, assumes, ensures, _) >


455 
List.iter nee assumes;


456 
List.iter nee ensures


457 
) s.behaviors


458 


459 


460 
(* The normalization phase introduces new local variables


461 
 output cannot be memories. If this happen, new local variables acting as


462 
memories are introduced.


463 
 array constants, pre, arrow, fby, ite, merge, calls to node with index


464 
access


465 
Thoses values are shared, ie. no duplicate expressions are introduced.


466 


467 
Concerning specification, a similar process is applied, replacing an


468 
expression by a list of local variables and definitions


469 
*)


470 


471 
(** normalize_node node returns a normalized node,


472 
ie.

374 
473 
 updated locals

375 
474 
 new equations

376 
475 


377 
476 
*)

378 

let normalize_node node =


477 
let normalize_node decls node =

379 
478 
reset_cpt_fresh ();

380 
479 
let inputs_outputs = node.node_inputs@node.node_outputs in


480 
let is_local v =


481 
List.for_all ((<>) v) inputs_outputs in

381 
482 
let orig_vars = inputs_outputs@node.node_locals in

382 
483 
let not_is_orig_var v =

383 
484 
List.for_all ((!=) v) orig_vars in

...  ...  
465 
566 
annots

466 
567 
) new_annots new_locals

467 
568 
in


569 
if !Options.spec <> "no" then


570 
begin


571 
(* Update mutable fields of eexpr to perform normalization of specification/annotations *)


572 
List.iter


573 
(fun a >


574 
List.iter


575 
(fun (_, ann) > normalize_eexpr decls node inputs_outputs ann)


576 
a.annots


577 
)


578 
node.node_annot;


579 
match node.node_spec with None > ()  Some s > normalize_spec decls node [] s


580 
end;


581 


582 


583 
let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)

468 
584 
let node =

469 
585 
{ node with

470 
586 
node_locals = all_locals;

...  ...  
477 
593 
)

478 
594 

479 
595 

480 

let normalize_decl decl =


596 
let normalize_decl (decls: program) (decl: top_decl) : top_decl =

481 
597 
match decl.top_decl_desc with

482 
598 
 Node nd >

483 

let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in


599 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in

484 
600 
Hashtbl.replace Corelang.node_table nd.node_id decl';

485 
601 
decl'

486 
602 
 Open _  ImportedNode _  Const _  TypeDef _ > decl

487 
603 

488 

let normalize_prog ?(backend="C") decls =


604 
let normalize_prog ?(backend="C") decls : program =

489 
605 
let old_unfold_arrow_active = !unfold_arrow_active in

490 
606 
let old_force_alias_ite = !force_alias_ite in

491 
607 
let old_force_alias_internal_fun = !force_alias_internal_fun in

...  ...  
505 
621 
in

506 
622 

507 
623 
(* Main algorithm: iterates over nodes *)

508 

let res = List.map normalize_decl decls in


624 
let res = List.map (normalize_decl decls) decls in

509 
625 

510 
626 
(* Restoring previous settings *)

511 
627 
unfold_arrow_active := old_unfold_arrow_active;
