module Deductive

using DataFrames, PrettyTables

export Predicate, truthtable, tableau, prove
export Ē, Ā


include("./utils.jl")
include("./common_algorithms.jl")
include("./expression.jl")
include("./manipulation.jl")
include("./search.jl")

include("./db/index.jl")
include("./db/expressions_index.jl")

include("./proof_utilities.jl")
include("./inference_rules.jl")
include("./transformation_proof.jl")
include("./assertion_proof.jl")
include("./atomic.jl")

include("./set/set.jl")
include("./set/set_operator.jl")
include("./set/set_proof.jl")
include("./set/special_definitions.jl")
include("./set/set_equality.jl")

include("./latex.jl")


# function FreeVariable(sym::Symbol, metadata::Symbol)
#     Sym{Any, Symbol}(sym, metadata)
# end
# function FreeVariable(sym::Symbol)
#     FreeVariable(sym, :free)
# end
FreeVariableType = LogicalSymbol
# LogicalSymbol = Sym{Bool}
# SB = Union{LogicalSymbol, Term}

# Predicate(sym::Symbol) = (st) -> begin
#     Term{Bool}(LogicalSymbol(sym), [st]; metadata=:predicate)
# end


# quantifiers
# todo: fix quantifier logic (see https://github.com/ctrekker/Deductive.jl/issues/2)
Ē = LogicalOperation((n, m) -> nothing, :Ē, 2, false, false)
Ā = LogicalOperation((n, m) -> nothing, :Ā, 2, false, false)
# function Ē(x::FreeVariableType, st::AbstractExpression)
#     quantified_var = Sym{Any, Symbol}(Symbolics.tosymbol(x), :quantified)
#     AbstractExpression(Ē, [quantified_var, replace(st, x => quantified_var)])
# end
# function Ā(x::FreeVariableType, st::AbstractExpression)
#     quantified_var = Sym{Any, Symbol}(Symbolics.tosymbol(x), :quantified)
#     Term(Ā, [quantified_var, substitute(st, x => quantified_var)])
# end

# function substitute_quantified(term::Term, substitution::FreeVariableType)
#     term_args = arguments(term)
#     substitute(term_args[2], term_args[1] => substitution)
# end


# free variable unary "placeholder"
# marker for substitution with a skolem variable
_f = LogicalSymbol(:_f, :definitionallyfree)


function truthtable(st::AbstractExpression)
    vars = sort([variables(st)...])
    combinations = 2 ^ length(vars)
    st_sym = Symbol(string(st))

    # prevent duplicate table keys if the expression is, for example, "a"
    if st_sym == Symbol(first(vars))
        st_sym = Symbol("_" * string(st))
    end

    table = DataFrame(Dict(Symbol(var) => Bool[] for var ∈ vars)..., Dict(st_sym => Bool[])...)

    for i ∈ 0:(combinations-1)
        variable_values = _dict_from_combination_index(vars, i)
        result = evaluate(st, variable_values)
        push!(table, merge(Dict(Symbol(k) => v for (k, v) ∈ variable_values), Dict(st_sym => result)))
    end

    table
end


p, q = LogicalSymbol.([:p, :q])
const demorgan_and = ¬(p ∧ q) => ¬p ∨ ¬q
const demorgan_or = ¬(p ∨ q) => ¬p ∧ ¬q
const double_negative = ¬¬p => p
const material_implication = p → q => ¬p ∨ q
const negated_material_implication = ¬(p → q) => p ∧ ¬q
const material_equivalence = p ⟷ q => (p ∧ q) ∨ (¬p ∧ ¬q)
const negated_material_equivalence = ¬(p ⟷ q) => (p ∧ ¬q) ∨ (¬p ∧ q)

const tableau_replacement_rules = Pair{AbstractExpression, AbstractExpression}[
    demorgan_and,
    demorgan_or,
    double_negative,
    material_implication,
    negated_material_implication,
    material_equivalence,
    negated_material_equivalence
]

# These rules require some extra things, such as substitution by skolem constants after rule application
x, y = LogicalSymbol.([:x, :y])
deny_universal =     ¬Ā(x, y) => ¬y
assert_existential =  Ē(x, y) =>  y
assert_universal =    Ā(x, y) =>  y
deny_existential =   ¬Ē(x, y) => ¬y


tableau(proposition::AbstractExpression; kw...) = tableau([proposition]; kw...)
tableau(propositions...; kw...) = tableau([propositions...]; kw...)
function tableau(propositions::Union{Set, Vector}; skolem_vars=[], proof::Vector{ProofLine}=ProofLine[])
    if length(proof) == 0
        for proposition ∈ propositions
            push!(proof, ProofLine(length(proof) + 1, proposition, "Assumption"))
        end
    end
    simplified_propositions = AbstractExpression[repeated_chain_simplify(p, tableau_replacement_rules) for p ∈ propositions]

    for proposition ∈ simplified_propositions
        if isnothing(find_proof_line_by_statement(proof, proposition))
            push!(proof, ProofLine(length(proof) + 1, proposition, "Replacement Rule <TODO>"))
        end
    end

    return _tableau_simplified(simplified_propositions; skolem_vars=skolem_vars, proof=proof)
end

