Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 95944ba1

History | View | Annotate | Download (27.4 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
type param_t =
33
  {
34
    unfold_arrow_active: bool;
35
    force_alias_ite: bool;
36
    force_alias_internal_fun: bool;
37
  }
38

    
39
let params = ref
40
               {
41
                 unfold_arrow_active = false;
42
                 force_alias_ite = false;
43
                 force_alias_internal_fun =false;
44
               }
45

    
46
type norm_ctx_t =
47
  {
48
    parentid: ident;
49
    vars: var_decl list;
50
    is_output: ident -> bool; 
51
  }
52

    
53
           
54
let expr_true loc ck =
55
{ expr_tag = Utils.new_tag ();
56
  expr_desc = Expr_const (Const_tag tag_true);
57
  expr_type = Type_predef.type_bool;
58
  expr_clock = ck;
59
  expr_delay = Delay.new_var ();
60
  expr_annot = None;
61
  expr_loc = loc }
62

    
63
let expr_false loc ck =
64
{ expr_tag = Utils.new_tag ();
65
  expr_desc = Expr_const (Const_tag tag_false);
66
  expr_type = Type_predef.type_bool;
67
  expr_clock = ck;
68
  expr_delay = Delay.new_var ();
69
  expr_annot = None;
70
  expr_loc = loc }
71

    
72
let expr_once loc ck =
73
 { expr_tag = Utils.new_tag ();
74
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
75
  expr_type = Type_predef.type_bool;
76
  expr_clock = ck;
77
  expr_delay = Delay.new_var ();
78
  expr_annot = None;
79
  expr_loc = loc }
80

    
81
let is_expr_once =
82
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
83
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
84

    
85
let unfold_arrow expr =
86
 match expr.expr_desc with
87
 | Expr_arrow (e1, e2) ->
88
    let loc = expr.expr_loc in
89
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
90
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
91
 | _                   -> assert false
92

    
93

    
94

    
95
(* Get the equation in [defs] with [expr] as rhs, if any *)
96
let get_expr_alias defs expr =
97
 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)
98
 with
99
 | Not_found -> None
100
  
101
(* Replace [expr] with (tuple of) [locals] *)
102
let replace_expr locals expr =
103
 match locals with
104
 | []  -> assert false
105
 | [v] -> { expr with
106
   expr_tag = Utils.new_tag ();
107
   expr_desc = Expr_ident v.var_id }
108
 | _   -> { expr with
109
   expr_tag = Utils.new_tag ();
110
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
111

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

    
125
(* IS IT USED ? TODO 
126
(* Create an alias for [expr], if none exists yet *)
127
let mk_expr_alias (parentid, vars) (defs, vars) expr =
128
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
129
  match get_expr_alias defs expr with
130
  | Some eq ->
131
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
132
    (defs, vars), replace_expr aliases expr
133
  | None    ->
134
    let new_aliases =
135
      List.map2
136
	(mk_fresh_var (parentid, vars) expr.expr_loc)
137
	(Types.type_list_of_type expr.expr_type)
138
	(Clocks.clock_list_of_clock expr.expr_clock) in
139
    let new_def =
140
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
141
    in
142
    (* 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; *)
143
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
144
 *)
145
  
146
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
147
   and [opt] is true *)
148
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
149
(*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;*)
150
  match expr.expr_desc with
151
  | Expr_ident alias ->
152
    (defs, vars), expr
153
  | _                ->
154
    match get_expr_alias defs expr with
155
    | Some eq ->
156
       (* Format.eprintf "Found a preexisting definition@."; *)
157
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
158
      (defs, vars), replace_expr aliases expr
159
    | None    ->
160
       (* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
161
        * Format.eprintf "existing defs are: @[[%a@]]@."
162
        *   (fprintf_list ~sep:"@ "(fun fmt eq ->
163
        *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
164
        *          Clocks.print_ck eq.eq_rhs.expr_clock
165
        *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
166
        *          (is_eq_expr eq.eq_rhs expr)
167
        *          Printers.pp_node_eq eq))
168
        *   defs; *)
169
      if opt
170
      then
171
	let new_aliases =
172
	  List.map2
173
	    (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
174
	    (Types.type_list_of_type expr.expr_type)
175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
176
	let new_def =
177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
178
	in
179
	(* Typing and Registering machine type *) 
180
	let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr  in
181
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
182
      else
183
	(defs, vars), expr
184

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

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

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

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

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

    
351
(* outputs cannot be memories as well. If so, introduce new local variable.
352
*)
353
let decouple_outputs norm_ctx defvars eq =
354
  let rec fold_lhs defvars lhs tys cks =
355
    match lhs, tys, cks with
356
    | [], [], []          -> defvars, []
357
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
358
			     if norm_ctx.is_output v
359
			     then
360
			       let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in
361
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
362
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
363
			     else
364
			       (defs_q, vars_q), v::lhs_q
365
    | _                   -> assert false in
366
  let defvars', lhs' =
367
    fold_lhs
368
      defvars
369
      eq.eq_lhs
370
      (Types.type_list_of_type eq.eq_rhs.expr_type)
371
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
372
  defvars', {eq with eq_lhs = lhs' }
