Project

General

Profile

Revision a38c681e src/normalization.ml

View differences:

src/normalization.ml
65 65
 match expr.expr_desc with
66 66
 | Expr_arrow (e1, e2) ->
67 67
    let loc = expr.expr_loc in
68
    let ck = expr.expr_clock in
68
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
69 69
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
70 70
 | _                   -> assert false
71 71

  
......
129 129

  
130 130
(* Create an alias for [expr], if none exists yet *)
131 131
let mk_expr_alias node (defs, vars) expr =
132
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132 133
  match get_expr_alias defs expr with
133 134
  | Some eq ->
134 135
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
......
387 388
  *)
388 389
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
389 390
  let norm_traceability = {
390
    annots = 
391
    annots =
391 392
      List.map 
392 393
	(fun v -> 
393 394
	  let expr = substitute_expr diff_vars defs (
394
	    let eq = List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs in
395
	    let eq = try
396
		       List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
397
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
395 398
	    eq.eq_rhs) in 
396 399
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
397 400
	  ["horn_backend";"trace"], pair 
398
    ) 
401
	)
399 402
    diff_vars ;
400 403
    annot_loc = Location.dummy_loc
401 404
  }

Also available in: Unified diff