Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 550e6a83

History | View | Annotate | Download (20.1 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12
open Utils
13
open LustreSpec
14
open Corelang
15
open Format
16
17 27dc3869 ploc
(** 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 non-alias 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 3436d1a6 ploc
let force_alias_internal_fun = ref false
36 27dc3869 ploc
37
  
38 2e6f9ba8 xthirioux
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 a38c681e xthirioux
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
74 2e6f9ba8 xthirioux
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
75
 | _                   -> assert false
76
77 22fe1c93 ploc
let cpt_fresh = ref 0
78
79
(* Generate a new local [node] variable *)
80
let mk_fresh_var node loc ty ck =
81 01c7d5e1 ploc
  let vars = get_node_vars node in
82 22fe1c93 ploc
  let rec aux () =
83
  incr cpt_fresh;
84
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
85
  if List.exists (fun v -> v.var_id = s) vars then aux () else
86
  {
87
    var_id = s;
88 54d032f5 xthirioux
    var_orig = false;
89 22fe1c93 ploc
    var_dec_type = dummy_type_dec;
90
    var_dec_clock = dummy_clock_dec;
91
    var_dec_const = false;
92 ec433d69 xthirioux
    var_dec_value = None;
93 22fe1c93 ploc
    var_type = ty;
94
    var_clock = ck;
95
    var_loc = loc
96
  }
97
  in aux ()
98
99
(* Get the equation in [defs] with [expr] as rhs, if any *)
100
let get_expr_alias defs expr =
101
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
102
 with
103 e49b6d55 xavier.thirioux
 | Not_found -> None
104
  
105 22fe1c93 ploc
(* Replace [expr] with (tuple of) [locals] *)
106
let replace_expr locals expr =
107
 match locals with
108
 | []  -> assert false
109
 | [v] -> { expr with
110
   expr_tag = Utils.new_tag ();
111
   expr_desc = Expr_ident v.var_id }
112
 | _   -> { expr with
113
   expr_tag = Utils.new_tag ();
114 fc886259 xthirioux
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
115 22fe1c93 ploc
116
let unfold_offsets e offsets =
117
  let add_offset e d =
118 fc886259 xthirioux
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
119
    let res = *)
120 22fe1c93 ploc
    { e with
121
      expr_tag = Utils.new_tag ();
122
      expr_loc = d.Dimension.dim_loc;
123
      expr_type = Types.array_element_type e.expr_type;
124 fc886259 xthirioux
      expr_desc = Expr_access (e, d) }
125
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
126
  in
127 22fe1c93 ploc
 List.fold_left add_offset e offsets
128
129
(* Create an alias for [expr], if none exists yet *)
130
let mk_expr_alias node (defs, vars) expr =
131 a38c681e xthirioux
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132 22fe1c93 ploc
  match get_expr_alias defs expr with
133
  | Some eq ->
134
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
135
    (defs, vars), replace_expr aliases expr
136
  | None    ->
137
    let new_aliases =
138
      List.map2
139
	(mk_fresh_var node expr.expr_loc)
140
	(Types.type_list_of_type expr.expr_type)
141
	(Clocks.clock_list_of_clock expr.expr_clock) in
142
    let new_def =
143
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
144 3ca6d126 ploc
    in
145 fc886259 xthirioux
    (* 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; *)
146 3ca6d126 ploc
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
147 22fe1c93 ploc
148 d4807c3d xthirioux
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
149
   and [opt] is true *)
150 04a63d25 xthirioux
let mk_expr_alias_opt opt node (defs, vars) expr =
151
(*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;*)
152 d4807c3d xthirioux
  match expr.expr_desc with
153
  | Expr_ident alias ->
154 04a63d25 xthirioux
    (defs, vars), expr
155 8deaa2dd tkahsai
  | _                ->
156 04a63d25 xthirioux
    match get_expr_alias defs expr with
157
    | Some eq ->
158
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
159
      (defs, vars), replace_expr aliases expr
160
    | None    ->
161
      if opt
162
      then
163
	let new_aliases =
164
	  List.map2
165
	    (mk_fresh_var node expr.expr_loc)
166
	    (Types.type_list_of_type expr.expr_type)
167
	    (Clocks.clock_list_of_clock expr.expr_clock) in
168
	let new_def =
169
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
170
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
171
      else
172
	(defs, vars), expr
173 22fe1c93 ploc
174 8deaa2dd tkahsai
(* Create a (normalized) expression from [ref_e],
175 22fe1c93 ploc
   replacing description with [norm_d],
176 8deaa2dd tkahsai
   taking propagated [offsets] into account
177 22fe1c93 ploc
   in order to change expression type *)
178
let mk_norm_expr offsets ref_e norm_d =
179 e49b6d55 xavier.thirioux
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
180 22fe1c93 ploc
  let drop_array_type ty =
181
    Types.map_tuple_type Types.array_element_type ty in
182
  { ref_e with
183
    expr_desc = norm_d;
184
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
185 e49b6d55 xavier.thirioux
														
186 22fe1c93 ploc
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
187
let rec normalize_list alias node offsets norm_element defvars elist =
188
  List.fold_right
189
    (fun t (defvars, qlist) ->
190
      let defvars, norm_t = norm_element alias node offsets defvars t in
191
      (defvars, norm_t :: qlist)
192
    ) elist (defvars, [])
193
194 0a10042e ploc
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
195 e49b6d55 xavier.thirioux
  (*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;*)
196 22fe1c93 ploc
  match expr.expr_desc with
197 8deaa2dd tkahsai
  | Expr_const _
198 22fe1c93 ploc
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
199
  | Expr_array elist ->
200 0a10042e ploc
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
201
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
202
     mk_expr_alias_opt alias node defvars norm_expr
203 22fe1c93 ploc
  | Expr_power (e1, d) when offsets = [] ->
204 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
205
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
206
     mk_expr_alias_opt alias node defvars norm_expr
207 22fe1c93 ploc
  | Expr_power (e1, d) ->
208 0a10042e ploc
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
209 22fe1c93 ploc
  | Expr_access (e1, d) ->
210 0a10042e ploc
     normalize_expr ~alias:alias node (d::offsets) defvars e1
211 8deaa2dd tkahsai
  | Expr_tuple elist ->
212 0a10042e ploc
     let defvars, norm_elist =
213
       normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
214
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
215 8deaa2dd tkahsai
  | Expr_appl (id, args, None)
216 04a63d25 xthirioux
      when Basic_library.is_homomorphic_fun id 
217 af5af1e8 ploc
	&& Types.is_array_type expr.expr_type ->
218 0a10042e ploc
     let defvars, norm_args =
219
       normalize_list
220
	 alias
221
	 node
222
	 offsets
223
	 (fun _ -> normalize_array_expr ~alias:true)
224
	 defvars
225
	 (expr_list_of_expr args)
226
     in
227
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
228 3436d1a6 ploc
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
229 0a10042e ploc
      && not (!force_alias_internal_fun || alias_basic) ->
230
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
231
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
232 22fe1c93 ploc
  | Expr_appl (id, args, r) ->
233 0a10042e ploc
     let defvars, r =
234
       match r with
235
       | None -> defvars, None
236
       | Some r ->
237
	  let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in
238
	  defvars, Some norm_r
239
     in
240
     let defvars, norm_args = normalize_expr node [] defvars args in
241
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
242
     if offsets <> []
243
     then
244
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
245
       normalize_expr ~alias:alias node offsets defvars norm_expr
246
     else
247
       mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
248
				    || not (Basic_library.is_expr_internal_fun expr)))
