Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 66359a5e

History | View | Annotate | Download (21.3 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 LustreSpec
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
let cpt_fresh = ref 0
78

    
79
(* Generate a new local [node] variable *)
80
let mk_fresh_var node loc ty ck =
81
  let vars = get_node_vars node in
82
  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
    var_orig = false;
89
    var_dec_type = dummy_type_dec;
90
    var_dec_clock = dummy_clock_dec;
91
    var_dec_const = false;
92
    var_dec_value = None;
93
    var_parent_nodeid = Some node.node_id;
94
    var_type = ty;
95
    var_clock = ck;
96
    var_loc = loc
97
  }
98
  in aux ()
99

    
100
(* Get the equation in [defs] with [expr] as rhs, if any *)
101
let get_expr_alias defs expr =
102
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
103
 with
104
 | Not_found -> None
105
  
106
(* Replace [expr] with (tuple of) [locals] *)
107
let replace_expr locals expr =
108
 match locals with
109
 | []  -> assert false
110
 | [v] -> { expr with
111
   expr_tag = Utils.new_tag ();
112
   expr_desc = Expr_ident v.var_id }
113
 | _   -> { expr with
114
   expr_tag = Utils.new_tag ();
115
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
116

    
117
let unfold_offsets e offsets =
118
  let add_offset e d =
119
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
120
    let res = *)
121
    { e with
122
      expr_tag = Utils.new_tag ();
123
      expr_loc = d.Dimension.dim_loc;
124
      expr_type = Types.array_element_type e.expr_type;
125
      expr_desc = Expr_access (e, d) }
126
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
127
  in
128
 List.fold_left add_offset e offsets
129

    
130
(* Create an alias for [expr], if none exists yet *)
131
let mk_expr_alias node (defs, vars) expr =
132
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
133
  match get_expr_alias defs expr with
134
  | Some eq ->
135
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
136
    (defs, vars), replace_expr aliases expr
137
  | None    ->
138
    let new_aliases =
139
      List.map2
140
	(mk_fresh_var node expr.expr_loc)
141
	(Types.type_list_of_type expr.expr_type)
142
	(Clocks.clock_list_of_clock expr.expr_clock) in
143
    let new_def =
144
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
145
    in
146
    (* 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; *)
147
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
148

    
149
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
150
   and [opt] is true *)
151
let mk_expr_alias_opt opt node (defs, vars) expr =
152
(*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;*)
153
  match expr.expr_desc with
154
  | Expr_ident alias ->
155
    (defs, vars), expr
156
  | _                ->
157
    match get_expr_alias defs expr with
158
    | Some eq ->
159
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
160
      (defs, vars), replace_expr aliases expr
161
    | None    ->
162
      if opt
163
      then
164
	let new_aliases =
165
	  List.map2
166
	    (mk_fresh_var node expr.expr_loc)
167
	    (Types.type_list_of_type expr.expr_type)
168
	    (Clocks.clock_list_of_clock expr.expr_clock) in
169
	let new_def =
170
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
171
	in
172
	(* Typing and Registering machine type *) 
173
	let _ = Machine_types.type_def node new_aliases expr  in
174
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
175
      else
176
	(defs, vars), expr
177

    
178
(* Create a (normalized) expression from [ref_e],
179
   replacing description with [norm_d],
180
   taking propagated [offsets] into account
181
   in order to change expression type *)
182
let mk_norm_expr offsets ref_e norm_d =
183
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
184
  let drop_array_type ty =
185
    Types.map_tuple_type Types.array_element_type ty in
186
  { ref_e with
187
    expr_desc = norm_d;
188
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
189
														
190
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
191
let rec normalize_list alias node offsets norm_element defvars elist =
192
  List.fold_right
193
    (fun t (defvars, qlist) ->
194
      let defvars, norm_t = norm_element alias node offsets defvars t in
195
      (defvars, norm_t :: qlist)
196
    ) elist (defvars, [])
197

    
198
let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =
199
  (*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;*)
200
  match expr.expr_desc with
201
  | Expr_const _
202
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
203
  | Expr_array elist ->
204
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
205
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
206
     mk_expr_alias_opt alias node defvars norm_expr
207
  | Expr_power (e1, d) when offsets = [] ->
208
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
209
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
210
     mk_expr_alias_opt alias node defvars norm_expr
211
  | Expr_power (e1, d) ->
212
     normalize_expr ~alias:alias node (List.tl offsets) defvars e1
213
  | Expr_access (e1, d) ->
214
     normalize_expr ~alias:alias node (d::offsets) defvars e1
215
  | Expr_tuple elist ->
216
     let defvars, norm_elist =
217
       normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
218
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
219
  | Expr_appl (id, args, None)
220
      when Basic_library.is_homomorphic_fun id 
221
	&& Types.is_array_type expr.expr_type ->
222
     let defvars, norm_args =
223
       normalize_list
224
	 alias
225
	 node
226
	 offsets
227
	 (fun _ -> normalize_array_expr ~alias:true)
228
	 defvars
229
	 (expr_list_of_expr args)
230
     in
231
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
232
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
233
      && not (!force_alias_internal_fun || alias_basic) ->
234
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
235
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
236
  | Expr_appl (id, args, r) ->
237
     let defvars, r =
238
       match r with
239
       | None -> defvars, None
240
       | Some r ->
241
	  let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in
242
	  defvars, Some norm_r
243
     in
244
     let defvars, norm_args = normalize_expr node [] defvars args in
245
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
246
     if offsets <> []
247
     then
248
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
249
       normalize_expr ~alias:alias node offsets defvars norm_expr
250
     else
251
       mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
252
				    || not (Basic_library.is_expr_internal_fun expr)))
