Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ f4cba4b8

History | View | Annotate | Download (31.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
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: in/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
  new_locals, defs,      
597
  {s with
598
    locals = s.locals @ new_locals;
599
    stmts = [];
600
    assume = assume';
601
    guarantees = guarantees';
602
    modes = modes'
603
  }
604
(* let nee _ = () in
605
 *   (\*normalize_eexpr decls iovars in *\)
606
 *   List.iter nee s.assume;
607
 *   List.iter nee s.guarantees;
608
 *   List.iter (fun m -> 
609
 *       List.iter nee m.require;
610
 *     List.iter nee m.ensure
611
 *     ) s.modes; *)
612
   
613

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

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

    
629
(** normalize_node node returns a normalized node, 
630
    ie. 
631
    - updated locals
632
    - new equations
633
    -
634
*)
635
let normalize_node decls node =
636
  reset_cpt_fresh ();
637
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
638
  let not_is_orig_var v =
639
    List.for_all ((!=) v) orig_vars in
640
  let norm_ctx = {
641
      parentid = node.node_id;
642
      vars = get_node_vars node;
643
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
644
    }
645
  in
646

    
647
  let eqs, auts = get_node_eqs node in
648
  if auts != [] then assert false; (* Automata should be expanded by now. *)
649
  let spec, new_vars, eqs =
650
    begin
651
      (* Update mutable fields of eexpr to perform normalization of
652
	 specification.
653

    
654
	 Careful: we do not normalize annotations, since they can have the form
655
	 x = (a, b, c) *)
656
      match node.node_spec with
657
      | None 
658
        | Some (NodeSpec _) -> node.node_spec, [], eqs
659
      | Some (Contract s) ->
660
         let new_locals, new_stmts, s' = normalize_spec
661
                    decls
662
                    node.node_id
663
                    (node.node_inputs, node.node_outputs, node.node_locals)
664
                    s
665
         in
666
         Some (Contract s'), new_locals, new_stmts@eqs
667
    end
668
  in
669
  let defs, vars =
670
    List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
671
  (* Normalize the asserts *)
672
  let vars, assert_defs, asserts =
673
    List.fold_left (
674
        fun (vars, def_accu, assert_accu) assert_ ->
675
	let assert_expr = assert_.assert_expr in
676
	let (defs, vars'), expr = 
677
	  normalize_expr 
678
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
679
	    norm_ctx 
680
	    [] (* empty offset for arrays *)
681
	    ([], vars) (* defvar only contains vars *)
682
	    assert_expr
683
	in
684
        (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
685
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
686
      ) (vars, [], []) node.node_asserts in
687
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
688
							  vars and initial locals ones *)
689
  
690
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
691
						       beginning of the list the
692
						       local declared ones *)
693
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
694

    
695

    
696
  (* Updating annotations: traceability and machine types for fresh variables *)
697
  
698
  (* Compute traceability info:
699
     - gather newly bound variables
700
     - compute the associated expression without aliases
701
   *)
702
  let new_annots =
703
    if !Options.traces then
704
      begin
705
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
706
	let norm_traceability = {
707
	    annots = List.map (fun v ->
708
	                 let eq =
709
	                   try
710
		             List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
711
	                   with Not_found -> 
712
		             (
713
		               Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
714
		               assert false
715
		             ) 
716
	                 in
717
	                 let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
718
	                 let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
719
	                 Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
720
	                 (["traceability"], pair)
721
	               ) diff_vars;
722
	    annot_loc = Location.dummy_loc
723
	  }
724
	in
725
	norm_traceability::node.node_annot
726
      end
727
    else
728
      node.node_annot
729
  in
730

    
731
  let new_annots =
732
    List.fold_left (fun annots v ->
733
        if Machine_types.is_active && Machine_types.is_exportable v then
734
	  let typ = Machine_types.get_specified_type v in
735
  	  let typ_name = Machine_types.type_name typ in
736

    
737
	  let loc = v.var_loc in
738
	  let typ_as_string =
739
	    mkexpr
740
	      loc
741
	      (Expr_const
742
	         (Const_string typ_name))
743
	  in
744
	  let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
745
	  Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
746
	  {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
747
        else
748
	  annots
749
      ) new_annots new_locals
750
  in
751
  
752
  
753
  let node =
754
    { node with
755
      node_locals = all_locals;
756
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
757
      node_asserts = asserts;
758
      node_annot = new_annots;
759
      node_spec = spec;
760
    }
761
  in ((*Printers.pp_node Format.err_formatter node;*)
762
      node
763
    )
764

    
765
let normalize_inode decls nd =
766
  reset_cpt_fresh ();
767
  match nd.nodei_spec with
768
    None | Some (NodeSpec _) -> nd
769
    | Some (Contract _) -> assert false
770
                         
771
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
772
  match decl.top_decl_desc with
773
  | Node nd ->
774
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
775
     update_node nd.node_id decl';
776
     decl'
777
  | ImportedNode nd ->
778
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
779
     update_node nd.nodei_id decl';
780
     decl'
781
     
782
    | Include _| Open _ | Const _ | TypeDef _ -> decl
783

    
784
let normalize_prog p decls =
785
  (* Backend specific configurations for normalization *)
786
  params := p;
787

    
788
  (* Main algorithm: iterates over nodes *)
789
  List.map (normalize_decl decls) decls
790

    
791

    
792
(* Fake interface for outside uses *)
793
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
794
  mk_expr_alias_opt
795
    opt
796
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
797
    (defs, vars)
798
    expr
799

    
800
    
801
           (* Local Variables: *)
802
           (* compile-command:"make -C .." *)
803
           (* End: *)
804