function _tableau_simplified(propositions::Vector{AbstractExpression}; skolem_vars=[], proof::Vector{ProofLine}=ProofLine[])
    # compile list of all free variables in all propositions
    free_vars = collect(Iterators.flatten([variables(p) for p ∈ propositions]))
    free_vars = filter([istree(v) ? first(arguments(v)) : v for v ∈ free_vars]) do v
        v.metadata == :free
    end

    # when a quantifier is simplified we find existing skolem variables and substitute them in for universal free variables
    # function populate_skolems(term::Term, unary_operator=identity)
    #     placeholder_assertion = unary_operator(substitute_quantified(term, _f))
    #     realized_assertions = [unary_operator(substitute_quantified(term, var)) for var ∈ Iterators.flatten([skolem_vars, free_vars])]

    #     Set([placeholder_assertion, realized_assertions...])
    # end

    # when a quantifier is simplified a new skolem variable can be created in some cases
    # this function creates a new skolem variable and substitutes it into all free variable predicates
    # function create_skolem(term::Term, reduced_propositions, unary_operator=identity)
    #     new_skolem_var = FreeVariable(Symbol("c" * string(length(skolem_vars) + 1)), :skolem)
    #     new_assertion = unary_operator(substitute_quantified(term, new_skolem_var))
    #     realized_placeholders = [substitute(st, _f => new_skolem_var) for st ∈ reduced_propositions]

    #     new_skolem_var, Set([realized_placeholders..., new_assertion])
    # end

    ordered_propositions = [propositions...]
    for p ∈ propositions
        pv = p

        if !istree(pv) || metadata(pv) == :predicate
            # check for contradiction
            contradiction_index = findfirst([isequal(¬p, q) for q ∈ ordered_propositions])
            if !isnothing(contradiction_index)
                contradictory_statement = ordered_propositions[contradiction_index]
                contradiction_references = [
                    find_proof_line_by_statement(proof, pv),
                    find_proof_line_by_statement(proof, contradictory_statement)
                ]

                if any(isnothing.(contradiction_references))
                    @error "Contradiction found, but one or more references is missing"
                else
                    push!(proof, ProofLine(length(proof) + 1, p ∧ contradictory_statement, "Contradiction", contradiction_references))
                end

                return false
            end
        else
            term_op = operation(pv)
            term_args = arguments(pv)
            reduced_propositions = setdiff(propositions, Set([p]))

            if length(term_args) == 2 # binary operation
                line_ref = find_proof_line_by_statement(proof, pv)

                if term_op == ∧
                    # break up term and make one recursive call

                    # add simplification to proof
                    push!(proof, ProofLine(length(proof) + 1, term_args[1], "Simplification", line_ref))
                    push!(proof, ProofLine(length(proof) + 1, term_args[2], "Simplification", line_ref))

                    if !tableau(reduced_propositions ∪ Set(term_args); skolem_vars=skolem_vars, proof=proof)
                        return false
                    end
                    break
                elseif term_op == ∨
                    # consider both arguments of term and make two recursive calls
                    
                    # case-by-case checking
                    case1_linenum, case2_linenum = length(proof) + 1, length(proof) + 2
                    push!(proof, ProofLine(case1_linenum, term_args[1], "Case 1", line_ref))
                    push!(proof, ProofLine(case2_linenum, term_args[2], "Case 2", line_ref))

                    if !tableau(reduced_propositions ∪ Set([term_args[1]]); skolem_vars=skolem_vars, proof=proof) && !tableau(reduced_propositions ∪ Set([term_args[2]]); skolem_vars=skolem_vars, proof=proof)
                        push!(proof, ProofLine(length(proof) + 1, ¬pv ∧ pv, "Contradiction", [proof[case1_linenum], proof[case2_linenum]]))

                        return false
                    end
                    break
                elseif term_op == Ā  # asserted universal quantifier
                    # create free variable
                    if !tableau(reduced_propositions ∪ populate_skolems(pv); skolem_vars=skolem_vars, proof=proof)
                        return false
                    end
                    break
                elseif term_op == Ē  # asserted existential quantifier
                    # substitute skolem variable
                    new_skolem_var, new_propositions = create_skolem(pv, reduced_propositions)
                    if !tableau(reduced_propositions ∪ new_propositions; skolem_vars=[skolem_vars..., new_skolem_var], proof=proof)
                        return false
                    end
                    break
                end
            else # unary operation (¬, logical statements)
                subterm = first(term_args)

                if istree(subterm)
                    subterm_op = operation(subterm)

                    # check for negated quantifiers
                    if subterm_op == Ā  # denied universal quantifier
                        new_skolem_var, new_propositions = create_skolem(subterm, reduced_propositions, ¬)
                        if !tableau(reduced_propositions ∪ new_propositions; skolem_vars=[skolem_vars..., new_skolem_var], proof=proof)
                            return false
                        end
                        break
                    elseif subterm_op == Ē  # denied existential quantifier
                        if !tableau(reduced_propositions ∪ populate_skolems(subterm, ¬); skolem_vars=skolem_vars, proof=proof)
                            return false
                        end
                        break
                    end
                end
            end
        end
    end
    
    return true
end


prove(proposition::AbstractExpression; kw...) = prove([proposition]; kw...)
prove(propositions...; kw...) = prove([propositions...]; kw...)
function prove(propositions::Union{Set, Vector})
    proof = ProofLine[]
    tableau(propositions; proof=proof)

    proof
end


_dict_from_combination_index(variables, index::Int) = Dict([variables[i] => Bool(index >> (i-1) & 1) for i ∈ 1:length(variables)])

end # module
