/* This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/.
 *
 * Author: pgess <v.melnychenko@xreate.org>
 * File: clasplayer.cpp
 */

/**
 * \file    clasplayer.h
 * \brief   Resoner. Wrapper over Clasp reasoner library
 */

#include "clasplayer.h"
#include "analysis/aux.h"
#include "utils.h"

#include <gringo/scripts.hh>
#include <boost/format.hpp>
#include <boost/algorithm/string/join.hpp>
#include <iostream>

using namespace std;

//TODO escape identifiers started with upper case symbol
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::Symbol params;
        std::tie(warningId, params) = parse<unsigned int, Gringo::Symbol>(warning->second);

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

bool
ClaspLayer::handleSolution(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::Symbol atom : model.atoms(clingo_show_type_atoms)) {
        atom.print(cout);
        cout <<" | "<< endl;

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

        __model.emplace(atomName, move(atom));
    }

    return true;
}

void
ClaspLayer::registerReport(IAnalysisReport* report){
    __reports.push_back(report);
}

void
ClaspLayer::runReports(){
    for(IAnalysisReport* report: __reports){
        report->print(__partGeneral);
        delete report;
    }

    __reports.clear();
}

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 xreate::analysis::compile(guard);
            });

    const list<string>& guards = xreate::analysis::multiplyLists(std::move(guardsRaw));
    list<string> &&branches = xreate::analysis::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;
        }
}



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();
    runReports();

    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(), {}, 0);

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

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

    if (result.satisfiable() == Gringo::SolveResult::Satisfiable) {
        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(const CodeScope* const scope) {
    auto pos = __indexScopes.emplace(scope, __indexScopes.size());
    if (pos.second)
        __registryScopes.push_back(scope);

    return pos.first->second;
}

size_t
ClaspLayer::getScopesCount() const{
    return __registryScopes.size();
}

SymbolPacked
ClaspLayer::pack(const Symbol& symbol, std::string hintSymbolName)
{
    SymbolPacked result(symbol.identifier.id, symbol.identifier.version, pack(symbol.scope));
    __indexSymbolNameHints.emplace(result, hintSymbolName);

    return result;
}

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

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

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

Expression
ParseImplAtom<Expression>::get(const Gringo::Symbol& atom) {
    switch (atom.type()) {
        case Gringo::SymbolType::Num: return Expression(atom.num());
        case Gringo::SymbolType::Str: return Expression(Atom<String_t>(std::string(atom.string().c_str())));

        case Gringo::SymbolType::Fun:
        {
            //FUNC
            Expression result(Operator::CALL,{Expression(Atom<Identifier_t>(std::string(atom.name().c_str())))});
            for (const Gringo::Symbol& arg : atom.args()) {
                result.addArg(ParseImplAtom<Expression>::get(arg));
            }

            return result;
        }

        default:
        {
            assert(false);
        }
    }
}

int
ParseImplAtom<int>::get(const Gringo::Symbol& atom) {
    switch (atom.type()){
        case Gringo::SymbolType::Num: return atom.num();
        default: break;
    }

    assert(false && "Inappropriate symbol type");
}

std::string
ParseImplAtom<std::string>::get(const Gringo::Symbol& atom) {
    switch (atom.type()) {
        case Gringo::SymbolType::Str: return atom.string().c_str();
        case Gringo::SymbolType::Fun: return atom.name().c_str();

        default: break;
    }

    assert(false && "Inappropriate symbol type");
}

SymbolPacked
ParseImplAtom<SymbolPacked>::get(const Gringo::Symbol& atom) {
    auto result = ClaspLayer::parse<unsigned int, unsigned int, unsigned int>(atom);
    return SymbolPacked(std::get<0>(result), std::get<1>(result), std::get<2>(result));
};

Gringo::Symbol
ParseImplAtom<Gringo::Symbol>::get(const Gringo::Symbol& atom) {
    return atom;
}

std::list<Gringo::Symbol>
ParseImplAtom<std::list<Gringo::Symbol>>::get(const Gringo::Symbol& atom){
    assert (atom.type() == Gringo::SymbolType::Fun);
    std::list<Gringo::Symbol> result;

    for (const Gringo::Symbol& arg: atom.args()) {
        result.push_back(ParseImplAtom<Gringo::Symbol>::get(arg));
    }

    return result;
}

} //end of xreate namespace

/**
 * \class xreate::ClaspLayer
 * \brief Reasoning and logic Solver.
 *
 * Wraps external brilliant fantastic tool [Clasp solver](https://potassco.org/clasp/)
 *
 * For building *logic program* for reasoning ClaspLayer takes input from:
 *  - Raw scripts. Client could append arbitrary ASP script to _logic program_. \ref addRawScript()
 *  - Includes. There is possibility to specify external files with ASP scripts
 *    to append to _logic program_. \ref involveImports() (private member)
 *  - Diagnostic rules. Rules that produce diagnostic messages during
 *    compilation(warnings) or even able to halt compilation with errors.
 *    addRuleWarning(), \ref registerWarning()
 *  - DFA data. \ref setDFAData()
 *  - CFA data. \ref setCFAData()
 *  - Dominators Analysis. See xreate::dominators::DominatorsTreeAnalysisProvider.
 *    Executed by \ref run()
 *  - Context rules. See xreate::ContextRule and general [Context Explanation](/w/concepts/context)
 *
 * Data sources implement xreate::IAnalysisReport. Generally, input could be loosely divided into three categories:
 *  - *Internally derived* data. CFA, DFA, Dominators analyses *automatically* feed reasoner by
 *     useful  insights about data, structure and algorithms of a program
 *  - *User provided* data. CFA, DFA, Diagnostic/Context rules feed reasoner by
 *      annotations Developer specifically  provides manually
 *  - *External* data. Raw scripts and includes feed reasoner with third-party data
 *    related to a different aspects of a program possibly produced by external analyzers
 *
 * Once ClaspLayer got input from all providers and logic program is fully constructed
 * it runs external Clasp solver and receives back desired solutions.
 *
 * Output of Clasp reasoner is recognized and accessed via *queries*.
 * IQuery represents an interface between reasoner's output and rest of Xreate.
 * Each query inherits xreate::IQuery interface. Currently there are queries as follows:
 *  - xreate::containers::Query to catch solutions regarding Containers implementation. See [Containers Explanation](/w/concepts/containers)
 *  - xreate::context::ContextQuery to catch solution regarding Context. See [Context Explanation](/w/concepts/context)
 *
 * \sa See xreate::dfa::DFAPass, xreate::cfa::CFAPass, xreate::IQuery, xreate::IAnalysisReport, xreate::dominators::DominatorsTreeAnalysisProvider
 */