lustrec / src / normalization.ml @ f4050bef
History  View  Annotate  Download (21.4 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11  
12 
open Utils 
13 
open LustreSpec 
14 
open Corelang 
15 
open Format 
16  
17 
(** Normalisation iters through the AST of expressions and bind fresh definition 
18 
when some criteria are met. This creation of fresh definition is performed by 
19 
the function mk_expr_alias_opt when the alias argument is on. 
20  
21 
Initial expressions, ie expressions attached a variable in an equation 
22 
definition are not aliased. This nonalias feature is propagated in the 
23 
expression AST for array access and power construct, tuple, and some special 
24 
cases of arrows. 
25  
26 
Two global variables may impact the normalization process: 
27 
 unfold_arrow_active 
28 
 force_alias_ite: when set, bind a fresh alias for then and else 
29 
definitions. 
30 
*) 
31  
32 
(* Two global variables *) 
33 
let unfold_arrow_active = ref true 
34 
let force_alias_ite = ref false 
35 
let force_alias_internal_fun = ref false 
36  
37 

38 
let expr_true loc ck = 
39 
{ expr_tag = Utils.new_tag (); 
40 
expr_desc = Expr_const (Const_tag tag_true); 
41 
expr_type = Type_predef.type_bool; 
42 
expr_clock = ck; 
43 
expr_delay = Delay.new_var (); 
44 
expr_annot = None; 
45 
expr_loc = loc } 
46  
47 
let expr_false loc ck = 
48 
{ expr_tag = Utils.new_tag (); 
49 
expr_desc = Expr_const (Const_tag tag_false); 
50 
expr_type = Type_predef.type_bool; 
51 
expr_clock = ck; 
52 
expr_delay = Delay.new_var (); 
53 
expr_annot = None; 
54 
expr_loc = loc } 
55  
56 
let expr_once loc ck = 
57 
{ expr_tag = Utils.new_tag (); 
58 
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); 
59 
expr_type = Type_predef.type_bool; 
60 
expr_clock = ck; 
61 
expr_delay = Delay.new_var (); 
62 
expr_annot = None; 
63 
expr_loc = loc } 
64  
65 
let is_expr_once = 
66 
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in 
67 
fun expr > Corelang.is_eq_expr expr dummy_expr_once 
68  
69 
let unfold_arrow expr = 
70 
match expr.expr_desc with 
71 
 Expr_arrow (e1, e2) > 
72 
let loc = expr.expr_loc in 
73 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 
74 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
75 
 _ > assert false 
76  
77 
let cpt_fresh = ref 0 
78  
79 
(* Generate a new local [node] variable *) 
80 
let mk_fresh_var node loc ty ck = 
81 
let vars = get_node_vars node in 
82 
let rec aux () = 
83 
incr cpt_fresh; 
84 
let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in 
85 
if List.exists (fun v > v.var_id = s) vars then aux () else 
86 
{ 
87 
var_id = s; 
88 
var_orig = false; 
89 
var_dec_type = dummy_type_dec; 
90 
var_dec_clock = dummy_clock_dec; 
91 
var_dec_const = false; 
92 
var_dec_value = None; 
93 
var_parent_nodeid = Some node.node_id; 
94 
var_type = ty; 
95 
var_clock = ck; 
96 
var_loc = loc 
97 
} 
98 
in aux () 
99  
100 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
101 
let get_expr_alias defs expr = 
102 
try Some (List.find (fun eq > is_eq_expr eq.eq_rhs expr) defs) 
103 
with 
104 
 Not_found > None 
105 

106 
(* Replace [expr] with (tuple of) [locals] *) 
107 
let replace_expr locals expr = 
108 
match locals with 
109 
 [] > assert false 
110 
 [v] > { expr with 
111 
expr_tag = Utils.new_tag (); 
112 
expr_desc = Expr_ident v.var_id } 
113 
 _ > { expr with 
114 
expr_tag = Utils.new_tag (); 
115 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 
116  
117 
let unfold_offsets e offsets = 
118 
let add_offset e d = 
119 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; 
120 
let res = *) 
121 
{ e with 
122 
expr_tag = Utils.new_tag (); 
123 
expr_loc = d.Dimension.dim_loc; 
124 
expr_type = Types.array_element_type e.expr_type; 
125 
expr_desc = Expr_access (e, d) } 
126 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 
127 
in 
128 
List.fold_left add_offset e offsets 
129  
130 
(* Create an alias for [expr], if none exists yet *) 
131 
let mk_expr_alias node (defs, vars) expr = 
132 
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 
133 
match get_expr_alias defs expr with 
134 
 Some eq > 
135 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
136 
(defs, vars), replace_expr aliases expr 
137 
 None > 
