A little logic language (L3).

l3.ex

# Discussed in https://www.ericpfahl.com/beyond-unification-a-basic-logical-toolkit/

defmodule L3.Var do
  alias L3.Var

  @type t :: %Var{id: any}
  defstruct [:id]

  @spec new(any) :: Var.t()
  def new(id), do: %Var{id: id}
end

defmodule L3.Types do
  defmacro __using__(_) do
    quote do
      @type variable :: Var.t()
      @type atomic :: number | atom | binary
      @type uterm :: atomic | variable | list(uterm)
      @type substitution :: %{} | %{variable => uterm}
      @type goal :: (substitution -> [substitution])
    end
  end
end

defmodule L3.Unification do
  use L3.Types
  alias L3.Var

  @spec unify(substitution, uterm, uterm) :: {:ok, substitution} | :error
  def unify(sub, term1, term2) do
    do_unify(sub, walk(sub, term1), walk(sub, term2))
  end

  defp do_unify(sub, term1, term2) when term1 == term2, do: {:ok, sub}
  defp do_unify(sub, %Var{} = var, term), do: extend(sub, var, term)
  defp do_unify(sub, term, %Var{} = var), do: extend(sub, var, term)

  defp do_unify(sub, [h1 | t1], [h2 | t2]) do
    with {:ok, sub} <- unify(sub, h1, h2) do
      unify(sub, t1, t2)
    end
  end

  defp do_unify(_sub, _term1, _term2), do: :error

  @spec extend(substitution, variable, uterm) :: {:ok, substitution}
  defp extend(sub, var, term), do: {:ok, Map.put(sub, var, term)}

  @spec walk(substitution, uterm) :: uterm
  def walk(sub, term) do
    case Map.fetch(sub, term) do
      {:ok, t} -> walk(sub, t)
      :error -> term
    end
  end

  @spec simplify(substitution, uterm) :: uterm
  def simplify(sub, term) do
    case walk(sub, term) do
      [h | t] -> [simplify(sub, h) | simplify(sub, t)]
      term -> term
    end
  end
end

defmodule L3 do
  use L3.Types
  alias L3.Unification, as: U

  @spec equal(uterm, uterm) :: goal
  def equal(term1, term2) do
    fn sub ->
      case U.unify(sub, term1, term2) do
        {:ok, sub} -> [sub]
        :error -> []
      end
    end
  end

  @spec both(goal, goal) :: goal
  def both(goal1, goal2) do
    fn sub ->
      Enum.flat_map(goal1.(sub), goal2)
    end
  end

  @spec either(goal, goal) :: goal
  def either(goal1, goal2) do
    fn sub ->
      Enum.concat(goal1.(sub), goal2.(sub))
    end
  end

  @spec present(goal, [variable]) :: [uterm]
  def present(goal, vars) do
    %{}
    |> goal.()
    |> Enum.map(&present_sub(&1, vars))
  end

  defp present_sub(sub, vars) do
    Enum.map(vars, fn v ->
      if Map.has_key?(sub, v) do
        U.simplify(sub, v)
      else
        v
      end
    end)
  end
end