#include "clasplayer.h"

#include <iostream>
#include "utils.h"
#include <boost/format.hpp>
#include <boost/algorithm/string/join.hpp>
#include <gringo/scripts.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;

        const string& atomBindVar = Config::get("clasp.bindings.variable");
        const string& atomBindFunc = Config::get("clasp.bindings.function");
        const string& atomBindScope = Config::get("clasp.bindings.scope");

        for (Gringo::Value atom : model.atoms(Gringo::Model::ATOMS)) {
            atom.print(cout);
            cout <<" | "<< endl;

            if (*atom.name() == atomBindVar || *atom.name() == atomBindFunc || *atom.name() == atomBindScope){
                string name = *std::get<1>(parse<Gringo::Value, Gringo::Value>(atom)).name();
                __model.emplace(move(name), move(atom));
            }

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

        return true;
    }

    list<string>
    multiplyLists(list<list<string>> &&lists) {
        typedef list<string> StringList;
        assert(lists.size());
        StringList result(*lists.begin());
        lists.pop_front();

        boost::format concat("%s, %s");
        for (StringList &list: lists) {
            StringList::const_iterator end = result.end();
            for (StringList::iterator expr1I = result.begin(); expr1I != end; ++expr1I) {
                if (list.size() == 0) continue;

                StringList::const_iterator expr2I = list.begin();
                for (int expr2No = 0, size = list.size() - 1; expr2No < size; ++expr2No, ++expr1I)
                    result.push_back(str(concat %(*expr1I) %(*expr2I)));

                *expr1I = str(concat %(*expr1I) %(*expr2I));
            }
        }

        return result;
    }

    void
    ClaspLayer::setCFAData(CFAGraph &&graph) {
    	cfagraph = graph;
    }

    void
    ClaspLayer::addDFAData(DFAGraph &&graph)
    {
        dfaData = 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;

        boost::format formatDfaConnection("dfa_connection(%1%, %2%, %3%).");
        boost::format format2Args("(%1%, %2%)");
        for (i1= dfaData.__edges.begin(), i2 = dfaData.__data.begin(); i1!= dfaData.__edges.end(); ++i1, ++i2 )
        {
            string edgeName;
            switch (*i2)
            {
                case DFGConnection::OPT: edgeName = "opt"; break;
                case DFGConnection::ALIAS: edgeName = "alias"; break;
                case DFGConnection::PROTO: edgeName = "proto"; break;
            }

            cout << formatDfaConnection
                    %(format2Args %(i1->first.identifier)  %(i1->first.scope)).str()
                    %(format2Args %(i1->second.identifier) %(i1->second.scope)).str()
                    %edgeName
                    << " %" <<getHintForPackedSymbol(i1->first) << " - " << getHintForPackedSymbol(i1->second)
					<<endl;

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

        boost::format formatBind("bind(%1%, %2%).");
        for (const pair<SymbolPacked, Expression>& tag:  dfaData.__tags)
        {
            for (string variant: compile(tag.second)) {
                cout << (formatBind
                    % (format2Args %(tag.first.identifier) %(tag.first.scope))
                    % (variant))
					<< "%" << getHintForPackedSymbol(tag.first)
                    << endl;
            }

            symbols.insert(tag.first);
        }

        for (const SymbolPacked& s: symbols)
        {
            cout << "v("  << format2Args % (s.identifier) % (s.scope) << ")."
            		<< " %" << getHintForPackedSymbol(s)
            		<<endl;
        }
    }

    void
    ClaspLayer::involveCFAData() {
        ostream &cout = __partTags;
		const std::string& atomBinding = Config::get("clasp.bindings.function");
		const std::string& atomBindingScope = Config::get("clasp.bindings.scope");

        	//show function tags
    	int counterTags = 0;

        boost::format formatFunction("function(%1%).");
        boost::format formatBind(atomBinding + "(%1%, %2%).");
        for (auto function: cfagraph.__nodesFunction.left) {
            cout << formatFunction % (function.second) << std::endl;


        	for (const auto& tag_: boost::make_iterator_range(cfagraph.__functionTags.equal_range(function.first))){
        		const Tag& tag = tag_.second;

                list<string> tagRaw = compile(tag.first);
				assert(tagRaw.size() == 1);

                cout << formatBind
                        % (function.second)
                        % (tagRaw.front())
                    << endl;
				++counterTags;
        	}
        }

        if (counterTags == 0) {
            cout << "%no tags at all" << endl;
        }

        	//declare scopes
        boost::format formatScope("scope(%1%).");
        for (auto scope: __indexScopes) {
        	//std::string function = scope.first.
            cout << formatScope % scope.second << std::endl;
        }

        //show context rules:
        for (auto rule: cfagraph.__contextRules) {
        	cout << ContextRule(rule.second).compile(rule.first) << std::endl;
        };

        	//show scope tags:
		counterTags = 0;
        boost::format formatScopeBind(atomBindingScope + "(%1%, %2%).");
		for (auto entry: cfagraph.__scopeTags) {
			ScopePacked scopeId = entry.first;
			const Expression& tag = entry.second;
            list<string> tagRaw = compile(tag);
			assert(tagRaw.size() == 1);

            cout << formatScopeBind % scopeId %(tagRaw.front()) << endl;
			++counterTags;
		}

		if (counterTags == 0) {
			cout << "%scope tags: no tags at all" << endl;
		}

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

			//parent connections
			//TEST CFG parent function
		boost::format formatFunctionParent("cfa_parent(%1%, function(%2%)).");
		for (const auto &relation: cfagraph.__parentFunctionRelations) {
			const string& function = cfagraph.__nodesFunction.left.at(relation.second);

			cout << formatFunctionParent % relation.first % function << endl;
		}

			//TEST CFG parent scope
		boost::format formatScopeParent("cfa_parent(%1%, scope(%2%)).");
		for (const auto &relation: cfagraph.__parentScopeRelations) {
			cout << formatScopeParent % relation.first % relation.second << endl;
		}

			//call connections
		boost::format formatCall("cfa_call(%1%, %2%).");

		for (const auto &relation: cfagraph.__callRelations) {
			const ScopePacked scopeFrom = relation.first;
			const string& functionTo = cfagraph.__nodesFunction.left.at(relation.second);

            cout << formatCall % (scopeFrom) % (functionTo) << endl;
		}
    }

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

        list<string> domains;
        boost::format formatDef("%1%(%2%)");
        std::transform(rule.__args.begin(), rule.__args.end(), std::inserter(domains, domains.begin()),
                [&formatDef](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 boost::str(formatDef % domain % argument.first);
                });

        list<string> 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();
                });

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

        const list<string>& guards = multiplyLists(std::move(guardsRaw));
        list<string> &&branches = compileNeg(rule.__condition);

        boost::format formatWarning("warning(%1%, (%2%)):- %3%, %4%, %5%.");
        for (const string &guardsJoined: guards)
            for (const string &branch: branches) {
                unsigned int hook = registerWarning(string(rule.__message));

                __partGeneral  <<  formatWarning
                        %(hook)
                        %(boost::algorithm::join(vars, ", "))
                        %(branch)
                        %(guardsJoined)
                        %(boost::algorithm::join(domains, ", "))
                    <<endl;
            }
    }

    std::list<std::string>
    ClaspLayer::compile(const Expression &e){
        list<string> result;

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

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

                list<string> &&operands_ = multiplyLists(std::move(operands));
                result.push_back(boost::str(boost::format("%1%(%2%)") % (e.__valueS) % (boost::algorithm::join(operands_, ", "))));
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                list<string> &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.push_back((boost::format("not %1%")%(rawOp.front())).str());
                break;
            };

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

                    case Expression::NUMBER:
                        result.push_back(to_string(e.__valueD));
                        break;

                    default:
                        assert(true);
                }
                break;
            }

            default: break;
        }

