lustrec / src / normalization.ml @ master
History  View  Annotate  Download (26.1 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 
(* Format.eprintf "Found a preexisting definition@."; *) 
139 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
140 
(defs, vars), replace_expr aliases expr 
141 
 None > 
142 
(* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; 
143 
* Format.eprintf "existing defs are: @[[%a@]]@." 
144 
* (fprintf_list ~sep:"@ "(fun fmt eq > 
145 
* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a" 
146 
* Clocks.print_ck eq.eq_rhs.expr_clock 
147 
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) 
148 
* (is_eq_expr eq.eq_rhs expr) 
149 
* Printers.pp_node_eq eq)) 
150 
* defs; *) 
151 
if opt 
152 
then 
153 
let new_aliases = 
154 
List.map2 
155 
(mk_fresh_var node expr.expr_loc) 
156 
(Types.type_list_of_type expr.expr_type) 
157 
(Clocks.clock_list_of_clock expr.expr_clock) in 
158 
let new_def = 
159 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
160 
in 
161 
(* Typing and Registering machine type *) 
162 
let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr in 
163 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
164 
else 
165 
(defs, vars), expr 
166  
167 
(* Create a (normalized) expression from [ref_e], 
168 
replacing description with [norm_d], 
169 
taking propagated [offsets] into account 
170 
in order to change expression type *) 
171 
let mk_norm_expr offsets ref_e norm_d = 
172 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
173 
let drop_array_type ty = 
174 
Types.map_tuple_type Types.array_element_type ty in 
175 
{ ref_e with 
176 
expr_desc = norm_d; 
177 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
178 

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

329 
and normalize_guard node defvars expr = 
330 
let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in 
331 
mk_expr_alias_opt true node defvars norm_expr 
332  
333 
(* outputs cannot be memories as well. If so, introduce new local variable. 
334 
*) 
335 
let decouple_outputs node defvars eq = 
336 
let rec fold_lhs defvars lhs tys cks = 
337 
match lhs, tys, cks with 
338 
 [], [], [] > defvars, [] 
339 
 v::qv, t::qt, c::qc > let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in 
340 
if List.exists (fun o > o.var_id = v) node.node_outputs 
341 
then 
342 
let newvar = mk_fresh_var node eq.eq_loc t c in 
343 
let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in 
344 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 
345 
else 
346 
(defs_q, vars_q), v::lhs_q 
347 
 _ > assert false in 
348 
let defvars', lhs' = 
349 
fold_lhs 
350 
defvars 
351 
eq.eq_lhs 
352 
(Types.type_list_of_type eq.eq_rhs.expr_type) 
353 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 
354 
defvars', {eq with eq_lhs = lhs' } 
355  
356 
let rec normalize_eq node defvars eq = 
357 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 
358 
match eq.eq_rhs.expr_desc with 
359 
 Expr_pre _ 
360 
 Expr_fby _ > 
361 
let (defvars', eq') = decouple_outputs node defvars eq in 
362 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in 
363 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
364 
(norm_eq::defs', vars') 
365 
 Expr_array _ > 
366 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
367 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
368 
(norm_eq::defs', vars') 
369 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type > 
370 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
371 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
372 
(norm_eq::defs', vars') 
373 
 Expr_appl _ > 
374 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in 
375 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
376 
(norm_eq::defs', vars') 
377 
 _ > 
378 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in 
379 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
380 
norm_eq::defs', vars' 
381  
382 
let normalize_eq_split node defvars eq = 
383 
try 
384 
let defs, vars = normalize_eq node defvars eq in 
385 
List.fold_right (fun eq (def, vars) > 
386 
let eq_defs = Splitting.tuple_split_eq eq in 
387 
if eq_defs = [eq] then 
388 
eq::def, vars 
389 
else 
390 
List.fold_left (normalize_eq node) (def, vars) eq_defs 
391 
) defs ([], vars) 
392  
393 
with _ > ( 
394 
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; 
395 
assert false 
396 
) 
397  
398 
let normalize_eexpr decls node vars ee = 
399 
(* New output variable *) 
400 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 
401 
let output_var = 
402 
mkvar_decl 
403 
ee.eexpr_loc 
404 
(output_id, 
405 
mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *) 
406 
mkclock ee.eexpr_loc Ckdec_any, 
407 
false (* not a constant *), 
408 
None, 
409 
None 
410 
) 
411 
in 
412 

