Project

General

Profile

Revision 53206908 src/normalization.ml

View differences:

src/normalization.ml
95 95

  
96 96
let unfold_offsets e offsets =
97 97
  let add_offset e d =
98
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
99
    let res = *)
98
(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*)
100 99
    { e with
101 100
      expr_tag = Utils.new_tag ();
102 101
      expr_loc = d.Dimension.dim_loc;
103 102
      expr_type = Types.array_element_type e.expr_type;
104
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
103
      expr_desc = Expr_access (e, d) } in
107 104
 List.fold_left add_offset e offsets
108 105

  
109 106
(* Create an alias for [expr], if none exists yet *)
......
121 118
	(Clocks.clock_list_of_clock expr.expr_clock) in
122 119
    let new_def =
123 120
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
124
    in
125
    (* 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; *)
126
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
121
    in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127 122

  
128 123
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129 124
   and [opt] is true *)
130
let mk_expr_alias_opt opt node defvars expr =
125
let mk_expr_alias_opt opt node (defs, vars) expr =
126
(*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;*)
131 127
  match expr.expr_desc with
132 128
  | Expr_ident alias ->
133
    defvars, expr
129
    (defs, vars), expr
134 130
  | _                ->
135
    if opt
136
    then
137
      mk_expr_alias node defvars expr
138
    else
139
      defvars, expr
131
    match get_expr_alias defs expr with
132
    | Some eq ->
133
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
134
      (defs, vars), replace_expr aliases expr
135
    | None    ->
136
      if opt
137
      then
138
	let new_aliases =
139
	  List.map2
140
	    (mk_fresh_var node expr.expr_loc)
141
	    (Types.type_list_of_type expr.expr_type)
142
	    (Clocks.clock_list_of_clock expr.expr_clock) in
143
	let new_def =
144
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
145
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
146
      else
147
	(defs, vars), expr
140 148

  
141 149
(* Create a (normalized) expression from [ref_e],
142 150
   replacing description with [norm_d],
......
159 167
    ) elist (defvars, [])
160 168

  
161 169
let rec normalize_expr ?(alias=true) node offsets defvars expr =
162
(*  Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
170
(*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;*)
163 171
  match expr.expr_desc with
164 172
  | Expr_const _
165 173
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
......
179 187
    let defvars, norm_elist =
180 188
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
181 189
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
182
  | Expr_appl (id, args, None)
183
      when Basic_library.is_internal_fun id
190
  | Expr_appl (id, args, None) 
191
      when Basic_library.is_homomorphic_fun id 
184 192
	&& Types.is_array_type expr.expr_type ->
185 193
    let defvars, norm_args =
186 194
      normalize_list
......
192 200
	(expr_list_of_expr args)
193 201
    in
194 202
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
195
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
203
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
196 204
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
197 205
    defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
198 206
  | Expr_appl (id, args, r) ->
......
203 211
      let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
204 212
      normalize_expr ~alias:alias node offsets defvars norm_expr
205 213
    else
206
      mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr
214
      mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr
207 215
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) -> (* Here we differ from Colaco paper: arrows are pushed to the top *)
208 216
    normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
209 217
  | Expr_arrow (e1,e2) ->
......
251 259
   hl (defvars, [])
252 260

  
253 261
and normalize_array_expr ?(alias=true) node offsets defvars expr =
254
(*  Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
262
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
255 263
  match expr.expr_desc with
256 264
  | Expr_power (e1, d) when offsets = [] ->
257 265
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
......
262 270
  | Expr_array elist when offsets = [] ->
263 271
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
264 272
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
265
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
273
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
266 274
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
267 275
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
268 276
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
......
310 318
  defvars', {eq with eq_lhs = lhs' }
311 319

  
312 320
let rec normalize_eq node defvars eq =
321
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
313 322
  match eq.eq_rhs.expr_desc with
314 323
  | Expr_pre _
315 324
  | Expr_fby _  ->
......
321 330
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
322 331
    let norm_eq = { eq with eq_rhs = norm_rhs } in
323 332
    (norm_eq::defs', vars')
324
  | Expr_appl (id, _, None) when Basic_library.is_internal_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
333
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
325 334
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
326 335
    let norm_eq = { eq with eq_rhs = norm_rhs } in
327 336
    (norm_eq::defs', vars')
......
353 362
    List.fold_left (
354 363
    fun (vars, def_accu, assert_accu) assert_ ->
355 364
      let assert_expr = assert_.assert_expr in
356
      let (defs, vars'), expr =
357
	normalize_expr
358
	  ~alias:true
359
	  node
365
      let (defs, vars'), expr = 
366
	normalize_expr 
367
	  ~alias:false 
368
	  node 
360 369
	  [] (* empty offset for arrays *)
361 370
	  ([], vars) (* defvar only contains vars *)
362 371
	  assert_expr
......
368 377
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
369 378

  
370 379
  let new_annots =
371
    if !Options.traces then
380
    if !Options.horntraces then
372 381
      begin
373 382
	(* Compute traceability info:
374 383
	   - gather newly bound variables
......
401 410
    node_asserts = asserts;
402 411
    node_annot = new_annots;
403 412
  }
404
  in ((*Printers.pp_node Format.err_formatter node;*)
405
    node
406
)
407

  
413
  in ((*Printers.pp_node Format.err_formatter node;*) node)
408 414

  
409 415
let normalize_decl decl =
410 416
  match decl.top_decl_desc with

Also available in: Unified diff