#include "clasplayer.h"

#include <clasp/program_builder.h>        // for defining logic programs
#include <clasp/unfounded_check.h>      // unfounded set checkers
#include <clasp/model_enumerators.h>  // for enumerating answer sets
#include <clasp/clasp_facade.h>

#include <clingocontrol.hh>

#include <iostream>
#include <clingo_lib.hh>

using namespace std;

namespace xreate {

    void
    ClaspLayer::printWarnings(std::ostream& out)
    {
        const std::string warningTag = "warning";

        auto warningsRange = __model.equal_range(warningTag);

        for (auto warning=warningsRange.first; warning!= warningsRange.second; ++warning) {
            unsigned int warningId;

            Gringo::Value params;
            std::tie(warningId, params) = parse<unsigned int, Gringo::Value>(warning->second);

            cout << "Warning: " << __warnings.at(warningId) << " ";
            params.print(out);
            out<<params;
        }
    }

    bool
    ClaspLayer::onModel(Gringo::Model const &model) {
        std::list<std::string> warnings;
        cout << "Model: " << endl;
        for (Gringo::Value atom : model.atoms(Gringo::Model::ATOMS)) {
            atom.print(cout);
            cout << endl;

            __model.emplace(*atom.name(), move(atom));
        }
    }

    QStringList multiplyLists(std::list<QStringList> &&lists) {
        QStringList result = lists.front();
        lists.pop_front();

        for (QStringList &list: lists) {
            QStringList::const_iterator end = result.end();
            for (QStringList::iterator expr1I = result.begin(); expr1I < end; ++expr1I) {
                if (list.size() == 0) continue;

                QStringList::const_iterator expr2I = list.begin();
                for (int expr2No = 0, size = list.size() - 1; expr2No < size; ++expr2No, ++expr1I)
                    result.append(QString("%1, %2").arg(*expr1I).arg(*expr2I));

                *expr1I = QString("%1, %2").arg(*expr1I).arg(*expr2I);
            }
        }

        return result;
    }

    void
    ClaspLayer::addCFAData(CFGraph &&graph) {
        ostream &cout = __partGeneral;

        cout << endl << "%\t\tStatic analysis: CFA" << endl;

        for (const std::pair<unsigned int, unsigned int> &relation: graph.__relations) {
            const string &tagFrom = graph.__nodes.at(relation.first);
            const string &tagTo = graph.__nodes.at(relation.second);

            cout << (QString("call(%1, %2) .").arg(tagFrom.c_str()).arg(tagTo.c_str())).toStdString() << endl;
        }
    }

    void
    ClaspLayer::addDFAData(DFGraph &&graph)
    {
        dfgData = graph;
        std::set<SymbolPacked> symbols;
        ostream &cout = __partGeneral;

        cout << endl << "%\t\tStatic analysis: DFA" << endl;

        std::vector<std::pair<SymbolPacked, SymbolPacked>>::iterator i1;
        std::vector<DFGConnection>::iterator i2;

        for (i1=dfgData.__edges.begin(), i2 = dfgData.__data.begin(); i1!= dfgData.__edges.end(); ++i1, ++i2 )
        {
            QString edgeData;
            switch (*i2)
            {
                case DFGConnection::OPT: edgeData = "opt"; break;
                case DFGConnection::STRONG: edgeData = "strong"; break;
                case DFGConnection::PROTO: edgeData = "proto"; break;
            }

            cout << QString("dfa_connection(%1, %2, %3).")
                    .arg(QString("(%1, %2)").arg(i1->first.identifier).arg(i1->first.scope))
                    .arg(QString("(%1, %2)").arg(i1->second.identifier).arg(i1->second.scope))
                    .arg(edgeData).toStdString() << endl;

            symbols.insert(i1->first);
            symbols.insert(i1->second);
        }

        for (const pair<SymbolPacked, Expression>& tag:  dfgData.__tags)
        {
            for (QString variant: compile(tag.second)) {
                cout << QString("bind(%1, %2).")
                        .arg(QString("(%1, %2)").arg(tag.first.identifier).arg(tag.first.scope))
                        .arg(variant).toStdString()<<endl;
            }

            symbols.insert(tag.first);
        }

        for (const SymbolPacked& s: symbols)
        {
            cout << QString("v((%1, %2)).").arg(s.identifier). arg(s.scope).toStdString()<<endl;
        }
    }

