# TODO: custom error messages in contracts
# TODO: auto-generate contract docs
defmodule Corsa do
  @moduledoc """

  `Corsa` is a library to write executable code contracts in Elixir.


  ## Installation

  The package can be installed by adding `corsa` to your list of dependencies in `mix.exs`:

      def deps do
        [
          {:corsa, "~> #{Corsa.MixProject.project[:version]}"}
        ]
      end

  ## Contracts

  Corsa contracts are written using normal pre- and post-condition contracts familiar from other
  programming languages and libraries such as Eiffel. To use the library in a module we must first
  insert a

      use Corsa

  statement in the module. Suppose next that we have implemented a function `list_to_nat` which
  converts an integer represented as a list of small numbers (between 0 and 9) to an integer:

  Suppose next that we have implemented a function `list_to_nat` which converts an integer
  represented as a list of small numbers (between 0 and 9) to an integer. We can require that the
  argument to `list_to_nat` is correct by specifying a `@pre` contract:

      iex> defmodule Example do
      ...>   use Corsa
      ...>   @pre list_to_nat(l), do: is_decimal_list(l)
      ...>   @post list_to_nat(l), do: is_integer(result)
      ...>   def list_to_nat(list), do: list_to_nat(list, 0)
      ...>   defp list_to_nat([], result), do: result
      ...>   defp list_to_nat([ n| rest ], acc) do
      ...>     list_to_nat(rest ,10*acc+n)
      ...>   end
      ...>   defp is_decimal_list([n|rest]) do
      ...>     is_decimal(n) and (n > 0)
      ...>     and Enum.all?(rest,&is_decimal/1)
      ...>   end
      ...>   defp is_decimal_list(_), do: false
      ...>   defp is_decimal(n) do
      ...>     is_integer(n) and (n >= 0) and (n < 10)
      ...>   end
      ...> end
      iex> Example.list_to_nat([1,5])
      15
      iex> Example.list_to_nat(5)
      ** (Corsa.PreViolationError) @pre does not hold in call 'CorsaDoctestTest.Example.list_to_nat(5)'

  If we now invoke the function with an incorrect argument by default an informative exception is
  raised.

  Similarly `@post` contracts check that the value returned by a function is correct:

  ## Assertions

  Assertions can be stated using the `@assert` construct:

      iex> defmodule AssertExample do
      ...>   use Corsa
      ...>   def f(y) do
      ...>     x = g(y)
      ...>     @assert x > 0
      ...>     x + 10
      ...>   end
      ...>   defp g(x) do x end
      ...> end
      iex> AssertExample.f(10)
      20
      iex> AssertExample.f(-10)
      ** (Corsa.AssertViolationError) @assert does not hold in expression 'x > 0' with values left '-10' and right '0'

  ## Termination Guarantees

  Corsa can check whether recursive functions eventually terminate, through specifying a measure
  using the `@decreases` construct:

      iex> defmodule DecreasesExample1 do
      ...>   use Corsa
      ...>   @decreases sum(l), do: length(l)
      ...>   def sum([]), do: 0
      ...>   def sum([n|rest]), do: n+sum(rest)
      ...> end
      iex> DecreasesExample1.sum([1,2,3])
      6

  The `@decreases` annotation specifies a function, that when applied to the arguments of the called
  function, calculates a measure (e.g., an integer). Corsa checks that measure when a function is
  invoked is strictly greater than the measure in recursive calls.  In the example above, the
  measure used is the length of the least which strictly decreases in recursive calls.  The check
  will be made even if the recursive call is made within another function.

  Note, however, that a decreasing measure does not necessarily guarantee termination:

      defmodule DecreasesExample2 do
        use Corsa
        @decreases fact(n), do: n
        def fact(1), do: 1
        def fact(n), do: n * fact(n - 1)
      end

  If the function is invoked with `fact(-1)` then it obviously never terminates (except possibly
  with an exception) but the measure always strictly decreases. Note you can "fix" the previous
  contract by using `abs/1`:

      iex> defmodule DecreasesExample3 do
      ...>   use Corsa
      ...>   @decreases fact(n), do: abs(n)
      ...>   def fact(1), do: 1
      ...>   def fact(n), do: n * fact(n - 1)
      ...> end
      iex> DecreasesExample3.fact(10)
      3628800
      iex> DecreasesExample3.fact(0)
      ** (Corsa.DecreasesViolationError) @decreases does not hold, call 'CorsaDoctestTest.DecreasesExample3.fact(-1)' does not decrease, previous measure: '0', new measure: '1'

  ## Time Contracts

  Time bounds for long a function application may execute can be specified with the `@within`
  construct:

      iex> defmodule WithinExample do
      ...>   use Corsa
      ...>   @within f(n) do n end
      ...>   def f(n) do Process.sleep(n + 10) end
      ...> end
      iex> WithinExample.f(1)
      ** (Corsa.WithinViolationError) @within does not hold in call 'CorsaDoctestTest.WithinExample.f(1)'

  If the call to f function does not return an answer within n + 10 milliseconds, an error is
  logged.

  ## Message Passing Contracts

  The `@expects` contract specifies the accepatble messages in a receive statement.

      iex> defmodule ExpectsExample do
      ...>   use Corsa
      ...>   def counter(state) do
      ...>     @expects v > 0, receive do
      ...>       :inc -> counter(state + 1)
      ...>       :dec -> counter(state - 1)
      ...>       {:set, v} -> counter(v)
      ...>     end
      ...>   end
      ...> end
      iex> send(self(), :inc)
      iex> send(self(), {:set, 10})
      iex> send(self(), {:set, -1})
      iex> ExpectsExample.counter(0)
      ** (Corsa.ExpectsViolationError) @expects does not hold in expression 'v > 0' with values left '-1' and right '0'

  ## Variable Contracts

  Variable contracts allow you to define variable contracts. In Corsa, these contracts restrict the values
  that may be assigned to a variable.


      # iex> defmodule DeclareExample do
      # ...>   use Corsa
      # ...>   @declare is_integer(n) && n > 0
      # ...>   def counter(n) do
      # ...>     receive do
      # ...>       :inc -> counter(n + 1)
      # ...>       :dec -> counter(n - 1)
      # ...>       {:set, n} -> counter(n)
      # ...>     end
      # ...>   end
      # ...> end
      # iex> send(self(), :inc)
      # iex> send(self(), {:set, 10})
      # iex> send(self(), {:set, -1})
      # iex> DeclareExample.counter(0)

  ## Type Contracts

  When using `Corsa` type annotations will be used to generate runtime typechecks for your
  functions.

      iex> defmodule TypedExample do
      ...>   use Corsa
      ...>   @spec id(integer()) :: integer()
      ...>   @spec id(boolean()) :: boolean()
      ...>   def id(x) do x end
      ...> end
      iex> TypedExample.id(10)
      10
      iex> TypedExample.id(true)
      true
      iex> TypedExample.id("hello")
      ** (Corsa.SpecArgViolationError) @spec does not hold in arguments in call 'CorsaDoctestTest.TypedExample.id("hello")'

  ## State Contracts

      iex> defmodule StateExample do
      ...>   use Corsa, state: true
      ...>   @init :not_started
      ...>
      ...>   @next start(), do: 0
      ...>   @throws start(), do: not started?(:not_started)
      ...>   def start() do
      ...>     try do
      ...>       :ets.new(:counter, [:named_table])
      ...>       :ets.insert(:counter, {"value", 0})
      ...>       :ok
      ...>     catch
      ...>       _, _ -> raise "error already started"
      ...>     end
      ...>   end
      ...>
      ...>   @next inc(), do: state + 1
      ...>   @throws inc(), do: started?(state)
      ...>   def inc() do
      ...>     [{"value", v}] = :ets.lookup(:counter, "value")
      ...>     :ets.insert(:counter, {"value", v + 1})
      ...>     :ok
      ...>   end
      ...>
      ...>   @throws get(), do: started?(state)
      ...>   def get() do
      ...>     [{"value", v}] = :ets.lookup(:counter, "value")
      ...>     v
      ...>   end
      ...>   def started?(state), do: state != :not_started
      ...> end
      iex> StateExample.start()
      iex> StateExample.inc()
      iex> StateExample.inc()
      iex> StateExample.get()
      2
      iex> StateExample.start()
      ** (RuntimeError) error already started

  ### Monitors

  ## Configuring Corsa

  Corsa can be configured to either (the default) raise exceptions whenever a contract is violated,
  or log contract violations, or do nothing.

  ### Logging levels

      iex> defmodule LogsExample do
      ...>   use Corsa, logger: :error
      ...>   @pre list_to_nat(l), do: is_decimal_list(l)
      ...>   @post list_to_nat(l), do: is_integer(result)
      ...>   def list_to_nat(list), do: list_to_nat(list, 0)
      ...>   defp list_to_nat([], result), do: result
      ...>   defp list_to_nat([ n| rest ], acc) do
      ...>     list_to_nat(rest ,10*acc+n)
      ...>   end
      ...>   defp is_decimal_list([n|rest]) do
      ...>     is_decimal(n) and (n > 0)
      ...>     and Enum.all?(rest,&is_decimal/1)
      ...>   end
      ...>   defp is_decimal_list(_), do: false
      ...>   defp is_decimal(n) do
      ...>     is_integer(n) and (n >= 0) and (n < 10)
      ...>   end
      ...> end

  ### Disabling contracts

      iex> defmodule DisabledContracts do
      ...>   use Corsa, disabled: true
      ...>   @pre f(x), do: x > 0
      ...>   @post f(x), do: result > 0
      ...>   def f(x), do: x
      ...> end
      iex> DisabledContracts.f(-1)
      -1

  """

  @doc false
  @spec __using__(logger: Logger.level(), state: boolean(), disabled: boolean()) :: Macro.t()
  defmacro __using__(opts) do
    context = __CALLER__.module
    Module.register_attribute(context, :corsa_options, accumulate: true)

    Keyword.get(opts, :disabled, Application.get_env(:corsa, :disabled))
    |> then(&Module.put_attribute(context, :corsa_options, {:disabled, &1}))

    quote context: context do
      require Corsa
      import Kernel, except: [@: 1]
      require Logger
      import Corsa.Utils, only: [to_corsa_call: 3]
      # The order here is important, as it tells how the macros are composed
      import Corsa
      # TODO check what is going on with declare
      # use Corsa.Declare
      use Corsa.Type
      use Corsa.Assert, unquote(opts)
      use Corsa.Expects
      use Corsa.Throws
      use Corsa.Within
      use Corsa.Spec
      use Corsa.Post
      use Corsa.Decreases
      use Corsa.Pre
      use Corsa.StateM, unquote(opts)
    end
  end

  @doc false
  defmacro @ast do
    context = __CALLER__.module
    state? = Module.get_attribute(context, :state)

    disabled? = Module.get_attribute(context, :corsa_options, []) |> Keyword.get(:disabled, false)

    case ast do
      {tag, _line, _expr}
      when disabled? and
             tag in [:assert, :declare, :pre, :post, :throws, :decreases, :within, :init, :next] ->
        []

      {:assert, _line, expr} ->
        quote context: context do
          Corsa.Assert.assert(unquote_splicing(expr))
        end

      {:expects, _line, expr} when disabled? ->
        {_, clauses} = Corsa.Utils.parse_expects(Enum.reverse(expr), __CALLER__)

        quote context: context do
          receive do
            unquote(clauses)
          end
        end

      {:expects, _line, expr} ->
        quote context: context do
          Corsa.Expects.expects(unquote(expr))
        end

      # {:declare, _line, expr} ->
      #   quote context: context do
      #     declare(unquote(expr))
      #   end

      {:pre, _line, [{:when, _context, _args}, [do: _body]]} ->
        reraise(
          Corsa.PreError,
          "guards are not supported in @pre",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:pre, _line, contract = [{_name, _, _args}, [do: _]]} ->
        quote context: context do
          Corsa.Pre.pre(unquote_splicing(contract))
        end

      {:pre, _, _} ->
        reraise(Corsa.PreError, "syntax error in @pre", Macro.Env.stacktrace(__CALLER__))

      {:post, _line, [{:when, _context, _args}, [do: _body]]} ->
        reraise(
          Corsa.PostError,
          "guards are not supported in @post",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:post, _line, contract = [{_name, _, _args}, [do: _]]} ->
        quote context: context do
          Corsa.Post.post(unquote_splicing(contract))
        end

      {:post, _, _} ->
        reraise(Corsa.PostError, "syntax error in @post", Macro.Env.stacktrace(__CALLER__))

      {:throws, _line, [{:when, _context, _args}, [do: _body]]} ->
        reraise(
          Corsa.ThrowsError,
          "guards are not supported in @throws",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:throws, _line, contract = [{_name, _, _args}, [do: _]]} ->
        quote context: context do
          Corsa.Throws.throws(unquote_splicing(contract))
        end

      {:throws, _, _} ->
        reraise(Corsa.ThrowsError, "syntax error in @throws", Macro.Env.stacktrace(__CALLER__))

      {:decreases, _line, [{:when, _context, _args}, [do: _body]]} ->
        reraise(
          Corsa.DecreasesError,
          "guards are not supported in @decreases",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:decreases, _line, contract = [{_name, _, _args}, [do: _]]} ->
        quote context: context do
          Corsa.Decreases.decreases(unquote_splicing(contract))
        end

      {:decreases, _, _} ->
        reraise(
          Corsa.DecreasesError,
          "syntax error in @decreases",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:within, _line, [{:when, _context, _args}, [do: _body]]} ->
        reraise(
          Corsa.WithinError,
          "guards are not supported in @within",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:within, _line, contract = [{_name, _, _args}, [do: _]]} ->
        quote context: context do
          Corsa.Within.within(unquote_splicing(contract))
        end

      {:within, _, _} ->
        reraise(Corsa.WithinError, "syntax error in @within", Macro.Env.stacktrace(__CALLER__))

      {:spec, _line, expr} when disabled? ->
        quote context: context do
          @spec unquote_splicing(expr)
        end

      {:spec, _line, expr = [{:"::", _, [f = {_name, _, _args}, result_type]}]} ->
        quote context: context do
          @spec unquote_splicing(expr)
          Corsa.Spec.spec(unquote(f), unquote(result_type))
        end

      {:init, _line, _expr} when not state? ->
        reraise(
          Corsa.StateM.InitError,
          "to use @init you need to add the option state: true",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:next, _line, _expr} when not state? ->
        reraise(
          Corsa.StateM.InitError,
          "to use @next you need to add the option state: true",
          Macro.Env.stacktrace(__CALLER__)
        )

      {:init, _line, expr} ->
        quote context: context do
          Corsa.StateM.Init.init(unquote_splicing(expr))
        end

      {:next, _line, contract} ->
        quote context: context do
          Corsa.StateM.Next.next(unquote_splicing(contract))
        end

      _ ->
        quote do
          Kernel.@(unquote(ast))
        end
    end
  end
end