lustrec / src / normalization.ml @ 95944ba1
History  View  Annotate  Download (27.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 
type param_t = 
33 
{ 
34 
unfold_arrow_active: bool; 
35 
force_alias_ite: bool; 
36 
force_alias_internal_fun: bool; 
37 
} 
38  
39 
let params = ref 
40 
{ 
41 
unfold_arrow_active = false; 
42 
force_alias_ite = false; 
43 
force_alias_internal_fun =false; 
44 
} 
45  
46 
type norm_ctx_t = 
47 
{ 
48 
parentid: ident; 
49 
vars: var_decl list; 
50 
is_output: ident > bool; 
51 
} 
52  
53 

54 
let expr_true loc ck = 
55 
{ expr_tag = Utils.new_tag (); 
56 
expr_desc = Expr_const (Const_tag tag_true); 
57 
expr_type = Type_predef.type_bool; 
58 
expr_clock = ck; 
59 
expr_delay = Delay.new_var (); 
60 
expr_annot = None; 
61 
expr_loc = loc } 
62  
63 
let expr_false loc ck = 
64 
{ expr_tag = Utils.new_tag (); 
65 
expr_desc = Expr_const (Const_tag tag_false); 
66 
expr_type = Type_predef.type_bool; 
67 
expr_clock = ck; 
68 
expr_delay = Delay.new_var (); 
69 
expr_annot = None; 
70 
expr_loc = loc } 
71  
72 
let expr_once loc ck = 
73 
{ expr_tag = Utils.new_tag (); 
74 
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); 
75 
expr_type = Type_predef.type_bool; 
76 
expr_clock = ck; 
77 
expr_delay = Delay.new_var (); 
78 
expr_annot = None; 
79 
expr_loc = loc } 
80  
81 
let is_expr_once = 
82 
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in 
83 
fun expr > Corelang.is_eq_expr expr dummy_expr_once 
84  
85 
let unfold_arrow expr = 
86 
match expr.expr_desc with 
87 
 Expr_arrow (e1, e2) > 
88 
let loc = expr.expr_loc in 
89 
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in 
90 
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } 
91 
 _ > assert false 
92  
93  
94  
95 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
96 
let get_expr_alias defs expr = 
97 
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) 
98 
with 
99 
 Not_found > None 
100 

101 
(* Replace [expr] with (tuple of) [locals] *) 
102 
let replace_expr locals expr = 
103 
match locals with 
104 
 [] > assert false 
105 
 [v] > { expr with 
106 
expr_tag = Utils.new_tag (); 
107 
expr_desc = Expr_ident v.var_id } 
108 
 _ > { expr with 
109 
expr_tag = Utils.new_tag (); 
110 
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } 
111  
112 
let unfold_offsets e offsets = 
113 
let add_offset e d = 
114 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; 
115 
let res = *) 
116 
{ e with 
117 
expr_tag = Utils.new_tag (); 
118 
expr_loc = d.Dimension.dim_loc; 
119 
expr_type = Types.array_element_type e.expr_type; 
120 
expr_desc = Expr_access (e, d) } 
121 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 
122 
in 
123 
List.fold_left add_offset e offsets 
124  
125 
(* IS IT USED ? TODO 
126 
(* Create an alias for [expr], if none exists yet *) 
127 
let mk_expr_alias (parentid, vars) (defs, vars) expr = 
128 
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) 
129 
match get_expr_alias defs expr with 
130 
 Some eq > 
131 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
132 
(defs, vars), replace_expr aliases expr 
133 
 None > 
134 
let new_aliases = 
135 
List.map2 
136 
(mk_fresh_var (parentid, vars) expr.expr_loc) 
137 
(Types.type_list_of_type expr.expr_type) 
138 
(Clocks.clock_list_of_clock expr.expr_clock) in 
139 
let new_def = 
140 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
141 
in 
142 
(* 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; *) 
143 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
144 
*) 
145 

146 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
147 
and [opt] is true *) 
148 
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = 
149 
(*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;*) 
150 
match expr.expr_desc with 
151 
 Expr_ident alias > 
152 
(defs, vars), expr 
153 
 _ > 
154 
match get_expr_alias defs expr with 
155 
 Some eq > 
156 
(* Format.eprintf "Found a preexisting definition@."; *) 
157 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
158 
(defs, vars), replace_expr aliases expr 
159 
 None > 
