lustrec / src / normalization.ml @ 949b2e1e
History  View  Annotate  Download (25.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 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 > 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 
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. 
473 
 updated locals 
474 
 new equations 
475 
 
476 
*) 
477 
let normalize_node decls node = 
478 
reset_cpt_fresh (); 
479 
let inputs_outputs = node.node_inputs@node.node_outputs in 
480 
let is_local v = 
481 
List.for_all ((<>) v) inputs_outputs in 
482 
let orig_vars = inputs_outputs@node.node_locals in 
483 
let not_is_orig_var v = 
484 
List.for_all ((!=) v) orig_vars in 
485 
let defs, vars = 
486 
let eqs, auts = get_node_eqs node in 
487 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
488 
List.fold_left (normalize_eq node) ([], orig_vars) eqs in 
489 
(* Normalize the asserts *) 
490 
let vars, assert_defs, asserts = 
491 
List.fold_left ( 
492 
fun (vars, def_accu, assert_accu) assert_ > 
493 
let assert_expr = assert_.assert_expr in 
494 
let (defs, vars'), expr = 
495 
normalize_expr 
496 
~alias:true (* forcing introduction of new equations for fcn calls *) 
497 
node 
498 
[] (* empty offset for arrays *) 
499 
([], vars) (* defvar only contains vars *) 
500 
assert_expr 
501 
in 
502 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
503 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
504 
) (vars, [], []) node.node_asserts in 
505 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
506 
vars and initial locals ones *) 
507 

508 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
509 
beginning of the list the 
510 
local declared ones *) 
511 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
512  
513  
514 
(* Updating annotations: traceability and machine types for fresh variables *) 
515 

516 
(* Compute traceability info: 
517 
 gather newly bound variables 
518 
 compute the associated expression without aliases 
519 
*) 
520 
let new_annots = 
521 
if !Options.traces then 
522 
begin 
523 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
524 
let norm_traceability = { 
525 
annots = List.map (fun v > 
526 
let eq = 
527 
try 
528 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
529 
with Not_found > 
530 
( 
531 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
532 
assert false 
533 
) 
534 
in 
535 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
536 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
537 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
538 
(["traceability"], pair) 
539 
) diff_vars; 
540 
annot_loc = Location.dummy_loc 
541 
} 
542 
in 
543 
norm_traceability::node.node_annot 
544 
end 
545 
else 
546 
node.node_annot 
547 
in 
548  
549 
let new_annots = 
550 
List.fold_left (fun annots v > 
551 
if Machine_types.is_active && Machine_types.is_exportable v then 
552 
let typ = Machine_types.get_specified_type v in 
553 
let typ_name = Machine_types.type_name typ in 
554  
555 
let loc = v.var_loc in 
556 
let typ_as_string = 
557 
mkexpr 
558 
loc 
559 
(Expr_const 
560 
(Const_string typ_name)) 
561 
in 
562 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
563 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
564 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
565 
else 
566 
annots 
567 
) new_annots new_locals 
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 ? *) 
584 
let node = 
585 
{ node with 
586 
node_locals = all_locals; 
587 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
588 
node_asserts = asserts; 
589 
node_annot = new_annots; 
590 
} 
591 
in ((*Printers.pp_node Format.err_formatter node;*) 
592 
node 
593 
) 
594  
595  
596 
let normalize_decl (decls: program) (decl: top_decl) : top_decl = 
597 
match decl.top_decl_desc with 
598 
 Node nd > 
599 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 
600 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 
601 
decl' 
602 
 Open _  ImportedNode _  Const _  TypeDef _ > decl 
603  
604 
let normalize_prog ?(backend="C") decls : program = 
605 
let old_unfold_arrow_active = !unfold_arrow_active in 
606 
let old_force_alias_ite = !force_alias_ite in 
607 
let old_force_alias_internal_fun = !force_alias_internal_fun in 
608 

609 
(* Backend specific configurations for normalization *) 
610 
let _ = 
611 
match backend with 
612 
 "lustre" > 
613 
(* Special treatment of arrows in lustre backend. We want to keep them *) 
614 
unfold_arrow_active := false; 
615 
 "emf" > ( 
616 
(* Forcing ite normalization *) 
617 
force_alias_ite := true; 
618 
force_alias_internal_fun := true; 
619 
) 
620 
 _ > () (* No fancy options for other backends *) 
621 
in 
622  
623 
(* Main algorithm: iterates over nodes *) 
624 
let res = List.map (normalize_decl decls) decls in 
625 

626 
(* Restoring previous settings *) 
627 
unfold_arrow_active := old_unfold_arrow_active; 
628 
force_alias_ite := old_force_alias_ite; 
629 
force_alias_internal_fun := old_force_alias_internal_fun; 
630 
res 
631 

632 
(* Local Variables: *) 
633 
(* compilecommand:"make C .." *) 
634 
(* End: *) 