defmodule QuintConnect.QuintCLI do
  @moduledoc """
  Builds `quint run` / `quint test` argument lists and environment for `System.cmd/3`.
  """

  alias QuintConnect.Config

  @type mode :: :run | :test

  @doc """
  argv for `System.cmd(executable, argv, opts)` — **does not** include the executable name.

  `out_itf` should include `{seq}` so Quint can emit multiple traces.
  """
  @spec argv(String.t(), String.t(), Config.t(), keyword()) :: [String.t()]
  def argv(spec_path, out_itf_path, %Config{} = config, opts \\ []) do
    mode = Keyword.get(opts, :mode, :run)
    base_args(mode, spec_path) ++ mode_args(mode, out_itf_path, config)
  end

  @doc """
  Environment list for `System.cmd/3`.
  """
  @spec merged_env(Config.t()) :: [{String.t(), String.t()}]
  def merged_env(%Config{} = config) do
    base = System.get_env() |> Map.to_list()

    base
    |> put_env_if("QUINT_SEED", config.seed)
    |> put_env_if("QUINT_VERBOSE", verbosity_string(config.verbosity))
  end

  defp base_args(:test, spec_path), do: ["test", spec_path]
  defp base_args(:run, spec_path), do: ["run", spec_path]

  defp mode_args(:test, out_itf_path, config) do
    []
    |> append_seed(config.seed)
    |> append_pair("--match", "^#{config.test_name}$")
    |> append_pair("--max-samples", Config.trace_count(config, :test))
    |> append_pair("--out-itf", out_itf_path)
    |> append_verbosity(config.verbosity || 0)
    |> append_if_present("--main", config.main_module)
  end

  defp mode_args(:run, out_itf_path, config) do
    []
    |> append_seed(config.seed)
    |> append_pair("--max-samples", Config.trace_count(config, :run))
    |> append_pair("--n-traces", Config.trace_count(config, :run))
    |> append_pair("--out-itf", out_itf_path)
    |> maybe_append("--mbt", config.mbt)
    |> append_verbosity(config.verbosity || 0)
    |> append_if_present("--init", config.init_action)
    |> append_if_present("--step", config.step_action)
    |> append_if_present("--max-steps", config.max_steps)
    |> append_if_present("--main", config.main_module)
    |> append_if_present("--backend", config.backend)
  end

  defp maybe_append(acc, _flag, false), do: acc
  defp maybe_append(acc, flag, true), do: acc ++ [flag]
  defp append_if_present(acc, _flag, nil), do: acc
  defp append_if_present(acc, flag, value), do: append_pair(acc, flag, value)
  defp append_pair(acc, flag, value), do: acc ++ [flag, to_string(value)]

  defp append_seed(acc, nil), do: acc
  defp append_seed(acc, seed), do: append_pair(acc, "--seed", seed)

  defp append_verbosity(acc, nil), do: acc
  defp append_verbosity(acc, v) when is_integer(v), do: append_pair(acc, "--verbosity", v)

  defp append_verbosity(acc, v) when is_binary(v) do
    case Integer.parse(v) do
      {n, _} -> append_pair(acc, "--verbosity", n)
      :error -> append_pair(acc, "--verbosity", v)
    end
  end

  defp put_env_if(env, _key, nil), do: env
  defp put_env_if(env, key, value), do: List.keystore(env, key, 0, {key, value})

  defp verbosity_string(nil), do: nil
  defp verbosity_string(v) when is_integer(v), do: Integer.to_string(v)
  defp verbosity_string(v) when is_binary(v), do: v
end