160 
(* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; 
161 
* Format.eprintf "existing defs are: @[[%a@]]@." 
162 
* (fprintf_list ~sep:"@ "(fun fmt eq > 
163 
* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a" 
164 
* Clocks.print_ck eq.eq_rhs.expr_clock 
165 
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) 
166 
* (is_eq_expr eq.eq_rhs expr) 
167 
* Printers.pp_node_eq eq)) 
168 
* defs; *) 
169 
if opt 
170 
then 
171 
let new_aliases = 
172 
List.map2 
173 
(mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc) 
174 
(Types.type_list_of_type expr.expr_type) 
175 
(Clocks.clock_list_of_clock expr.expr_clock) in 
176 
let new_def = 
177 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
178 
in 
179 
(* Typing and Registering machine type *) 
180 
let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr in 
181 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
182 
else 
183 
(defs, vars), expr 
184  
185 
(* Create a (normalized) expression from [ref_e], 
186 
replacing description with [norm_d], 
187 
taking propagated [offsets] into account 
188 
in order to change expression type *) 
189 
let mk_norm_expr offsets ref_e norm_d = 
190 
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) 
191 
let drop_array_type ty = 
192 
Types.map_tuple_type Types.array_element_type ty in 
193 
{ ref_e with 
194 
expr_desc = norm_d; 
195 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
196 

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

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

431 
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
432 
(* Calls are first inlined *) 
433 
let nodes = get_nodes decls in 
434 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 
435 
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes 
436 
let calls = List.map 
437 
(fun called_nd > List.find (fun nd2 > nd2.node_id = called_nd) nodes) calls 
438 
in 
439 
*) 
440 
(*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; *) 
441 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in 
442 
let locals = node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in 
443 
let (new_locals, eqs) = 
444 
if calls = [] && not (eq_has_arrows eq) then 
445 
(locals, [eq]) 
446 
else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *) 
447 
(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in 
448 
(*Format.eprintf "eqs %a@.@?" 
449 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *) 
450 
(new_locals, eqs) 
451 
*) 
452 
(locals, [eq]) 
453 

454 
) in 
455 
(* Normalizing expr and eqs *) 
456 
let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in 
457 
let todefine = List.fold_left 
458 
(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) 
459 
(ISet.add output_id ISet.empty) vars in 
460 

461 
try 
462 
let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in 
463 
let env = Typing.type_var_decl [] env output_var in (* typing the variable *) 
464 
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) 
465 
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in 
466 
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*) 
467 
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in 
468 
(* check that table is empty *) 
469 
if (not (ISet.is_empty undefined_vars)) then 
470 
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars)); 
471 

472 
(*Format.eprintf "normalized eqs %a@.@?" 
473 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) 
474 
ee.eexpr_normalized < Some (output_var, defs, vars) 
475 

476 
with (Types.Error (loc,err)) as exc > 
477 
eprintf "Typing error for eexpr %a: %a%a%a@." 
478 
Printers.pp_eexpr ee 
479 
Types.pp_error err 
480 
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs 
481 
Location.pp_loc loc 
482 

483 

484 
; 
485 
raise exc 
486 
*) 
487 

488 

489 
let normalize_spec decls iovars s = s (* 
490 
(* Each stmt is normalized *) 
491 
let orig_vars = iovars @ s.locals in 
492 
let not_is_orig_var v = 
493 
List.for_all ((!=) v) orig_vars in 
494 
let defs, vars = 
495 
let eqs, auts = List.fold_right (fun (el,al) s > match s with Eq e > e::el, al  Aut a > el, a::al) s.stmts ([], []) in 
496 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
497 
List.fold_left (normalize_eq node) ([], orig_vars) eqs 
498 
in 
499 
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) 
500  
501 
(* 
502 

503 
{s with 
504 
locals = s.locals @ new_locals; 
505 
stmts = List.map (fun eq > Eq eq) defs; 
506 
let nee _ = () in 
507 
(*normalize_eexpr decls iovars in *) 
508 
List.iter nee s.assume; 
509 
List.iter nee s.guarantees; 
510 
List.iter (fun m > 
511 
List.iter nee m.require; 
512 
List.iter nee m.ensure 
513 
) s.modes; 
514 
*) 
515 
s 
516 
*) 
517 

518 
(* The normalization phase introduces new local variables 
519 
 output cannot be memories. If this happen, new local variables acting as 
520 
memories are introduced. 
521 
 array constants, pre, arrow, fby, ite, merge, calls to node with index 
522 
access 
523 
Thoses values are shared, ie. no duplicate expressions are introduced. 
524  
525 
Concerning specification, a similar process is applied, replacing an 
526 
expression by a list of local variables and definitions 
527 
*) 
528  
529 
(** normalize_node node returns a normalized node, 
530 
ie. 
531 
 updated locals 
532 
 new equations 
533 
 
534 
*) 
535 
let normalize_node decls node = 
536 
reset_cpt_fresh (); 
537 
let inputs_outputs = node.node_inputs@node.node_outputs in 
538 
let orig_vars = inputs_outputs@node.node_locals in 
539 
let not_is_orig_var v = 
540 
List.for_all ((!=) v) orig_vars in 
541 
let norm_ctx = { 
542 
parentid = node.node_id; 
543 
vars = get_node_vars node; 
544 
is_output = (fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs); 
545 
} 
546 
in 
547 