253
	 node defvars norm_expr
254
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
255
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
256
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
257
  | Expr_arrow (e1,e2) ->
258
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
259
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
260
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
261
     mk_expr_alias_opt alias node defvars norm_expr
262
  | Expr_pre e ->
263
     let defvars, norm_e = normalize_expr node offsets defvars e in
264
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
265
     mk_expr_alias_opt alias node defvars norm_expr
266
  | Expr_fby (e1, e2) ->
267
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
268
     let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
269
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
270
     mk_expr_alias_opt alias node defvars norm_expr
271
  | Expr_when (e, c, l) ->
272
     let defvars, norm_e = normalize_expr node offsets defvars e in
273
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
274
  | Expr_ite (c, t, e) ->
275
     let defvars, norm_c = normalize_guard node defvars c in
276
     let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
277
     let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
278
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
279
     mk_expr_alias_opt alias node defvars norm_expr
280
  | Expr_merge (c, hl) ->
281
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
282
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
283
     mk_expr_alias_opt alias node defvars norm_expr
284

    
285
(* Creates a conditional with a merge construct, which is more lazy *)
286
(*
287
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
288
  match expr.expr_desc with
289
  | Expr_ite (c, t, e) ->
290
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
291
  | _ -> assert false
292
*)
293
and normalize_branches node offsets defvars hl =
294
  List.fold_right
295
    (fun (t, h) (defvars, norm_q) ->
296
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
297
      defvars, (t, norm_h) :: norm_q
298
    )
299
    hl (defvars, [])
300

    
301
and normalize_array_expr ?(alias=true) node offsets defvars expr =
302
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
303
  match expr.expr_desc with
304
  | Expr_power (e1, d) when offsets = [] ->
305
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
306
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
307
  | Expr_power (e1, d) ->
308
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
309
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
310
  | Expr_array elist when offsets = [] ->
311
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
312
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
313
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
314
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
315
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
316
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
317

    
318
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
319
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
320
  match expr.expr_desc with
321
  | Expr_access (e1, d) ->
322
     normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
323
  | Expr_ite (c, t, e) ->
324
     let defvars, norm_c = normalize_guard node defvars c in
325
     let defvars, norm_t = normalize_cond_expr node offsets defvars t in
326
     let defvars, norm_e = normalize_cond_expr node offsets defvars e in
327
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
328
  | Expr_merge (c, hl) ->
329
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
330
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
331
  | _ when !force_alias_ite ->
332
     (* Forcing alias creation for then/else expressions *)
333
     let defvars, norm_expr =
334
       normalize_expr ~alias:alias node offsets defvars expr
335
     in
336
     mk_expr_alias_opt true node defvars norm_expr
337
  | _ -> (* default case without the force_alias_ite option *)
338
     normalize_expr ~alias:alias node offsets defvars expr
339
       
340
and normalize_guard node defvars expr =
341
  let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in
342
  mk_expr_alias_opt true node defvars norm_expr
343

    
344
(* outputs cannot be memories as well. If so, introduce new local variable.
345
*)
346
let decouple_outputs node defvars eq =
347
  let rec fold_lhs defvars lhs tys cks =
348
   match lhs, tys, cks with
349
   | [], [], []          -> defvars, []
350
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
351
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
352
			    then
353
			      let newvar = mk_fresh_var node eq.eq_loc t c in
354
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
355
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
356
			    else
357
			      (defs_q, vars_q), v::lhs_q
358
   | _                   -> assert false in
359
  let defvars', lhs' =
360
    fold_lhs
361
      defvars
362
      eq.eq_lhs
363
      (Types.type_list_of_type eq.eq_rhs.expr_type)
364
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
365
  defvars', {eq with eq_lhs = lhs' }
366

    
367
let rec normalize_eq node defvars eq =
368
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
369
  match eq.eq_rhs.expr_desc with
370
  | Expr_pre _
371
  | Expr_fby _  ->
