-module(metamon@relation).
-compile([no_auto_import, nowarn_unused_vars, nowarn_unused_function, nowarn_nomatch, inline]).
-define(FILEPATH, "src/metamon/relation.gleam").
-export([new/2, equal/0, not_equal/0, equivalent_under/2, approximately/1, permutation_of/0, subset_of/0, monotone/1, implies/2, 'and'/2, 'or'/2, invert/1, rename/2, n_new/2, all_equal/0, pairwise/1]).
-export_type([relation/1, relation_n/1]).

-if(?OTP_RELEASE >= 27).
-define(MODULEDOC(Str), -moduledoc(Str)).
-define(DOC(Str), -doc(Str)).
-else.
-define(MODULEDOC(Str), -compile([])).
-define(DOC(Str), -compile([])).
-endif.

?MODULEDOC(
    " Named two-argument predicates used by metamorphic relations.\n"
    "\n"
    " A `Relation(b)` answers \"do these two outputs satisfy the\n"
    " constraint?\". The `name` is surfaced in failure reports so the\n"
    " user immediately sees which property broke.\n"
).

-type relation(GDB) :: {relation, binary(), fun((GDB, GDB) -> boolean())}.

-type relation_n(GDC) :: {relation_n, binary(), fun((list(GDC)) -> boolean())}.

-file("src/metamon/relation.gleam", 17).
?DOC(" Construct a relation from a name and a binary predicate.\n").
-spec new(binary(), fun((GDD, GDD) -> boolean())) -> relation(GDD).
new(Name, Holds) ->
    {relation, Name, Holds}.

-file("src/metamon/relation.gleam", 22).
?DOC(" Equality (Gleam's structural `==`).\n").
-spec equal() -> relation(any()).
equal() ->
    {relation, <<"equal"/utf8>>, fun(Left, Right) -> Left =:= Right end}.

-file("src/metamon/relation.gleam", 27).
?DOC(" Inequality.\n").
-spec not_equal() -> relation(any()).
not_equal() ->
    {relation, <<"not_equal"/utf8>>, fun(Left, Right) -> Left /= Right end}.

-file("src/metamon/relation.gleam", 33).
?DOC(
    " Equality after a shared normalisation step. Useful for\n"
    " \"equal modulo whitespace / key order / formatting\".\n"
).
-spec equivalent_under(fun((GDJ) -> any()), binary()) -> relation(GDJ).
equivalent_under(Via, Name) ->
    {relation,
        <<<<"equivalent_under("/utf8, Name/binary>>/binary, ")"/utf8>>,
        fun(Left, Right) -> Via(Left) =:= Via(Right) end}.

-file("src/metamon/relation.gleam", 40).
?DOC(" Floats within `epsilon` of each other.\n").
-spec approximately(float()) -> relation(float()).
approximately(Epsilon) ->
    {relation,
        <<<<"approximately("/utf8,
                (gleam_stdlib:float_to_string(Epsilon))/binary>>/binary,
            ")"/utf8>>,
        fun(Left, Right) ->
            Diff = case Left >= Right of
                true ->
                    Left - Right;

                false ->
                    Right - Left
            end,
            Diff =< Epsilon
        end}.

-file("src/metamon/relation.gleam", 81).
-spec remove_one_loop(GEC, list(GEC), list(GEC)) -> {ok, list(GEC)} |
    {error, nil}.
remove_one_loop(Target, Items, Acc) ->
    case Items of
        [] ->
            {error, nil};

        [First | Rest] ->
            case First =:= Target of
                true ->
                    {ok, lists:append(lists:reverse(Acc), Rest)};

                false ->
                    remove_one_loop(Target, Rest, [First | Acc])
            end
    end.

-file("src/metamon/relation.gleam", 77).
-spec remove_one(GDX, list(GDX)) -> {ok, list(GDX)} | {error, nil}.
remove_one(Target, Items) ->
    remove_one_loop(Target, Items, []).

-file("src/metamon/relation.gleam", 65).
-spec remove_each(list(GDT), list(GDT)) -> list(GDT).
remove_each(To_remove, Remaining) ->
    case To_remove of
        [] ->
            Remaining;

        [First | Rest] ->
            case remove_one(First, Remaining) of
                {ok, Remaining_after} ->
                    remove_each(Rest, Remaining_after);

                {error, _} ->
                    [First]
            end
    end.

-file("src/metamon/relation.gleam", 58).
-spec is_permutation(list(GDQ), list(GDQ)) -> boolean().
is_permutation(Left, Right) ->
    case erlang:length(Left) =:= erlang:length(Right) of
        false ->
            false;

        true ->
            remove_each(Left, Right) =:= []
    end.

-file("src/metamon/relation.gleam", 54).
?DOC(" Two lists are permutations of each other (same multiset).\n").
-spec permutation_of() -> relation(list(any())).
permutation_of() ->
    {relation, <<"permutation_of"/utf8>>, fun is_permutation/2}.

-file("src/metamon/relation.gleam", 101).
-spec is_subset(list(GEL), list(GEL)) -> boolean().
is_subset(Left, Right) ->
    case Left of
        [] ->
            true;

        [First | Rest] ->
            case remove_one(First, Right) of
                {ok, Remaining} ->
                    is_subset(Rest, Remaining);

                {error, _} ->
                    false
            end
    end.

