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

-export([disjunctive_syllogism/2, excluded_middle/0, double_negate/1, adjunction/1, double_negation_elimination/1, contramap/2, implies/1, modus_ponens/2, de_morgan_1/1, de_morgan_2/1, de_morgan_3/1, de_morgan_4/1, function_to_coexponential/1, coexponential_to_function/1, pierces_law/1]).

-spec disjunctive_syllogism(
    fluoresce:cont(FWI, {ok, FWJ} | {error, FWK}),
    fun((FWK) -> FWI)
) -> fluoresce:cont(FWI, FWJ).
disjunctive_syllogism(E, Not_a) ->
    fluoresce:apply(E, Not_a).

-spec excluded_middle() -> fluoresce:cont(FWT, {ok, fun((FWU) -> FWT)} |
    {error, FWU}).
excluded_middle() ->
    fluoresce:co(
        fun(K) -> fluoresce:wrap(K) end,
        fun(Cofn) -> fluoresce:wrap(Cofn) end
    ).

-spec double_negate(FXB) -> fluoresce:cont(FXC, fun((fun((FXB) -> FXC)) -> FXC)).
double_negate(A) ->
    fluoresce:bind(excluded_middle(), fun(Lem) -> case Lem of
                {error, Not_a} ->
                    fluoresce:throw(A, Not_a);

                {ok, Not_not_a} ->
                    fluoresce:wrap(Not_not_a)
            end end).

-spec adjunction(fun((fun((FXK) -> FXJ)) -> fluoresce:cont(FXJ, FXN))) -> fluoresce:cont(FXJ, fun((fun((FXN) -> FXJ)) -> fluoresce:cont(FXJ, FXK))).
adjunction(F) ->
    fluoresce:co(
        fun(K) -> F(K) end,
        fun(S) ->
            T = fluoresce:wrap(case S of
                    {error, A} ->
                        {ok, A};

                    {ok, B} ->
                        {error, B}
                end),
            fluoresce:wrap(fun(Not_b) -> disjunctive_syllogism(T, Not_b) end)
        end
    ).

-spec double_negation_elimination(fun((fun((FXX) -> FXW)) -> FXW)) -> fluoresce:cont(FXW, FXX).
double_negation_elimination(Not_not_a) ->
    fluoresce:bind(
        adjunction(fun(Not_a) -> fluoresce:wrap(Not_a) end),
        fun(F) -> F(Not_not_a) end
    ).

-spec contramap(fun((FYF) -> FYE), fun((FYI) -> fluoresce:cont(FYE, FYF))) -> fluoresce:cont(FYE, fun((FYI) -> FYE)).
contramap(Not_b, F) ->
    fluoresce:bind(
        adjunction(
            fun(Not_not_a) ->
                fluoresce:bind(
                    double_negation_elimination(Not_not_a),
                    fun(A) -> F(A) end
                )
            end
        ),
        fun(F2) -> F2(Not_b) end
    ).

-spec implies(fun((FYP) -> fluoresce:cont(FYQ, FYR))) -> fluoresce:cont(FYQ, {ok,
        FYR} |
    {error, fun((FYP) -> FYQ)}).
implies(F) ->
    fluoresce:co(
        fun(Not_not_a) ->
            fluoresce:bind(double_negation_elimination(Not_not_a), F)
        end,
        fun(S) -> fluoresce:wrap(S) end
    ).

-spec modus_ponens({ok, FZA} | {error, fun((FZC) -> FZB)}, FZC) -> fluoresce:cont(FZB, FZA).
modus_ponens(F, A) ->
    fluoresce:bind(
        double_negate(A),
        fun(Not_not_a) ->
            disjunctive_syllogism(fluoresce:wrap(F), Not_not_a)
        end
    ).

-spec de_morgan_1(fun(({ok, FZL} | {error, FZM}) -> FZK)) -> fluoresce:cont(FZK, {fun((FZM) -> FZK),
    fun((FZL) -> FZK)}).
