isabelle_elixir

defmodule IsabelleClient.Session do
  @moduledoc """
  Isabelle server session resource.

  Sessions live in the Isabelle server process and may be used from different
  client connections when their `id` is known.
  """

  defstruct [:id, :tmp_dir, :args, :label]

  @typedoc """
  Isabelle server session known to the Elixir client.

  `id` is Isabelle's session handle. `tmp_dir`, `args`, and `label` are local
  conveniences recorded from session startup.
  """
  @type t :: %__MODULE__{
          id: String.t(),
          tmp_dir: String.t() | nil,
          args: map() | nil,
          label: String.t() | nil
        }

  @doc "Builds a session struct from a `session_start` result map, or returns `nil`."
  def from_result(result, args \\ nil, label \\ nil)

  def from_result(%{"session_id" => id} = result, args, label) when is_binary(id) do
    %__MODULE__{id: id, tmp_dir: Map.get(result, "tmp_dir"), args: args, label: label}
  end

  def from_result(_, _, _), do: nil

  @doc false
  def prepare_start_args(args) do
    args = IsabelleClient.Arguments.normalize(args)
    {Map.delete(args, "label"), Map.get(args, "label")}
  end

  @doc false
  def args(opts) do
    opts
    |> Keyword.get(:session_args, [])
    |> IsabelleClient.Arguments.normalize()
    |> Map.put_new("session", Keyword.get(opts, :session, "HOL"))
  end

  @doc "Returns the session id from a session struct or id string."
  def id(%__MODULE__{id: id}), do: id
  def id(id) when is_binary(id), do: id
  def id(nil), do: nil

  @doc false
  def put_id(args, active_id),
    do: args |> IsabelleClient.Arguments.normalize() |> do_put_id(active_id)

  defp do_put_id(%{"session_id" => session_id} = args, _active_id) when is_binary(session_id),
    do: {:ok, args}

  defp do_put_id(args, active_id) when is_binary(active_id),
    do: {:ok, Map.put(args, "session_id", active_id)}

  defp do_put_id(_args, _active_id), do: :error

  @doc false
  def has_id?(args) do
    match?({:ok, _}, put_id(args, nil))
  end

  @doc false
  def push(%{sessions: sessions} = client, %__MODULE__{} = session),
    do: %{client | sessions: [session | sessions]}

  @doc false
  def active(%{sessions: [session | _]}), do: session
  def active(%{sessions: []}), do: nil

  @doc false
  def active_id(client), do: client |> active() |> id()

  @doc false
  def remove(%{sessions: sessions} = client, session_id) when is_binary(session_id) do
    %{client | sessions: Enum.reject(sessions, &(&1.id == session_id))}
  end

  def remove(client, _session_id), do: client

  @doc false
  def default_master_dir(%__MODULE__{id: session_id, tmp_dir: tmp_dir}, %{
        "session_id" => session_id
      })
      when is_binary(session_id) and is_binary(tmp_dir),
      do: tmp_dir

  def default_master_dir(%__MODULE__{tmp_dir: tmp_dir}, args) when is_binary(tmp_dir) do
    if Map.has_key?(args, "session_id"), do: fresh_tmp_dir(), else: tmp_dir
  end

  def default_master_dir(_session, _args), do: fresh_tmp_dir()

  @doc false
  def fetch(%__MODULE__{id: id}, key) when key in [:id, :session_id, "id", "session_id"],
    do: {:ok, id}

  def fetch(%__MODULE__{tmp_dir: tmp_dir}, key) when key in [:tmp_dir, "tmp_dir"],
    do: {:ok, tmp_dir}

  def fetch(%__MODULE__{args: args}, key) when key in [:args, "args"], do: {:ok, args}
  def fetch(%__MODULE__{label: label}, key) when key in [:label, "label"], do: {:ok, label}

  def fetch(%__MODULE__{}, _key), do: :error

  defp fresh_tmp_dir do
    Path.join(System.tmp_dir!(), "isabelle_elixir_#{System.unique_integer([:positive])}")
  end
end