249
	 node defvars norm_expr
250 5fb5b031 Ploc
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
251 0a10042e ploc
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
252
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
253 2e6f9ba8 xthirioux
  | Expr_arrow (e1,e2) ->
254 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
255
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
256
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
257
     mk_expr_alias_opt alias node defvars norm_expr
258 22fe1c93 ploc
  | Expr_pre e ->
259 0a10042e ploc
     let defvars, norm_e = normalize_expr node offsets defvars e in
260
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
261
     mk_expr_alias_opt alias node defvars norm_expr
262 22fe1c93 ploc
  | Expr_fby (e1, e2) ->
263 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
264
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
265
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
266
     mk_expr_alias_opt alias node defvars norm_expr
267 22fe1c93 ploc
  | Expr_when (e, c, l) ->
268 0a10042e ploc
     let defvars, norm_e = normalize_expr node offsets defvars e in
269
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
270 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
271 0a10042e ploc
     let defvars, norm_c = normalize_guard node defvars c in
272
     let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
273
     let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
274
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
275
     mk_expr_alias_opt alias node defvars norm_expr
276 22fe1c93 ploc
  | Expr_merge (c, hl) ->
277 0a10042e ploc
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
278
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
279
     mk_expr_alias_opt alias node defvars norm_expr
280 8deaa2dd tkahsai
281 52cfee34 xthirioux
(* Creates a conditional with a merge construct, which is more lazy *)
282
(*
283 0a10042e ploc
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
284
  match expr.expr_desc with
285
  | Expr_ite (c, t, e) ->
286
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
287
  | _ -> assert false
288 52cfee34 xthirioux
*)
289 22fe1c93 ploc
and normalize_branches node offsets defvars hl =
290 0a10042e ploc
  List.fold_right
