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

-export([wrap/1, do/2, bind/2, join/1, co/2, disjunctive_syllogism/2, callcc/1, throw/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, main/0]).
-export_type([not_not/2]).

-type not_not(FQU, FQV) :: {cont, fun((fun((FQV) -> FQU)) -> FQU)}.

-spec compose(fun((FRD) -> FRE), fun((FRF) -> FRD)) -> fun((FRF) -> FRE).
compose(F, G) ->
    fun(X) -> F(G(X)) end.

-spec wrap(FRG) -> not_not(any(), FRG).
wrap(A) ->
    {cont, fun(K) -> K(A) end}.

-spec do(not_not(FRK, FRL), fun((FRL) -> FRO)) -> not_not(FRK, FRO).
do(C, F) ->
    {cont, fun(K) -> (erlang:element(2, C))(fun(A) -> K(F(A)) end) end}.

-spec bind(not_not(FRR, FRS), fun((FRS) -> not_not(FRR, FRV))) -> not_not(FRR, FRV).
bind(C, F) ->
    {cont,
        fun(K) ->
            (erlang:element(2, C))(fun(A) -> (erlang:element(2, F(A)))(K) end)
        end}.

-spec join(not_not(FSA, not_not(FSA, FSB))) -> not_not(FSA, FSB).
join(A) ->
    {cont,
        fun(K) ->
            (erlang:element(2, A))(fun(B) -> (erlang:element(2, B))(K) end)
        end}.

-spec co(
    fun((fun((FSJ) -> FSI)) -> not_not(FSI, FSM)),
    fun(({ok, FSM} | {error, FSJ}) -> not_not(FSI, FSR))
) -> not_not(FSI, FSR).
co(F, Rest) ->
    {cont,
        fun(K) ->
            K2 = fun(A) -> (erlang:element(2, Rest(A)))(K) end,
            (erlang:element(
                2,
                F(compose(K2, fun(Field@0) -> {error, Field@0} end))
            ))(compose(K2, fun(Field@0) -> {ok, Field@0} end))
        end}.

-spec disjunctive_syllogism(
    not_not(FSW, {ok, FSX} | {error, FSY}),
    fun((FSY) -> FSW)
) -> not_not(FSW, FSX).
disjunctive_syllogism(E, Not_a) ->
    {cont, fun(K) -> (erlang:element(2, E))(fun(Res) -> case Res of
                        {error, A} ->
                            Not_a(A);

                        {ok, E@1} ->
                            K(E@1)
                    end end) end}.

-spec callcc(fun((fun((FTI) -> FTH)) -> FTI)) -> not_not(FTH, FTI).
callcc(F) ->
    co(fun(K) -> wrap(F(K)) end, fun(S) -> _pipe = case S of
                {error, A} ->
                    A;

                {ok, A@1} ->
                    A@1
            end,
            wrap(_pipe) end).

-spec throw(FTN, fun((FTN) -> FTO)) -> not_not(FTO, any()).
throw(A, Not_a) ->
    Instant_fail = wrap({error, A}),
    disjunctive_syllogism(Instant_fail, Not_a).

-spec excluded_middle() -> not_not(FTU, {ok, fun((FTV) -> FTU)} | {error, FTV}).
excluded_middle() ->
    co(fun(K) -> wrap(K) end, fun(Cofn) -> wrap(Cofn) end).

