#include <cstdio>
#include <stdlib.h>
#include <sys/stat.h>
#include <unistd.h>
#include <readline/history.h>
#include <readline/readline.h>

#include <iostream>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <fstream>

#include "src/EpicSolverCmd.hpp"
#include "util/json.hpp"
#include "src/TclInterpController.h"
#include "src/EpicApp.h"

using json_t = nlohmann::json;

std::unordered_map<std::string, std::string> EpicSolverCmd::solver_res_map;
std::vector<std::string> EpicSolverCmd::engine_arr;
std::vector<std::string> EpicSolverCmd::script_arr;
std::vector<std::string> EpicSolverCmd::file_arr;
std::string EpicSolverCmd::filelist;
std::vector<std::string> EpicSolverCmd::verilog_file_arr;
std::unordered_map<std::string, std::string> EpicSolverCmd::macro_map;
std::string EpicSolverCmd::m_clock_name;
std::string EpicSolverCmd::m_reset_name;
std::string EpicSolverCmd::m_cycle_reset_num;
std::string EpicSolverCmd::m_cycle_simulate_num;
bool EpicSolverCmd::is_sim_run = false;
bool EpicSolverCmd::m_reset_polarity = false;

DsgInfo *DsgInfo::instance_;

std::unordered_set<std::string> my_command = {"set_mode",   "set_depth", "set_worker", "set_engines", "create_clock",
                                              "create_rst", "sim_run",   "read_file",  "chformal",    "check_fv",
                                              "history",    "help",      "exit",       "quit"};

void printCopyright() {
    std::cout << " /"
                 "-----------------------------------------------------------"
                 "-----------------\\"
              << std::endl;
    std::cout << " |                                                         "
                 "                   |"
              << std::endl;
    std::cout << " |          EpicFV(TM)                                     "
                 "                   |"
              << std::endl;
    // std::cout << " |  Version xxxx -- Tue Aug 4 08:53:19 2020 |" <<
    // std::endl;
    std::cout << " |    Copyright (c) 2020 by XEPIC Co., Ltd.                "
                 "                   |"
              << std::endl;
    std::cout << " |      ALL RIGHTS RESERVED                                "
                 "                   |"
              << std::endl;
    std::cout << " |                                                         "
                 "                   |"
              << std::endl;
    std::cout << " | This program is proprietary and confidential "
                 "information of XEPIC Co., Ltd.|"
              << std::endl;
    std::cout << " | and may be used and disclosed only as authorized in a "
                 "licence agreement    |"
              << std::endl;
    std::cout << " | controlling such use and disclosure.                    "
                 "                   |"
              << std::endl;
    std::cout << " |                                                         "
                 "                   |"
              << std::endl;
    std::cout << " \\--------------------------------------------------------"
                 "--------------------/"
              << std::endl;
}

char *readline_cmd_generator(const char *text, int state) {
    static std::unordered_set<std::string>::iterator it;
    static int len;

    if (!state) {
        it = my_command.begin();
        len = strlen(text);
    }

    for (; it != my_command.end(); it++) {
        if ((*it).compare(0, len, text) == 0) {
            return strdup((*it++).c_str());
        }
    }
    return nullptr;
}

char **readline_completion(const char *text, int start, int end) {
    if (start == 0) {
        return rl_completion_matches(text, readline_cmd_generator);
    }
    return NULL;
}

const char *create_prompt() {
    static char buffer[100];
    std::string str = "\n";
    str += "epicfv_shell";

    snprintf(buffer, 100, "%s> ", str.c_str());
    return buffer;
}

void split(const std::string &s, std::vector<std::string> &tokens, const std::string &delimiters = " ") {
    std::string::size_type lastPos = s.find_first_not_of(delimiters, 0);
    std::string::size_type pos = s.find_first_of(delimiters, lastPos);
    while (std::string::npos != pos || std::string::npos != lastPos) {
        tokens.push_back(s.substr(lastPos, pos - lastPos));
        lastPos = s.find_first_not_of(delimiters, pos);
        pos = s.find_first_of(delimiters, lastPos);
    }
}

void call(const std::string &command) {
    std::vector<std::string> args;
    split(command, args);
    if (args[0] == "history") {
        add_history(command.c_str());
        for (HIST_ENTRY **list = history_list(); *list != NULL; list++)
            std::cout << (*list)->line << std::endl;
    } else if (args[0] == "help") {
        add_history(command.c_str());
        std::cout << std::endl;
        std::cout << "    help                        list all commands" << std::endl;
        std::cout << "    set_mode                    set work mode" << std::endl;
        std::cout << "    set_worker                  set worker process number" << std::endl;
        std::cout << "    set_depth                   set depth(live mode not support)" << std::endl;
        std::cout << "    set_engines                 set engines" << std::endl;
        std::cout << "    create_clock                create clock" << std::endl;
        std::cout << "    create_rst                  set reset signal" << std::endl;
        std::cout << "    sim_run                     set simulate and reset config" << std::endl;
        std::cout << "    chformal                    assert2assume or assume2assert" << std::endl;
        std::cout << "    read_file                   set RTL filelist" << std::endl;
        std::cout << "    check_fv                    run formal verification" << std::endl;
        std::cout << "    history                     show command history" << std::endl;
        std::cout << "    exit                        exit EpicFV" << std::endl;
        std::cout << "    quit                        exit EpicFV" << std::endl;
    } else if (my_command.count(args[0]) > 0) {
        add_history(command.c_str());
        TclInterpController::executeCommand(command);
    } else {
        std::cerr << "ERROR: No such command: " << args[0] << std::endl;
    }
}