138 
let new_aliases = 
139 
List.map2 
140 
(mk_fresh_var node expr.expr_loc) 
141 
(Types.type_list_of_type expr.expr_type) 
142 
(Clocks.clock_list_of_clock expr.expr_clock) in 
143 
let new_def = 
144 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
145 
in 
146 
(* Format.eprintf "Checking def of alias: %a > %a@." (fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *) 
147 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
148  
149 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
150 
and [opt] is true *) 
151 
let mk_expr_alias_opt opt node (defs, vars) expr = 
152 
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 
153 
match expr.expr_desc with 
154 
 Expr_ident alias > 
155 
(defs, vars), expr 
156 
 _ > 
157 
match get_expr_alias defs expr with 
158 
 Some eq > 
159 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
160 
(defs, vars), replace_expr aliases expr 
161 
 None > 
162 
if opt 
163 
then 
164 
let new_aliases = 
165 
List.map2 
166 
(mk_fresh_var node expr.expr_loc) 
167 
(Types.type_list_of_type expr.expr_type) 
168 
(Clocks.clock_list_of_clock expr.expr_clock) in 
169 
let new_def = 
170 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
171 
in 
172 
(* Typing and Registering machine type *) 
173 
let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr in 
174 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
175 
else 
176 
(defs, vars), expr 
177  
178 
(* Create a (normalized) expression from [ref_e], 
179 
replacing description with [norm_d], 
180 
taking propagated [offsets] into account 
181 
in order to change expression type *) 
182 
let mk_norm_expr offsets ref_e norm_d = 
183 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
184 
let drop_array_type ty = 
185 
Types.map_tuple_type Types.array_element_type ty in 
186 
{ ref_e with 
187 
expr_desc = norm_d; 
188 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
189 

190 
(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 
191 
let rec normalize_list alias node offsets norm_element defvars elist = 
192 
List.fold_right 
193 
(fun t (defvars, qlist) > 
194 
let defvars, norm_t = norm_element alias node offsets defvars t in 
195 
(defvars, norm_t :: qlist) 
196 
) elist (defvars, []) 
197  
198 
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr = 
199 
(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
200 
match expr.expr_desc with 
201 
 Expr_const _ 
202 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
203 
 Expr_array elist > 
204 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
205 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 
206 
mk_expr_alias_opt alias node defvars norm_expr 
207 
 Expr_power (e1, d) when offsets = [] > 
208 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
209 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in 
210 
mk_expr_alias_opt alias node defvars norm_expr 
211 
 Expr_power (e1, d) > 
212 
normalize_expr ~alias:alias node (List.tl offsets) defvars e1 
213 
 Expr_access (e1, d) > 
214 
normalize_expr ~alias:alias node (d::offsets) defvars e1 
215 
 Expr_tuple elist > 
216 
let defvars, norm_elist = 
217 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in 
218 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
219 
 Expr_appl (id, args, None) 
220 
when Basic_library.is_homomorphic_fun id 
221 
&& Types.is_array_type expr.expr_type > 
222 
let defvars, norm_args = 
223 
normalize_list 
224 
alias 
225 
node 
226 
offsets 
227 
(fun _ > normalize_array_expr ~alias:true) 
228 
defvars 
229 
(expr_list_of_expr args) 
230 
in 
231 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
232 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr 
233 
&& not (!force_alias_internal_fun  alias_basic) > 
234 
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in 
235 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 
236 
 Expr_appl (id, args, r) > 
237 
let defvars, r = 
238 
match r with 
239 
 None > defvars, None 
240 
 Some r > 
241 
let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in 
242 
defvars, Some norm_r 
243 
in 
244 
let defvars, norm_args = normalize_expr node [] defvars args in 
245 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 
246 
if offsets <> [] 
247 
then 
248 
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in 
249 
normalize_expr ~alias:alias node offsets defvars norm_expr 
250 
else 
251 
mk_expr_alias_opt (alias && (!force_alias_internal_fun  alias_basic 
252 
 not (Basic_library.is_expr_internal_fun expr))) 
253 
node defvars norm_expr 
254 
 Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) > 
255 
(* Here we differ from Colaco paper: arrows are pushed to the top *) 
256 
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr) 
257 
 Expr_arrow (e1,e2) > 
258 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
259 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in 
260 
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in 
261 
mk_expr_alias_opt alias node defvars norm_expr 
262 
 Expr_pre e > 
263 
let defvars, norm_e = normalize_expr node offsets defvars e in 
264 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 
265 
mk_expr_alias_opt alias node defvars norm_expr 
266 
 Expr_fby (e1, e2) > 
267 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
268 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in 
269 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in 
270 
mk_expr_alias_opt alias node defvars norm_expr 
271 
 Expr_when (e, c, l) > 
272 
let defvars, norm_e = normalize_expr node offsets defvars e in 
273 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) 
274 
 Expr_ite (c, t, e) > 
