CristalCaveGem » LustreC

let inject_node node = 

  cpt_fresh := 0;

  let inputs_outputs = node.node_inputs@node.node_outputs in

  let is_local v =

    List.for_all ((!=) v) inputs_outputs in

  let orig_vars = inputs_outputs@node.node_locals in

  let defs, vars =

    let eqs, auts = get_node_eqs node in

    if auts != [] then assert false; (* Automata should be expanded by now. *)

  (* Normalize the asserts *)

  let vars, assert_defs, asserts = 

    List.fold_left (

      let (defs, vars'), expr = 

	inject_expr 

	  ~alias:false 

	  ([], vars) (* defvar only contains vars *)

	  assert_expr

      in