/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/app_builder.h"

namespace lean {
optional<expr> mk_constructor_eq_constructor_inconsistency_proof(type_context & ctx, expr const & e1, expr const & e2, expr const & h) {
    // TODO(Leo, Daniel): add support for generalized inductive datatypes
    environment const & env = ctx.env();
    optional<name> c1 = is_constructor_app(env, e1);
    if (!c1) return none_expr();
    optional<name> c2 = is_constructor_app(env, e2);
    if (!c2) return none_expr();
    if (*c1 == *c2) return none_expr();
    expr A = ctx.relaxed_whnf(ctx.infer(e1));
    expr I = get_app_fn(A);
    if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I)))
        return none_expr();
    name nc_name(const_name(I), "no_confusion");
    if (!env.find(nc_name)) return none_expr();
    expr pr = mk_app(ctx, nc_name, {mk_false(), e1, e2, h});
    return some_expr(pr);
}

optional<expr> mk_constructor_ne_constructor_proof(type_context & ctx, expr const & e1, expr const & e2) {
    type_context::tmp_locals locals(ctx);
    expr h  = locals.push_local("_h", mk_eq(ctx, e1, e2));
    if (optional<expr> pr = mk_constructor_eq_constructor_inconsistency_proof(ctx, e1, e2, h))
        return some_expr(locals.mk_lambda(*pr));
    else
        return none_expr();
}

optional<expr> mk_constructor_eq_constructor_implied_core(type_context & ctx, expr const & e1, expr const & e2, expr const & h, buffer<expr_pair> & implied_pairs) {
    // TODO(Leo, Daniel): add support for generalized inductive datatypes
    // TODO(Leo): add a definition for this proof at inductive datatype declaration time?
    environment const & env = ctx.env();
    optional<name> c1 = is_constructor_app(env, e1);
    if (!c1) return none_expr();
    optional<name> c2 = is_constructor_app(env, e2);
    if (!c2) return none_expr();
    if (*c1 != *c2) return none_expr();
    expr A = ctx.relaxed_whnf(ctx.infer(e1));
    expr I = get_app_fn(A);
    if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I)))
        return none_expr();
    name nct_name(const_name(I), "no_confusion_type");
    if (!env.find(nct_name)) return none_expr();
    unsigned num_params  = *inductive::get_num_params(env, const_name(I));
    buffer<expr> e1_args, e2_args;
    get_app_args(e1, e1_args);
    get_app_args(e2, e2_args);
    unsigned cnstr_arity = get_arity(env.get(*c1).get_type());
    if (e1_args.size() != cnstr_arity) return none_expr();
    lean_assert(cnstr_arity >= num_params);
    lean_assert(e1_args.size() == e2_args.size());
    unsigned num_new_eqs = cnstr_arity - num_params;
    /* Collect implied equalities */
    buffer<expr> implied_eqs;
    for (unsigned i = num_params; i < e1_args.size(); i++) {
        expr const & arg1 = e1_args[i];
        expr const & arg2 = e2_args[i];
        implied_pairs.emplace_back(arg1, arg2);
        implied_eqs.push_back(mk_eq(ctx, arg1, arg2));
    }
    /* Construct motive (eq_1 /\ ... /\ eq_n), where eq_i's are the implied equalities */
    if (implied_eqs.empty()) return none_expr();
    expr motive = implied_eqs.back();
    unsigned i  = implied_eqs.size() - 1;
    while (i > 0) {
        --i;
        motive  = mk_and(implied_eqs[i], motive);
    }
    /* Construct proof for (eq_1 /\ ... /\ eq_n) using no_confusion.
       The proof is of the form:
           I.no_confusion motive e1 e2 h (fun eq_1 ... eq_n, and.intro eq_1 ... eq_n) */
    name nc_name(const_name(I), "no_confusion");
    expr result_prefix = mk_app(ctx, nc_name, {motive, e1, e2, h});
    expr nct = ctx.relaxed_whnf(mk_app(ctx, nct_name, motive, e1, e2));
    if (!is_pi(nct)) return none_expr();
    expr it  = binding_domain(nct);
    type_context::tmp_locals locals(ctx);
    buffer<expr> eq_proofs;
    for (unsigned i = 0; i < num_new_eqs; i++) {
        /* Remark: some of the hypotheses are heterogeneous, we should convert them
           back into homogeneous. */
        if (!is_pi(it)) return none_expr();
        expr heq = locals.push_local_from_binding(it);
        if (is_heq(binding_domain(it)))
            eq_proofs.push_back(mk_eq_of_heq(ctx, heq));
        else
            eq_proofs.push_back(heq);
        it = ctx.relaxed_whnf(instantiate(binding_body(it), heq));
    }
    expr body_pr = eq_proofs.back();
    i = eq_proofs.size() - 1;
    while (i > 0) {
        --i;
        body_pr = mk_and_intro(ctx, eq_proofs[i], body_pr);
    }
    expr fun = locals.mk_lambda(body_pr);
    return some_expr(mk_app(result_prefix, fun));
}

bool mk_constructor_eq_constructor_implied_eqs(type_context & ctx, expr const & e1, expr const & e2, expr const & h, buffer<std::tuple<expr, expr, expr>> & result) {
    buffer<expr_pair> implied_pairs;
    optional<expr> conj_pr = mk_constructor_eq_constructor_implied_core(ctx, e1, e2, h, implied_pairs);
    if (!conj_pr) return false;
    expr pr = *conj_pr;
    unsigned sz = implied_pairs.size();
    for (unsigned i = 0; i < sz - 1; i++) {
        result.emplace_back(implied_pairs[i].first, implied_pairs[i].second, mk_and_elim_left(ctx, pr));
        pr = mk_and_elim_right(ctx, pr);
    }
    result.emplace_back(implied_pairs.back().first, implied_pairs.back().second, pr);
    return true;
}
}