    void
    ClaspLayer::addFunctionTags(const std::string &function, const std::vector<Tag> &tags) {
        ostream &cout = __partTags;

        cout << (QString("function(%1) .").arg(function.c_str())).toStdString() << std::endl;

        int tagsCount = 0;
        for (const Tag &tag: tags) {
            QStringList tagRaw = compile(tag.first);
            assert(tagRaw.size() == 1);

            cout << QString("tag(%1, %2).").arg(function.c_str()).arg(tagRaw.at(0)).toStdString() << endl;
            ++tagsCount;
        }
        if (tagsCount == 0) {
            cout << "%no tags at all" << endl;
        }
    }

    void
    ClaspLayer::addRuleWarning(const RuleWarning &rule) {
        //__partGeneral << rule << endl;

        QStringList domains;
        std::transform(rule.__args.begin(), rule.__args.end(), std::inserter(domains, domains.begin()),
                [](const std::pair<std::string, DomainAnnotation> &argument) {
                    string domain;
                    switch (argument.second) {
                        case DomainAnnotation::FUNCTION:
                            domain = "function";
                            break;
                        case DomainAnnotation::VARIABLE:
                            domain = "variable";
                            break;
                    }

                    return QString("%1(%2)").arg(domain.c_str()).arg(argument.first.c_str());
                });

        QStringList vars;
        std::transform(rule.__args.begin(), rule.__args.end(), std::inserter(vars, vars.begin()),
                [](const std::pair<std::string, DomainAnnotation> &argument) {
                    return argument.first.c_str();
                });

        std::list<QStringList> guardsRaw;
        std::transform(rule.__guards.begin(), rule.__guards.end(), std::inserter(guardsRaw, guardsRaw.begin()),
                [this](const Expression &guard) {
                    return compile(guard);
                });

        QStringList guards = multiplyLists(std::move(guardsRaw));
        QStringList &&branches = compileNeg(rule.__condition);

        for (const QString &guardsJoined: guards)
            for (const QString &branch: branches) {
                unsigned int hook = registerWarning(string(rule.__message));

                QString result = QString("warning(%1, (%2)):- %3, %4, %5.")
                        .arg(hook)
                        .arg(vars.join(", "))
                        .arg(branch)
                        .arg(guardsJoined)
                        .arg(domains.join(", "));

                __partGeneral << result.toStdString() << endl;
            }
    }

    QStringList
    ClaspLayer::compile(const Expression &e) const {
        QStringList result;

        switch (e.op) {
            case Operator::CALL: {
                assert(e.__state == Expression::COMPOUND);

                std::list<QStringList> operands;
                std::transform(e.operands.begin(), e.operands.end(), std::inserter(operands, operands.begin()),
                        [this](const Expression &e) {
                            return compile(e);
                        });

                QStringList &&operands_ = multiplyLists(std::move(operands));
                result.append(QString("%1(%2)").arg(e.__valueS.c_str()).arg(operands_.join(", ")));
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                QStringList &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.append(QString("not %1").arg(rawOp.at(0)));
                break;
            };

            case Operator::NONE: {
                switch (e.__state) {
                    case Expression::IDENT:
                        result.append(QString(e.__valueS.c_str()));
                        break;

                    case Expression::NUMBER:
                        result.append(QString::number(e.__valueD));
                        break;

                    default:
                        assert(true);
                }
                break;
            }
        }

        return result;
    }

    QStringList
    ClaspLayer::compileNeg(const Expression &e) const {
        QStringList result;
        switch (e.op) {
            case Operator::IMPL: {
                assert(e.__state == Expression::COMPOUND);
                assert(e.operands.size() == 2);
                QStringList operands1 = compile(e.operands.at(0));
                QStringList operands2 = compile(e.operands.at(1));

                for (const auto &op1: operands1)
                    for (const auto &op2: operands2) {
                        result.append(QString("%1, not %2").arg(op1).arg(op2));
                    }
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                QStringList &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.append(rawOp.at(0));
                break;
            };

            default:
                assert(true);
        }

        return result;
    }

    unsigned int
    ClaspLayer::registerWarning(std::string &&message) {
        static int warningId = 0;
        __warnings.emplace(warningId, message);
        return warningId++;;
    }

    void
    ClaspLayer::addImports()    {
        ostream &out = __partGeneral;

        for (string fn: ast->__rawImports)
        {
            std::ifstream file(fn);
            if (!file) continue;

            while(!file.eof()){
                string line;
                std::getline(file, line);
                out << line << endl;
            }
        }
    }