372
    let (defvars', eq') = decouple_outputs node defvars eq in
373
    let (defs', vars'), norm_rhs = normalize_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
  | Expr_array _ ->
377
    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 (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
381
    let (defs', vars'), norm_rhs = normalize_array_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
  | Expr_appl _ ->
385
    let (defs', vars'), norm_rhs = normalize_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
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
390
    let norm_eq = { eq with eq_rhs = norm_rhs } in
391
    norm_eq::defs', vars'
392

    
393
(** normalize_node node returns a normalized node,
394
    ie.
395
    - updated locals
396
    - new equations
397
    -
398
*)
399
let normalize_node node =
400
  cpt_fresh := 0;
401
  let inputs_outputs = node.node_inputs@node.node_outputs in
402
  let orig_vars = inputs_outputs@node.node_locals in
403
  let not_is_orig_var v =
404
    List.for_all ((!=) v) orig_vars in
405
  let defs, vars =
406
    let eqs, auts = get_node_eqs node in
407
    if auts != [] then assert false; (* Automata should be expanded by now. *)
408
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
409
  (* Normalize the asserts *)
410
  let vars, assert_defs, asserts =
411
    List.fold_left (
412
      fun (vars, def_accu, assert_accu) assert_ ->
413
	let assert_expr = assert_.assert_expr in
414
	let (defs, vars'), expr = 
415
	  normalize_expr 
416
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
417
	    node 
418
	    [] (* empty offset for arrays *)
419
	    ([], vars) (* defvar only contains vars *)
420
	    assert_expr
421
	in
422
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
423
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
424
    ) (vars, [], []) node.node_asserts in
425
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
426
							  vars and initial locals ones *)
427
  
428
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
429
						       beginning of the list the
430
						       local declared ones *)
431
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
432

    
433

    
434
  (* Updating annotations: traceability and machine types for fresh variables *)
435
  
436
  (* Compute traceability info:
437
     - gather newly bound variables
438
     - compute the associated expression without aliases
439
  *)
440
  let new_annots =
441
    if !Options.traces then
442
      begin
443
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
444
	let norm_traceability = {
445
	  annots = List.map (fun v ->
446
	    let eq =
447
	      try
448
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
449
	      with Not_found -> 
450
		(
451
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
452
		  assert false
453
		) 
454
	    in
455
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
456
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
457
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
458
	    (["traceability"], pair)
459
	  ) diff_vars;
460
	  annot_loc = Location.dummy_loc
461
	}
462
	in
463
	norm_traceability::node.node_annot
464
      end
465
    else
466
      node.node_annot
467
  in
468

    
469
  let new_annots =
470
    List.fold_left (fun annots v ->
471
      if Machine_types.is_exportable v then
472
	let typ = Machine_types.get_specified_type v in
473
  	let typ_name = Machine_types.type_name typ in
474

    
475
	let loc = v.var_loc in
476
	let typ_as_string =
477
	  mkexpr
478
	    loc
479
	    (Expr_const
480
	       (Const_string typ_name))
481
	in
482
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
483
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
484
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
485
      else
486
	annots
487
    ) new_annots new_locals
488
  in
489
  let node =
490
    { node with
491
      node_locals = all_locals;
492
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
493
      node_asserts = asserts;
494
      node_annot = new_annots;
495
    }
496
  in ((*Printers.pp_node Format.err_formatter node;*)
497
    node
498
  )
499

    
500

    
501
let normalize_decl decl =
502
  match decl.top_decl_desc with
503
  | Node nd ->
504
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
505
    Hashtbl.replace Corelang.node_table nd.node_id decl';
506
    decl'
507
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
508

    
509
let normalize_prog ?(backend="C") decls =
510
  let old_unfold_arrow_active = !unfold_arrow_active in
511
  let old_force_alias_ite = !force_alias_ite in
512
  let old_force_alias_internal_fun = !force_alias_internal_fun in
513
  
514
  (* Backend specific configurations for normalization *)
515
  let _ =
516
    match backend with
517
    | "lustre" ->
518
    (* Special treatment of arrows in lustre backend. We want to keep them *)
519
       unfold_arrow_active := false;
520
    | "emf" -> (
521
       (* Forcing ite normalization *)
522
      force_alias_ite := true;
523
      force_alias_internal_fun := true;
524
    )
525
    | _ -> () (* No fancy options for other backends *)
526
  in
527

    
528
  (* Main algorithm: iterates over nodes *)
529
  let res = List.map normalize_decl decls in
530
  
531
  (* Restoring previous settings *)
532
  unfold_arrow_active := old_unfold_arrow_active;
533
  force_alias_ite := old_force_alias_ite;
534
  force_alias_internal_fun := old_force_alias_internal_fun;
535
  res
536
  
537
  (* Local Variables: *)
538
(* compile-command:"make -C .." *)
539
(* End: *)