Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 0bd19a92

History | View | Annotate | Download (20.9 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 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
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
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
139
      (defs, vars), replace_expr aliases expr
140
    | None    ->
141
      if opt
142
      then
143
	let new_aliases =
144
	  List.map2
145
	    (mk_fresh_var node expr.expr_loc)
146
	    (Types.type_list_of_type expr.expr_type)
147
	    (Clocks.clock_list_of_clock expr.expr_clock) in
148
	let new_def =
149
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
150
	in
151
	(* Typing and Registering machine type *) 
152
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
153
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
154
      else
155
	(defs, vars), expr
156

    
157
(* Create a (normalized) expression from [ref_e],
158
   replacing description with [norm_d],
159
   taking propagated [offsets] into account
160
   in order to change expression type *)
161
let mk_norm_expr offsets ref_e norm_d =
162
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
163
  let drop_array_type ty =
164
    Types.map_tuple_type Types.array_element_type ty in
165
  { ref_e with
166
    expr_desc = norm_d;
167
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
168
														
169
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
170
let rec normalize_list alias node offsets norm_element defvars elist =
171
  List.fold_right
172
    (fun t (defvars, qlist) ->
173
      let defvars, norm_t = norm_element alias node offsets defvars t in
174
      (defvars, norm_t :: qlist)
175
    ) elist (defvars, [])
176

    
177
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
178
  (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
179
  match expr.expr_desc with
180
  | Expr_const _
181
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
182
  | Expr_array elist ->
183
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
184
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
185
     mk_expr_alias_opt alias node defvars norm_expr
186
  | Expr_power (e1, d) when offsets = [] ->
187
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
188
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
189
     mk_expr_alias_opt alias node defvars norm_expr
190
  | Expr_power (e1, d) ->
191
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
192
  | Expr_access (e1, d) ->
193
     normalize_expr ~alias:alias node (d::offsets) defvars e1
194
  | Expr_tuple elist ->
195
     let defvars, norm_elist =
196
       normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
197
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
198
  | Expr_appl (id, args, None)
199
      when Basic_library.is_homomorphic_fun id 
200
	&& Types.is_array_type expr.expr_type ->
201
     let defvars, norm_args =
202
       normalize_list
203
	 alias
204
	 node
205
	 offsets
206
	 (fun _ -> normalize_array_expr ~alias:true)
207
	 defvars
208
	 (expr_list_of_expr args)
209
     in
210
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
211
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
212
      && not (!force_alias_internal_fun || alias_basic) ->
213
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
214
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
215
  | Expr_appl (id, args, r) ->
216
     let defvars, r =
217
       match r with
218
       | None -> defvars, None
219
       | Some r ->
220
	  let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in
221
	  defvars, Some norm_r
222
     in
223
     let defvars, norm_args = normalize_expr node [] defvars args in
224
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
225
     if offsets <> []
226
     then
227
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
228
       normalize_expr ~alias:alias node offsets defvars norm_expr
229
     else
230
       mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
231
				    || not (Basic_library.is_expr_internal_fun expr)))
232
	 node defvars norm_expr
233
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
234
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
235
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
236
  | Expr_arrow (e1,e2) ->
237
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
238
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
239
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
240
     mk_expr_alias_opt alias node defvars norm_expr
241
  | Expr_pre e ->
242
     let defvars, norm_e = normalize_expr node offsets defvars e in
243
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
244
     mk_expr_alias_opt alias node defvars norm_expr
245
  | Expr_fby (e1, e2) ->
246
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
247
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
248
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
249
     mk_expr_alias_opt alias node defvars norm_expr
250
  | Expr_when (e, c, l) ->
251
     let defvars, norm_e = normalize_expr node offsets defvars e in
252
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
253
  | Expr_ite (c, t, e) ->
254
     let defvars, norm_c = normalize_guard node defvars c in
255
     let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
256
     let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
257
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
258
     mk_expr_alias_opt alias node defvars norm_expr
259
  | Expr_merge (c, hl) ->
260
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
261
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
262
     mk_expr_alias_opt alias node defvars norm_expr
263

    
264
(* Creates a conditional with a merge construct, which is more lazy *)
265
(*
266
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
267
  match expr.expr_desc with
268
  | Expr_ite (c, t, e) ->
269
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
270
  | _ -> assert false
271
*)
272
and normalize_branches node offsets defvars hl =
273
  List.fold_right
274
    (fun (t, h) (defvars, norm_q) ->
275
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
276
      defvars, (t, norm_h) :: norm_q
277
    )
278
    hl (defvars, [])
279

    
280
and normalize_array_expr ?(alias=true) node offsets defvars expr =
281
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
282
  match expr.expr_desc with
283
  | Expr_power (e1, d) when offsets = [] ->
284
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
285
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
286
  | Expr_power (e1, d) ->
287
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
288
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
289
  | Expr_array elist when offsets = [] ->
290
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
291
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
292
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
293
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
294
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
295
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
296

    
297
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
298
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
299
  match expr.expr_desc with
300
  | Expr_access (e1, d) ->
301
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
302
  | Expr_ite (c, t, e) ->
303
     let defvars, norm_c = normalize_guard node defvars c in
304
     let defvars, norm_t = normalize_cond_expr node offsets defvars t in
305
     let defvars, norm_e = normalize_cond_expr node offsets defvars e in
306
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
307
  | Expr_merge (c, hl) ->
308
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
309
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
310
  | _ when !force_alias_ite ->
311
     (* Forcing alias creation for then/else expressions *)
312
     let defvars, norm_expr =
313
       normalize_expr ~alias:alias node offsets defvars expr
314
     in
315
     mk_expr_alias_opt true node defvars norm_expr
316
  | _ -> (* default case without the force_alias_ite option *)
317
     normalize_expr ~alias:alias node offsets defvars expr
318
       
319
and normalize_guard node defvars expr =
320
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
321
  mk_expr_alias_opt true node defvars norm_expr
322

    
323
(* outputs cannot be memories as well. If so, introduce new local variable.
324
*)
325
let decouple_outputs node defvars eq =
326
  let rec fold_lhs defvars lhs tys cks =
327
   match lhs, tys, cks with
328
   | [], [], []          -> defvars, []
329
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
330
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
331
			    then
332
			      let newvar = mk_fresh_var node eq.eq_loc t c in
333
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
334
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
335
			    else
336
			      (defs_q, vars_q), v::lhs_q
337
   | _                   -> assert false in
338
  let defvars', lhs' =
339
    fold_lhs
340
      defvars
341
      eq.eq_lhs
342
      (Types.type_list_of_type eq.eq_rhs.expr_type)
343
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
344
  defvars', {eq with eq_lhs = lhs' }
