Project

General

Profile

Revision 95944ba1

View differences:

src/causality.ml
395 395
      (fun td ->
396 396
	match td.top_decl_desc with 
397 397
	| Node nd ->
398
	   let prednode n = is_generic_node (Hashtbl.find node_table n) in
398
	   let prednode n = is_generic_node (node_from_name n) in
399 399
	   nd.node_gencalls <- get_calls prednode nd
400 400
	| _ -> ()
401 401
	   
src/compiler_stages.ml
67 67

  
68 68
  (* Importing source *)
69 69
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
70
  
70

  
71 71
  (* Registering types and clocks for future checks *)
72 72
  Global.type_env := Env.overwrite !Global.type_env typ_env;
73 73
  Global.clock_env := Env.overwrite !Global.clock_env clk_env;
src/corelang.ml
307 307
  | _ -> assert false
308 308

  
309 309
let node_from_name id =
310
  try
311
    Hashtbl.find node_table id
312
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
313
		     assert false)
310
      Hashtbl.find node_table id
311
  (* with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
312
   *       	     assert false) *)
313

  
314
let update_node id top =
315
  Hashtbl.replace node_table id top
314 316

  
315 317
let is_imported_node td =
316 318
  match td.top_decl_desc with 
......
1221 1223
let reset_cpt_fresh () =
1222 1224
    cpt_fresh := 0
1223 1225
    
1224
let mk_fresh_var node loc ty ck =
1225
  let vars = get_node_vars node in
1226
let mk_fresh_var (parentid, ctx_env) loc ty ck =
1226 1227
  let rec aux () =
1227 1228
  incr cpt_fresh;
1228
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
1229
  if List.exists (fun v -> v.var_id = s) vars then aux () else
1229
  let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in
1230
  if List.exists (fun v -> v.var_id = s) ctx_env then aux () else