//TODO Null ad hoc ClaspLayer implementation
//        if (e.isNone()){
//             result.push_back(e.__valueS);
//        }

        assert(result.size());
        return result;
    }

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

                boost::format formatNeg("%1%, not %2%");
                for (const auto &op1: operands1)
                    for (const auto &op2: operands2) {
                        result.push_back(boost::str(formatNeg %(op1) % (op2)));
                    }
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                list<string> &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.push_back(rawOp.front());
                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::involveImports()    {
        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::addRawScript(std::string&& script){
    	__partGeneral << script;
    }

    void
    ClaspLayer::run() {
        involveImports();
        involveCFAData();

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

        std::vector<char const *> args{"clingo", nullptr};
        DefaultGringoModule moduleDefault;
        Gringo::Scripts scriptsDefault(moduleDefault);
        ClingoLib ctl(scriptsDefault, 0, args.data());

        ctl.add("base", {}, program.str());
        ctl.ground({{"base", {}}}, nullptr);

//          solve
        Gringo::SolveResult result = ctl.solve([this](Gringo::Model const &model) {
            this->onModel(model);
            return true;
        }, {});

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

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

    ClaspLayer::ClaspLayer() {
    }

    ClaspLayer::ModelFragment
    ClaspLayer::query(const std::string& atom)
    {
        if (! __model.count(atom)){
            return boost::none;
        }

        return ModelFragment(__model.equal_range(atom));
    }

    ScopePacked
	ClaspLayer::pack(CodeScope* scope) {
    	auto pos = __indexScopes.emplace(scope, __indexScopes.size());
        if (pos.second)
        	__registryScopes.push_back(scope);

        return pos.first->second;
    }

    SymbolPacked
	ClaspLayer::pack(const Symbol& symbol, std::string hintSymbolName)
    {
        SymbolPacked result;

        result.scope = pack(symbol.scope);
        result.identifier = symbol.identifier;
        __indexSymbolNameHints.emplace(result, hintSymbolName);

        return result;
    }

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

    std::string
	ClaspLayer::getHintForPackedSymbol(const SymbolPacked& symbol){
    	auto result = __indexSymbolNameHints.find(symbol);
    	return (result == __indexSymbolNameHints.end())? "" : result->second;
    }

/*
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;
}

*/
/*****************************************
 *                      CFAGraph
 *****************************************
 */
    void
    CFAGraph::addFunctionAnnotations(const std::string& function, const std::vector<Tag>&tags) {
        unsigned int fid = registerNodeFunction(function);

        for (Tag tag: tags){
        	__functionTags.emplace(fid, tag);
        }
    }

    void
	CFAGraph::addScopeAnnotations(const ScopePacked& scope, const std::vector<Expression>& tags){
    	for (Expression tag: tags){
    		__scopeTags.emplace(scope, tag);
    	}
    }

    void
	CFAGraph::addContextRules(const ScopePacked& scope, const std::vector<Expression>& rules){
    	for (Expression rule: rules){
    		__contextRules.emplace(scope, rule);
    	}
    }

    void
	CFAGraph::addCallConnection(const ScopePacked& scopeFrom, const std::string& functionTo) {
        unsigned int idFuncTo = registerNodeFunction(functionTo);

        __callRelations.emplace(scopeFrom, idFuncTo);
    }

    void
	CFAGraph::addParentConnection(const ScopePacked& scope, const std::string& functionParent){
    	__parentFunctionRelations.emplace(scope, registerNodeFunction(functionParent));
    }

    void
	CFAGraph::addParentConnection(const ScopePacked& scope, const ScopePacked& scopeParent){
    	__parentScopeRelations.emplace(scope, scopeParent);
    }

    unsigned int
	CFAGraph::registerNodeFunction(const std::string& fname){
    	auto pos = __nodesFunction.left.insert(make_pair(__nodesFunction.size(), fname));

        return pos.first->first;
    }



/*****************************************
 *                      DFAGraph
 *****************************************
 */

    class VisitorAddTag: public boost::static_visitor<>  {
    public:
        void operator()(const SymbolPacked& symbol){
            __graph->__tags.emplace(symbol, move(__tag));
        }

        void operator()(SymbolTransient& symbol){
            symbol.tags.push_back(move(__tag));
        }

        void operator()(const SymbolInvalid& symbol){
            assert(false && "Undefined behaviour");
        }

        VisitorAddTag(DFAGraph* const dfagraph, Expression&& tag):
            __graph(dfagraph), __tag(tag) {}

    private:
        DFAGraph* const __graph;
        Expression __tag;
    };

    class VisitorAddLink: public boost::static_visitor<>  {
    public:
        void operator()(const SymbolPacked& nodeFrom){
            if (!__graph->isConnected(__nodeTo, nodeFrom))
            {
                __graph->__edges.emplace_back(__nodeTo, nodeFrom);
                __graph->__data.push_back(__link);

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

        void operator()(const SymbolTransient& symbolFrom){
            if (__link != DFGConnection::ALIAS){
                assert(false && "Undefined behaviour");
            }

            for (const Expression& tag: symbolFrom.tags){
                __graph->__tags.emplace(__nodeTo, tag);
            }
        }

        void operator()(const SymbolInvalid&){
            if (__link == DFGConnection::ALIAS) return;
            if (__link == DFGConnection::OPT) return;

            assert(false && "Undefined behaviour");
        }

        VisitorAddLink(DFAGraph* const dfagraph, const SymbolPacked& nodeTo, DFGConnection link):
            __graph(dfagraph), __nodeTo(nodeTo), __link(link) {}

    private:
        DFAGraph* const __graph;
        SymbolPacked __nodeTo;
        DFGConnection __link;
    };

    bool
    DFAGraph::isConnected(const SymbolPacked& identifierTo, const SymbolPacked& identifierFrom)
    {
        auto range = __outEdges.equal_range(identifierFrom);

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

        return false;
    }

    void
    DFAGraph::addConnection(const SymbolPacked& nodeTo, const SymbolNode& nodeFrom, DFGConnection link) {
        VisitorAddLink visitor(this, nodeTo, link);
        boost::apply_visitor(visitor, nodeFrom);
    }

    void
    DFAGraph::addAnnotation(SymbolNode& node, Expression&& tag) {
        VisitorAddTag visitor(this, move(tag));
        boost::apply_visitor(visitor, node);
    }

    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);
    }

    IQuery*
	ClaspLayer::registerQuery(IQuery *query, const QueryId& id) {
        return __queries.emplace(id, query).first->second;
    }

    IQuery*
	ClaspLayer::getQuery(const QueryId& id){
    	assert(__queries.count(id) && "Undefined query");
    	return __queries.at(id);
    }
}