corsa

defmodule Corsa.Post do
  @moduledoc """

  Postconditions are specifications which must be fulfilled after the execution of a function,
  thereby certifying that the anticipated output criteria have been satisfied. In Corsa,
  postconditions are evaluated at runtime. If a postcondition is not satisfied, either an exception
  or a log is generated.

  ## Example

      iex> defmodule #{__MODULE__}.Example do
      ...>   use Corsa.Assert
      ...>   use Corsa.Post
      ...>   post f(x, y) do result > x end
      ...>   def f(x, y) do x + y end
      ...> end
      iex> #{__MODULE__}.Example.f(2, 1)
      3
      iex> #{__MODULE__}.Example.f(1, -1)
      ** (Corsa.PostViolationError) @post does not hold in call '#{inspect(__MODULE__)}.Example.f(1, -1)' with result '0'

  """

  import Corsa.Utils

  @doc false
  @spec __using__([]) :: Macro.t()
  defmacro __using__([]) do
    context = __CALLER__.module
    Module.register_attribute(context, :post, accumulate: true)

    quote do
      require unquote(__MODULE__)
      @before_compile unquote(__MODULE__)
    end
  end

  @doc """

  ## Errors

      iex> defmodule #{__MODULE__}.ExampleError1 do
      ...>   use Corsa.Assert
      ...>   use Corsa.Post
      ...>   post f(x, y) do x > y end
      ...>   post f(x, y) do x > y end
      ...>   def f(x, y) do x + y end
      ...> end
      ** (Corsa.PostError) @post for function 'f/2' already defined

      iex> defmodule #{__MODULE__}.ExampleError2 do
      ...>   use Corsa.Assert
      ...>   use Corsa.Post
      ...>   post f(x, x) do x > y end
      ...>   def f(x, y) do x + y end
      ...> end
      ** (Corsa.PostError) arguments in @post should contain different names

      iex> defmodule #{__MODULE__}.ExampleError3 do
      ...>   use Corsa.Assert
      ...>   use Corsa.Post
      ...>   post f(x, _) do x > y end
      ...>   def f(x, y) do x + y end
      ...> end
      ** (Corsa.PostError) arguments in @post cannot be ignored with _

      iex> defmodule #{__MODULE__}.ExampleError4 do
      ...>   use Corsa.Assert
      ...>   use Corsa.Post
      ...>   post f(x, result) do x > y end
      ...>   def f(x, y) do x + y end
      ...> end
      ** (Corsa.PostError) result cannot be an argument in @post

  """
  defmacro post({name, _, args}, do: body) do
    arity = length(args)
    context = __CALLER__.module
    stacktrace = Macro.Env.stacktrace(__CALLER__)
    check_args!(name, args, context, stacktrace)
    Module.put_attribute(context, :post, {name, arity})
    def_post(name, args, body, context)
  end

  defmacro post(_, _) do
    reraise(Corsa.PostError, "syntax error in @post", Macro.Env.stacktrace(__CALLER__))
  end

  defp def_post(name, args, body, context) do
    result = Macro.var(:result, nil)
    args = ignore_unused(args ++ [result], body)

    quote generated: true, context: context do
      Kernel.defp unquote(:"#{name}_post")(unquote_splicing(args)) do
        unquote(body)
      end
    end
  end

  @doc false
  @spec __before_compile__(Macro.Env.t()) :: Macro.t()
  defmacro __before_compile__(env) do
    module = env.module

    defs =
      Module.definitions_in(module, :def) |> Enum.map(fn {name, arity} -> {:def, name, arity} end)

    defps =
      Module.definitions_in(module, :defp) |> Enum.map(fn {name, arity} -> {:defp, name, arity} end)

    for f = {_def_t, name, arity} <- defs ++ defps,
        post?(f, module),
        {_, _, location, _} = Module.get_definition(module, {name, arity}) do
      file = __CALLER__.file
      Module.make_overridable(module, [{name, arity}])
      new_def(f, module, location ++ [file: file])
    end
  end

  defp new_def({def_t, name, arity}, context, location) do
    line = Keyword.get(location, :line)
    args = Macro.generate_arguments(arity, nil)

    result =
      quote context: context do
        Corsa.Assert.assert(
          unquote(:"#{name}_post")(unquote_splicing(args), result),
          Corsa.PostViolationError,
          Corsa.PostError,
          call: call,
          result: result
        )
      end

    new_def(def_t, name, args, [], [], result, context, line)
  end

  ##############################################################################
  # Helpers
  ##############################################################################

  defp post?({_, name, arity}, module) do
    defs = Module.definitions_in(module)
    {:"#{name}_post", arity + 1} in defs
  end

  defp check_args!(name, args, context, stacktrace) do
    arity = length(args)

    if {name, arity} in Module.get_attribute(context, :post) do
      "@post for function '#{name}/#{arity}' already defined"
      |> then(&reraise(Corsa.PostError, &1, stacktrace))
    end

    for {arg, _, _} <- args, arg = Atom.to_string(arg), match?("_" <> _, arg) do
      "arguments in @post cannot be ignored with _"
      |> then(&reraise(Corsa.PostError, &1, stacktrace))
    end

    for {arg, _, _} <- args, arg == :result do
      "result cannot be an argument in @post"
      |> then(&reraise(Corsa.PostError, &1, stacktrace))
    end

    unless args == Enum.uniq(args) do
      "arguments in @post should contain different names"
      |> then(&reraise(Corsa.PostError, &1, stacktrace))
    end
  end
end