makina

defmodule Makina.Composition do
  import Makina.Helpers

  alias Makina.Info

  ##############################################################################
  # Type definitions and module docs
  ##############################################################################

  @moduledoc false
  @typep attribute_info() :: %{module: module(), name: atom(), s_type: Macro.t(), d_type: Macro.t()}
  @typep invariant_info() :: %{module: module(), name: atom()}
  @typep command_info() :: Makina.Command.Base.info()

  ##############################################################################
  # Exposed macros
  ##############################################################################

  @spec __using__([Macro.t()]) :: Macro.t()
  defmacro __using__(extends: modules) do
    modules = Enum.map(modules, &Macro.expand(&1, __CALLER__))
    for module <- modules, do: ensure_model_loaded!(module)

    state_decl = generate_state(modules)
    invariants_decl = generate_invariants(modules)
    commands_decl = generate_commands(modules)

    quote do
      use Makina

      unquote(state_decl)
      unquote(invariants_decl)
      unquote_splicing(commands_decl)
    end
  end

  defmacro __using__(_opts) do
    Makina.Error.throw_error("syntax error in `use #{inspect(__MODULE__)}`")
  end

  ##############################################################################
  # State composition
  ##############################################################################

  @spec generate_state([module()]) :: Macro.t()
  defp generate_state(modules) do
    for module <- modules, do: ensure_model_loaded!(module)

    attrs =
      modules
      |> Enum.map(&Info.get_state!/1)
      |> Enum.map(fn %{
                       module: module,
                       attributes: attrs,
                       dynamic_types: d_types,
                       symbolic_types: s_types
                     } ->
        for attr <- attrs do
          %{
            module: module,
            name: attr,
            d_type: d_types[attr],
            s_type: s_types[attr]
          }
        end
      end)
      |> Enum.concat()
      |> Enum.group_by(fn %{name: n} -> n end)

    decl =
      for {_, attrs} <- attrs, attr = Enum.reduce(attrs, nil, &merge_attribute/2) do
        %{name: name, module: module, s_type: s_t, d_type: d_t} = attr
        impl = quote do: unquote(module).unquote(name)()
        type = if s_t == d_t, do: d_t, else: quote(do: symbolic(unquote(d_t)))
        expr = quote do: unquote(impl) :: unquote(type)
        {name, expr}
      end

    quote do
      state unquote(decl)
    end
  end

  @spec merge_attribute(attribute_info(), attribute_info() | nil) :: attribute_info()
  # TODO: this merge function should throw a warning if types are not equivalent.
  defp merge_attribute(attr, nil), do: attr
  defp merge_attribute(_, acc), do: acc

  ##############################################################################
  # Invariant composition
  ##############################################################################

  @spec generate_invariants([module()]) :: Macro.t()
  defp generate_invariants(modules) do
    invs =
      modules
      |> Enum.map(&Info.get_invariants!/1)
      |> Enum.map(fn %{invariants: invs, module: module} ->
        for inv <- invs, do: %{name: inv, module: module}
      end)
      |> Enum.concat()
      |> Enum.group_by(fn %{name: name} -> name end)

    invariants =
      for {inv_name, invs} <- invs,
          impl = Enum.reduce(invs, nil, &merge_invariants/2),
          do: {inv_name, impl}

    quote do
      invariants unquote(invariants)
    end
  end

  @spec merge_invariants(invariant_info(), nil | Macro.t()) :: Macro.t()
  defp merge_invariants(%{name: name, module: module}, nil) do
    state = Macro.var(:state, nil)
    quote do: unquote(module).unquote(name)(unquote(state))
  end

  defp merge_invariants(%{name: name, module: module}, acc) do
    state = Macro.var(:state, nil)
    quote do: unquote(module).unquote(name)(unquote(state)) and unquote(acc)
  end

  ##############################################################################
  # Command composition
  ##############################################################################

  @spec generate_commands([module()]) :: [Macro.t()]
  defp generate_commands(modules) do
    cmds =
      for module <- modules do
        Info.get_commands!(module) |> Enum.map(&Info.get_command!(module, &1))
      end
      |> Enum.concat()
      |> Enum.group_by(fn %{name: name} -> name end)

    for {command, info} <- cmds do
      args =
        Enum.reduce(info, [], &merge_arguments/2)
        |> Enum.uniq_by(fn {k, _} -> k end)
        |> Enum.map(fn {n, t} -> quote do: unquote(Macro.var(n, nil)) :: unquote(t) end)

      return = Enum.reduce(info, [], &merge_result/2)

      callbacks =
        for cb = callback <- callbacks() do
          modules = Enum.filter(info, fn %{callbacks: cs} -> cb in cs end) |> Enum.map(& &1.module)
          generate_callback(callback, modules, command)
        end

      quote do
        command unquote(command)(unquote_splicing(args)) :: unquote(return) do
          (unquote_splicing(callbacks))
        end
      end
    end
  end

  # TODO: This function should throw a warning when merging non-equivalent types.
  @spec merge_arguments(command_info(), Keyword.t(Macro.t())) :: Keyword.t(Macro.t())
  defp merge_arguments(%{arguments: arguments}, acc), do: arguments ++ acc

  # TODO: This function should throw a warning when merging non-equivalent types.
  @spec merge_result(command_info(), Keyword.t(Macro.t())) :: Keyword.t(Macro.t())
  defp merge_result(%{result: result}, _acc), do: result

  @spec generate_callback(atom(), [module()], atom()) :: Macro.t()
  # pre is the disjunction of the submodel pre's
  defp generate_callback(:pre, modules, _name) do
    state = Macro.var(:state, nil)

    pres =
      Enum.reduce(modules, false, fn
        m, acc -> quote do: unquote(m).pre(unquote(state)) or unquote(acc)
      end)

    quote do
      pre do: unquote(pres)
    end
  end

  # args makes a random choice of a model whose pre is true
  defp generate_callback(:args, modules, _name) do
    state = Macro.var(:state, nil)

    quote do
      args do
        viable_module = Enum.filter(unquote(modules), fn m -> m.args(unquote(state)) end)

        let [module <- oneof(viable_module)] do
          module.args(unquote(state))
        end
      end
    end
  end

  # valid_args is the conjuction of the submodels valid_args's
  defp generate_callback(:valid_args, modules, _name) do
    state = Macro.var(:state, nil)
    arguments = Macro.var(:arguments, nil)

    valid_args =
      Enum.reduce(modules, true, fn
        m, acc ->
          quote do
            unquote(m).valid_args(unquote_splicing([state, arguments])) and
              unquote(acc)
          end
      end)

    quote do
      valid_args do: unquote(valid_args)
    end
  end

  # features is the concatenation of the submodels features's
  defp generate_callback(:features, modules, _name) do
    state = Macro.var(:state, nil)
    arguments = Macro.var(:arguments, nil)
    result = Macro.var(:result, nil)

    features =
      Enum.reduce(modules, [], fn
        m, acc ->
          quote do
            unquote(m).features(unquote_splicing([state, arguments, result])) ++ unquote(acc)
          end
      end)

    quote do
      features do: unquote(features)
    end
  end

  # call is the random choice of the submodels call's
  # TODO: WARNING! How can we deal with different arities in call?
  defp generate_callback(:call, modules, _name) do
    arguments = Macro.var(:arguments, nil)

    quote do
      call do
        module = Enum.random(unquote(modules))
        module.call(unquote(arguments))
      end
    end
  end

  # next is the sequential composition
  defp generate_callback(:next, modules, _name) do
    state = Macro.var(:state, nil)
    arguments = Macro.var(:arguments, nil)
    result = Macro.var(:result, nil)

    nexts =
      Enum.reduce(modules, [], fn m, acc ->
        quote do
          unquote(m).next(unquote_splicing([state, arguments, result])) ++
            unquote(acc)
        end
      end)

    quote do
      next do: unquote(nexts)
    end
  end

  # post is the conjuction
  defp generate_callback(:post, modules, _name) do
    state = Macro.var(:state, nil)
    arguments = Macro.var(:arguments, nil)
    result = Macro.var(:result, nil)

    posts =
      Enum.reduce(modules, true, fn m, acc ->
        quote do
          unquote(m).post(unquote_splicing([state, arguments, result])) and unquote(acc)
        end
      end)

    quote do
      post do: unquote(posts)
    end
  end

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

  # Function that stores the allowed callback in a command with its arity.
  defp callbacks(), do: [:pre, :args, :valid_args, :call, :next, :post, :features]
end