Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 0d54d8a8

History | View | Annotate | Download (25.5 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Utils
13
open Lustre_types
14
open Corelang
15
open Format
16

    
17
(** Normalisation iters through the AST of expressions and bind fresh definition
18
    when some criteria are met. This creation of fresh definition is performed by
19
    the function mk_expr_alias_opt when the alias argument is on.
20

    
21
    Initial expressions, ie expressions attached a variable in an equation
22
    definition are not aliased. This non-alias feature is propagated in the
23
    expression AST for array access and power construct, tuple, and some special
24
    cases of arrows.
25

    
26
    Two global variables may impact the normalization process:
27
    - unfold_arrow_active
28
    - force_alias_ite: when set, bind a fresh alias for then and else
29
      definitions.
30
*)
31

    
32
(* Two global variables *)
33
let unfold_arrow_active = ref true
34
let force_alias_ite = ref false
35
let force_alias_internal_fun = ref false
36

    
37
  
38
let expr_true loc ck =
39
{ expr_tag = Utils.new_tag ();
40
  expr_desc = Expr_const (Const_tag tag_true);
41
  expr_type = Type_predef.type_bool;
42
  expr_clock = ck;
43
  expr_delay = Delay.new_var ();
44
  expr_annot = None;
45
  expr_loc = loc }
46

    
47
let expr_false loc ck =
48
{ expr_tag = Utils.new_tag ();
49
  expr_desc = Expr_const (Const_tag tag_false);
50
  expr_type = Type_predef.type_bool;
51
  expr_clock = ck;
52
  expr_delay = Delay.new_var ();
53
  expr_annot = None;
54
  expr_loc = loc }
55

    
56
let expr_once loc ck =
57
 { expr_tag = Utils.new_tag ();
58
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
59
  expr_type = Type_predef.type_bool;
60
  expr_clock = ck;
61
  expr_delay = Delay.new_var ();
62
  expr_annot = None;
63
  expr_loc = loc }
64

    
65
let is_expr_once =
66
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
67
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
68

    
69
let unfold_arrow expr =
70
 match expr.expr_desc with
71
 | Expr_arrow (e1, e2) ->
72
    let loc = expr.expr_loc in
73
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
74
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
75
 | _                   -> assert false
76

    
77

    
78

    
79
(* Get the equation in [defs] with [expr] as rhs, if any *)
80
let get_expr_alias defs expr =
81
 try Some (List.find (fun eq -> Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs)
82
 with
83
 | Not_found -> None
84
  
85
(* Replace [expr] with (tuple of) [locals] *)
86
let replace_expr locals expr =
87
 match locals with
88
 | []  -> assert false
89
 | [v] -> { expr with
90
   expr_tag = Utils.new_tag ();
91
   expr_desc = Expr_ident v.var_id }
92
 | _   -> { expr with
93
   expr_tag = Utils.new_tag ();
94
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
95

    
96
let unfold_offsets e offsets =
97
  let add_offset e d =
98
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
99
    let res = *)
100
    { e with
101
      expr_tag = Utils.new_tag ();
102
      expr_loc = d.Dimension.dim_loc;
103
      expr_type = Types.array_element_type e.expr_type;
104
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
107
 List.fold_left add_offset e offsets
108

    
109
(* Create an alias for [expr], if none exists yet *)
110
let mk_expr_alias node (defs, vars) expr =
111
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
112
  match get_expr_alias defs expr with
113
  | Some eq ->
114
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
115
    (defs, vars), replace_expr aliases expr
116
  | None    ->
117
    let new_aliases =
118
      List.map2
119
	(mk_fresh_var node expr.expr_loc)
120
	(Types.type_list_of_type expr.expr_type)
121
	(Clocks.clock_list_of_clock expr.expr_clock) in
122
    let new_def =
123
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
124
    in
125
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
126
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127

    
128
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129
   and [opt] is true *)
130
let mk_expr_alias_opt opt node (defs, vars) expr =
131
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132
  match expr.expr_desc with
133
  | Expr_ident alias ->
134
    (defs, vars), expr
135
  | _                ->
136
    match get_expr_alias defs expr with
137
    | Some eq ->
138
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
139
      (defs, vars), replace_expr aliases expr
140
    | None    ->
141
      if opt
142
      then
143
	let new_aliases =
144
	  List.map2
145
	    (mk_fresh_var node expr.expr_loc)
146
	    (Types.type_list_of_type expr.expr_type)
147
	    (Clocks.clock_list_of_clock expr.expr_clock) in
148
	let new_def =
149
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
150
	in
151
	(* Typing and Registering machine type *) 
152
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
153
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
154
      else
155
	(defs, vars), expr
156

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

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

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

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

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

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

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

    
372
let normalize_eq_split node defvars eq =
373
  try
374
    let defs, vars = normalize_eq node defvars eq in
375
  List.fold_right (fun eq (def, vars) -> 
376
    let eq_defs = Splitting.tuple_split_eq eq in
377
    if eq_defs = [eq] then
378
      eq::def, vars 
379
    else
380
      List.fold_left (normalize_eq node) (def, vars) eq_defs
381
  ) defs ([], vars)  
382

    
383
  with _ -> (
384
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
385
    assert false
386
  )
387

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

    
478
   Concerning specification, a similar process is applied, replacing an
479
   expression by a list of local variables and definitions
480
*)
481

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

    
522

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

    
558
  let new_annots =
559
    List.fold_left (fun annots v ->
560
      if Machine_types.is_active && Machine_types.is_exportable v then
561
	let typ = Machine_types.get_specified_type v in
562
  	let typ_name = Machine_types.type_name typ in
563

    
564
	let loc = v.var_loc in
565
	let typ_as_string =
566
	  mkexpr
567
	    loc
568
	    (Expr_const
569
	       (Const_string typ_name))
570
	in
571
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
572
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
573
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
574
      else
575
	annots
576
    ) new_annots new_locals
577
  in
578
  if !Options.spec <> "no" then 
579
    begin
580
      (* Update mutable fields of eexpr to perform normalization of
581
	 specification.
582

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

    
607

    
608
let normalize_decl (decls: program) (decl: top_decl) : top_decl =
609
  match decl.top_decl_desc with
610
  | Node nd ->
611
    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
612
    Hashtbl.replace Corelang.node_table nd.node_id decl';
613
    decl'
614
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
615

    
616
let normalize_prog ?(backend="C") decls : program =
617
  let old_unfold_arrow_active = !unfold_arrow_active in
618
  let old_force_alias_ite = !force_alias_ite in
619
  let old_force_alias_internal_fun = !force_alias_internal_fun in
620
  
621
  (* Backend specific configurations for normalization *)
622
  let _ =
623
    match backend with
624
    | "lustre" ->
625
    (* Special treatment of arrows in lustre backend. We want to keep them *)
626
       unfold_arrow_active := false;
627
    | "emf" -> (
628
       (* Forcing ite normalization *)
629
      force_alias_ite := true;
630
      force_alias_internal_fun := true;
631
    )
632
    | _ -> () (* No fancy options for other backends *)
633
  in
634

    
635
  (* Main algorithm: iterates over nodes *)
636
  let res = List.map (normalize_decl decls) decls in
637
  
638
  (* Restoring previous settings *)
639
  unfold_arrow_active := old_unfold_arrow_active;
640
  force_alias_ite := old_force_alias_ite;
641
  force_alias_internal_fun := old_force_alias_internal_fun;
642
  res
643
  
644
  (* Local Variables: *)
645
(* compile-command:"make -C .." *)
646
(* End: *)