Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 684d39e7

History | View | Annotate | Download (25.6 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
  
47
let expr_true loc ck =
48
{ expr_tag = Utils.new_tag ();
49
  expr_desc = Expr_const (Const_tag tag_true);
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_false loc ck =
57
{ expr_tag = Utils.new_tag ();
58
  expr_desc = Expr_const (Const_tag tag_false);
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 expr_once loc ck =
66
 { expr_tag = Utils.new_tag ();
67
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
68
  expr_type = Type_predef.type_bool;
69
  expr_clock = ck;
70
  expr_delay = Delay.new_var ();
71
  expr_annot = None;
72
  expr_loc = loc }
73

    
74
let is_expr_once =
75
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
76
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
77

    
78
let unfold_arrow expr =
79
 match expr.expr_desc with
80
 | Expr_arrow (e1, e2) ->
81
    let loc = expr.expr_loc in
82
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
83
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
84
 | _                   -> assert false
85

    
86

    
87

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

    
105
let unfold_offsets e offsets =
106
  let add_offset e d =
107
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
108
    let res = *)
109
    { e with
110
      expr_tag = Utils.new_tag ();
111
      expr_loc = d.Dimension.dim_loc;
112
      expr_type = Types.array_element_type e.expr_type;
113
      expr_desc = Expr_access (e, d) }
114
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
115
  in
116
 List.fold_left add_offset e offsets
117

    
118
(* Create an alias for [expr], if none exists yet *)
119
let mk_expr_alias node (defs, vars) expr =
120
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
121
  match get_expr_alias defs expr with
122
  | Some eq ->
123
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
124
    (defs, vars), replace_expr aliases expr
125
  | None    ->
126
    let new_aliases =
127
      List.map2
128
	(mk_fresh_var node expr.expr_loc)
129
	(Types.type_list_of_type expr.expr_type)
130
	(Clocks.clock_list_of_clock expr.expr_clock) in
131
    let new_def =
132
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
133
    in
134
    (* 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; *)
135
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
136

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

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

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

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

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

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

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

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

    
391
let normalize_eq_split node defvars eq =
392
  try
393
    let defs, vars = normalize_eq node defvars eq in
394
  List.fold_right (fun eq (def, vars) -> 
395
    let eq_defs = Splitting.tuple_split_eq eq in
396
    if eq_defs = [eq] then
397
      eq::def, vars 
398
    else
399
      List.fold_left (normalize_eq node) (def, vars) eq_defs
400
  ) defs ([], vars)  
401

    
402
  with _ -> (
403
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
404
    assert false
405
  )
406

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

    
497
   Concerning specification, a similar process is applied, replacing an
498
   expression by a list of local variables and definitions
499
*)
500

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

    
541

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

    
577
  let new_annots =
578
    List.fold_left (fun annots v ->
579
      if Machine_types.is_active && Machine_types.is_exportable v then
580
	let typ = Machine_types.get_specified_type v in
581
  	let typ_name = Machine_types.type_name typ in
582

    
583
	let loc = v.var_loc in
584
	let typ_as_string =
585
	  mkexpr
586
	    loc
587
	    (Expr_const
588
	       (Const_string typ_name))
589
	in
590
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
591
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
592
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
593
      else
594
	annots
595
    ) new_annots new_locals
596
  in
597
  if !Options.spec <> "no" then 
598
    begin
599
      (* Update mutable fields of eexpr to perform normalization of
600
	 specification.
601

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

    
626

    
627
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
628
  match decl.top_decl_desc with
629
  | Node nd ->
630
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
631
    Hashtbl.replace Corelang.node_table nd.node_id decl';
632
    decl'
633
    | Include _| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
634

    
635
let normalize_prog p decls =
636
  (* Backend specific configurations for normalization *)
637
  params := p;
638

    
639
  (* Main algorithm: iterates over nodes *)
640
  List.map (normalize_decl decls) decls
641

    
642
    
643
           (* Local Variables: *)
644
           (* compile-command:"make -C .." *)
645
           (* End: *)
646