345

    
346
let rec normalize_eq node defvars eq =
347
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
348
  match eq.eq_rhs.expr_desc with
349
  | Expr_pre _
350
  | Expr_fby _  ->
351
    let (defvars', eq') = decouple_outputs node defvars eq in
352
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
353
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
354
    (norm_eq::defs', vars')
355
  | Expr_array _ ->
356
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
357
    let norm_eq = { eq with eq_rhs = norm_rhs } in
358
    (norm_eq::defs', vars')
359
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
360
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
361
    let norm_eq = { eq with eq_rhs = norm_rhs } in
362
    (norm_eq::defs', vars')
363
  | Expr_appl _ ->
364
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
365
    let norm_eq = { eq with eq_rhs = norm_rhs } in
366
    (norm_eq::defs', vars')
367
  | _ ->
368
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
369
    let norm_eq = { eq with eq_rhs = norm_rhs } in
370
    norm_eq::defs', vars'
371

    
372
(** normalize_node node returns a normalized node,
373
    ie.
374
    - updated locals
375
    - new equations
376
    -
377
*)
378
let normalize_node node =
379
  reset_cpt_fresh ();
380
  let inputs_outputs = node.node_inputs@node.node_outputs in
381
  let orig_vars = inputs_outputs@node.node_locals in
382
  let not_is_orig_var v =
383
    List.for_all ((!=) v) orig_vars in
384
  let defs, vars =
385
    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
  (* Normalize the asserts *)
389
  let vars, assert_defs, asserts =
390
    List.fold_left (
391
      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
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
402
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
403
    ) (vars, [], []) node.node_asserts in
404
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
405
							  vars and initial locals ones *)
406
  
407
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
408
						       beginning of the list the
409
						       local declared ones *)
410
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
411

    
412

    
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
  let new_annots =
420
    if !Options.traces then
421
      begin
422
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
423
	let norm_traceability = {
424
	  annots = List.map (fun v ->
425
	    let eq =
426
	      try
427
		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
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
435
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
436
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
437
	    (["traceability"], pair)
438
	  ) diff_vars;
439
	  annot_loc = Location.dummy_loc
440
	}
441
	in
442
	norm_traceability::node.node_annot
443
      end
444
    else
445
      node.node_annot
446
  in
447

    
448
  let new_annots =
449
    List.fold_left (fun annots v ->
450
      if Machine_types.is_active && Machine_types.is_exportable v then
451
	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
  let node =
469
    { node with
470
      node_locals = all_locals;
471
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
472
      node_asserts = asserts;
473
      node_annot = new_annots;
474
    }
475
  in ((*Printers.pp_node Format.err_formatter node;*)
476
    node
477
  )
478

    
479

    
480
let normalize_decl decl =
481
  match decl.top_decl_desc with
482
  | Node nd ->
483
    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
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
487

    
488
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
  let old_force_alias_internal_fun = !force_alias_internal_fun in
492
  
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
    | "emf" -> (
500
       (* Forcing ite normalization *)
501
      force_alias_ite := true;
502
      force_alias_internal_fun := true;
503
    )
504
    | _ -> () (* No fancy options for other backends *)
505
  in
506

    
507
  (* 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
  force_alias_internal_fun := old_force_alias_internal_fun;
514
  res
515
  
516
  (* Local Variables: *)
517
(* compile-command:"make -C .." *)
518
(* End: *)