    void
    ClaspLayer::run() {
        addImports();

        ostringstream program;
        program << __partTags.str() << __partGeneral.str();
        cout << program.str() << endl;

        const char *argv[] = {nullptr, nullptr};
        ClingoLib ctl(2, argv);

        //prg.add("p", ["t"], "q(t).")
        Gringo::FWStringVec vars{};
        ctl.add("base", vars, program.str());

        //prg.ground([("p", [2])])
        Gringo::Control::GroundVec vals{std::make_pair("base", Gringo::FWValVec {})};
        ctl.ground(vals, Gringo::Any());

        //solve
        Gringo::Control::Assumptions as;
        Gringo::SolveResult result = ctl.solve(Gringo::Control::ModelHandler([&](Gringo::Model const &model) {
            return this->onModel(model);
        }), std::move(as));

        if (result == Gringo::SolveResult::SAT) {
            cout << "SUCCESSFULLY" << endl;
        } else {
            cout << "UNSUCCESSFULLY" << endl;
        }

                // invoke all query plugins to process clasp data
        for (IQuery* q: __queries)
        {
            q->init(this);
        }
    }

    ClaspLayer::ClaspLayer() {
    }

    std::pair<ClaspLayer::ModelIterator, ClaspLayer::ModelIterator>
    ClaspLayer::query(const std::string& atom)
    {
        return __model.equal_range(atom);
    }



/*
void AspOutPrinter::reportSolution(const Clasp::Solver&, const Clasp::Enumerator&, bool complete) {
    if (complete) std::cout << "No more models!" << std::endl;
    else          std::cout << "More models possible!" << std::endl;
}


void AspOutPrinter::reportModel(const Clasp::Solver& s, const Clasp::Enumerator&) {
    std::cout << "Model " << s.stats.solve.models << ": \n";
// get the symbol table from the solver
    const Clasp::AtomIndex& symTab = *s.strategies().symTab;
    for (Clasp::AtomIndex::const_iterator it = symTab.begin(); it != symTab.end(); ++it)
    {
// print each named atom that is true w.r.t the current assignment
    }
    std::cout << std::endl;
}

*/
/*****************************************
 *                      CFGraph
 *****************************************
 */

    void
    CFGraph::addNode(unsigned int function, std::string &&tag) {
        __nodes.emplace(function, tag);
    }

    bool
    CFGraph::existsNode(unsigned int function) const {
        return __nodes.count(function);
    }

    void
    CFGraph::addLink(unsigned int nodeFrom, unsigned int nodeTo) {
        __relations.insert(std::make_pair(nodeFrom, nodeTo));
    }


/*****************************************
 *                      DFGraph
 *****************************************
 */
    bool
    DFGraph::linkExists(const SymbolPacked& node1, const SymbolPacked& node2)
    {
        auto range = __outEdges.equal_range(node2);

        for(std::multimap<SymbolPacked, EdgeId>::iterator edge = range.first; edge != range.second; ++edge)
        {
            if (__edges[edge->second].second == node1)
                return true;
        }

        return false;
    }

    void
    DFGraph::addLink(const SymbolPacked& nodeTo, const SymbolPacked& nodeFrom, DFGConnection link) {
        if (!linkExists(nodeTo, nodeFrom))
        {
            __edges.emplace_back(nodeTo, nodeFrom);
            __data.push_back(link);

            EdgeId eid = __edges.size()-1;
            __outEdges.emplace(nodeFrom, eid);
        }
    }

    void
    DFGraph::addTag(const SymbolPacked &node, Expression &&tag) {
        __tags.emplace(node, tag);
    }

    SymbolPacked
    DFGraph::pack(const Symbol& symbol, std::string hintSymbolName)
    {
        std::unordered_map<const CodeScope*, unsigned int>::iterator pos
                = __hash.emplace(symbol.scope, __hash.size()).first;
        __hashedScopes.push_back(symbol.scope);

        SymbolPacked result;
        result.scope = pos->second;
        result.identifier = symbol.identifier;
    }

    Symbol
    DFGraph::unpack(const SymbolPacked& symbol)
    {
        return Symbol{symbol.identifier, __hashedScopes[symbol.scope]};
    };

    bool SymbolPacked::isValid() const
    {
        return this->scope != SYMBOL_INVALID.scope && identifier != SYMBOL_INVALID.identifier;
    }

    bool operator==(const SymbolPacked& s1, const SymbolPacked& s2)
    {
        return s1.identifier == s2.identifier && s1.scope == s2.scope;
    }

    bool operator<(const SymbolPacked& s1, const SymbolPacked& s2)
    {
        return  s1.scope < s2.scope  || (s1.scope ==  s2.scope && s1.identifier < s2.identifier);
    }

    void ClaspLayer::registerdQuery(IQuery *query) {
        __queries.push_back(query);
    }
}