int main(int argc, char **argv) {
    try {
        printCopyright();
        std::string epicfv_home = getenv("EPICFV_HOME");
        if (epicfv_home.empty()) {
            throw "ERROR: cannot find env EPICFV_HOME!";
        }
        std::string tools_dir = epicfv_home + "/binary";
        std::string yosys = tools_dir + "/bin/yosys";
        std::string abc = tools_dir + "/bin/yosys-abc";
        std::string smtbmc = tools_dir + "/bin/yosys-smtbmc";
        std::string avy = tools_dir + "/bin/avy";
        std::string btormc = tools_dir + "/bin/btormc";
        std::string btorsim = tools_dir + "/bin/btorsim";

        setenv("TOOLS_DIR", tools_dir.c_str(), 1);
        setenv("YOSYS", yosys.c_str(), 1);
        setenv("ABC", abc.c_str(), 1);
        setenv("SMTBMC", smtbmc.c_str(), 1);
        setenv("AVY", avy.c_str(), 1);
        setenv("BTORMC", btormc.c_str(), 1);
        setenv("BTORSIM", btorsim.c_str(), 1);

        std::string mpirun = tools_dir + "/share/openmpi/bin/orterun";  //"mpirun";

        if (argc < 3) {
            //    throw "ERROR: missing Tclfile";

            EpicApp::getInstance();

            rl_readline_name = (char *)"epicfv_shell";
            rl_attempted_completion_function = readline_completion;
            rl_basic_word_break_characters = (char *)" \t\n";

            char *command = NULL;
            while ((command = readline(create_prompt())) != NULL) {
                if (command[strspn(command, " \t\r\n")] == 0)
                    continue;

                char *p = command + strspn(command, " \t\r\n");
                call(command);
                if (!strncmp(p, "exit", 4) || !strncmp(p, "quit", 4)) {
                    TclInterpController::shutdown();

                    p += 4;
                    p += strspn(p, " \t\r\n");
                    if (*p == 0) {
                        break;
                    }
                }
            }
            if (command == NULL)
                printf("exit\n");

        } else {
            std::string process_num = argv[1];

            int pn = std::stoi(process_num) + 1;

            std::string tclfile = argv[2];

            struct stat fileStat;
            if ((stat(tclfile.c_str(), &fileStat) != 0) || !S_ISREG(fileStat.st_mode)) {
                throw "ERROR: cannot find tclfile";
            }

            EpicSolverCmd solver_cmd;
            solver_cmd.call(tclfile);

            std::unordered_map<std::string, std::string> res_map = solver_cmd.get_solver_res_map();
            std::vector<std::string> engine_arr = solver_cmd.get_engines();
            std::vector<std::string> script_arr = solver_cmd.get_scripts();
            std::vector<std::string> file_arr = solver_cmd.get_files();
            const std::string filelist = solver_cmd.get_filelist();
            std::unordered_map<std::string, std::string> marco_map = solver_cmd.get_macro_map();
            std::vector<std::string> verilog_file_arr = solver_cmd.get_verl_files();
            bool is_sim_run = solver_cmd.get_sim_run();
            std::string clock_name;
            std::string reset_name;
            std::string cycle_reset_num;
            std::string cycle_simulate_num;
            bool reset_polarity = true;
            solver_cmd.get_sim_param(clock_name, reset_name, cycle_reset_num, cycle_simulate_num, reset_polarity);

            json_t j;
            j["res_map"] = res_map;
            j["engine_arr"] = engine_arr;
            j["script_arr"] = script_arr;
            j["file_arr"] = file_arr;
            j["filelist"] = filelist;
            j["marco_map"] = marco_map;
            j["verilog_file_arr"] = verilog_file_arr;
            j["is_sim_run"] = is_sim_run;
            j["clock_name"] = clock_name;
            j["reset_name"] = reset_name;
            j["cycle_reset_num"] = cycle_simulate_num;
            j["cycle_simulate_num"] = cycle_simulate_num;
            j["reset_polarity"] = reset_polarity;

            const std::string json_str = j.dump();

            std::ofstream fout(".tcl.json");
            if (fout) {
                fout << json_str;
                fout.close();
                fout.clear();
            }

            std::string cmdline = mpirun + " --oversubscribe -x LD_LIBRARY_PATH -np " + std::to_string(pn) + " " +
                                  tools_dir + "/epic_fv_bin -f -b " + tclfile;
            system(cmdline.c_str());

            if ((stat(".tcl.json", &fileStat) == 0) && S_ISREG(fileStat.st_mode) && !getenv("EPICFV_INT_DEBUG")) {
                system("rm .tcl.json");
            }
        }

    } catch (const char *msg) {
        std::cerr << msg << std::endl;
    } catch (const std::string &str) {
        std::cerr << str << std::endl;
    }
}