Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ master

History | View | Annotate | Download (26.1 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
       (* Format.eprintf "Found a preexisting definition@."; *)
139
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
140
      (defs, vars), replace_expr aliases expr
141
    | None    ->
142
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
143
        * Format.eprintf "existing defs are: @[[%a@]]@."
144
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
145
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
146
        *          Clocks.print_ck eq.eq_rhs.expr_clock
147
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
148
        *          (is_eq_expr eq.eq_rhs expr)
149
        *          Printers.pp_node_eq eq))
150
        *   defs; *)
151
      if opt
152
      then
153
	let new_aliases =
154
	  List.map2
155
	    (mk_fresh_var node expr.expr_loc)
156
	    (Types.type_list_of_type expr.expr_type)
157
	    (Clocks.clock_list_of_clock expr.expr_clock) in
158
	let new_def =
159
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
160
	in
161
	(* Typing and Registering machine type *) 
162
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
163
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
164
      else
165
	(defs, vars), expr
166

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

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

    
274
(* Creates a conditional with a merge construct, which is more lazy *)
275
(*
276
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
277
  match expr.expr_desc with
278
  | Expr_ite (c, t, e) ->
279
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
280
  | _ -> assert false
281
*)
282
and normalize_branches node offsets defvars hl =
283
  List.fold_right
284
    (fun (t, h) (defvars, norm_q) ->
285
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
286
      defvars, (t, norm_h) :: norm_q
287
    )
288
    hl (defvars, [])
289

    
290
and normalize_array_expr ?(alias=true) node offsets defvars expr =
291
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
292
  match expr.expr_desc with
293
  | Expr_power (e1, d) when offsets = [] ->
294
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
295
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
296
  | Expr_power (e1, d) ->
297
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
298
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
299
  | Expr_array elist when offsets = [] ->
300
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
301
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
302
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
303
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
304
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
305
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
306

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

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

    
356
let rec normalize_eq node defvars eq =
357
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
358
  match eq.eq_rhs.expr_desc with
359
  | Expr_pre _
360
  | Expr_fby _  ->
361
    let (defvars', eq') = decouple_outputs node defvars eq in
362
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
363
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
364
    (norm_eq::defs', vars')
365
  | Expr_array _ ->
366
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
367
    let norm_eq = { eq with eq_rhs = norm_rhs } in
368
    (norm_eq::defs', vars')
369
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
370
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
371
    let norm_eq = { eq with eq_rhs = norm_rhs } in
372
    (norm_eq::defs', vars')
373
  | Expr_appl _ ->
374
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
375
    let norm_eq = { eq with eq_rhs = norm_rhs } in
376
    (norm_eq::defs', vars')
377
  | _ ->
378
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
379
    let norm_eq = { eq with eq_rhs = norm_rhs } in
380
    norm_eq::defs', vars'
381

    
382
let normalize_eq_split node defvars eq =
383
  try
384
    let defs, vars = normalize_eq node defvars eq in
385
  List.fold_right (fun eq (def, vars) -> 
386
    let eq_defs = Splitting.tuple_split_eq eq in
387
    if eq_defs = [eq] then
388
      eq::def, vars 
389
    else
390
      List.fold_left (normalize_eq node) (def, vars) eq_defs
391
  ) defs ([], vars)  
392

    
393
  with _ -> (
394
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
395
    assert false
396
  )
397

    
398
let normalize_eexpr decls node vars ee =
399
  (* New output variable *)
400
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
401
  let output_var = 
402
    mkvar_decl 
403
      ee.eexpr_loc 
404
      (output_id, 
405
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
406
       mkclock ee.eexpr_loc Ckdec_any, 
407
       false (* not a constant *),
408
       None,
409
       None
410
      ) 
411
  in
412
  
413
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
414
  (* Calls are first inlined *)
415
  let nodes = get_nodes decls in
416
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
417
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
418
   let calls = List.map 
419
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
420
  in
421
*)
422
  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
423
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
424
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
425
  let (new_locals, eqs) =
426
    if calls = [] && not (eq_has_arrows eq) then
427
      (locals, [eq])     
428
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
429
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
430
      (*Format.eprintf "eqs %a@.@?" 
431
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
432
      (new_locals, eqs)
433
*)
434
           (locals, [eq])     
435
 
436
    ) in
437
  (* Normalizing expr and eqs *)
438
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
439
    let todefine = List.fold_left
440
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
441
    (ISet.add output_id ISet.empty) vars in
442
  
443
  try
444
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
445
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
446
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
447
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
448
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
449
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
450
  (* check that table is empty *)
451
    if (not (ISet.is_empty undefined_vars)) then
452
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
453
    