1230 1231
  {
1231 1232
    var_id = s;
1232 1233
    var_orig = false;
......
1234 1235
    var_dec_clock = dummy_clock_dec;
1235 1236
    var_dec_const = false;
1236 1237
    var_dec_value = None;
1237
    var_parent_nodeid = Some node.node_id;
1238
    var_parent_nodeid = Some parentid;
1238 1239
    var_type = ty;
1239 1240
    var_clock = ck;
1240 1241
    var_loc = loc
src/corelang.mli
49 49
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
50 50
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
51 51
  
52
val node_table : (ident, top_decl) Hashtbl.t
52
(*val node_table : (ident, top_decl) Hashtbl.t*)
53 53
val print_node_table:  Format.formatter -> unit -> unit
54 54
val node_name: top_decl -> ident
55 55
val node_inputs: top_decl -> var_decl list
56 56
val node_from_name: ident -> top_decl
57
val update_node: ident -> top_decl -> unit
57 58
val is_generic_node: top_decl -> bool
58 59
val is_imported_node: top_decl -> bool
59 60

  
......
173 174
val expr_contains_expr: tag -> expr -> bool
174 175

  
175 176
val reset_cpt_fresh: unit -> unit
176
val mk_fresh_var: node_desc -> Location.t -> Types.type_expr ->  Clocks.clock_expr -> var_decl
177
  
178
(* mk_fresh_var parentid to be registered as parent_nodeid, vars is the list of existing vars in that context *)
179
val mk_fresh_var: (ident * var_decl list) -> Location.t -> Types.type_expr ->  Clocks.clock_expr -> var_decl
177 180

  
178 181
val find_eq: ident list -> eq list -> eq * eq list
179 182
val get_expr_calls: top_decl list -> expr -> Utils.ISet.t
src/features/machine_types/machine_types.ml
417 417
  in
418 418
  typing_env := env
419 419

  
420
let type_expr nd expr =
420
let type_expr (parentid, init_vars) expr =
421 421
  let init_env = !typing_env in
422 422
  (* Format.eprintf "Init env: %a@." (Env.pp_env MTypes.print_ty) init_env; *)
423
  let init_vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
424 423
  (* Rebuilding the variables environment from accumulated knowledge *)
425 424
  let env,vars = (* First, we add non specified variables *)
426 425
    List.fold_left (fun (env, vars) v ->
......
435 434
  (* Then declared ones *)
436 435
  let env, vars =
437 436
    Hashtbl.fold (fun vdecl machine_type (env, vds) ->
438
      if vdecl.var_parent_nodeid = Some nd.node_id then (
437
      if vdecl.var_parent_nodeid = Some parentid then (
439 438
	 (* Format.eprintf "Adding variable %a to the environement@.@?" Printers.pp_var vdecl;  *)
440 439
	let env = Env.add_value env vdecl.var_id machine_type in
441 440
	env, vdecl::vds
src/modules.ml
27 27
let add_imported_node name value =
28 28
(*Format.eprintf "add_imported_node %s %a (owner=%s)@." name Printers.pp_imported_node (imported_node_of_top value) value.top_decl_owner;*)
29 29
  try
30
    let value' = Hashtbl.find node_table name in
30
    let value' = node_from_name name in
31 31
    let owner' = value'.top_decl_owner in
32 32
    let itf' = value'.top_decl_itf in
33 33
    let owner = value.top_decl_owner in
34 34
    let itf = value.top_decl_itf in
35 35
    match value'.top_decl_desc, value.top_decl_desc with
36
    | Node _        , ImportedNode _  when owner = owner' && itf' && (not itf) -> Hashtbl.add node_table name value
36
    | Node _        , ImportedNode _  when owner = owner' && itf' && (not itf) -> update_node name value
37 37
    | ImportedNode _, ImportedNode _            -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
38 38
    | _                                         -> assert false
39 39
  with
40
    Not_found                                   -> Hashtbl.add node_table name value
40
    Not_found                                   -> update_node name value
41 41

  
42 42
let add_node name value =
43 43
(*Format.eprintf "add_node %s %a (owner=%s)@." name Printers.pp_imported_node (get_node_interface (node_of_top value)) value.top_decl_owner;*)
44 44
  try
45
    let value' = Hashtbl.find node_table name in
45
    let value' = node_from_name name in
46 46
    let owner' = value'.top_decl_owner in
47 47
    let itf' = value'.top_decl_itf in
48 48
    let owner = value.top_decl_owner in
......
52 52
    | Node _        , Node _                    -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
53 53
    | _                                         -> assert false
54 54
  with
55
    Not_found                                   -> Hashtbl.add node_table name value
55
    Not_found                                   -> update_node name value
56 56

  
57 57

  
58 58
let add_tag loc name typ =
src/normalization.ml
43 43
                 force_alias_internal_fun =false;
44 44
               }
45 45

  
46
  
46
type norm_ctx_t =
47
  {
48
    parentid: ident;
49
    vars: var_decl list;
50
    is_output: ident -> bool; 
51
  }
52

  
53
           
47 54
let expr_true loc ck =
48 55
{ expr_tag = Utils.new_tag ();
49 56
  expr_desc = Expr_const (Const_tag tag_true);
......
115 122
  in
116 123
 List.fold_left add_offset e offsets
117 124

  
125
(* IS IT USED ? TODO 
118 126
(* Create an alias for [expr], if none exists yet *)
119
let mk_expr_alias node (defs, vars) expr =
127
let mk_expr_alias (parentid, vars) (defs, vars) expr =
120 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;*)
121 129
  match get_expr_alias defs expr with
122 130
  | Some eq ->
......
125 133
  | None    ->
126 134
    let new_aliases =
127 135
      List.map2
128
	(mk_fresh_var node expr.expr_loc)
136
	(mk_fresh_var (parentid, vars) expr.expr_loc)
129 137
	(Types.type_list_of_type expr.expr_type)
130 138
	(Clocks.clock_list_of_clock expr.expr_clock) in
131 139
    let new_def =
......
133 141
    in
134 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; *)
135 143
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
136

  
144
 *)
145
  
137 146
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
138 147
   and [opt] is true *)
139
let mk_expr_alias_opt opt node (defs, vars) expr =
148
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
140 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;*)
141 150
  match expr.expr_desc with
142 151
  | Expr_ident alias ->
......
161 170
      then
162 171
	let new_aliases =
163 172
	  List.map2
164
	    (mk_fresh_var node expr.expr_loc)
173
	    (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
165 174
	    (Types.type_list_of_type expr.expr_type)
166 175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
167 176
	let new_def =
168 177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
169 178
	in
170 179
	(* Typing and Registering machine type *) 
171
	let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr  in
180
	let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr  in
172 181
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
173 182
      else
174 183
	(defs, vars), expr
......
186 195
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
187 196
														
188 197
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
189
let rec normalize_list alias node offsets norm_element defvars elist =
198
let rec normalize_list alias norm_ctx offsets norm_element defvars elist =
190 199
  List.fold_right
191 200
    (fun t (defvars, qlist) ->
192
      let defvars, norm_t = norm_element alias node offsets defvars t in
201
      let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
193 202
      (defvars, norm_t :: qlist)
194 203
    ) elist (defvars, [])
195 204

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

  
283 292
(* Creates a conditional with a merge construct, which is more lazy *)
284 293
(*
......
288 297
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
289 298
  | _ -> assert false
290 299
*)
291
and normalize_branches node offsets defvars hl =
300
and normalize_branches norm_ctx offsets defvars hl =
292 301
  List.fold_right
293 302
    (fun (t, h) (defvars, norm_q) ->
294
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
303
      let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in
295 304
      defvars, (t, norm_h) :: norm_q
296 305
    )
297 306
    hl (defvars, [])
298 307

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

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

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

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

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

  
402 411
  with _ -> (
......
404 413
    assert false
405 414
  )
406 415

  
407
let normalize_eexpr decls node vars ee =
416
let normalize_eexpr decls norm_ctx vars ee = ee (*
408 417
  (* New output variable *)
409 418
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
410 419
  let output_var = 
......
474 483
      
475 484
    ;
476 485
    raise exc
477
    
486
                                                 *)    
478 487
 
479 488
    
480
let normalize_spec decls node vars s =
481
  let nee = normalize_eexpr decls node vars in
489
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 *)
482 508
  List.iter nee s.assume;
483 509
  List.iter nee s.guarantees;
484 510
  List.iter (fun m -> 
485 511
      List.iter nee m.require;
486 512
    List.iter nee m.ensure
487
  ) s.modes
488
  
513
    ) s.modes;
