Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 59020713

History | View | Annotate | Download (31.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
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@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
181
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
182
        in
183
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
184
      else
185
	(defs, vars), expr
186

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

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

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

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

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

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

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

    
402
let normalize_eq_split norm_ctx defvars eq =
403
  try
404
    let defs, vars = normalize_eq norm_ctx defvars eq in
405
    List.fold_right (fun eq (def, vars) -> 
406
        let eq_defs = Splitting.tuple_split_eq eq in
407
        if eq_defs = [eq] then
408
          eq::def, vars 
409
        else
410
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
411
      ) defs ([], vars)  
412
    
413
  with ex -> (
414
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
415
    raise ex
416
  )
417

    
418
(* Projecting an eexpr to an eexpr associated to a single
419
   variable. Returns the updated ee, the bounded variable and the
420
   associated statement *)
421
let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
422
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
423
  (* don't do anything is eexpr is just a variable *)
424
  let skip =
425
    match ee.eexpr_qfexpr.expr_desc with
426
    | Expr_ident _ | Expr_const _ -> true
427
    | _ -> false
428
  in
429
  if skip then
430
    ee, (def, vars)
431
  else (
432
    (* New output variable *)
433
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
434
    let output_var = 
435
      mkvar_decl 
436
        ee.eexpr_loc 
437
        (output_id, 
438
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
439
         mkclock ee.eexpr_loc Ckdec_any, 
440
         false (* not a constant *),
441
         None,
442
         None
443
        ) 
444
    in
445
    let output_expr = expr_of_vdecl output_var in
446
    (* Rebuilding an eexpr with a silly expression, just a variable *)
447
    let ee' = { ee with eexpr_qfexpr = output_expr } in
448

    
449
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
450
       inline possible calls within, normalize it and type/clock the
451
       result.  *)
452
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
453
    (* Inlining any calls *)
454
    let nodes = get_nodes decls in
455
    let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
456
    let vars, eqs =
457
      if calls = [] && not (eq_has_arrows eq) then
458
        vars, [eq]    
459
      else
460
        assert false (* TODO *)
461
    in
462
    
463
    (* Normalizing expr and eqs *)
464
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in
465
(*    let todefine =
466
      List.fold_left
467
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
468
        (ISet.add output_id ISet.empty) vars in
469
 *)      
470

    
471
    (* Typing / Clocking *)
472
    try
473
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
474
        (*
475
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
476
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
477
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
478
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
479
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
480
  (* check that table is empty *)
481
    if (not (ISet.is_empty undefined_vars)) then
482
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
483
    
484
    (*Format.eprintf "normalized eqs %a@.@?" 
485
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
486
         *)
487

    
488
    ee', (defs, vars)
489
    
490
  with (Types.Error (loc,err)) as exc ->
491
    eprintf "Typing error for eexpr %a: %a%a%a@."
492
      Printers.pp_eexpr ee
493
      Types.pp_error err
494
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
495
      Location.pp_loc loc
496
  
497
      
498
    ;
499
    raise exc
500
                                     
501
  )
502
    
503
   (*
504
  
505
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
506
  (* Calls are first inlined *)
507
  
508
  (*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;  *)
509
  let (new_locals, eqs) =
510
    if calls = [] && not (eq_has_arrows eq) then
511
      (locals, [eq])     
512
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
513
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
514
      (*Format.eprintf "eqs %a@.@?" 
515
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
516
      (new_locals, eqs)
517
*)
518
           (locals, [eq])     
519
 
520
    ) in
521
  (* Normalizing expr and eqs *)
522
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
523
    let todefine = List.fold_left
524
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
525
    (ISet.add output_id ISet.empty) vars in
526
  
527
  try
528
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
529
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
530
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
531
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
532
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
533
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
534
  (* check that table is empty *)
535
    if (not (ISet.is_empty undefined_vars)) then
536
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
537
    
538
    (*Format.eprintf "normalized eqs %a@.@?" 
539
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
540
    ee.eexpr_normalized <- Some (output_var, defs, vars)
541
    
542
  with (Types.Error (loc,err)) as exc ->
543
    eprintf "Typing error for eexpr %a: %a%a%a@."
544
      Printers.pp_eexpr ee
545
      Types.pp_error err
546
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
547
      Location.pp_loc loc
548
  
549
      
550
    ;
551
    raise exc
552
                                                 *)    
553
 
554

    
555
(* We use node local vars to make sure we are creating fresh variables *) 
556
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
557
  (* Original set of variables actually visible from here: iun/out and
558
     spec locals (no node locals) *)
559
  let orig_vars = in_vars @ out_vars @ s.locals in
560
  let not_is_orig_var v =
561
    List.for_all ((!=) v) orig_vars in
562
  let norm_ctx = {
563
      parentid = parentid;
564
      vars = in_vars @ out_vars @ l_vars;
565
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
566
    }
567
  in
568
  (* Normalizing existing stmts *)
569
  let eqs, auts = List.fold_right (fun s (el,al)  -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
570
  if auts != [] then assert false; (* Automata should be expanded by now. *)
571
  let defsvars = 
572
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
573
  in
574
  (* Iterate through predicates and normalize them on the go, creating
575
     fresh variables for any guarantees/assumes/require/ensure *)
576
  let process_predicates l defvars =
577
    List.fold_right (fun ee (accu, defvars) ->
578
        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
579
        ee'::accu, defvars
580
      ) l ([], defvars)
581
  in
582

    
583
  
584
  let assume', defsvars = process_predicates s.assume defsvars in
585
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
586
  let modes', (defs, vars) =
587
    List.fold_right (
588
        fun m (accu_m, defsvars) ->
589
        let require', defsvars = process_predicates m.require defsvars in
590
        let ensure', defsvars = process_predicates m.ensure defsvars in
591
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
592
      ) s.modes ([], defsvars)
593
  in
594
  
595
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
596
   
597
      
598
  {s with
599
    locals = s.locals @ new_locals;
600
    stmts = List.map (fun eq -> Eq eq) defs;
601
    assume = assume';
602
    guarantees = guarantees';
603
    modes = modes'
604
  }
605
(* let nee _ = () in
606
 *   (\*normalize_eexpr decls iovars in *\)
607
 *   List.iter nee s.assume;
608
 *   List.iter nee s.guarantees;
609
 *   List.iter (fun m -> 
610
 *       List.iter nee m.require;
611
 *     List.iter nee m.ensure
612
 *     ) s.modes; *)
613
   
614

    
615
                                                                     
616
  
617
  
618
    
619
(* The normalization phase introduces new local variables
620
   - output cannot be memories. If this happen, new local variables acting as
621
   memories are introduced. 
622
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
623
   access
624
   Thoses values are shared, ie. no duplicate expressions are introduced.
625

    
626
   Concerning specification, a similar process is applied, replacing an
627
   expression by a list of local variables and definitions
628
*)
629

    
630
(** normalize_node node returns a normalized node, 
631
    ie. 
632
    - updated locals
633
    - new equations
634
    -
635
*)
636
let normalize_node decls node =
637
  reset_cpt_fresh ();
638
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
639
  let not_is_orig_var v =
640
    List.for_all ((!=) v) orig_vars in
641
  let norm_ctx = {
642
      parentid = node.node_id;
643
      vars = get_node_vars node;
644
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
645
    }
646
  in
647
  
648
  let defs, vars =
649
    let eqs, auts = get_node_eqs node in
650
    if auts != [] then assert false; (* Automata should be expanded by now. *)
651
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
652
  (* Normalize the asserts *)
653
  let vars, assert_defs, asserts =
654
    List.fold_left (
655
      fun (vars, def_accu, assert_accu) assert_ ->
656
	let assert_expr = assert_.assert_expr in
657
	let (defs, vars'), expr = 
658
	  normalize_expr 
659
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
660
	    norm_ctx 
661
	    [] (* empty offset for arrays *)
662
	    ([], vars) (* defvar only contains vars *)
663
	    assert_expr
664
	in
665
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
666
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
667
    ) (vars, [], []) node.node_asserts in
668
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
669
							  vars and initial locals ones *)
670
  
671
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
672
						       beginning of the list the
673
						       local declared ones *)
674
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
675

    
676

    
677
  (* Updating annotations: traceability and machine types for fresh variables *)
678
  
679
  (* Compute traceability info:
680
     - gather newly bound variables
681
     - compute the associated expression without aliases
682
  *)
683
  let new_annots =
684
    if !Options.traces then
685
      begin
686
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
687
	let norm_traceability = {
688
	  annots = List.map (fun v ->
689
	    let eq =
690
	      try
691
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
692
	      with Not_found -> 
693
		(
694
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
695
		  assert false
696
		) 
697
	    in
698
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
699
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
700
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
701
	    (["traceability"], pair)
702
	  ) diff_vars;
703
	  annot_loc = Location.dummy_loc
704
	}
705
	in
706
	norm_traceability::node.node_annot
707
      end
708
    else
709
      node.node_annot
710
  in
711

    
712
  let new_annots =
713
    List.fold_left (fun annots v ->
714
      if Machine_types.is_active && Machine_types.is_exportable v then
715
	let typ = Machine_types.get_specified_type v in
716
  	let typ_name = Machine_types.type_name typ in
717

    
718
	let loc = v.var_loc in
719
	let typ_as_string =
720
	  mkexpr
721
	    loc
722
	    (Expr_const
723
	       (Const_string typ_name))
724
	in
725
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
726
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
727
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
728
      else
729
	annots
730
    ) new_annots new_locals
731
  in
732
  let spec =
733
    begin
734
      (* Update mutable fields of eexpr to perform normalization of
735
	 specification.
736

    
737
	 Careful: we do not normalize annotations, since they can have the form
738
	 x = (a, b, c) *)
739
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 
740
    end
741
  in
742
  
743
  
744
  let node =
745
    { node with
746
      node_locals = all_locals;
747
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
748
      node_asserts = asserts;
749
      node_annot = new_annots;
750
      node_spec = spec;
751
    }
752
  in ((*Printers.pp_node Format.err_formatter node;*)
753
    node
754
  )
755

    
756
let normalize_inode decls nd =
757
  reset_cpt_fresh ();
758
  match nd.nodei_spec with
759
    None -> nd
760
  | Some s ->
761
     let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
762
     { nd with nodei_spec = Some s }
763
  
764
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
765
  match decl.top_decl_desc with
766
  | Node nd ->
767
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
768
     update_node nd.node_id decl';
769
     decl'
770
  | ImportedNode nd ->
771
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
772
     update_node nd.nodei_id decl';
773
     decl'
774
     
775
    | Include _| Open _ | Const _ | TypeDef _ -> decl
776

    
777
let normalize_prog p decls =
778
  (* Backend specific configurations for normalization *)
779
  params := p;
780

    
781
  (* Main algorithm: iterates over nodes *)
782
  List.map (normalize_decl decls) decls
783

    
784

    
785
(* Fake interface for outside uses *)
786
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
787
  mk_expr_alias_opt
788
    opt
789
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
790
    (defs, vars)
791
    expr
792

    
793
    
794
           (* Local Variables: *)
795
           (* compile-command:"make -C .." *)
796
           (* End: *)
797