Project

General

Profile

Revision 66359a5e src/normalization.ml

View differences:

src/normalization.ml
90 90
    var_dec_clock = dummy_clock_dec;
91 91
    var_dec_const = false;
92 92
    var_dec_value = None;
93
    var_parent_nodeid = Some node.node_id;
93 94
    var_type = ty;
94 95
    var_clock = ck;
95 96
    var_loc = loc
......
167 168
	    (Clocks.clock_list_of_clock expr.expr_clock) in
168 169
	let new_def =
169 170
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
170
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
171
	in
172
	(* Typing and Registering machine type *) 
173
	let _ = Machine_types.type_def node new_aliases expr  in
174
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
171 175
      else
172 176
	(defs, vars), expr
173 177

  
......
420 424
    ) (vars, [], []) node.node_asserts in
421 425
  let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
422 426
							  vars and initial locals ones *)
423
  let new_locals = node.node_locals @ new_locals in (* we add again, at the
427
  
428
  let all_locals = node.node_locals @ new_locals in (* we add again, at the
424 429
						       beginning of the list the
425 430
						       local declared ones *)
426 431
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
427 432

  
433

  
434
  (* Updating annotations: traceability and machine types for fresh variables *)
435
  
436
  (* Compute traceability info:
437
     - gather newly bound variables
438
     - compute the associated expression without aliases
439
  *)
428 440
  let new_annots =
429 441
    if !Options.traces then
430 442
      begin
431
	(* Compute traceability info:
432
	   - gather newly bound variables
433
	   - compute the associated expression without aliases
434
	*)
435
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
443
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
436 444
	let norm_traceability = {
437 445
	  annots = List.map (fun v ->
438 446
	    let eq =
......
446 454
	    in
447 455
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
448 456
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
457
	    Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
449 458
	    (["traceability"], pair)
450 459
	  ) diff_vars;
451 460
	  annot_loc = Location.dummy_loc
......
457 466
      node.node_annot
458 467
  in
459 468

  
469
  let new_annots =
470
    List.fold_left (fun annots v ->
471
      if Machine_types.is_exportable v then
472
	let typ = Machine_types.get_specified_type v in
473
  	let typ_name = Machine_types.type_name typ in
474

  
475
	let loc = v.var_loc in
476
	let typ_as_string =
477
	  mkexpr
478
	    loc
479
	    (Expr_const
480
	       (Const_string typ_name))
481
	in
482
	let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
483
	Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
484
	{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
485
      else
486
	annots
487
    ) new_annots new_locals
488
  in
460 489
  let node =
461 490
    { node with
462
      node_locals = new_locals;
491
      node_locals = all_locals;
463 492
      node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
464 493
      node_asserts = asserts;
465 494
      node_annot = new_annots;

Also available in: Unified diff