275 
let defvars, norm_c = normalize_guard node defvars c in 
276 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
277 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in 
278 
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in 
279 
mk_expr_alias_opt alias node defvars norm_expr 
280 
 Expr_merge (c, hl) > 
281 
let defvars, norm_hl = normalize_branches node offsets defvars hl in 
282 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 
283 
mk_expr_alias_opt alias node defvars norm_expr 
284  
285 
(* Creates a conditional with a merge construct, which is more lazy *) 
286 
(* 
287 
let norm_conditional_as_merge alias node norm_expr offsets defvars expr = 
288 
match expr.expr_desc with 
289 
 Expr_ite (c, t, e) > 
290 
let defvars, norm_t = norm_expr (alias node offsets defvars t in 
291 
 _ > assert false 
292 
*) 
293 
and normalize_branches node offsets defvars hl = 
294 
List.fold_right 
295 
(fun (t, h) (defvars, norm_q) > 
296 
let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in 
297 
defvars, (t, norm_h) :: norm_q 
298 
) 
299 
hl (defvars, []) 
300  
301 
and normalize_array_expr ?(alias=true) node offsets defvars expr = 
302 
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
303 
match expr.expr_desc with 
304 
 Expr_power (e1, d) when offsets = [] > 
305 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
306 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) 
307 
 Expr_power (e1, d) > 
308 
normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1 
309 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias node (d::offsets) defvars e1 
310 
 Expr_array elist when offsets = [] > 
311 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
312 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 
313 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr > 
314 
let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 
315 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
316 
 _ > normalize_expr ~alias:alias node offsets defvars expr 
317  
318 
and normalize_cond_expr ?(alias=true) node offsets defvars expr = 
319 
(*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
320 
match expr.expr_desc with 
321 
 Expr_access (e1, d) > 
322 
normalize_cond_expr ~alias:alias node (d::offsets) defvars e1 
323 
 Expr_ite (c, t, e) > 
324 
let defvars, norm_c = normalize_guard node defvars c in 
325 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
326 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in 
327 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 
328 
 Expr_merge (c, hl) > 
329 
let defvars, norm_hl = normalize_branches node offsets defvars hl in 
330 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) 
331 
 _ when !force_alias_ite > 
332 
(* Forcing alias creation for then/else expressions *) 
333 
let defvars, norm_expr = 
334 
normalize_expr ~alias:alias node offsets defvars expr 
335 
in 
336 
mk_expr_alias_opt true node defvars norm_expr 
337 
 _ > (* default case without the force_alias_ite option *) 
338 
normalize_expr ~alias:alias node offsets defvars expr 
339 

340 
and normalize_guard node defvars expr = 
341 
let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in 
342 
mk_expr_alias_opt true node defvars norm_expr 
343  
344 
(* outputs cannot be memories as well. If so, introduce new local variable. 
345 
*) 
346 
let decouple_outputs node defvars eq = 
347 
let rec fold_lhs defvars lhs tys cks = 
348 
match lhs, tys, cks with 
349 
 [], [], [] > defvars, [] 
350 
 v::qv, t::qt, c::qc > let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in 
351 
if List.exists (fun o > o.var_id = v) node.node_outputs 
352 
then 
353 
let newvar = mk_fresh_var node eq.eq_loc t c in 
354 
let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in 
355 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 
356 
else 
357 
(defs_q, vars_q), v::lhs_q 
358 
 _ > assert false in 
359 
let defvars', lhs' = 
360 
fold_lhs 
361 
defvars 
362 
eq.eq_lhs 
363 
(Types.type_list_of_type eq.eq_rhs.expr_type) 
364 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 
365 
defvars', {eq with eq_lhs = lhs' } 
366  
367 
let rec normalize_eq node defvars eq = 
368 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 
369 
match eq.eq_rhs.expr_desc with 
370 
 Expr_pre _ 
371 
 Expr_fby _ > 
372 
let (defvars', eq') = decouple_outputs node defvars eq in 
373 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in 
374 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
375 
(norm_eq::defs', vars') 
376 
 Expr_array _ > 
377 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
378 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
379 
(norm_eq::defs', vars') 
380 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type > 
381 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
382 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
383 
(norm_eq::defs', vars') 
384 
 Expr_appl _ > 
385 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in 
386 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
387 
(norm_eq::defs', vars') 
388 
 _ > 
