Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 95944ba1

History | View | Annotate | Download (27.4 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12
open Utils
13 8446bf03 ploc
open Lustre_types
14 22fe1c93 ploc
open Corelang
15
open Format
16
17 27dc3869 ploc
(** 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 ad4774b0 ploc
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 27dc3869 ploc
46 95944ba1 ploc
type norm_ctx_t =
47
  {
48
    parentid: ident;
49
    vars: var_decl list;
50
    is_output: ident -> bool; 
51
  }
52
53
           
54 2e6f9ba8 xthirioux
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 a38c681e xthirioux
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
90 2e6f9ba8 xthirioux
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
91
 | _                   -> assert false
92
93 22fe1c93 ploc
94
95
(* Get the equation in [defs] with [expr] as rhs, if any *)
96
let get_expr_alias defs expr =
97 0bd19a92 THIRIOUX Xavier
 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 22fe1c93 ploc
 with
99 e49b6d55 xavier.thirioux
 | Not_found -> None
100
  
101 22fe1c93 ploc
(* 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 fc886259 xthirioux
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
111 22fe1c93 ploc
112
let unfold_offsets e offsets =
113
  let add_offset e d =
114 fc886259 xthirioux
(*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 22fe1c93 ploc
    { 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 fc886259 xthirioux
      expr_desc = Expr_access (e, d) }
121
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
122
  in
123 22fe1c93 ploc
 List.fold_left add_offset e offsets
124
125 95944ba1 ploc
(* IS IT USED ? TODO 
126 22fe1c93 ploc
(* Create an alias for [expr], if none exists yet *)
127 95944ba1 ploc
let mk_expr_alias (parentid, vars) (defs, vars) expr =
128 a38c681e xthirioux
(*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 22fe1c93 ploc
  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 95944ba1 ploc
	(mk_fresh_var (parentid, vars) expr.expr_loc)
137 22fe1c93 ploc
	(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 3ca6d126 ploc
    in
142 fc886259 xthirioux
    (* 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 3ca6d126 ploc
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
144 95944ba1 ploc
 *)
145
  
146 d4807c3d xthirioux
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
147
   and [opt] is true *)
148 95944ba1 ploc
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
149 04a63d25 xthirioux
(*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 d4807c3d xthirioux
  match expr.expr_desc with
151
  | Expr_ident alias ->
152 04a63d25 xthirioux
    (defs, vars), expr
153 8deaa2dd tkahsai
  | _                ->
154 04a63d25 xthirioux
    match get_expr_alias defs expr with
155
    | Some eq ->
156 c35de73b ploc
       (* Format.eprintf "Found a preexisting definition@."; *)
157 04a63d25 xthirioux
      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 c35de73b ploc
       (* 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 04a63d25 xthirioux
      if opt
170
      then
171
	let new_aliases =
172
	  List.map2
173 95944ba1 ploc
	    (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
174 04a63d25 xthirioux
	    (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 66359a5e ploc
	in
179
	(* Typing and Registering machine type *) 
180 95944ba1 ploc
	let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr  in
181 66359a5e ploc
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
182 04a63d25 xthirioux
      else
183
	(defs, vars), expr
184 22fe1c93 ploc
185 8deaa2dd tkahsai
(* Create a (normalized) expression from [ref_e],
186 22fe1c93 ploc
   replacing description with [norm_d],
187 8deaa2dd tkahsai
   taking propagated [offsets] into account
188 22fe1c93 ploc
   in order to change expression type *)
189
let mk_norm_expr offsets ref_e norm_d =
190 e49b6d55 xavier.thirioux
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
191 22fe1c93 ploc
  let drop_array_type ty =
192
    Types.map_tuple_type Types.array_element_type ty in
193
  { ref_e with
194
    expr_desc = norm_d;
195
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
196 e49b6d55 xavier.thirioux
														
197 22fe1c93 ploc
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
198 95944ba1 ploc
let rec normalize_list alias norm_ctx offsets norm_element defvars elist =
199 22fe1c93 ploc
  List.fold_right
200
    (fun t (defvars, qlist) ->
201 95944ba1 ploc
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
202 22fe1c93 ploc
      (defvars, norm_t :: qlist)
203
    ) elist (defvars, [])
204
205 95944ba1 ploc
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr =
206 e49b6d55 xavier.thirioux
  (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
207 22fe1c93 ploc
  match expr.expr_desc with
208 8deaa2dd tkahsai
  | Expr_const _
209 22fe1c93 ploc
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
210
  | Expr_array elist ->
211 95944ba1 ploc
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
212 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
213 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
214 22fe1c93 ploc
  | Expr_power (e1, d) when offsets = [] ->
215 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
216 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
217 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
218 22fe1c93 ploc
  | Expr_power (e1, d) ->
219 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
220 22fe1c93 ploc
  | Expr_access (e1, d) ->
221 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1
222 8deaa2dd tkahsai
  | Expr_tuple elist ->
223 0a10042e ploc
     let defvars, norm_elist =
224 95944ba1 ploc
       normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in
225 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
226 8deaa2dd tkahsai
  | Expr_appl (id, args, None)
227 04a63d25 xthirioux
      when Basic_library.is_homomorphic_fun id 
228 af5af1e8 ploc
	&& Types.is_array_type expr.expr_type ->
229 0a10042e ploc
     let defvars, norm_args =
230
       normalize_list
231
	 alias
232 95944ba1 ploc
	 norm_ctx
233 0a10042e ploc
	 offsets
234
	 (fun _ -> normalize_array_expr ~alias:true)
235
	 defvars
236
	 (expr_list_of_expr args)
237
     in
238
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
239 3436d1a6 ploc
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
240 ad4774b0 ploc
      && not (!params.force_alias_internal_fun || alias_basic) ->
241 95944ba1 ploc
     let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in
242 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
243 22fe1c93 ploc
  | Expr_appl (id, args, r) ->
244 0a10042e ploc
     let defvars, r =
245
       match r with
246
       | None -> defvars, None
247
       | Some r ->
248 95944ba1 ploc
	  let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in
249 0a10042e ploc
	  defvars, Some norm_r
250
     in
251 95944ba1 ploc
     let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
252 0a10042e ploc
     let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
253
     if offsets <> []
254
     then
255 95944ba1 ploc
       let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
256
       normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr
257 0a10042e ploc
     else
258 ad4774b0 ploc
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
259 0a10042e ploc
				    || not (Basic_library.is_expr_internal_fun expr)))
260 95944ba1 ploc
	 norm_ctx defvars norm_expr
261 ad4774b0 ploc
  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
262 0a10042e ploc
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
263 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)
264 2e6f9ba8 xthirioux
  | Expr_arrow (e1,e2) ->
265 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
266
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
267 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
268 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
269 22fe1c93 ploc
  | Expr_pre e ->
270 95944ba1 ploc
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
271 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
272 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
273 22fe1c93 ploc
  | Expr_fby (e1, e2) ->
274 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
275
     let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
276 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
277 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
278 22fe1c93 ploc
  | Expr_when (e, c, l) ->
279 95944ba1 ploc
     let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
280 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
281 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
282 95944ba1 ploc
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
283
     let defvars, norm_t = normalize_cond_expr  norm_ctx offsets defvars t in
284
     let defvars, norm_e = normalize_cond_expr  norm_ctx offsets defvars e in
285 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
286 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
287 22fe1c93 ploc
  | Expr_merge (c, hl) ->
288 95944ba1 ploc
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
289 0a10042e ploc
     let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
290 95944ba1 ploc
     mk_expr_alias_opt alias norm_ctx defvars norm_expr
291 8deaa2dd tkahsai
292 52cfee34 xthirioux
(* Creates a conditional with a merge construct, which is more lazy *)
293
(*
294 0a10042e ploc
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
295
  match expr.expr_desc with
296
  | Expr_ite (c, t, e) ->
297
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
298
  | _ -> assert false
299 52cfee34 xthirioux
*)
300 95944ba1 ploc
and normalize_branches norm_ctx offsets defvars hl =
301 0a10042e ploc
  List.fold_right
302
    (fun (t, h) (defvars, norm_q) ->
303 95944ba1 ploc
      let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in
304 0a10042e ploc
      defvars, (t, norm_h) :: norm_q
305
    )
306
    hl (defvars, [])
307 22fe1c93 ploc
308 95944ba1 ploc
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
309 04a63d25 xthirioux
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
310 22fe1c93 ploc
  match expr.expr_desc with
311
  | Expr_power (e1, d) when offsets = [] ->
312 95944ba1 ploc
     let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
313 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
314 22fe1c93 ploc
  | Expr_power (e1, d) ->
315 95944ba1 ploc
     normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
316
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1
317 22fe1c93 ploc
  | Expr_array elist when offsets = [] ->
318 95944ba1 ploc
     let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
319 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
320 04a63d25 xthirioux
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
321 95944ba1 ploc
     let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
322 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
323 95944ba1 ploc
  |  _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr
324 22fe1c93 ploc
325 95944ba1 ploc
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr =
326 22fe1c93 ploc
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
327
  match expr.expr_desc with
328
  | Expr_access (e1, d) ->
329 95944ba1 ploc
     normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
330 22fe1c93 ploc
  | Expr_ite (c, t, e) ->
331 95944ba1 ploc
     let defvars, norm_c = normalize_guard norm_ctx defvars c in
332
     let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
333
     let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
334 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
335 22fe1c93 ploc
  | Expr_merge (c, hl) ->
336 95944ba1 ploc
     let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
337 0a10042e ploc
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
338 ad4774b0 ploc
  | _ when !params.force_alias_ite ->
339 27dc3869 ploc
     (* Forcing alias creation for then/else expressions *)
340
     let defvars, norm_expr =
341 95944ba1 ploc
       normalize_expr ~alias:alias norm_ctx offsets defvars expr
342 27dc3869 ploc
     in
343 95944ba1 ploc
     mk_expr_alias_opt true norm_ctx defvars norm_expr
344 27dc3869 ploc
  | _ -> (* default case without the force_alias_ite option *)
345 95944ba1 ploc
     normalize_expr ~alias:alias norm_ctx offsets defvars expr
346 0a10042e ploc
       
347 95944ba1 ploc
and normalize_guard norm_ctx defvars expr =
348
  let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in
349
  mk_expr_alias_opt true norm_ctx defvars norm_expr
350 22fe1c93 ploc
351
(* outputs cannot be memories as well. If so, introduce new local variable.
352
*)
353 95944ba1 ploc
let decouple_outputs norm_ctx defvars eq =
354 22fe1c93 ploc
  let rec fold_lhs defvars lhs tys cks =
355 a742719e ploc
    match lhs, tys, cks with
356
    | [], [], []          -> defvars, []
357
    | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
358 95944ba1 ploc
			     if norm_ctx.is_output v
359 a742719e ploc
			     then
360 95944ba1 ploc
			       let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in
361 a742719e ploc
			       let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
362
			       (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
363
			     else
364
			       (defs_q, vars_q), v::lhs_q
365
    | _                   -> assert false in
366 22fe1c93 ploc
  let defvars', lhs' =
367
    fold_lhs
368
      defvars
369
      eq.eq_lhs
370
      (Types.type_list_of_type eq.eq_rhs.expr_type)
371
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
372
  defvars', {eq with eq_lhs = lhs' }
373
374 95944ba1 ploc
let rec normalize_eq norm_ctx defvars eq =
375 04a63d25 xthirioux
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
376 22fe1c93 ploc
  match eq.eq_rhs.expr_desc with
377
  | Expr_pre _
378
  | Expr_fby _  ->
379 95944ba1 ploc
    let (defvars', eq') = decouple_outputs norm_ctx defvars eq in
380
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in
381 22fe1c93 ploc
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
382
    (norm_eq::defs', vars')
383
  | Expr_array _ ->
384 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
385 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
386
    (norm_eq::defs', vars')
387 04a63d25 xthirioux
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
388 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
389 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
390
    (norm_eq::defs', vars')
391
  | Expr_appl _ ->
392 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
393 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
394
    (norm_eq::defs', vars')
395
  | _ ->
396 95944ba1 ploc
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in
397 22fe1c93 ploc
    let norm_eq = { eq with eq_rhs = norm_rhs } in
398
    norm_eq::defs', vars'
399
400 95944ba1 ploc
let normalize_eq_split norm_ctx defvars eq =
401 8fa4e28e ploc
  try
402 95944ba1 ploc
    let defs, vars = normalize_eq norm_ctx defvars eq in
403 949b2e1e ploc
  List.fold_right (fun eq (def, vars) -> 
404
    let eq_defs = Splitting.tuple_split_eq eq in
405
    if eq_defs = [eq] then
406
      eq::def, vars 
407
    else
408 95944ba1 ploc
      List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
409 949b2e1e ploc
  ) defs ([], vars)  
410
411 8fa4e28e ploc
  with _ -> (
412
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
413
    assert false
414
  )
415
416 95944ba1 ploc
let normalize_eexpr decls norm_ctx vars ee = ee (*
417 949b2e1e ploc
  (* New output variable *)
418
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
419
  let output_var = 
420
    mkvar_decl 
421
      ee.eexpr_loc 
422
      (output_id, 
423
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
424
       mkclock ee.eexpr_loc Ckdec_any, 
425
       false (* not a constant *),
426
       None,
427
       None
428
      ) 
429
  in
430 8fa4e28e ploc
  
431 949b2e1e ploc
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
432
  (* Calls are first inlined *)
433
  let nodes = get_nodes decls in
434
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
435
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
436
   let calls = List.map 
437
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
438
  in
439
*)
440
  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
441
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
442
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
443
  let (new_locals, eqs) =
444
    if calls = [] && not (eq_has_arrows eq) then
445
      (locals, [eq])     
446
    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
447
(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
448
      (*Format.eprintf "eqs %a@.@?" 
449
	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
450
      (new_locals, eqs)
451
*)
452
           (locals, [eq])     
453
 
454
    ) in
455
  (* Normalizing expr and eqs *)
456 8fa4e28e ploc
    let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
457
    let todefine = List.fold_left
458 949b2e1e ploc
    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
459
    (ISet.add output_id ISet.empty) vars in
460 8fa4e28e ploc
  
461 949b2e1e ploc
  try
462 2d27eedd ploc
    let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
463 949b2e1e ploc
    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
464
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
465
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
466
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
467
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
468
  (* check that table is empty *)
469
    if (not (ISet.is_empty undefined_vars)) then
470
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
471
    
472
    (*Format.eprintf "normalized eqs %a@.@?" 
473
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
474
    ee.eexpr_normalized <- Some (output_var, defs, vars)
475 8fa4e28e ploc
    
476 949b2e1e ploc
  with (Types.Error (loc,err)) as exc ->
477
    eprintf "Typing error for eexpr %a: %a%a%a@."
478
      Printers.pp_eexpr ee
479
      Types.pp_error err
480
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
481
      Location.pp_loc loc
482 8fa4e28e ploc
  
483 949b2e1e ploc
      
484 8fa4e28e ploc
    ;
485 949b2e1e ploc
    raise exc
486 95944ba1 ploc
                                                 *)    
487 8fa4e28e ploc
 
488
    
489 95944ba1 ploc
let normalize_spec decls iovars s = s (*
490
  (* Each stmt is normalized *)
491
  let orig_vars = iovars @ s.locals in
492
  let not_is_orig_var v =
493
    List.for_all ((!=) v) orig_vars in
494
  let defs, vars = 
495
    let eqs, auts = List.fold_right (fun (el,al) s -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
496
    if auts != [] then assert false; (* Automata should be expanded by now. *)
497
    List.fold_left (normalize_eq node) ([], orig_vars) eqs
498
  in
499
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
500
501
  (*
502
      
503
  {s with
504
    locals = s.locals @ new_locals;
505
    stmts = List.map (fun eq -> Eq eq) defs;
506
  let nee _ = () in
507
  (*normalize_eexpr decls iovars in *)
508 778c80fd ploc
  List.iter nee s.assume;
509
  List.iter nee s.guarantees;
510
  List.iter (fun m -> 
511
      List.iter nee m.require;
512
    List.iter nee m.ensure
513 95944ba1 ploc
    ) s.modes;
514
   *)
515
  s
516
                                       *)
517 949b2e1e ploc
    
518
(* The normalization phase introduces new local variables
519
   - output cannot be memories. If this happen, new local variables acting as
520
   memories are introduced. 
521
   - array constants, pre, arrow, fby, ite, merge, calls to node with index
522
   access
523
   Thoses values are shared, ie. no duplicate expressions are introduced.
524
525
   Concerning specification, a similar process is applied, replacing an
526
   expression by a list of local variables and definitions
527
*)
528
529
(** normalize_node node returns a normalized node, 
530
    ie. 
531 af5af1e8 ploc
    - updated locals
532
    - new equations
533 8deaa2dd tkahsai
    -
534 af5af1e8 ploc
*)
535 949b2e1e ploc
let normalize_node decls node =
536 7065d912 ploc
  reset_cpt_fresh ();
537 22fe1c93 ploc
  let inputs_outputs = node.node_inputs@node.node_outputs in
538 af5af1e8 ploc
  let orig_vars = inputs_outputs@node.node_locals in
539 50dadc21 ploc
  let not_is_orig_var v =
540
    List.for_all ((!=) v) orig_vars in
541 95944ba1 ploc
  let norm_ctx = {
542
      parentid = node.node_id;
543
      vars = get_node_vars node;
544
      is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
545
    }
546
  in
547
  
548 8deaa2dd tkahsai
  let defs, vars =
549 333e3a25 ploc
    let eqs, auts = get_node_eqs node in
550
    if auts != [] then assert false; (* Automata should be expanded by now. *)
551 95944ba1 ploc
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
552 af5af1e8 ploc
  (* Normalize the asserts *)
553 8deaa2dd tkahsai
  let vars, assert_defs, asserts =
554 af5af1e8 ploc
    List.fold_left (
555 50dadc21 ploc
      fun (vars, def_accu, assert_accu) assert_ ->
556
	let assert_expr = assert_.assert_expr in
557
	let (defs, vars'), expr = 
558
	  normalize_expr 
559
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
560 95944ba1 ploc
	    norm_ctx 
561 50dadc21 ploc
	    [] (* empty offset for arrays *)
562
	    ([], vars) (* defvar only contains vars *)
563
	    assert_expr
564
	in
565 8deaa2dd tkahsai
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
566 50dadc21 ploc
	vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
567 af5af1e8 ploc
    ) (vars, [], []) node.node_asserts in
568 50dadc21 ploc
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
569
							  vars and initial locals ones *)
570 66359a5e ploc
  
571
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
572 50dadc21 ploc
						       beginning of the list the
573
						       local declared ones *)
574 8deaa2dd tkahsai
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
575 f2b1c245 ploc
576 66359a5e ploc
577
  (* Updating annotations: traceability and machine types for fresh variables *)
578
  
579
  (* Compute traceability info:
580
     - gather newly bound variables
581
     - compute the associated expression without aliases
582
  *)
583 ea1c2906 ploc
  let new_annots =
584
    if !Options.traces then
585
      begin
586 66359a5e ploc
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
587 ea1c2906 ploc
	let norm_traceability = {
588
	  annots = List.map (fun v ->
589
	    let eq =
590
	      try
591 45f0f48d xthirioux
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
592
	      with Not_found -> 
593
		(
594
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
595
		  assert false
596
		) 
597
	    in
598 b98a4a58 ploc
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
599 ea1c2906 ploc
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
600 66359a5e ploc
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
601 ea1c2906 ploc
	    (["traceability"], pair)
602
	  ) diff_vars;
603
	  annot_loc = Location.dummy_loc
604 8deaa2dd tkahsai
	}
605 ea1c2906 ploc
	in
606
	norm_traceability::node.node_annot
607
      end
608
    else
609
      node.node_annot
610 af5af1e8 ploc
  in
611 ea1c2906 ploc
612 66359a5e ploc
  let new_annots =
613
    List.fold_left (fun annots v ->
614 f4050bef ploc
      if Machine_types.is_active && Machine_types.is_exportable v then
615 66359a5e ploc
	let typ = Machine_types.get_specified_type v in
616
  	let typ_name = Machine_types.type_name typ in
617
618
	let loc = v.var_loc in
619
	let typ_as_string =
620
	  mkexpr
621
	    loc
622
	    (Expr_const
623
	       (Const_string typ_name))
624
	in
625
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
626
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
627
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
628
      else
629
	annots
630
    ) new_annots new_locals
631
  in
632 95944ba1 ploc
  let spec =
633 949b2e1e ploc
    begin
634 8fa4e28e ploc
      (* Update mutable fields of eexpr to perform normalization of
635
	 specification.
636
637
	 Careful: we do not normalize annotations, since they can have the form
638
	 x = (a, b, c) *)
639 95944ba1 ploc
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls inputs_outputs s) 
640
    end
641
  in
642
  
643 949b2e1e ploc
  
644 22fe1c93 ploc
  let node =
645 50dadc21 ploc
    { node with
646 66359a5e ploc
      node_locals = all_locals;
647 50dadc21 ploc
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
648
      node_asserts = asserts;
649
      node_annot = new_annots;
650 95944ba1 ploc
      node_spec = spec;
651 50dadc21 ploc
    }
652 8deaa2dd tkahsai
  in ((*Printers.pp_node Format.err_formatter node;*)
653 f2b1c245 ploc
    node
654 50dadc21 ploc
  )
655 f2b1c245 ploc
656 95944ba1 ploc
let normalize_inode decls nd =
657
  reset_cpt_fresh ();
658
  match nd.nodei_spec with
659
    None -> nd
660
  | Some s ->
661
     let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in
662
     let s = normalize_spec decls inputs_outputs s in
663
     { nd with nodei_spec = Some s }
664
  
665 82906771 ploc
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
666 22fe1c93 ploc
  match decl.top_decl_desc with
667
  | Node nd ->
668 95944ba1 ploc
     let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
669
     update_node nd.node_id decl';
670
     decl'
671
  | ImportedNode nd ->
672
     let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
673
     update_node nd.nodei_id decl';
674
     decl'
675
     
676
    | Include _| Open _ | Const _ | TypeDef _ -> decl
677 8deaa2dd tkahsai
678 ad4774b0 ploc
let normalize_prog p decls =
679 27dc3869 ploc
  (* Backend specific configurations for normalization *)
680 ad4774b0 ploc
  params := p;
681 22fe1c93 ploc
682 27dc3869 ploc
  (* Main algorithm: iterates over nodes *)
683 82906771 ploc
  List.map (normalize_decl decls) decls
684 ad4774b0 ploc
685 95944ba1 ploc
686
(* Fake interface for outside uses *)
687
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
688
  mk_expr_alias_opt
689
    opt
690
    {parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) }
691
    (defs, vars)
692
    expr
693
694 ad4774b0 ploc
    
695
           (* Local Variables: *)
696
           (* compile-command:"make -C .." *)
697
           (* End: *)
698