lucid

-module(lucid@logic).
-compile([no_auto_import, nowarn_unused_vars, nowarn_unused_function, nowarn_nomatch]).

-export([var/2, term/2, constant/1, elim/4, solve/2]).
-export_type([var/0, term_/0]).

-type var() :: {var, binary(), integer()}.

-type term_() :: {v, var()} | {t, binary(), list(term_())}.

-file("src/lucid/logic.gleam", 13).
-spec any(list(EXL), fun((EXL) -> boolean())) -> boolean().
any(L, F) ->
    case L of
        [] ->
            false;

        [El | Rest] ->
            F(El) orelse any(Rest, F)
    end.

-file("src/lucid/logic.gleam", 20).
-spec map(list(EXP), fun((EXP) -> EXT)) -> list(EXT).
map(L, F) ->
    case L of
        [] ->
            [];

        [El | Rest] ->
            [F(El) | map(Rest, F)]
    end.

-file("src/lucid/logic.gleam", 27).
-spec apply(var(), list({var(), term_()})) -> term_().
apply(V, Subst) ->
    case Subst of
        [] ->
            {v, V};

        [{X, T} | _] when X =:= V ->
            T;

        [_ | Rest] ->
            apply(V, Rest)
    end.

-file("src/lucid/logic.gleam", 35).
-spec lift(term_(), list({var(), term_()})) -> term_().
lift(T, Subst) ->
    case T of
        {v, V} ->
            apply(V, Subst);

        {t, F, Ts} ->
            {t, F, map(Ts, fun(_capture) -> lift(_capture, Subst) end)}
    end.

-file("src/lucid/logic.gleam", 42).
-spec occurs(var(), term_()) -> boolean().
occurs(V, T) ->
    case T of
        {v, V2} ->
            V =:= V2;

        {t, _, Ts} ->
            any(Ts, fun(_capture) -> occurs(V, _capture) end)
    end.

-file("src/lucid/logic.gleam", 49).
-spec zip(list(EYG), list(EYH)) -> {ok, list({EYG, EYH})} | {error, nil}.
zip(L1, L2) ->
    case {L1, L2} of
        {[], []} ->
            {ok, []};

        {[El1 | Rest1], [El2 | Rest2]} ->
            case zip(Rest1, Rest2) of
                {error, nil} ->
                    {error, nil};

                {ok, Z} ->
                    {ok, [{El1, El2} | Z]}
            end;

        {_, _} ->
            {error, nil}
    end.

-file("src/lucid/logic.gleam", 61).
-spec append(list(EYY), list(EYY)) -> list(EYY).
append(L1, L2) ->
    case L1 of
        [] ->
            L2;

        [El | Rest] ->
            [El | append(Rest, L2)]
    end.

-file("src/lucid/logic.gleam", 96).
-spec var(binary(), integer()) -> term_().
var(Name, Id) ->
    {v, {var, Name, Id}}.

-file("src/lucid/logic.gleam", 100).
-spec term(binary(), list(term_())) -> term_().
term(Name, Args) ->
    {t, Name, Args}.

-file("src/lucid/logic.gleam", 104).
-spec constant(binary()) -> term_().
constant(Name) ->
    {t, Name, []}.

-file("src/lucid/logic.gleam", 83).
-spec elim(var(), term_(), list({term_(), term_()}), list({var(), term_()})) -> {ok,
        list({var(), term_()})} |
    {error, binary()}.
elim(V, T, Eqns, So_far) ->
    case occurs(V, T) of
        true ->
            {error, <<"occurs check"/utf8>>};

        false ->
            Vt = fun(_capture) -> lift(_capture, [{V, T}]) end,
            solve(
                map(
                    Eqns,
                    fun(Eqn) ->
                        {Vt(erlang:element(1, Eqn)), Vt(erlang:element(2, Eqn))}
                    end
                ),
                [{V, T} |
                    map(
                        So_far,
                        fun(Subst) ->
                            {erlang:element(1, Subst),
                                Vt(erlang:element(2, Subst))}
                        end
                    )]
            )
    end.

-file("src/lucid/logic.gleam", 68).
-spec solve(list({term_(), term_()}), list({var(), term_()})) -> {ok,
        list({var(), term_()})} |
    {error, binary()}.
solve(Eqns, So_far) ->
    case Eqns of
        [] ->
            {ok, So_far};

        [{{v, V1}, {v, V2}} | Rest] when V1 =:= V2 ->
            solve(Rest, So_far);

        [{{v, V}, T} | Rest@1] ->
            elim(V, T, Rest@1, So_far);

        [{T, {v, V}} | Rest@1] ->
            elim(V, T, Rest@1, So_far);

        [{{t, F, Ts}, {t, G, Us}} | Rest@2] when F =:= G ->
            case zip(Ts, Us) of
                {error, nil} ->
                    {error, <<"arity mismatch"/utf8>>};

                {ok, Z} ->
                    solve(append(Z, Rest@2), So_far)
            end;

        [{{t, F@1, _}, {t, G@1, _}} | _] ->
            {error,
                <<<<<<"incompatible operators "/utf8, F@1/binary>>/binary,
                        " and "/utf8>>/binary,
                    G@1/binary>>}
    end.