389 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in 
390 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
391 
norm_eq::defs', vars' 
392  
393 
(** normalize_node node returns a normalized node, 
394 
ie. 
395 
 updated locals 
396 
 new equations 
397 
 
398 
*) 
399 
let normalize_node node = 
400 
cpt_fresh := 0; 
401 
let inputs_outputs = node.node_inputs@node.node_outputs in 
402 
let orig_vars = inputs_outputs@node.node_locals in 
403 
let not_is_orig_var v = 
404 
List.for_all ((!=) v) orig_vars in 
405 
let defs, vars = 
406 
let eqs, auts = get_node_eqs node in 
407 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
408 
List.fold_left (normalize_eq node) ([], orig_vars) eqs in 
409 
(* Normalize the asserts *) 
410 
let vars, assert_defs, asserts = 
411 
List.fold_left ( 
412 
fun (vars, def_accu, assert_accu) assert_ > 
413 
let assert_expr = assert_.assert_expr in 
414 
let (defs, vars'), expr = 
415 
normalize_expr 
416 
~alias:true (* forcing introduction of new equations for fcn calls *) 
417 
node 
418 
[] (* empty offset for arrays *) 
419 
([], vars) (* defvar only contains vars *) 
420 
assert_expr 
421 
in 
422 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
423 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
424 
) (vars, [], []) node.node_asserts in 
425 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
426 
vars and initial locals ones *) 
427 

428 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
429 
beginning of the list the 
430 
local declared ones *) 
431 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
432  
433  
434 
(* Updating annotations: traceability and machine types for fresh variables *) 
435 

436 
(* Compute traceability info: 
437 
 gather newly bound variables 
438 
 compute the associated expression without aliases 
439 
*) 
440 
let new_annots = 
441 
if !Options.traces then 
442 
begin 
443 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
444 
let norm_traceability = { 
445 
annots = List.map (fun v > 
446 
let eq = 
447 
try 
448 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
449 
with Not_found > 
450 
( 
451 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
452 
assert false 
453 
) 
454 
in 
455 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
456 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
457 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
458 
(["traceability"], pair) 
459 
) diff_vars; 
460 
annot_loc = Location.dummy_loc 
461 
} 
462 
in 
463 
norm_traceability::node.node_annot 
464 
end 
465 
else 
466 
node.node_annot 
467 
in 
468  
469 
let new_annots = 
470 
List.fold_left (fun annots v > 
471 
if Machine_types.is_active && Machine_types.is_exportable v then 
472 
let typ = Machine_types.get_specified_type v in 
473 
let typ_name = Machine_types.type_name typ in 
474  
475 
let loc = v.var_loc in 
476 
let typ_as_string = 
477 
mkexpr 
478 
loc 
479 
(Expr_const 
480 
(Const_string typ_name)) 
481 
in 
482 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
483 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
484 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
485 
else 
486 
annots 
487 
) new_annots new_locals 
488 
in 
489 
let node = 
490 
{ node with 
491 
node_locals = all_locals; 
492 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
493 
node_asserts = asserts; 
494 
node_annot = new_annots; 
495 
} 
496 
in ((*Printers.pp_node Format.err_formatter node;*) 
497 
node 
498 
) 
499  
500  
501 
let normalize_decl decl = 
502 
match decl.top_decl_desc with 
503 
 Node nd > 
504 
let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in 
505 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 
506 
decl' 
507 
 Open _  ImportedNode _  Const _  TypeDef _ > decl 
508  
509 
let normalize_prog ?(backend="C") decls = 
510 
let old_unfold_arrow_active = !unfold_arrow_active in 
511 
let old_force_alias_ite = !force_alias_ite in 
512 
let old_force_alias_internal_fun = !force_alias_internal_fun in 
513 

514 
(* Backend specific configurations for normalization *) 
515 
let _ = 
516 
match backend with 
517 
 "lustre" > 
518 
(* Special treatment of arrows in lustre backend. We want to keep them *) 
519 
unfold_arrow_active := false; 
520 
 "emf" > ( 
521 
(* Forcing ite normalization *) 
522 
force_alias_ite := true; 
523 
force_alias_internal_fun := true; 
524 
) 
525 
 _ > () (* No fancy options for other backends *) 
526 
in 
527  
528 
(* Main algorithm: iterates over nodes *) 
529 
let res = List.map normalize_decl decls in 
530 

531 
(* Restoring previous settings *) 
532 
unfold_arrow_active := old_unfold_arrow_active; 
533 
force_alias_ite := old_force_alias_ite; 
534 
force_alias_internal_fun := old_force_alias_internal_fun; 
535 
res 
536 

537 
(* Local Variables: *) 
538 
(* compilecommand:"make C .." *) 
539 
(* End: *) 