defmodule QuintConnect.Case do
  @moduledoc """
  ExUnit DSL for replaying Quint traces against Elixir drivers.
  """

  alias QuintConnect.{Config, ITF.Trace, Replay, Runner}

  defmacro __using__(opts) do
    spec = Keyword.fetch!(opts, :spec)

    quote do
      use ExUnit.Case, async: false
      import QuintConnect.Case, only: [quint_run: 2, quint_test: 2]
      @quint_connect_spec unquote(spec)
      def quint_connect_spec, do: @quint_connect_spec
    end
  end

  defmacro quint_run(name, opts) do
    quote do
      test unquote(name), context do
        opts = Keyword.put_new(unquote(opts), :spec, @quint_connect_spec)
        assert :ok = QuintConnect.Case.run_quint(:run, opts, context)
      end
    end
  end

  defmacro quint_test(name, opts) do
    quote do
      test unquote(name), context do
        opts = unquote(opts) |> Keyword.put_new(:spec, @quint_connect_spec)
        opts = Keyword.put_new(opts, :test_name, unquote(name))
        assert :ok = QuintConnect.Case.run_quint(:test, opts, context)
      end
    end
  end

  @doc false
  @spec run_quint(:run | :test, keyword(), map()) :: :ok | {:error, term()}
  def run_quint(mode, opts, context \\ %{}) do
    with {:ok, driver} <- fetch_driver(opts),
         {:ok, traces} <- traces(mode, opts, context) do
      replay_all(driver, traces, opts)
    end
  end

  defp fetch_driver(opts), do: opts |> Keyword.fetch(:driver) |> map_fetch_error(:missing_driver)

  defp traces(mode, opts, context) do
    case Keyword.get(opts, :trace_paths) do
      nil -> run_quint_cli(mode, opts, context)
      paths -> read_traces(paths)
    end
  end

  defp run_quint_cli(mode, opts, context) do
    config = config(mode, opts)

    with {:ok, result} <- Runner.run(opts[:spec], runner_opts(mode, opts, config, context)),
         do: traces_from_result(result)
  end

  defp runner_opts(mode, opts, config, context) do
    [
      mode: mode,
      config: config,
      cwd: Keyword.get(opts, :cwd, Map.get(context, :cwd, File.cwd!()))
    ]
  end

  defp config(:test, opts), do: opts |> put_test_name() |> Config.new() |> unwrap_config()
  defp config(:run, opts), do: opts |> Config.new() |> unwrap_config()

  defp put_test_name(opts), do: Keyword.put_new(opts, :test_name, Keyword.get(opts, :test))

  defp unwrap_config({:ok, config}), do: config

  defp unwrap_config({:error, reason}),
    do: raise(ArgumentError, "invalid Quint config: #{inspect(reason)}")

  defp traces_from_result(%{exit_status: 0, itf_paths: paths}), do: read_traces(paths)

  defp traces_from_result(result),
    do: {:error, {:quint_failed, result.exit_status, result.stdout}}

  defp read_traces(paths) do
    paths |> Enum.map(&Trace.from_file/1) |> collect_traces()
  end

  defp collect_traces(results), do: Enum.reduce_while(results, {:ok, []}, &collect_trace/2)

  defp collect_trace({:ok, trace}, {:ok, acc}), do: {:cont, {:ok, [trace | acc]}}
  defp collect_trace({:error, reason}, _acc), do: {:halt, {:error, reason}}

  defp replay_all(driver, traces, opts) do
    traces |> Enum.reverse() |> Enum.reduce_while(:ok, &replay_trace(driver, opts, &1, &2))
  end

  defp replay_trace(driver, opts, trace, :ok) do
    case Replay.run(driver, trace, opts) do
      :ok -> {:cont, :ok}
      {:error, reason} -> {:halt, {:error, reason}}
    end
  end

  defp map_fetch_error({:ok, value}, _reason), do: {:ok, value}
  defp map_fetch_error(:error, reason), do: {:error, reason}
end