Project

General

Profile

Revision 3b2bd83d src/normalization.ml

View differences:

src/normalization.ml
127 127

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

  
141 154
(* Create a (normalized) expression from [ref_e],
142 155
   replacing description with [norm_d],
......
159 172
    ) elist (defvars, [])
160 173

  
161 174
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;*)
175
(*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 176
  match expr.expr_desc with
164 177
  | Expr_const _
165 178
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
......
180 193
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
181 194
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
182 195
  | Expr_appl (id, args, None)
183
      when Basic_library.is_internal_fun id
196
      when Basic_library.is_homomorphic_fun id 
184 197
	&& Types.is_array_type expr.expr_type ->
185 198
    let defvars, norm_args =
186 199
      normalize_list
......
192 205
	(expr_list_of_expr args)
193 206
    in
194 207
    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 ->
208
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
196 209
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
197 210
    defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
198 211
  | Expr_appl (id, args, r) ->
......
203 216
      let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
204 217
      normalize_expr ~alias:alias node offsets defvars norm_expr
205 218
    else
206
      mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr
219
      mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr
207 220
  | 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 221
    normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
209 222
  | Expr_arrow (e1,e2) ->
......
251 264
   hl (defvars, [])
252 265

  
253 266
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;*)
267
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
255 268
  match expr.expr_desc with
256 269
  | Expr_power (e1, d) when offsets = [] ->
257 270
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
......
262 275
  | Expr_array elist when offsets = [] ->
263 276
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
264 277
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
265
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
278
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
266 279
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
267 280
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
268 281
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
......
310 323
  defvars', {eq with eq_lhs = lhs' }
311 324

  
312 325
let rec normalize_eq node defvars eq =
326
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
313 327
  match eq.eq_rhs.expr_desc with
314 328
  | Expr_pre _
315 329
  | Expr_fby _  ->
......
321 335
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
322 336
    let norm_eq = { eq with eq_rhs = norm_rhs } in
323 337
    (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 ->
338
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
325 339
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
326 340
    let norm_eq = { eq with eq_rhs = norm_rhs } in
327 341
    (norm_eq::defs', vars')
......
353 367
    List.fold_left (
354 368
    fun (vars, def_accu, assert_accu) assert_ ->
355 369
      let assert_expr = assert_.assert_expr in
356
      let (defs, vars'), expr =
357
	normalize_expr
358
	  ~alias:true
359
	  node
370
      let (defs, vars'), expr = 
371
	normalize_expr 
372
	  ~alias:false 
373
	  node 
360 374
	  [] (* empty offset for arrays *)
361 375
	  ([], vars) (* defvar only contains vars *)
362 376
	  assert_expr
......
379 393
	  annots = List.map (fun v ->
380 394
	    let eq =
381 395
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
396
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
397
	      with Not_found -> 
398
		(
399
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
400
		  assert false
401
		) 
402
	    in
384 403
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385 404
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386 405
	    (["traceability"], pair)

Also available in: Unified diff