514
   *)
515
  s
516
                                       *)
489 517
    
490 518
(* The normalization phase introduces new local variables
491 519
   - output cannot be memories. If this happen, new local variables acting as
......
510 538
  let orig_vars = inputs_outputs@node.node_locals in
511 539
  let not_is_orig_var v =
512 540
    List.for_all ((!=) v) orig_vars in
541
  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
  
513 548
  let defs, vars =
514 549
    let eqs, auts = get_node_eqs node in
515 550
    if auts != [] then assert false; (* Automata should be expanded by now. *)
516
    List.fold_left (normalize_eq node) ([], orig_vars) eqs in
551
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
517 552
  (* Normalize the asserts *)
518 553
  let vars, assert_defs, asserts =
519 554
    List.fold_left (
......
522 557
	let (defs, vars'), expr = 
523 558
	  normalize_expr 
524 559
	    ~alias:true (* forcing introduction of new equations for fcn calls *) 
525
	    node 
560
	    norm_ctx 
526 561
	    [] (* empty offset for arrays *)
527 562
	    ([], vars) (* defvar only contains vars *)
528 563
	    assert_expr
......
594 629
	annots
595 630
    ) new_annots new_locals
596 631
  in
597
  if !Options.spec <> "no" then 
632
  let spec =
598 633
    begin
599 634
      (* Update mutable fields of eexpr to perform normalization of
600 635
	 specification.
601 636

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

  
626

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

  
635 678
let normalize_prog p decls =
636 679
  (* Backend specific configurations for normalization *)
......
639 682
  (* Main algorithm: iterates over nodes *)
640 683
  List.map (normalize_decl decls) decls
641 684

  
685

  
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

  
642 694
    
643 695
           (* Local Variables: *)
644 696
           (* compile-command:"make -C .." *)
src/normalization.mli
1
open Lustre_types
2

  
1 3
type param_t =
2 4
  {
3 5
    unfold_arrow_active: bool;
......
6 8
  }
7 9

  
8 10

  
9
val mk_expr_alias_opt: bool -> Lustre_types.node_desc -> (Lustre_types.eq list * Lustre_types.var_decl list)-> Lustre_types.expr -> (Lustre_types.eq list * Lustre_types.var_decl list) * Lustre_types.expr
10
val normalize_prog: param_t -> Lustre_types.program_t -> Lustre_types.program_t
11
val mk_expr_alias_opt: bool -> (ident * var_decl list) -> (eq list * var_decl list)-> expr -> (eq list * var_decl list) * expr
12
val normalize_prog: param_t -> program_t -> program_t
src/plugins/mpfr/mpfr.ml
262 262
let inject_node node = 
263 263
  cpt_fresh := 0;
264 264
  let inputs_outputs = node.node_inputs@node.node_outputs in
265
  let norm_ctx = (node.node_id, get_node_vars node) in
265 266
  let is_local v =
266 267
    List.for_all ((!=) v) inputs_outputs in
267 268
  let orig_vars = inputs_outputs@node.node_locals in
268 269
  let defs, vars =
269 270
    let eqs, auts = get_node_eqs node in
270 271
    if auts != [] then assert false; (* Automata should be expanded by now. *)
271
    List.fold_left (inject_eq node) ([], orig_vars) eqs in
272
    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in
272 273
  (* Normalize the asserts *)
273 274
  let vars, assert_defs, asserts = 
274 275
    List.fold_left (
......
277 278
      let (defs, vars'), expr = 
278 279
	inject_expr 
279 280
	  ~alias:false 
280
	  node 
281
	  norm_ctx 
281 282
	  ([], vars) (* defvar only contains vars *)
282 283
	  assert_expr
283 284
      in

Also available in: Unified diff