454
    (*Format.eprintf "normalized eqs %a@.@?" 
455
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
456
    ee.eexpr_normalized <- Some (output_var, defs, vars)
457
    
458
  with (Types.Error (loc,err)) as exc ->
459
    eprintf "Typing error for eexpr %a: %a%a%a@."
460
      Printers.pp_eexpr ee
461
      Types.pp_error err
462
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
463
      Location.pp_loc loc
464
  
465
      
466
    ;
467
    raise exc
468
    
469
 
470
    
471
let normalize_spec decls node vars s =
472
  let nee = normalize_eexpr decls node vars in
473
  List.iter nee s.assume;
474
  List.iter nee s.guarantees;
475
  List.iter (fun m -> 
476
      List.iter nee m.require;
477
    List.iter nee m.ensure
478
  ) s.modes
479
  
480
    
481
(* The normalization phase introduces new local variables
482
   - output cannot be memories. If this happen, new local variables acting as
483
   memories are introduced. 
484
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
485
   access
486
   Thoses values are shared, ie. no duplicate expressions are introduced.
487

    
488
   Concerning specification, a similar process is applied, replacing an
489
   expression by a list of local variables and definitions
490
*)
491

    
492
(** normalize_node node returns a normalized node, 
493
    ie. 
494
    - updated locals
495
    - new equations
496
    -
497
*)
498
let normalize_node decls node =
499
  reset_cpt_fresh ();
500
  let inputs_outputs = node.node_inputs@node.node_outputs in
501
  let orig_vars = inputs_outputs@node.node_locals in
502
  let not_is_orig_var v =
503
    List.for_all ((!=) v) orig_vars in
504
  let defs, vars =
505
    let eqs, auts = get_node_eqs node in
506
    if auts != [] then assert false; (* Automata should be expanded by now. *)
507
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
508
  (* Normalize the asserts *)
509
  let vars, assert_defs, asserts =
510
    List.fold_left (
511
      fun (vars, def_accu, assert_accu) assert_ ->
512
	let assert_expr = assert_.assert_expr in
513
	let (defs, vars'), expr = 
514
	  normalize_expr 
515
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
516
	    node 
517
	    [] (* empty offset for arrays *)
518
	    ([], vars) (* defvar only contains vars *)
519
	    assert_expr
520
	in
521
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
522
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
523
    ) (vars, [], []) node.node_asserts in
524
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
525
							  vars and initial locals ones *)
526
  
527
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
528
						       beginning of the list the
529
						       local declared ones *)
530
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
531

    
532

    
533
  (* Updating annotations: traceability and machine types for fresh variables *)
534
  
535
  (* Compute traceability info:
536
     - gather newly bound variables
537
     - compute the associated expression without aliases
538
  *)
539
  let new_annots =
540
    if !Options.traces then
541
      begin
542
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
543
	let norm_traceability = {
544
	  annots = List.map (fun v ->
545
	    let eq =
546
	      try
547
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
548
	      with Not_found -> 
549
		(
550
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
551
		  assert false
552
		) 
553
	    in
554
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
555
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
556
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
557
	    (["traceability"], pair)
558
	  ) diff_vars;
559
	  annot_loc = Location.dummy_loc
560
	}
561
	in
562
	norm_traceability::node.node_annot
563
      end
564
    else
565
      node.node_annot
566
  in
567

    
568
  let new_annots =
569
    List.fold_left (fun annots v ->
570
      if Machine_types.is_active && Machine_types.is_exportable v then
571
	let typ = Machine_types.get_specified_type v in
572
  	let typ_name = Machine_types.type_name typ in
573

    
574
	let loc = v.var_loc in
575
	let typ_as_string =
576
	  mkexpr
577
	    loc
578
	    (Expr_const
579
	       (Const_string typ_name))
580
	in
581
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
582
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
583
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
584
      else
585
	annots
586
    ) new_annots new_locals
587
  in
588
  if !Options.spec <> "no" then 
589
    begin
590
      (* Update mutable fields of eexpr to perform normalization of
591
	 specification.
592

    
593
	 Careful: we do not normalize annotations, since they can have the form
594
	 x = (a, b, c) *)
595
      (* List.iter  *)
596
      (* 	(fun a ->  *)
597
      (* 	  List.iter  *)
598
      (* 	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann)  *)
599
      (* 	    a.annots *)
600
      (* 	) *)
601
      (* 	node.node_annot; *)
602
      match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s 
603
    end;
604
  
605
 
606
  let node =
607
    { node with
608
      node_locals = all_locals;
609
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
610
      node_asserts = asserts;
611
      node_annot = new_annots;
612
    }
613
  in ((*Printers.pp_node Format.err_formatter node;*)
614
    node
615
  )
616

    
617

    
618
let normalize_decl (decls: program) (decl: top_decl) : top_decl =
619
  match decl.top_decl_desc with
620
  | Node nd ->
621
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
622
    Hashtbl.replace Corelang.node_table nd.node_id decl';
623
    decl'
624
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
625

    
626
let normalize_prog ?(backend="C") decls : program =
627
  let old_unfold_arrow_active = !unfold_arrow_active in
628
  let old_force_alias_ite = !force_alias_ite in
629
  let old_force_alias_internal_fun = !force_alias_internal_fun in
630
  
631
  (* Backend specific configurations for normalization *)
632
  let _ =
633
    match backend with
634
    | "lustre" ->
635
    (* Special treatment of arrows in lustre backend. We want to keep them *)
636
       unfold_arrow_active := false;
637
    | "emf" -> (
638
       (* Forcing ite normalization *)
639
      force_alias_ite := true;
640
      force_alias_internal_fun := true;
641
    )
642
    | _ -> () (* No fancy options for other backends *)
643
  in
644

    
645
  (* Main algorithm: iterates over nodes *)
646
  let res = List.map (normalize_decl decls) decls in
647
  
648
  (* Restoring previous settings *)
649
  unfold_arrow_active := old_unfold_arrow_active;
650
  force_alias_ite := old_force_alias_ite;
651
  force_alias_internal_fun := old_force_alias_internal_fun;
652
  res
653
  
654
  (* Local Variables: *)
655
(* compile-command:"make -C .." *)
656
(* End: *)