Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 0bd19a92

History | View | Annotate | Download (20.9 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 8446bf03 ploc
open Lustre_types
14 22fe1c93 ploc
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
78
79
(* Get the equation in [defs] with [expr] as rhs, if any *)
80
let get_expr_alias defs expr =
81 0bd19a92 THIRIOUX Xavier
 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 22fe1c93 ploc
 with
83 e49b6d55 xavier.thirioux
 | Not_found -> None
84
  
85 22fe1c93 ploc
(* 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 fc886259 xthirioux
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
95 22fe1c93 ploc
96
let unfold_offsets e offsets =
97
  let add_offset e d =
98 fc886259 xthirioux
(*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 22fe1c93 ploc
    { 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 fc886259 xthirioux
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
107 22fe1c93 ploc
 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 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;*)
112 22fe1c93 ploc
  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 3ca6d126 ploc
    in
125 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; *)
126 3ca6d126 ploc
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127 22fe1c93 ploc
128 d4807c3d xthirioux
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129
   and [opt] is true *)
130 04a63d25 xthirioux
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 d4807c3d xthirioux
  match expr.expr_desc with
133
  | Expr_ident alias ->
134 04a63d25 xthirioux
    (defs, vars), expr
135 8deaa2dd tkahsai
  | _                ->
136 04a63d25 xthirioux
    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 66359a5e ploc
	in
151
	(* Typing and Registering machine type *) 
152 f4050bef ploc
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
153 66359a5e ploc
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
154 04a63d25 xthirioux
      else
155
	(defs, vars), expr
156 22fe1c93 ploc
157 8deaa2dd tkahsai
(* Create a (normalized) expression from [ref_e],
158 22fe1c93 ploc
   replacing description with [norm_d],
159 8deaa2dd tkahsai
   taking propagated [offsets] into account
160 22fe1c93 ploc
   in order to change expression type *)
161
let mk_norm_expr offsets ref_e norm_d =
162 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};*)
163 22fe1c93 ploc
  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 e49b6d55 xavier.thirioux
														
169 22fe1c93 ploc
(* 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 0a10042e ploc
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
178 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;*)
179 22fe1c93 ploc
  match expr.expr_desc with
180 8deaa2dd tkahsai
  | Expr_const _
181 22fe1c93 ploc
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
182
  | Expr_array elist ->
183 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_power (e1, d) when offsets = [] ->
187 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_power (e1, d) ->
191 0a10042e ploc
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
192 22fe1c93 ploc
  | Expr_access (e1, d) ->
193 0a10042e ploc
     normalize_expr ~alias:alias node (d::offsets) defvars e1
194 8deaa2dd tkahsai
  | Expr_tuple elist ->
195 0a10042e ploc
     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 8deaa2dd tkahsai
  | Expr_appl (id, args, None)
199 04a63d25 xthirioux
      when Basic_library.is_homomorphic_fun id 
200 af5af1e8 ploc
	&& Types.is_array_type expr.expr_type ->
201 0a10042e ploc
     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 3436d1a6 ploc
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
212 0a10042e ploc
      && 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 22fe1c93 ploc
  | Expr_appl (id, args, r) ->
216 0a10042e ploc
     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 5fb5b031 Ploc
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
234 0a10042e ploc
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
235
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
236 2e6f9ba8 xthirioux
  | Expr_arrow (e1,e2) ->
237 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_pre e ->
242 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_fby (e1, e2) ->
246 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_when (e, c, l) ->
251 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
254 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_merge (c, hl) ->
260 0a10042e ploc
     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 8deaa2dd tkahsai
264 52cfee34 xthirioux
(* Creates a conditional with a merge construct, which is more lazy *)
265
(*
266 0a10042e ploc
  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 52cfee34 xthirioux
*)
272 22fe1c93 ploc
and normalize_branches node offsets defvars hl =
273 0a10042e ploc
  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 22fe1c93 ploc
280
and normalize_array_expr ?(alias=true) node offsets defvars expr =
281 04a63d25 xthirioux
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
282 22fe1c93 ploc
  match expr.expr_desc with
283
  | Expr_power (e1, d) when offsets = [] ->
284 0a10042e ploc
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
285
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
286 22fe1c93 ploc
  | Expr_power (e1, d) ->
287 0a10042e ploc
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
288 22fe1c93 ploc
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
289
  | Expr_array elist when offsets = [] ->
290 0a10042e ploc
     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 04a63d25 xthirioux
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
293 0a10042e ploc
     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 22fe1c93 ploc
  |  _ -> 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 0a10042e ploc
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
302 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
303 0a10042e ploc
     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 22fe1c93 ploc
  | Expr_merge (c, hl) ->
308 0a10042e ploc
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
309
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
310 27dc3869 ploc
  | _ 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 0a10042e ploc
       
319 22fe1c93 ploc
and normalize_guard node defvars expr =
320 0a10042e ploc
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
321 d4807c3d xthirioux
  mk_expr_alias_opt true node defvars norm_expr