-spec double_negate(FUC) -> not_not(FUD, fun((fun((FUC) -> FUD)) -> FUD)).
double_negate(A) ->
    bind(excluded_middle(), fun(Lem) -> case Lem of
                {error, Not_a} ->
                    throw(A, Not_a);

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

-spec adjunction(fun((fun((FUL) -> FUK)) -> not_not(FUK, FUO))) -> not_not(FUK, fun((fun((FUO) -> FUK)) -> not_not(FUK, FUL))).
adjunction(F) ->
    co(
        fun(K) -> F(K) end,
        fun(S) ->
            T = wrap(case S of
                    {error, A} ->
                        {ok, A};

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

-spec double_negation_elimination(fun((fun((FUY) -> FUX)) -> FUX)) -> not_not(FUX, FUY).
double_negation_elimination(Not_not_a) ->
    bind(adjunction(fun(Not_a) -> wrap(Not_a) end), fun(F) -> F(Not_not_a) end).

-spec contramap(fun((FVG) -> FVF), fun((FVJ) -> not_not(FVF, FVG))) -> not_not(FVF, fun((FVJ) -> FVF)).
contramap(Not_b, F) ->
    bind(
        adjunction(
            fun(Not_not_a) ->
                bind(double_negation_elimination(Not_not_a), fun(A) -> F(A) end)
            end
        ),
        fun(F2) -> F2(Not_b) end
    ).

-spec implies(fun((FVQ) -> not_not(FVR, FVS))) -> not_not(FVR, {ok, FVS} |
    {error, fun((FVQ) -> FVR)}).
implies(F) ->
    co(
        fun(Not_not_a) -> bind(double_negation_elimination(Not_not_a), F) end,
        fun(S) -> wrap(S) end
    ).

-spec modus_ponens({ok, FWB} | {error, fun((FWD) -> FWC)}, FWD) -> not_not(FWC, FWB).
modus_ponens(F, A) ->
    bind(
        double_negate(A),
        fun(Not_not_a) -> disjunctive_syllogism(wrap(F), Not_not_a) end
    ).

-spec de_morgan_1(fun(({ok, FWM} | {error, FWN}) -> FWL)) -> not_not(FWL, {fun((FWN) -> FWL),
    fun((FWM) -> FWL)}).
de_morgan_1(X) ->
    bind(
        contramap(X, compose(fun wrap/1, fun(Field@0) -> {error, Field@0} end)),
        fun(L) ->
            bind(
                contramap(
                    X,
                    compose(fun wrap/1, fun(Field@0) -> {ok, Field@0} end)
                ),
                fun(R) -> wrap({L, R}) end
            )
        end
    ).

-spec de_morgan_2({fun((FWZ) -> FWY), fun((FXC) -> FWY)}) -> not_not(FWY, fun(({ok,
        FXC} |
    {error, FWZ}) -> FWY)).
de_morgan_2(X) ->
    {Not_a, Not_b} = X,
    contramap(Not_b, fun(A) -> disjunctive_syllogism(wrap(A), Not_a) end).

-spec de_morgan_3(fun(({FXM, FXN}) -> FXL)) -> not_not(FXL, {ok,
        fun((FXN) -> FXL)} |
    {error, fun((FXM) -> FXL)}).
de_morgan_3(X) ->
    bind(
        adjunction(
            fun(Y) ->
                bind(
                    de_morgan_1(Y),
                    fun(_use0) ->
                        {Not_not_a, Not_not_b} = _use0,
                        bind(
                            double_negation_elimination(Not_not_a),
                            fun(A) ->
                                bind(
                                    double_negation_elimination(Not_not_b),
                                    fun(B) -> wrap({A, B}) end
                                )
                            end
                        )
                    end
                )
            end
        ),
        fun(F) -> F(X) end
    ).

-spec de_morgan_4({ok, fun((FXZ) -> FXY)} | {error, fun((FYC) -> FXY)}) -> not_not(FXY, fun(({FYC,
    FXZ}) -> FXY)).
de_morgan_4(X) ->
    bind(excluded_middle(), fun(Lem) -> case Lem of
                {error, {A, B}} ->
                    case X of
                        {error, Not_a} ->
                            throw(A, Not_a);

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

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

-spec function_to_coexponential(fun((FYL) -> not_not(FYM, FYN))) -> not_not(FYM, fun(({FYL,
    fun((FYN) -> FYM)}) -> FYM)).
function_to_coexponential(F) ->
    bind(implies(F), fun(Or) -> case Or of
                {error, Not_a} ->
                    de_morgan_4({error, Not_a});

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

-spec coexponential_to_function(fun(({FYY, fun((FYZ) -> FYX)}) -> FYX)) -> not_not(FYX, fun((FYY) -> not_not(FYX, FYZ))).
coexponential_to_function(C) ->
    _pipe = fun(A) -> bind(de_morgan_3(C), fun(Or) -> case Or of
                    {error, Not_a} ->
                        throw(A, Not_a);

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

-spec pierces_law(fun((fun((FZJ) -> not_not(FZK, any()))) -> not_not(FZK, FZJ))) -> not_not(FZK, FZJ).
pierces_law(F) ->
    bind(implies(F), fun(Or) -> case Or of
                {error, Not_a} ->
                    bind(
                        adjunction(fun coexponential_to_function/1),
                        fun(F@1) ->
                            do(
                                F@1(Not_a),
                                fun(_use0) ->
                                    {Out, _} = _use0,
                                    Out
                                end
                            )
                        end
                    );

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

-spec main() -> integer().
main() ->
    gleam@io:println(<<"Hello from fluoresce!"/utf8>>),
    G = (bind(
        double_negate(3),
        fun(Not_not_a) ->
            bind(
                callcc(fun(_) -> gleam@io:debug(<<"hi"/utf8>>) end),
                fun(_) -> do(excluded_middle(), fun(Lem) -> case Lem of
                                {error, Not_a} ->
                                    throw(Not_a, Not_not_a);

                                {ok, _} ->
                                    double_negation_elimination(Not_not_a)
                            end end) end
            )
        end
    )),
    (erlang:element(2, G))(
        fun(A) -> (erlang:element(2, A))(fun gleam@io:debug/1) end
    ).