291
    (fun (t, h) (defvars, norm_q) ->
292
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
293
      defvars, (t, norm_h) :: norm_q
294
    )
295
    hl (defvars, [])
296 22fe1c93 ploc
297
and normalize_array_expr ?(alias=true) node offsets defvars expr =
298 04a63d25 xthirioux
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
299 22fe1c93 ploc
  match expr.expr_desc with
300
  | Expr_power (e1, d) when offsets = [] ->
301 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
302
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
303 22fe1c93 ploc
  | Expr_power (e1, d) ->
304 0a10042e ploc
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
305 22fe1c93 ploc
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
306
  | Expr_array elist when offsets = [] ->
307 0a10042e ploc
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
308
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
309 04a63d25 xthirioux
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
310 0a10042e ploc
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
311
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
312 22fe1c93 ploc
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
313
314
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
315
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
316
  match expr.expr_desc with
317
  | Expr_access (e1, d) ->
318 0a10042e ploc
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
319 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
320 0a10042e ploc
     let defvars, norm_c = normalize_guard node defvars c in
321
     let defvars, norm_t = normalize_cond_expr node offsets defvars t in
322
     let defvars, norm_e = normalize_cond_expr node offsets defvars e in
323
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
324 22fe1c93 ploc
  | Expr_merge (c, hl) ->
325 0a10042e ploc
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
326
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
327 27dc3869 ploc
  | _ when !force_alias_ite ->
328
     (* Forcing alias creation for then/else expressions *)
329
     let defvars, norm_expr =
330
       normalize_expr ~alias:alias node offsets defvars expr
331
     in
332
     mk_expr_alias_opt true node defvars norm_expr
333
  | _ -> (* default case without the force_alias_ite option *)
334
     normalize_expr ~alias:alias node offsets defvars expr
335 0a10042e ploc
       
336 22fe1c93 ploc
and normalize_guard node defvars expr =
337 0a10042e ploc
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
338 d4807c3d xthirioux
  mk_expr_alias_opt true node defvars norm_expr
339 22fe1c93 ploc
340
(* outputs cannot be memories as well. If so, introduce new local variable.
341
*)
342
let decouple_outputs node defvars eq =
343
  let rec fold_lhs defvars lhs tys cks =
344
   match lhs, tys, cks with
345
   | [], [], []          -> defvars, []
346
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
347
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
348
			    then
349
			      let newvar = mk_fresh_var node eq.eq_loc t c in
350 fc886259 xthirioux
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
351 22fe1c93 ploc
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
352
			    else
353
			      (defs_q, vars_q), v::lhs_q
354
   | _                   -> assert false in
355
  let defvars', lhs' =
356
    fold_lhs
357
      defvars
358
      eq.eq_lhs
359
      (Types.type_list_of_type eq.eq_rhs.expr_type)
360
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
361
  defvars', {eq with eq_lhs = lhs' }
362
363 8deaa2dd tkahsai
let rec normalize_eq node defvars eq =
364 04a63d25 xthirioux
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
365 22fe1c93 ploc
  match eq.eq_rhs.expr_desc with
366
  | Expr_pre _
367
  | Expr_fby _  ->
368
    let (defvars', eq') = decouple_outputs node defvars eq in
369
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
370
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
371
    (norm_eq::defs', vars')
372
  | Expr_array _ ->
373
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
374
    let norm_eq = { eq with eq_rhs = norm_rhs } in
375
    (norm_eq::defs', vars')
376 04a63d25 xthirioux
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
377 22fe1c93 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
378
    let norm_eq = { eq with eq_rhs = norm_rhs } in
379
    (norm_eq::defs', vars')
380
  | Expr_appl _ ->
381
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
382
    let norm_eq = { eq with eq_rhs = norm_rhs } in
383
    (norm_eq::defs', vars')
384
  | _ ->
385
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
386
    let norm_eq = { eq with eq_rhs = norm_rhs } in
387
    norm_eq::defs', vars'
388
389 8deaa2dd tkahsai
(** normalize_node node returns a normalized node,
390
    ie.
391 af5af1e8 ploc
    - updated locals
392
    - new equations
393 8deaa2dd tkahsai
    -
394 af5af1e8 ploc
*)
395 8deaa2dd tkahsai
let normalize_node node =
396 22fe1c93 ploc
  cpt_fresh := 0;
397
  let inputs_outputs = node.node_inputs@node.node_outputs in
398
  let is_local v =
399
    List.for_all ((!=) v) inputs_outputs in