322 22fe1c93 ploc
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 fc886259 xthirioux
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
334 22fe1c93 ploc
			      (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 8deaa2dd tkahsai
let rec normalize_eq node defvars eq =
347 04a63d25 xthirioux
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
348 22fe1c93 ploc
  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 04a63d25 xthirioux
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
360 22fe1c93 ploc
    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 8deaa2dd tkahsai
(** normalize_node node returns a normalized node,
373
    ie.
374 af5af1e8 ploc
    - updated locals
375
    - new equations
376 8deaa2dd tkahsai
    -
377 af5af1e8 ploc
*)
378 8deaa2dd tkahsai
let normalize_node node =
379 7065d912 ploc
  reset_cpt_fresh ();
380 22fe1c93 ploc
  let inputs_outputs = node.node_inputs@node.node_outputs in
381 af5af1e8 ploc
  let orig_vars = inputs_outputs@node.node_locals in
382 50dadc21 ploc
  let not_is_orig_var v =
383
    List.for_all ((!=) v) orig_vars in
384 8deaa2dd tkahsai
  let defs, vars =
385 333e3a25 ploc
    let eqs, auts = get_node_eqs node in
386
    if auts != [] then assert false; (* Automata should be expanded by now. *)
387
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
388 af5af1e8 ploc
  (* Normalize the asserts *)
389 8deaa2dd tkahsai
  let vars, assert_defs, asserts =
390 af5af1e8 ploc
    List.fold_left (
391 50dadc21 ploc
      fun (vars, def_accu, assert_accu) assert_ ->
392
	let assert_expr = assert_.assert_expr in
393
	let (defs, vars'), expr = 
394
	  normalize_expr 
395
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
396
	    node 
397
	    [] (* empty offset for arrays *)
398
	    ([], vars) (* defvar only contains vars *)
399
	    assert_expr
400
	in
401 8deaa2dd tkahsai
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
402 50dadc21 ploc
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
403 af5af1e8 ploc
    ) (vars, [], []) node.node_asserts in
404 50dadc21 ploc
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
405
							  vars and initial locals ones *)
406 66359a5e ploc
  
407
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
408 50dadc21 ploc
						       beginning of the list the
409
						       local declared ones *)
410 8deaa2dd tkahsai
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
411 f2b1c245 ploc
412 66359a5e ploc
413
  (* Updating annotations: traceability and machine types for fresh variables *)
414
  
415
  (* Compute traceability info:
416
     - gather newly bound variables
417
     - compute the associated expression without aliases
418
  *)
419 ea1c2906 ploc
  let new_annots =
420
    if !Options.traces then
421
      begin
422 66359a5e ploc
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
423 ea1c2906 ploc
	let norm_traceability = {
424
	  annots = List.map (fun v ->
425
	    let eq =
426
	      try
427 45f0f48d xthirioux
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
428
	      with Not_found -> 
429
		(
430
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
431
		  assert false
432
		) 
433
	    in
434 b98a4a58 ploc
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
435 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
436 66359a5e ploc
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
437 ea1c2906 ploc
	    (["traceability"], pair)
438
	  ) diff_vars;
439
	  annot_loc = Location.dummy_loc
440 8deaa2dd tkahsai
	}
441 ea1c2906 ploc
	in
442
	norm_traceability::node.node_annot
443
      end
444
    else
445
      node.node_annot
446 af5af1e8 ploc
  in
447 ea1c2906 ploc
448 66359a5e ploc
  let new_annots =
449
    List.fold_left (fun annots v ->
450 f4050bef ploc
      if Machine_types.is_active && Machine_types.is_exportable v then
451 66359a5e ploc
	let typ = Machine_types.get_specified_type v in
452
  	let typ_name = Machine_types.type_name typ in
453
454
	let loc = v.var_loc in
455
	let typ_as_string =
456
	  mkexpr
457
	    loc
458
	    (Expr_const
459
	       (Const_string typ_name))
460
	in
461
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
462
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
463
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
464
      else
465
	annots
466
    ) new_annots new_locals
467
  in
468 22fe1c93 ploc
  let node =
469 50dadc21 ploc
    { node with
470 66359a5e ploc
      node_locals = all_locals;
471 50dadc21 ploc
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
472
      node_asserts = asserts;
473
      node_annot = new_annots;
474
    }
475 8deaa2dd tkahsai
  in ((*Printers.pp_node Format.err_formatter node;*)
476 f2b1c245 ploc
    node
477 50dadc21 ploc
  )
478 f2b1c245 ploc
479 22fe1c93 ploc
480
let normalize_decl decl =
481
  match decl.top_decl_desc with
482
  | Node nd ->
483 f2b1c245 ploc
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
484
    Hashtbl.replace Corelang.node_table nd.node_id decl';
485
    decl'
486 ef34b4ae xthirioux
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
487 8deaa2dd tkahsai
488 27dc3869 ploc
let normalize_prog ?(backend="C") decls =
489
  let old_unfold_arrow_active = !unfold_arrow_active in
490
  let old_force_alias_ite = !force_alias_ite in
491 3436d1a6 ploc
  let old_force_alias_internal_fun = !force_alias_internal_fun in
492 27dc3869 ploc
  
493
  (* Backend specific configurations for normalization *)
494
  let _ =
495
    match backend with
496
    | "lustre" ->
497
    (* Special treatment of arrows in lustre backend. We want to keep them *)
498
       unfold_arrow_active := false;
499 3436d1a6 ploc
    | "emf" -> (
500
       (* Forcing ite normalization *)
501
      force_alias_ite := true;
502
      force_alias_internal_fun := true;
503
    )
504 27dc3869 ploc
    | _ -> () (* No fancy options for other backends *)
505
  in
506 22fe1c93 ploc
507 27dc3869 ploc
  (* Main algorithm: iterates over nodes *)
508
  let res = List.map normalize_decl decls in
509
  
510
  (* Restoring previous settings *)
511
  unfold_arrow_active := old_unfold_arrow_active;
512
  force_alias_ite := old_force_alias_ite;
513 3436d1a6 ploc
  force_alias_internal_fun := old_force_alias_internal_fun;
514 27dc3869 ploc
  res
515
  
516
  (* Local Variables: *)
517 22fe1c93 ploc
(* compile-command:"make -C .." *)
518
(* End: *)