/* 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/utils.h"
#include "utils.h"

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

using namespace std;

//TODO escape identifiers started with upper case symbol

namespace xreate {
    bool operator==(const SymbolAnonymous& s1, const SymbolAnonymous& s2){
        return s1.id == s2.id && s1.flagIsUsed == s2.flagIsUsed;
    }

    struct VisitorSymbolNodeHash : public boost::static_visitor<size_t> {
        std::size_t operator()(const xreate::SymbolPacked& node) const noexcept{
            return 2* (node.identifier +  3 * node.scope + 5 * std::abs(node.version));
        }

        std::size_t operator()(const xreate::SymbolAnonymous& node) const noexcept{
            return 7 * node.id;
        }
    };
}

namespace std {
    std::size_t
    hash<xreate::SymbolNode>::operator()(xreate::SymbolNode const& s) const noexcept {
        return boost::apply_visitor(xreate::VisitorSymbolNodeHash(), s);
    }

    std::size_t
    hash<xreate::SymbolGeneralized>::operator()(xreate::SymbolGeneralized const& s) const noexcept {
        return xreate::AttachmentsId<xreate::SymbolGeneralized>::getId(s);
    }
}

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

    auto warningsModel = query(warningTag);

    if(warningsModel.size())
    for (auto warning: warningsModel) {
        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) {
    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");
    const string& atomLateStatement = "late";

    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 atomAlias = std::get<1>(parse<Gringo::Symbol, Gringo::Symbol>(atom)).name().c_str();
            __model.addStaticAtom(atomAlias, atom);

        } else if(atomName == atomLateStatement){
            //late atom format: (Symbol, (tuple of keys), (tuple of values), late-annotation)
            auto atomLate = parse<SymbolPacked, std::list<SymbolPacked>, std::list<Expression>, Gringo::Symbol>(atom);
            const string& atomAlias = get<3>(atomLate).name().c_str();
            __model.addLateAtom(atomAlias, get<0>(atomLate),
                                get<3>(atomLate), get<1>(atomLate),
                                get<2>(atomLate));
        }

        __model.addStaticAtom(atomName, 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;

    if(ast)
    for (string fn: ast->__rawImports)
    {
        std::ifstream file(fn);
        if (!file){
            std::cout << "Can't process script file: " << fn << std::endl;
            assert(false);
        }

        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(): __model(this), ast(nullptr){
}

const ReasoningModel&
ClaspLayer::queryCompiled() {
    return __model;
}

StaticModel
ClaspLayer::query(const std::string& atom){
    return __model.queryStatic(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;
}

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

class VisitorUnpackSymbol: public boost::static_visitor<SymbolGeneralized> {
public:
    VisitorUnpackSymbol(ClaspLayer* clasp): __clasp(clasp) {}

    SymbolGeneralized operator()(const SymbolPacked& symbol) const {
        return __clasp->unpack(symbol);
    }

    SymbolGeneralized operator()(const SymbolAnonymous& symbol) const {
        return symbol;
    }

private:
    ClaspLayer* __clasp;
};

class VisitorPackSymbol: public boost::static_visitor<SymbolNode> {
public:
    VisitorPackSymbol(ClaspLayer* clasp, const std::string& hintSymbolName)
        : __clasp(clasp), __hint(hintSymbolName) {}

    SymbolNode operator()(const Symbol& symbol) const {
        return __clasp->pack(symbol, __hint);
    }

    SymbolNode operator()(const SymbolAnonymous& symbol) const {
        return symbol;
    }

private:
    ClaspLayer* __clasp;
    std::string __hint;
};

SymbolNode ClaspLayer::pack(const SymbolGeneralized& symbol, const std::string& hintSymbolName){
    return boost::apply_visitor(VisitorPackSymbol(this, hintSymbolName), symbol);
}

SymbolGeneralized ClaspLayer::unpack(const SymbolNode& symbol)
{
    return boost::apply_visitor(VisitorUnpackSymbol(this), symbol);
}

boost::optional<Gringo::Symbol>
GuardedAnnotation::get(const std::list<Expression>& keys) const{
    for (const auto& entry: guardedSymbols){
        const std::list<Expression>& keysExpected = entry.first;

        auto keysIt = keys.begin();
        bool result = true;
        for(const Expression& keyExpected: keysExpected){
            if(! (keyExpected == *keysIt)) {result = false; break; }
            ++keysIt;
        }
        if(!result) continue;
        return entry.second;
    }

    return boost::none;
}

std::list<Expression>
ReasoningModel::findKeys(const std::list<SymbolPacked>& keys) const{
    std::list<Expression> result;
    std::transform(keys.begin(), keys.end(), std::inserter(result, result.end()), [this](const SymbolPacked& key){
       return Attachments::get<LateBinding>(this->clasp->unpack(key));
    });

    return result;
}

void ReasoningModel::addStaticAtom(const std::string& atomAlias, const Gringo::Symbol& atom){
    modelStatic.emplace(atomAlias, atom);
}

void ReasoningModel::addLateAtom(const std::string& alias, const SymbolNode& symbol,
                                 const Gringo::Symbol& atom,   const std::list<SymbolPacked>& guardKeys,
                                 const std::list<Expression>& guardBindings){
    LateModel& model = modelGuarded[alias];
    if(!model.bindings.count(symbol)){
        model.bindings.emplace(symbol, guardKeys);
    }

    GuardedAnnotation& annotation = model.annotations[symbol];
    annotation.guardedSymbols.push_back(make_pair(guardBindings, atom));
}

StaticModel
ReasoningModel::queryStatic(const std::string& alias) const{
    StaticModel result;

    if (! modelStatic.count(alias)){
        return result;
    }

    auto currentDataRange = modelStatic.equal_range(alias);
    std::copy(currentDataRange.first, currentDataRange.second, std::inserter(result, result.end()));
    return result;
}

StaticModel
ReasoningModel::queryLate(const std::string& alias, const SymbolNode& symbol) const{
    StaticModel result;
    if (!modelGuarded.count(alias)) return StaticModel();

    const LateModel& model = modelGuarded.at(alias);
    assert(model.bindings.count(symbol));
    const list<SymbolPacked>& bindings = model.bindings.at(symbol);
    list<Expression>&& keys = findKeys(bindings);

    const GuardedAnnotation& annGuarded = model.annotations.at(symbol);
    auto ann = annGuarded.get(keys);
    if(ann){
        result.emplace(make_pair(alias, *ann));
    }

    return result;
}

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

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<int, int, 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;
}

SymbolNode
ParseImplAtom<SymbolNode>::get(const Gringo::Symbol& atom) {
    assert(atom.type() == Gringo::SymbolType::Fun
        && "Inappropriate symbol type");

    if (atom.name() == "a"){
        return SymbolAnonymous{(unsigned int) std::get<0>(ClaspLayer::parse<int>(atom))};

    } else if (atom.name() == "s"){
        return ParseImplAtom<SymbolPacked>::get(atom);
    }

    assert(false && "Wrong symbol format");
}

class VisitorSymbolId: public boost::static_visitor<unsigned int> {
public:
    unsigned int operator()(const Symbol& symbol) const {
        return AttachmentsId<Symbol>::getId(symbol);
    }

    unsigned int operator()(const SymbolAnonymous& symbol) const {
        return symbol.id;
    }
};

unsigned int
AttachmentsId<SymbolGeneralized>::getId(const SymbolGeneralized& symbol){
    return boost::apply_visitor(VisitorSymbolId(), symbol);
}

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