373

    
374
let rec normalize_eq norm_ctx defvars eq =
375
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
376
  match eq.eq_rhs.expr_desc with
377
  | Expr_pre _
378
  | Expr_fby _  ->
379
    let (defvars', eq') = decouple_outputs norm_ctx defvars eq in
380
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in
381
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
382
    (norm_eq::defs', vars')
383
  | Expr_array _ ->
384
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
385
    let norm_eq = { eq with eq_rhs = norm_rhs } in
386
    (norm_eq::defs', vars')
387
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
388
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
389
    let norm_eq = { eq with eq_rhs = norm_rhs } in
390
    (norm_eq::defs', vars')
391
  | Expr_appl _ ->
392
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
393
    let norm_eq = { eq with eq_rhs = norm_rhs } in
394
    (norm_eq::defs', vars')
395
  | _ ->
396
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
397
    let norm_eq = { eq with eq_rhs = norm_rhs } in
398
    norm_eq::defs', vars'
399

    
400
let normalize_eq_split norm_ctx defvars eq =
401
  try
402
    let defs, vars = normalize_eq norm_ctx defvars eq in
403
  List.fold_right (fun eq (def, vars) -> 
404
    let eq_defs = Splitting.tuple_split_eq eq in
405
    if eq_defs = [eq] then
406
      eq::def, vars 
407
    else
408
      List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
409
  ) defs ([], vars)  
410

    
411
  with _ -> (
412
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
413
    assert false
414
  )
415

    
416
let normalize_eexpr decls norm_ctx vars ee = ee (*
417
  (* New output variable *)
418
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
419
  let output_var = 
420
    mkvar_decl 
421
      ee.eexpr_loc 
422
      (output_id, 
423
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
424
       mkclock ee.eexpr_loc Ckdec_any, 
425
       false (* not a constant *),
426
       None,
427
       None
428
      ) 
429
  in
430
  
431
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
432
  (* Calls are first inlined *)
433
  let nodes = get_nodes decls in
434
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
435
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
436
   let calls = List.map 
437
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
438
  in
439
*)
440
  (*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;  *)
441
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
442
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
443
  let (new_locals, eqs) =
444
    if calls = [] && not (eq_has_arrows eq) then
445
      (locals, [eq])     
446
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
447
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
448
      (*Format.eprintf "eqs %a@.@?" 
449
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
450
      (new_locals, eqs)
451
*)
452
           (locals, [eq])     
453
 
454
    ) in
455
  (* Normalizing expr and eqs *)
456
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
457
    let todefine = List.fold_left
458
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
459
    (ISet.add output_id ISet.empty) vars in
460
  
461
  try
462
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
463
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
464
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
465
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
466
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
467
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
468
  (* check that table is empty *)
469
    if (not (ISet.is_empty undefined_vars)) then
470
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
471
    
472
    (*Format.eprintf "normalized eqs %a@.@?" 
473
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
474
    ee.eexpr_normalized <- Some (output_var, defs, vars)
475
    
476
  with (Types.Error (loc,err)) as exc ->
477
    eprintf "Typing error for eexpr %a: %a%a%a@."
478
      Printers.pp_eexpr ee
479
      Types.pp_error err
480
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
481
      Location.pp_loc loc
482
  
483
      
484
    ;
485
    raise exc
486
                                                 *)    
487
 
488
    