413 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
414 
(* Calls are first inlined *) 
415 
let nodes = get_nodes decls in 
416 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 
417 
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes 
418 
let calls = List.map 
419 
(fun called_nd > List.find (fun nd2 > nd2.node_id = called_nd) nodes) calls 
420 
in 
421 
*) 
422 
(*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; *) 
423 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in 
424 
let locals = node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in 
425 
let (new_locals, eqs) = 
426 
if calls = [] && not (eq_has_arrows eq) then 
427 
(locals, [eq]) 
428 
else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *) 
429 
(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in 
430 
(*Format.eprintf "eqs %a@.@?" 
431 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *) 
432 
(new_locals, eqs) 
433 
*) 
434 
(locals, [eq]) 
435 

436 
) in 
437 
(* Normalizing expr and eqs *) 
438 
let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in 
439 
let todefine = List.fold_left 
440 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) 
441 
(ISet.add output_id ISet.empty) vars in 
442 

443 
try 
444 
let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in 
445 
let env = Typing.type_var_decl [] env output_var in (* typing the variable *) 
446 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 
447 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 
448 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) 
449 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in 
450 
(* check that table is empty *) 
451 
if (not (ISet.is_empty undefined_vars)) then 
452 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); 
453 

454 
(*Format.eprintf "normalized eqs %a@.@?" 
455 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 
456 
ee.eexpr_normalized < Some (output_var, defs, vars) 
457 

458 
with (Types.Error (loc,err)) as exc > 
459 
eprintf "Typing error for eexpr %a: %a%a%a@." 
460 
Printers.pp_eexpr ee 
461 
Types.pp_error err 
462 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs 
463 
Location.pp_loc loc 
464 

465 

466 
; 
467 
raise exc 
468 

469 

470 

471 
let normalize_spec decls node vars s = 
472 
let nee = normalize_eexpr decls node vars in 
473 
List.iter nee s.assume; 
474 
List.iter nee s.guarantees; 
475 
List.iter (fun m > 
476 
List.iter nee m.require; 
477 
List.iter nee m.ensure 
478 
) s.modes 
479 

480 

481 
(* The normalization phase introduces new local variables 
482 
 output cannot be memories. If this happen, new local variables acting as 
483 
memories are introduced. 
484 
 array constants, pre, arrow, fby, ite, merge, calls to node with index 
485 
access 
486 
Thoses values are shared, ie. no duplicate expressions are introduced. 
487  
488 
Concerning specification, a similar process is applied, replacing an 
489 
expression by a list of local variables and definitions 
490 
*) 
491  
492 
(** normalize_node node returns a normalized node, 
493 
ie. 
494 
 updated locals 
495 
 new equations 
496 
 
497 
*) 
498 
let normalize_node decls node = 
499 
reset_cpt_fresh (); 
500 
let inputs_outputs = node.node_inputs@node.node_outputs in 
501 
let orig_vars = inputs_outputs@node.node_locals in 
502 
let not_is_orig_var v = 
503 
List.for_all ((!=) v) orig_vars in 
504 
let defs, vars = 
505 
let eqs, auts = get_node_eqs node in 
506 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
507 
List.fold_left (normalize_eq node) ([], orig_vars) eqs in 
508 
(* Normalize the asserts *) 
509 
let vars, assert_defs, asserts = 
510 
List.fold_left ( 
511 
fun (vars, def_accu, assert_accu) assert_ > 
512 
let assert_expr = assert_.assert_expr in 
513 
let (defs, vars'), expr = 
514 
normalize_expr 
515 
~alias:true (* forcing introduction of new equations for fcn calls *) 
516 
node 
517 
[] (* empty offset for arrays *) 
518 
([], vars) (* defvar only contains vars *) 
519 
assert_expr 
520 
in 
521 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
522 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
523 
) (vars, [], []) node.node_asserts in 
524 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
525 
vars and initial locals ones *) 
526 

527 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
528 
beginning of the list the 
529 
local declared ones *) 
530 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
531  
532  
533 
(* Updating annotations: traceability and machine types for fresh variables *) 
534 

