Project

General

Profile

Revision 0a10042e

View differences:

src/normalization.ml
191 191
      (defvars, norm_t :: qlist)
192 192
    ) elist (defvars, [])
193 193

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

  
274 281
(* Creates a conditional with a merge construct, which is more lazy *)
275 282
(*
276
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
277
 match expr.expr_desc with
278
 | Expr_ite (c, t, e) ->
279
   let defvars, norm_t = norm_expr (alias node offsets defvars t in
280
 | _ -> assert false
283
  let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
284
  match expr.expr_desc with
285
  | Expr_ite (c, t, e) ->
286
  let defvars, norm_t = norm_expr (alias node offsets defvars t in
287
  | _ -> assert false
281 288
*)
282 289
and normalize_branches node offsets defvars hl =
283
 List.fold_right
284
   (fun (t, h) (defvars, norm_q) ->
285
     let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
286
     defvars, (t, norm_h) :: norm_q
287
   )
288
   hl (defvars, [])
290
  List.fold_right
291
    (fun (t, h) (defvars, norm_q) ->
292
      let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
293
      defvars, (t, norm_h) :: norm_q
294
    )
295
    hl (defvars, [])
289 296

  
290 297
and normalize_array_expr ?(alias=true) node offsets defvars expr =
291 298
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
292 299
  match expr.expr_desc with
293 300
  | Expr_power (e1, d) when offsets = [] ->
294
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
295
    defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
301
     let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
302
     defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
296 303
  | Expr_power (e1, d) ->
297
    normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
304
     normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
298 305
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
299 306
  | Expr_array elist when offsets = [] ->
300
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
301
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
307
     let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
308
     defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
302 309
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
303
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
304
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
310
     let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
311
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
305 312
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
306 313

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

  
333 340
(* outputs cannot be memories as well. If so, introduce new local variable.

Also available in: Unified diff