-file("src/metamon/relation.gleam", 97).
?DOC(" `left` is a sub-multiset of `right`.\n").
-spec subset_of() -> relation(list(any())).
subset_of() ->
    {relation,
        <<"subset_of"/utf8>>,
        fun(Left, Right) -> is_subset(Left, Right) end}.

-file("src/metamon/relation.gleam", 113).
?DOC(" `cmp(left, right)` returns `Lt` or `Eq` (i.e. left ≤ right).\n").
-spec monotone(fun((GEO, GEO) -> gleam@order:order())) -> relation(GEO).
monotone(Cmp) ->
    {relation, <<"monotone"/utf8>>, fun(Left, Right) -> case Cmp(Left, Right) of
                lt ->
                    true;

                eq ->
                    true;

                gt ->
                    false
            end end}.

-file("src/metamon/relation.gleam", 126).
?DOC(
    " Conditional relation: if `antecedent(left, right)` is `True`, the\n"
    " inner relation must hold. Otherwise the relation is trivially\n"
    " satisfied.\n"
).
-spec implies(fun((GEQ, GEQ) -> boolean()), relation(GEQ)) -> relation(GEQ).
implies(Antecedent, Inner) ->
    {relation,
        <<<<"implies("/utf8, (erlang:element(2, Inner))/binary>>/binary,
            ")"/utf8>>,
        fun(Left, Right) -> case Antecedent(Left, Right) of
                false ->
                    true;

                true ->
                    (erlang:element(3, Inner))(Left, Right)
            end end}.

-file("src/metamon/relation.gleam", 136).
?DOC(" Both `r1` and `r2` must hold.\n").
-spec 'and'(relation(GET), relation(GET)) -> relation(GET).
'and'(R1, R2) ->
    {relation,
        <<<<(erlang:element(2, R1))/binary, " and "/utf8>>/binary,
            (erlang:element(2, R2))/binary>>,
        fun(Left, Right) ->
            (erlang:element(3, R1))(Left, Right) andalso (erlang:element(3, R2))(
                Left,
                Right
            )
        end}.

-file("src/metamon/relation.gleam", 143).
?DOC(" At least one of `r1` and `r2` must hold.\n").
-spec 'or'(relation(GEX), relation(GEX)) -> relation(GEX).
'or'(R1, R2) ->
    {relation,
        <<<<(erlang:element(2, R1))/binary, " or "/utf8>>/binary,
            (erlang:element(2, R2))/binary>>,
        fun(Left, Right) ->
            (erlang:element(3, R1))(Left, Right) orelse (erlang:element(3, R2))(
                Left,
                Right
            )
        end}.

-file("src/metamon/relation.gleam", 150).
?DOC(" Negate a relation.\n").
-spec invert(relation(GFB)) -> relation(GFB).
invert(R) ->
    {relation,
        <<<<"not("/utf8, (erlang:element(2, R))/binary>>/binary, ")"/utf8>>,
        fun(Left, Right) -> not (erlang:element(3, R))(Left, Right) end}.

-file("src/metamon/relation.gleam", 157).
?DOC(" Override a relation's name.\n").
-spec rename(relation(GFE), binary()) -> relation(GFE).
rename(R, Name) ->
    {relation, Name, erlang:element(3, R)}.

-file("src/metamon/relation.gleam", 173).
?DOC(" Construct an N-ary relation directly.\n").
-spec n_new(binary(), fun((list(GFH)) -> boolean())) -> relation_n(GFH).
n_new(Name, Holds) ->
    {relation_n, Name, Holds}.

-file("src/metamon/relation.gleam", 183).
-spec all_equal_loop(list(any())) -> boolean().
all_equal_loop(Items) ->
    case Items of
        [] ->
            true;

        [_] ->
            true;

        [First, Second | Rest] ->
            case First =:= Second of
                true ->
                    all_equal_loop([Second | Rest]);

                false ->
                    false
            end
    end.

-file("src/metamon/relation.gleam", 179).
?DOC(
    " All elements of the input list are equal under structural `==`.\n"
    " Trivially `True` for lists of length 0 or 1.\n"
).
-spec all_equal() -> relation_n(any()).
all_equal() ->
    {relation_n, <<"all_equal"/utf8>>, fun(Items) -> all_equal_loop(Items) end}.

-file("src/metamon/relation.gleam", 205).
-spec pairwise_loop(relation(GFR), list(GFR)) -> boolean().
pairwise_loop(R, Items) ->
    case Items of
        [] ->
            true;

        [_] ->
            true;

        [First, Second | Rest] ->
            case (erlang:element(3, R))(First, Second) of
                true ->
                    pairwise_loop(R, [Second | Rest]);

                false ->
                    false
            end
    end.

-file("src/metamon/relation.gleam", 199).
?DOC(
    " Lift a binary `Relation(b)` to an N-ary relation by checking it\n"
    " pairwise: every consecutive pair `(items[i], items[i+1])` must\n"
    " satisfy `r`. For `name == \"equal\"` this gives a chain of equal\n"
    " values; for `monotone` it gives a sorted chain.\n"
).
-spec pairwise(relation(GFO)) -> relation_n(GFO).
pairwise(R) ->
    {relation_n,
        <<<<"pairwise("/utf8, (erlang:element(2, R))/binary>>/binary, ")"/utf8>>,
        fun(Items) -> pairwise_loop(R, Items) end}.