lustrec / src / normalization.ml @ 0bd19a92
History  View  Annotate  Download (20.9 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 Lustre_types 
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  
78  
79 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
80 
let get_expr_alias defs expr = 
81 
try Some (List.find (fun eq > Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs) 
82 
with 
83 
 Not_found > None 
84 

85 
(* Replace [expr] with (tuple of) [locals] *) 
86 
let replace_expr locals expr = 
87 
match locals with 
88 
 [] > assert false 
89 
 [v] > { expr with 
90 
expr_tag = Utils.new_tag (); 
91 
expr_desc = Expr_ident v.var_id } 
92 
 _ > { expr with 
93 
expr_tag = Utils.new_tag (); 
94 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 
95  
96 
let unfold_offsets e offsets = 
97 
let add_offset e d = 
98 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; 
99 
let res = *) 
100 
{ e with 
101 
expr_tag = Utils.new_tag (); 
102 
expr_loc = d.Dimension.dim_loc; 
103 
expr_type = Types.array_element_type e.expr_type; 
104 
expr_desc = Expr_access (e, d) } 
105 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 
106 
in 
107 
List.fold_left add_offset e offsets 
108  
109 
(* Create an alias for [expr], if none exists yet *) 
110 
let mk_expr_alias node (defs, vars) expr = 
111 
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 
112 
match get_expr_alias defs expr with 
113 
 Some eq > 
114 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
115 
(defs, vars), replace_expr aliases expr 
116 
 None > 
117 
let new_aliases = 
118 
List.map2 
119 
(mk_fresh_var node expr.expr_loc) 
120 
(Types.type_list_of_type expr.expr_type) 
121 
(Clocks.clock_list_of_clock expr.expr_clock) in 
122 
let new_def = 
123 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
124 
in 
125 
(* 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; *) 
126 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
127  
128 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
129 
and [opt] is true *) 
130 
let mk_expr_alias_opt opt node (defs, vars) expr = 
131 
(*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;*) 
132 
match expr.expr_desc with 
133 
 Expr_ident alias > 
134 
(defs, vars), expr 
135 
 _ > 
136 
match get_expr_alias defs expr with 
137 
 Some eq > 
138 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
139 
(defs, vars), replace_expr aliases expr 
140 
 None > 
141 
if opt 
142 
then 
143 
let new_aliases = 
144 
List.map2 
145 
(mk_fresh_var node expr.expr_loc) 
146 
(Types.type_list_of_type expr.expr_type) 
147 
(Clocks.clock_list_of_clock expr.expr_clock) in 
148 
let new_def = 
149 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
150 
in 
151 
(* Typing and Registering machine type *) 
152 
let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr in 
153 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
154 
else 
155 
(defs, vars), expr 
156  
157 
(* Create a (normalized) expression from [ref_e], 
158 
replacing description with [norm_d], 
159 
taking propagated [offsets] into account 
160 
in order to change expression type *) 
161 
let mk_norm_expr offsets ref_e norm_d = 
162 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
163 
let drop_array_type ty = 
164 
Types.map_tuple_type Types.array_element_type ty in 
165 
{ ref_e with 
166 
expr_desc = norm_d; 
167 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
168 

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

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

407 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
408 
beginning of the list the 
409 
local declared ones *) 
410 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
411  
412  
413 
(* Updating annotations: traceability and machine types for fresh variables *) 
414 

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

493 
(* Backend specific configurations for normalization *) 
494 
let _ = 
495 
match backend with 
496 
 "lustre" > 
497 
(* Special treatment of arrows in lustre backend. We want to keep them *) 
498 
unfold_arrow_active := false; 
499 
 "emf" > ( 
500 
(* Forcing ite normalization *) 
501 
force_alias_ite := true; 
502 
force_alias_internal_fun := true; 
503 
) 
504 
 _ > () (* No fancy options for other backends *) 
505 
in 
506  
507 
(* Main algorithm: iterates over nodes *) 
508 
let res = List.map normalize_decl decls in 
509 

510 
(* Restoring previous settings *) 
511 
unfold_arrow_active := old_unfold_arrow_active; 
512 
force_alias_ite := old_force_alias_ite; 
513 
force_alias_internal_fun := old_force_alias_internal_fun; 
514 
res 
515 

516 
(* Local Variables: *) 
517 
(* compilecommand:"make C .." *) 
518 
(* End: *) 