de_morgan_1(X) ->
    fluoresce:bind(
        contramap(
            X,
            fluoresce:compose(
                fun fluoresce:wrap/1,
                fun(Field@0) -> {error, Field@0} end
            )
        ),
        fun(L) ->
            fluoresce:bind(
                contramap(
                    X,
                    fluoresce:compose(
                        fun fluoresce:wrap/1,
                        fun(Field@0) -> {ok, Field@0} end
                    )
                ),
                fun(R) -> fluoresce:wrap({L, R}) end
            )
        end
    ).

-spec de_morgan_2({fun((FZY) -> FZX), fun((GAB) -> FZX)}) -> fluoresce:cont(FZX, fun(({ok,
        GAB} |
    {error, FZY}) -> FZX)).
de_morgan_2(X) ->
    {Not_a, Not_b} = X,
    contramap(
        Not_b,
        fun(A) -> disjunctive_syllogism(fluoresce:wrap(A), Not_a) end
    ).

-spec de_morgan_3(fun(({GAL, GAM}) -> GAK)) -> fluoresce:cont(GAK, {ok,
        fun((GAM) -> GAK)} |
    {error, fun((GAL) -> GAK)}).
de_morgan_3(X) ->
    fluoresce:bind(
        adjunction(
            fun(Y) ->
                fluoresce:bind(
                    de_morgan_1(Y),
                    fun(_use0) ->
                        {Not_not_a, Not_not_b} = _use0,
                        fluoresce:bind(
                            double_negation_elimination(Not_not_a),
                            fun(A) ->
                                fluoresce:bind(
                                    double_negation_elimination(Not_not_b),
                                    fun(B) -> fluoresce:wrap({A, B}) end
                                )
                            end
                        )
                    end
                )
            end
        ),
        fun(F) -> F(X) end
    ).

-spec de_morgan_4({ok, fun((GAY) -> GAX)} | {error, fun((GBB) -> GAX)}) -> fluoresce:cont(GAX, fun(({GBB,
    GAY}) -> GAX)).
de_morgan_4(X) ->
    fluoresce:bind(excluded_middle(), fun(Lem) -> case Lem of
                {error, {A, B}} ->
                    case X of
                        {error, Not_a} ->
                            fluoresce:throw(A, Not_a);

                        {ok, Not_b} ->
                            fluoresce:throw(B, Not_b)
                    end;

                {ok, Not_pair} ->
                    fluoresce:wrap(Not_pair)
            end end).

-spec function_to_coexponential(fun((GBK) -> fluoresce:cont(GBL, GBM))) -> fluoresce:cont(GBL, fun(({GBK,
    fun((GBM) -> GBL)}) -> GBL)).
function_to_coexponential(F) ->
    fluoresce:bind(implies(F), fun(Or) -> case Or of
                {error, Not_a} ->
                    de_morgan_4({error, Not_a});

                {ok, B} ->
                    fluoresce:bind(
                        double_negate(B),
                        fun(Not_not_b) -> de_morgan_4({ok, Not_not_b}) end
                    )
            end end).

-spec coexponential_to_function(fun(({GBX, fun((GBY) -> GBW)}) -> GBW)) -> fluoresce:cont(GBW, fun((GBX) -> fluoresce:cont(GBW, GBY))).
coexponential_to_function(C) ->
    _pipe = fun(A) -> fluoresce:bind(de_morgan_3(C), fun(Or) -> case Or of
                    {error, Not_a} ->
                        fluoresce:throw(A, Not_a);

                    {ok, Not_not_b} ->
                        double_negation_elimination(Not_not_b)
                end end) end,
    fluoresce:wrap(_pipe).

-spec pierces_law(
    fun((fun((GCI) -> fluoresce:cont(GCJ, any()))) -> fluoresce:cont(GCJ, GCI))
) -> fluoresce:cont(GCJ, GCI).
pierces_law(F) ->
    fluoresce:bind(implies(F), fun(Or) -> case Or of
                {error, Not_a} ->
                    fluoresce:bind(
                        adjunction(fun coexponential_to_function/1),
                        fun(F@1) ->
                            fluoresce:bind(
                                F@1(Not_a),
                                fun(_use0) ->
                                    {Out, _} = _use0,
                                    fluoresce:wrap(Out)
                                end
                            )
                        end
                    );

                {ok, A} ->
                    fluoresce:wrap(A)
            end end).