CristalCaveGem » LustreC

module OrdVarDecl:Map.OrderedType with type t=var_decl =

  struct type t = var_decl;; let compare = compare end

let rec pp_val fmt v =

  match v.value_desc with

    Format.eprintf "Unable to find node %s in list [%a]@.@?"

      id

      (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls

    raise Not_found

  )

  (* Format.eprintf "trnaslating ident: %s@." id; *)

  try (* id is a node var *)

    let var_id = get_node_var id node in

    then (

      (* Format.eprintf "a STATE VAR@."; *)

      mk_val (StateVar var_id) var_id.var_type

      Utils.IMap.add o (arrow_top_decl, []) j,

      d,

      (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)

     let var_x = get_node_var x node in

      si,

      j,

      d,

      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s)

     let var_x = get_node_var x node in

      mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si,

      j,

      d,

  let locals_list = nd.node_locals @ new_locals in

  let nd = { nd with node_locals = locals_list } in

  (* memories, init instructions, node calls, local variables (including memories), step instrs *)

  let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in

  assert (init0 = []);

  assert (Utils.IMap.is_empty j0);

  let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in

  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in

  {

    mname = nd;

    mcalls = mmap;

    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;

    minit = init;

    mstep = {

      step_inputs = nd.node_inputs;

      step_outputs = nd.node_outputs;

      step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;

      step_instrs = (

	(* special treatment depending on the active backend. For horn backend,

let rec assigns_instr instr assign =

  match get_instr_desc instr with  

  | MLocalAssign (i,_)

  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign

  | _                  -> assign

let machine_cse subst machine =

  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)

  let subst, instrs = instrs_cse subst machine.mstep.step_instrs in

  in

  {

    machine with

      mstep = { 

	machine.mstep with 

	  step_instrs = instrs

      }

  }