548 
let defs, vars = 
549 
let eqs, auts = get_node_eqs node in 
550 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
551 
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in 
552 
(* Normalize the asserts *) 
553 
let vars, assert_defs, asserts = 
554 
List.fold_left ( 
555 
fun (vars, def_accu, assert_accu) assert_ > 
556 
let assert_expr = assert_.assert_expr in 
557 
let (defs, vars'), expr = 
558 
normalize_expr 
559 
~alias:true (* forcing introduction of new equations for fcn calls *) 
560 
norm_ctx 
561 
[] (* empty offset for arrays *) 
562 
([], vars) (* defvar only contains vars *) 
563 
assert_expr 
564 
in 
565 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
566 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 
567 
) (vars, [], []) node.node_asserts in 
568 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 
569 
vars and initial locals ones *) 
570 

571 
let all_locals = node.node_locals @ new_locals in (* we add again, at the 
572 
beginning of the list the 
573 
local declared ones *) 
574 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
575  
576  
577 
(* Updating annotations: traceability and machine types for fresh variables *) 
578 

579 
(* Compute traceability info: 
580 
 gather newly bound variables 
581 
 compute the associated expression without aliases 
582 
*) 
583 
let new_annots = 
584 
if !Options.traces then 
585 
begin 
586 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in 
587 
let norm_traceability = { 
588 
annots = List.map (fun v > 
589 
let eq = 
590 
try 
591 
List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
592 
with Not_found > 
593 
( 
594 
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
595 
assert false 
596 
) 
597 
in 
598 
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in 
599 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
600 
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; 
601 
(["traceability"], pair) 
602 
) diff_vars; 
603 
annot_loc = Location.dummy_loc 
604 
} 
605 
in 
606 
norm_traceability::node.node_annot 
607 
end 
608 
else 
609 
node.node_annot 
610 
in 
611  
612 
let new_annots = 
613 
List.fold_left (fun annots v > 
614 
if Machine_types.is_active && Machine_types.is_exportable v then 
615 
let typ = Machine_types.get_specified_type v in 
616 
let typ_name = Machine_types.type_name typ in 
617  
618 
let loc = v.var_loc in 
619 
let typ_as_string = 
620 
mkexpr 
621 
loc 
622 
(Expr_const 
623 
(Const_string typ_name)) 
624 
in 
625 
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in 
626 
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; 
627 
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots 
628 
else 
629 
annots 
630 
) new_annots new_locals 
631 
in 
632 
let spec = 
633 
begin 
634 
(* Update mutable fields of eexpr to perform normalization of 
635 
specification. 
636  
637 
Careful: we do not normalize annotations, since they can have the form 
638 
x = (a, b, c) *) 
639 
match node.node_spec with None > None  Some s > Some (normalize_spec decls inputs_outputs s) 
640 
end 
641 
in 
642 

643 

644 
let node = 
645 
{ node with 
646 
node_locals = all_locals; 
647 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
648 
node_asserts = asserts; 
649 
node_annot = new_annots; 
650 
node_spec = spec; 
651 
} 
652 
in ((*Printers.pp_node Format.err_formatter node;*) 
653 
node 
654 
) 
655  
656 
let normalize_inode decls nd = 
657 
reset_cpt_fresh (); 
658 
match nd.nodei_spec with 
659 
None > nd 
660 
 Some s > 
661 
let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in 
662 
let s = normalize_spec decls inputs_outputs s in 
663 
{ nd with nodei_spec = Some s } 
664 

665 
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl = 
666 
match decl.top_decl_desc with 
667 
 Node nd > 
668 
let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in 
669 
update_node nd.node_id decl'; 
670 
decl' 
671 
 ImportedNode nd > 
672 
let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in 
673 
update_node nd.nodei_id decl'; 
674 
decl' 
675 

676 
 Include _ Open _  Const _  TypeDef _ > decl 
677  
678 
let normalize_prog p decls = 
679 
(* Backend specific configurations for normalization *) 
680 
params := p; 
681  
682 
(* Main algorithm: iterates over nodes *) 
683 
List.map (normalize_decl decls) decls 
684  
685  
686 
(* Fake interface for outside uses *) 
687 
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = 
688 
mk_expr_alias_opt 
689 
opt 
690 
{parentid = parentid; vars = ctx_vars; is_output = (fun _ > false) } 
691 
(defs, vars) 
692 
expr 
693  
694 

695 
(* Local Variables: *) 
696 
(* compilecommand:"make C .." *) 
697 
(* End: *) 
698 
