bond

defmodule Bond.Compiler.Assertion do
  @moduledoc internal: true
  @moduledoc """
  Struct representing an assertion that appears as part of contract specifications, such as in
  preconditions or postconditions attached to functions.

  Assertions are constructed at compile-time and as such the fields in this struct are quoted
  expressions or compile-time environment data. At run-time, the assertion `:expression` is
  evaluated by unquoting it in the context of the function to which the assertion is attached.
  """

  alias __MODULE__

  @enforce_keys [:id, :expression, :kind, :definition_env, :meta]
  defstruct [
    :id,
    :label,
    :expression,
    :code,
    :kind,
    :definition_env,
    :meta,
    # Only set on :invariant assertions. Atom name of the local variable the invariant's
    # expression refers to (the `stack` in `@invariant stack, ...`). Used by
    # `Bond.Compiler.AnnotatedFunction` to rebind that name to the function's actual struct
    # argument or extracted return value at emission time.
    :binding_name
  ]

  @type t :: t(Bond.assertion_kind())

  @type t(kind) :: %__MODULE__{
          id: String.t(),
          label: Bond.assertion_label(),
          expression: Bond.assertion_expression(),
          code: String.t(),
          kind: kind,
          definition_env: Macro.Env.t(),
          meta: list(),
          binding_name: atom() | nil
        }

  @type function_info :: {atom(), non_neg_integer()}

  defguard is_assertion_expression(expression)
           when is_tuple(expression) and
                  tuple_size(expression) == 3 and
                  is_atom(elem(expression, 0)) and is_list(elem(expression, 1)) and
                  is_list(elem(expression, 2))

  @doc """
  Construct a new `t:t/0` struct.

  Each assertion is tagged with a unique random `:id` so that it has a stable identity that
  survives macro expansion. The `:code` field is the human-readable form of the quoted
  `expression`, suitable for inclusion in error messages and generated documentation.
  """
  def new(kind, label, expression, %Macro.Env{} = env \\ __ENV__, meta \\ [])
      when is_assertion_expression(expression) do
    %__MODULE__{
      id: generate_unique_id(),
      kind: kind,
      label: label,
      expression: expression,
      code: Macro.to_string(expression),
      definition_env: env,
      meta: meta,
      binding_name: Keyword.get(meta, :binding_name)
    }
  end

  @doc """
  Returns a quoted block that, when spliced into a function body, evaluates each of the given
  `assertions` in order.

  On the first assertion failure the block throws `{:assertion_failure, info}`, where `info`
  is a map containing enough metadata to construct a `Bond.PreconditionError` /
  `Bond.PostconditionError` / `Bond.CheckError` struct, plus the runtime `binding()` from
  inside the enclosing function.

  `function_info` must be a `{name, arity}` tuple identifying the function the assertions are
  attached to; it is embedded in the error info so error messages can report the calling
  function's MFA.

  The block imports `Bond.Predicates` so operators like `~>` and `|||` are available to
  assertion expressions. It is intended to be used as the body of a `defp` generated by
  `Bond.Compiler.AnnotatedFunction` (one per kind per function) — see that module for the
  call-site shape that invokes the generated defp through `Bond.Runtime.Eval`.
  """
  @spec assertions_body([t()], function_info()) :: Macro.t()
  def assertions_body(assertions, function_info)
      when is_list(assertions) and is_tuple(function_info) do
    assertions_eval =
      for %Assertion{expression: expression, definition_env: assertion_env} = assertion <-
            assertions do
        assertion_info = %{
          assertion_id: assertion.id,
          kind: assertion.kind,
          label: assertion.label,
          expression: assertion.code,
          file: assertion_env.file,
          line: assertion_env.line,
          module: assertion_env.module,
          function: function_info
        }

        quote do
          if unquote(expression) do
            :ok
          else
            assertion_info = unquote(Macro.escape(assertion_info))
            # Sort the binding so failure messages are stable across runs and easy to diff.
            throw({:assertion_failure, Map.put(assertion_info, :binding, Enum.sort(binding()))})
          end
        end
      end

    quote do
      import Bond.Predicates

      (unquote_splicing(assertions_eval))
    end
  end

  @doc """
  Returns a quoted block intended to be used as the body of the lifted private function
  that evaluates module-scoped `@invariant`s.

  Each invariant has a `:binding_name` (e.g. `stack` in `@invariant stack, ...`) that is
  declared local to the function via `<name> = bond_invariant_value`, so the
  assertion's expression (which references the binding name) resolves to the value being
  checked. On the first failure the block throws `{:assertion_failure, info}` with
  `:kind => :invariant`, mirroring `assertions_body/2`'s shape for `@pre`/`@post`.

  `function_info` is the `{name, arity}` of the function the invariant is being checked
  around. Both the pre-invariant check (on entry, value = arg) and the post-invariant
  check (on exit, value = extracted return) share this same defp.
  """
  @spec invariants_body([t(:invariant)], function_info()) :: Macro.t()
  def invariants_body(invariants, function_info)
      when is_list(invariants) and is_tuple(function_info) do
    invariants_eval =
      for %Assertion{
            kind: :invariant,
            expression: expression,
            definition_env: env,
            binding_name: binding_name
          } = invariant <- invariants do
        assertion_info = %{
          assertion_id: invariant.id,
          kind: :invariant,
          label: invariant.label,
          expression: invariant.code,
          file: env.file,
          line: env.line,
          module: env.module,
          function: function_info
        }

        rebind_var = Macro.var(binding_name, nil)

        quote do
          unquote(rebind_var) = var!(bond_invariant_value)

          if unquote(expression) do
            :ok
          else
            assertion_info = unquote(Macro.escape(assertion_info))
            throw({:assertion_failure, Map.put(assertion_info, :binding, Enum.sort(binding()))})
          end
        end
      end

    quote do
      import Bond.Predicates

      (unquote_splicing(invariants_eval))
    end
  end

  @doc """
  Returns a quoted block intended to be used as the body of a 0-arity closure passed to
  `Bond.Runtime.Eval.evaluate_check/2`.

  On success the block evaluates to the value of the assertion expression (so that callers of
  `Bond.check/1,2` continue to receive the expression's value back). On failure it throws
  `{:assertion_failure, info}`, mirroring the shape used by `assertions_body/2` for
  `@pre`/`@post`; the throw is caught by `Bond.Runtime.Eval` and re-raised as a
  `Bond.CheckError`.
  """
  @spec check_body(t(:check)) :: Macro.t()
  def check_body(
        %__MODULE__{kind: :check, expression: expression, definition_env: env} = assertion
      ) do
    assertion_info = %{
      assertion_id: assertion.id,
      kind: :check,
      label: assertion.label,
      expression: assertion.code,
      file: env.file,
      line: env.line,
      module: env.module,
      function: env.function
    }

    quote do
      import Bond.Predicates

      if value = unquote(expression) do
        value
      else
        assertion_info = unquote(Macro.escape(assertion_info))
        throw({:assertion_failure, Map.put(assertion_info, :binding, Enum.sort(binding()))})
      end
    end
  end

  @id_chars ~c"0123456789abcdefghijklmnopqrstuvwxyz"

  defp generate_unique_id do
    for _ <- 1..32, into: "", do: <<Enum.random(@id_chars)>>
  end

  defimpl String.Chars do
    def to_string(%Bond.Compiler.Assertion{label: label, expression: expression, kind: kind}) do
      "#{kind}(#{inspect(label)}) => #{Macro.to_string(expression)}"
    end
  end
end