400 af5af1e8 ploc
  let orig_vars = inputs_outputs@node.node_locals in
401 8deaa2dd tkahsai
  let defs, vars =
402 b08ffca7 xthirioux
    List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
403 af5af1e8 ploc
  (* Normalize the asserts *)
404 8deaa2dd tkahsai
  let vars, assert_defs, asserts =
405 af5af1e8 ploc
    List.fold_left (
406
    fun (vars, def_accu, assert_accu) assert_ ->
407
      let assert_expr = assert_.assert_expr in
408 04a63d25 xthirioux
      let (defs, vars'), expr = 
409
	normalize_expr 
410 728be1e1 ploc
	  ~alias:true (* forcing introduction of new equations for fcn calls *) 
411 04a63d25 xthirioux
	  node 
412 af5af1e8 ploc
	  [] (* empty offset for arrays *)
413
	  ([], vars) (* defvar only contains vars *)
414
	  assert_expr
415
      in
416 8deaa2dd tkahsai
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
417 af5af1e8 ploc
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
418
    ) (vars, [], []) node.node_asserts in
419 22fe1c93 ploc
  let new_locals = List.filter is_local vars in
420 8deaa2dd tkahsai
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
421 f2b1c245 ploc
422 ea1c2906 ploc
  let new_annots =
423
    if !Options.traces then
424
      begin
425 8deaa2dd tkahsai
	(* Compute traceability info:
426 ea1c2906 ploc
	   - gather newly bound variables
427 8deaa2dd tkahsai
	   - compute the associated expression without aliases
428 ea1c2906 ploc
	*)
429
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
430
	let norm_traceability = {
431
	  annots = List.map (fun v ->
432
	    let eq =
433
	      try
434 45f0f48d xthirioux
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
435
	      with Not_found -> 
436
		(
437
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
438
		  assert false
439
		) 
440
	    in
441 b98a4a58 ploc
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
442 ea1c2906 ploc
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
443
	    (["traceability"], pair)
444
	  ) diff_vars;
445
	  annot_loc = Location.dummy_loc
446 8deaa2dd tkahsai
	}
447 ea1c2906 ploc
	in
448
	norm_traceability::node.node_annot
449
      end
450
    else
451
      node.node_annot
452 af5af1e8 ploc
  in
453 ea1c2906 ploc
454 22fe1c93 ploc
  let node =
455 8deaa2dd tkahsai
  { node with
456
    node_locals = new_locals;
457 b08ffca7 xthirioux
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
458 af5af1e8 ploc
    node_asserts = asserts;
459 ea1c2906 ploc
    node_annot = new_annots;
460 af5af1e8 ploc
  }
461 8deaa2dd tkahsai
  in ((*Printers.pp_node Format.err_formatter node;*)
462 f2b1c245 ploc
    node
463
)
464
465 22fe1c93 ploc
466
let normalize_decl decl =
467
  match decl.top_decl_desc with
468
  | Node nd ->
469 f2b1c245 ploc
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
470
    Hashtbl.replace Corelang.node_table nd.node_id decl';
471
    decl'
472 ef34b4ae xthirioux
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
473 8deaa2dd tkahsai
474 27dc3869 ploc
let normalize_prog ?(backend="C") decls =
475
  let old_unfold_arrow_active = !unfold_arrow_active in
476
  let old_force_alias_ite = !force_alias_ite in
477 3436d1a6 ploc
  let old_force_alias_internal_fun = !force_alias_internal_fun in
478 27dc3869 ploc
  
479
  (* Backend specific configurations for normalization *)
480
  let _ =
481
    match backend with
482
    | "lustre" ->
483
    (* Special treatment of arrows in lustre backend. We want to keep them *)
484
       unfold_arrow_active := false;
485 3436d1a6 ploc
    | "emf" -> (
486
       (* Forcing ite normalization *)
487
      force_alias_ite := true;
488
      force_alias_internal_fun := true;
489
    )
490 27dc3869 ploc
    | _ -> () (* No fancy options for other backends *)
491
  in
492 22fe1c93 ploc
493 27dc3869 ploc
  (* Main algorithm: iterates over nodes *)
494
  let res = List.map normalize_decl decls in
495
  
496
  (* Restoring previous settings *)
497
  unfold_arrow_active := old_unfold_arrow_active;
498
  force_alias_ite := old_force_alias_ite;
499 3436d1a6 ploc
  force_alias_internal_fun := old_force_alias_internal_fun;
500 27dc3869 ploc
  res
501
  
502
  (* Local Variables: *)
503 22fe1c93 ploc
(* compile-command:"make -C .." *)
504
(* End: *)