535 
(* Compute traceability info: 
536 
 gather newly bound variables 
537 
 compute the associated expression without aliases 
538 
*) 
539 
let new_annots = 
540 
if !Options.traces then 
541 
begin 
542 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
543 
let norm_traceability = { 
544 
annots = List.map (fun v > 
545 
let eq = 
546 
try 
547 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
548 
with Not_found > 
549 
( 
550 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
551 
assert false 
552 
) 
553 
in 
554 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
555 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
556 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
557 
(["traceability"], pair) 
558 
) diff_vars; 
559 
annot_loc = Location.dummy_loc 
560 
} 
561 
in 
562 
norm_traceability::node.node_annot 
563 
end 
564 
else 
565 
node.node_annot 
566 
in 
567  
568 
let new_annots = 
569 
List.fold_left (fun annots v > 
570 
if Machine_types.is_active && Machine_types.is_exportable v then 
571 
let typ = Machine_types.get_specified_type v in 
572 
let typ_name = Machine_types.type_name typ in 
573  
574 
let loc = v.var_loc in 
575 
let typ_as_string = 
576 
mkexpr 
577 
loc 
578 
(Expr_const 
579 
(Const_string typ_name)) 
580 
in 
581 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
582 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
583 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
584 
else 
585 
annots 
586 
) new_annots new_locals 
587 
in 
588 
if !Options.spec <> "no" then 
589 
begin 
590 
(* Update mutable fields of eexpr to perform normalization of 
591 
specification. 
592  
593 
Careful: we do not normalize annotations, since they can have the form 
594 
x = (a, b, c) *) 
595 
(* List.iter *) 
596 
(* (fun a > *) 
597 
(* List.iter *) 
598 
(* (fun (_, ann) > normalize_eexpr decls node inputs_outputs ann) *) 
599 
(* a.annots *) 
600 
(* ) *) 
601 
(* node.node_annot; *) 
602 
match node.node_spec with None > ()  Some s > normalize_spec decls node [] s 
603 
end; 
604 

605 

606 
let node = 
607 
{ node with 
608 
node_locals = all_locals; 
609 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
610 
node_asserts = asserts; 
611 
node_annot = new_annots; 
612 
} 
613 
in ((*Printers.pp_node Format.err_formatter node;*) 
614 
node 
615 
) 
616  
617  
618 
let normalize_decl (decls: program) (decl: top_decl) : top_decl = 
619 
match decl.top_decl_desc with 
620 
 Node nd > 
621 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 
622 
Hashtbl.replace Corelang.node_table nd.node_id decl'; 
623 
decl' 
624 
 Open _  ImportedNode _  Const _  TypeDef _ > decl 
625  
626 
let normalize_prog ?(backend="C") decls : program = 
627 
let old_unfold_arrow_active = !unfold_arrow_active in 
628 
let old_force_alias_ite = !force_alias_ite in 
629 
let old_force_alias_internal_fun = !force_alias_internal_fun in 
630 

631 
(* Backend specific configurations for normalization *) 
632 
let _ = 
633 
match backend with 
634 
 "lustre" > 
635 
(* Special treatment of arrows in lustre backend. We want to keep them *) 
636 
unfold_arrow_active := false; 
637 
 "emf" > ( 
638 
(* Forcing ite normalization *) 
639 
force_alias_ite := true; 
640 
force_alias_internal_fun := true; 
641 
) 
642 
 _ > () (* No fancy options for other backends *) 
643 
in 
644  
645 
(* Main algorithm: iterates over nodes *) 
646 
let res = List.map (normalize_decl decls) decls in 
647 

648 
(* Restoring previous settings *) 
649 
unfold_arrow_active := old_unfold_arrow_active; 
650 
force_alias_ite := old_force_alias_ite; 
651 
force_alias_internal_fun := old_force_alias_internal_fun; 
652 
res 
653 

654 
(* Local Variables: *) 
655 
(* compilecommand:"make C .." *) 
656 
(* End: *) 