489
let normalize_spec decls iovars s = s (*
490
  (* Each stmt is normalized *)
491
  let orig_vars = iovars @ s.locals in
492
  let not_is_orig_var v =
493
    List.for_all ((!=) v) orig_vars in
494
  let defs, vars = 
495
    let eqs, auts = List.fold_right (fun (el,al) s -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
496
    if auts != [] then assert false; (* Automata should be expanded by now. *)
497
    List.fold_left (normalize_eq node) ([], orig_vars) eqs
498
  in
499
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
500

    
501
  (*
502
      
503
  {s with
504
    locals = s.locals @ new_locals;
505
    stmts = List.map (fun eq -> Eq eq) defs;
506
  let nee _ = () in
507
  (*normalize_eexpr decls iovars in *)
508
  List.iter nee s.assume;
509
  List.iter nee s.guarantees;
510
  List.iter (fun m -> 
511
      List.iter nee m.require;
512
    List.iter nee m.ensure
513
    ) s.modes;
514
   *)
515
  s
516
                                       *)
517
    
518
(* The normalization phase introduces new local variables
519
   - output cannot be memories. If this happen, new local variables acting as
520
   memories are introduced. 
521
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
522
   access
523
   Thoses values are shared, ie. no duplicate expressions are introduced.
524

    
525
   Concerning specification, a similar process is applied, replacing an
526
   expression by a list of local variables and definitions
527
*)
528

    
529
(** normalize_node node returns a normalized node, 
530
    ie. 
531
    - updated locals
532
    - new equations
533
    -
534
*)
535
let normalize_node decls node =
536
  reset_cpt_fresh ();
537
  let inputs_outputs = node.node_inputs@node.node_outputs in
538
  let orig_vars = inputs_outputs@node.node_locals in
539
  let not_is_orig_var v =
540
    List.for_all ((!=) v) orig_vars in
541
  let norm_ctx = {
542
      parentid = node.node_id;
543
      vars = get_node_vars node;
544
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
545
    }
546
  in
547
  
548
  let defs, vars =
549
    let eqs, auts = get_node_eqs node in
550
    if auts != [] then assert false; (* Automata should be expanded by now. *)
551
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
552
  (* Normalize the asserts *)
553
  let vars, assert_defs, asserts =
554
    List.fold_left (
555
      fun (vars, def_accu, assert_accu) assert_ ->
556
	let assert_expr = assert_.assert_expr in
557
	let (defs, vars'), expr = 
558
	  normalize_expr 
559
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
560
	    norm_ctx 
561
	    [] (* empty offset for arrays *)
562
	    ([], vars) (* defvar only contains vars *)
563
	    assert_expr
564
	in
565
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
566
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
567
    ) (vars, [], []) node.node_asserts in
568
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
569
							  vars and initial locals ones *)
570
  
571
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
572
						       beginning of the list the
573
						       local declared ones *)
574
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
575

    
576

    
577
  (* Updating annotations: traceability and machine types for fresh variables *)
578
  
579
  (* Compute traceability info:
580
     - gather newly bound variables
581
     - compute the associated expression without aliases
582
  *)
583
  let new_annots =
584
    if !Options.traces then
585
      begin
586
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
587
	let norm_traceability = {
588
	  annots = List.map (fun v ->
589
	    let eq =
590
	      try
591
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
592
	      with Not_found -> 
593
		(
594
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
595
		  assert false
596
		) 
597
	    in
598
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
599
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
600
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
601
	    (["traceability"], pair)
602
	  ) diff_vars;
603
	  annot_loc = Location.dummy_loc
604
	}
605
	in
606
	norm_traceability::node.node_annot
607
      end
608
    else
609
      node.node_annot
610
  in
611

    
612
  let new_annots =
613
    List.fold_left (fun annots v ->
614
      if Machine_types.is_active && Machine_types.is_exportable v then
615
	let typ = Machine_types.get_specified_type v in
616
  	let typ_name = Machine_types.type_name typ in
617

    
618
	let loc = v.var_loc in
619
	let typ_as_string =
620
	  mkexpr
621
	    loc
622
	    (Expr_const
623
	       (Const_string typ_name))
624
	in
625
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
626
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
627
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
628
      else
629
	annots
630
    ) new_annots new_locals
631
  in
632
  let spec =
633
    begin
634
      (* Update mutable fields of eexpr to perform normalization of
635
	 specification.
636

    
637
	 Careful: we do not normalize annotations, since they can have the form
638
	 x = (a, b, c) *)
639
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls inputs_outputs s) 
640
    end
641
  in
642
  
643
  
644
  let node =
645
    { node with
646
      node_locals = all_locals;
647
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
648
      node_asserts = asserts;
649
      node_annot = new_annots;
650
      node_spec = spec;
651
    }
652
  in ((*Printers.pp_node Format.err_formatter node;*)
653
    node
654
  )
655

    
656
let normalize_inode decls nd =
657
  reset_cpt_fresh ();
658
  match nd.nodei_spec with
659
    None -> nd
660
  | Some s ->
661
     let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in
662
     let s = normalize_spec decls inputs_outputs s in
663
     { nd with nodei_spec = Some s }
664
  
665
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
666
  match decl.top_decl_desc with
667
  | Node nd ->
668
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
669
     update_node nd.node_id decl';
670
     decl'
671
  | ImportedNode nd ->
672
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
673
     update_node nd.nodei_id decl';
674
     decl'
675
     
676
    | Include _| Open _ | Const _ | TypeDef _ -> decl
677

    
678
let normalize_prog p decls =
679
  (* Backend specific configurations for normalization *)
680
  params := p;
681

    
682
  (* Main algorithm: iterates over nodes *)
683
  List.map (normalize_decl decls) decls
684

    
685

    
686
(* Fake interface for outside uses *)
687
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
688
  mk_expr_alias_opt
689
    opt
690
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
691
    (defs, vars)
692
    expr
693

    
694
    
695
           (* Local Variables: *)
696
           (* compile-command:"make -C .." *)
697
           (* End: *)
698