CristalCaveGem » LustreC

let pp_var fmt id = Format.pp_print_string fmt id.var_id

let rename_machine_list p = List.map (rename_machine p)

let rename_current =  rename (fun n -> n ^ "_c")

let rename_current_list = List.map rename_current

let rename_next = rename (fun n -> n ^ "_x")

  List.find (fun m  -> m.mname.node_id = node_name) machines 

let full_memory_vars machines machine =

      List.fold_left (fun accu (id, (n, _)) -> 

	let name = node_name n in 

	if name = "_arrow" then accu else

	  let machine_n = get_machine machines name in

      ) [] (m.minstances) 

  in

  aux true machine.mname.node_id machine

(* Used to print boolean constants *)

let pp_horn_tag fmt t =

(* Prints a constant value *)

let rec pp_horn_const fmt c =

    | StateVar v    ->

      if Types.is_array_type v.var_type

      then assert false 

    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl

(* Prints a [value] indexed by the suffix list [loop_vars] *)

	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)

	    (Utils.pp_final_char_if_non_empty " " outputs)

	    (Utils.fprintf_list ~sep:" " pp_var) (

	     )

	  else

	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"

	      (Utils.pp_final_char_if_non_empty " " outputs)

	      (Utils.fprintf_list ~sep:" " pp_var) (

	       )

	     end

    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;

    (* We print the types of the main node "memory tree" TODO: add the output *)

    let main_memory_next = 

    in

    let main_memory_current = 

    in

    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."

      (Utils.fprintf_list ~sep:" " pp_type)