<commit_before>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/

#include "frontends/lean/parser.h"
#include "library/module.h"
#include "shell/server.h"
#include <list>

namespace lean {

class null_message_stream : public message_stream {
public:
    void report(message const &) override {}
};

server::server(unsigned num_threads, environment const & initial_env, io_state const & ios) :
        m_num_threads(num_threads), m_initial_env(initial_env), m_ios(ios) {
    m_ios.set_regular_channel(std::make_shared<stderr_channel>());
    m_ios.set_diagnostic_channel(std::make_shared<stderr_channel>());
    m_ios.set_message_channel(std::make_shared<null_message_stream>());
}

server::~server() {
}

void server::run() {
    scope_global_ios scoped_ios(m_ios);

    while (true) {
        try {
            std::string req_string;
            std::getline(std::cin, req_string);
            if (std::cin.eof()) return;

            json req = json::parse(req_string);

            json res = handle_request(req);
            std::cout << res << std::endl;
        } catch (std::exception & ex) {
            json res;
            res["response"] = "error";
            res["message"] = ex.what();
            std::cout << res << std::endl;
        }
    }
}

json server::handle_request(json const & req) {
    std::string command = req["command"];

    if (command == "sync") {
        return handle_sync(req);
    } else if (command == "check") {
        return handle_check(req);
    }

    json res;
    res["response"] = "error";
    res["message"] = "unknown command";
    return res;
}

static optional<pos_info> diff(std::string a, std::string b) {
    std::istringstream in_a(a), in_b(b);
    for (unsigned line = 1;; line++) {
        if (in_a.eof() && in_b.eof()) return optional<pos_info>();
        if (in_a.eof() || in_b.eof()) return optional<pos_info>(line, 0);

        std::string line_a, line_b;
        std::getline(in_a, line_a);
        std::getline(in_b, line_b);
        // TODO(gabriel): return column as well
        if (line_a != line_b) return optional<pos_info>(line, 0);
    }
}

json server::handle_sync(json const & req) {
    std::string new_file_name = req["file_name"];
    std::string new_content = req["content"];

    json res;
    res["response"] = "ok";

    if (m_file_name != new_file_name) {
        m_file_name = new_file_name;
        m_content = new_content;
        m_only_checked_until = optional<pos_info>(-1, 0);
        res["message"] = "new file name, reloading";
    } else {
        if (auto diff_pos = diff(m_content, new_content)) {
            m_content = new_content;
            // TODO(gabriel): implement min on pos_info
            if (m_only_checked_until && m_only_checked_until->first < diff_pos->first) {
                // we have not yet checked up to the differing position
            } else {
                m_only_checked_until = diff_pos;
            }
            res["message"] = "file partially invalidated";
        } else {
            res["message"] = "no file changes";
        }
    }
    return res;
}

json server::handle_check(json const &) {
    if (imports_have_changed(m_checked_env))
        m_only_checked_until = optional<pos_info>(-1, 0);

    if (m_only_checked_until) {
        snapshot_vector new_snapshots;
        for (snapshot const & snap : m_snapshots) {
            if (snap.m_pos.first < m_only_checked_until->first) {
                new_snapshots.push_back(snap);<commit_msg>fix(shell/server): remove static integer underflow<commit_after>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/

#include "frontends/lean/parser.h"
#include "library/module.h"
#include "shell/server.h"
#include <list>

namespace lean {

class null_message_stream : public message_stream {
public:
    void report(message const &) override {}
};

server::server(unsigned num_threads, environment const & initial_env, io_state const & ios) :
        m_num_threads(num_threads), m_initial_env(initial_env), m_ios(ios) {
    m_ios.set_regular_channel(std::make_shared<stderr_channel>());
    m_ios.set_diagnostic_channel(std::make_shared<stderr_channel>());
    m_ios.set_message_channel(std::make_shared<null_message_stream>());
}

server::~server() {
}

void server::run() {
    scope_global_ios scoped_ios(m_ios);

    while (true) {
        try {
            std::string req_string;
            std::getline(std::cin, req_string);
            if (std::cin.eof()) return;

            json req = json::parse(req_string);

            json res = handle_request(req);
            std::cout << res << std::endl;
        } catch (std::exception & ex) {
            json res;
            res["response"] = "error";
            res["message"] = ex.what();
            std::cout << res << std::endl;
        }
    }
}

json server::handle_request(json const & req) {
    std::string command = req["command"];

    if (command == "sync") {
        return handle_sync(req);
    } else if (command == "check") {
        return handle_check(req);
    }

    json res;
    res["response"] = "error";
    res["message"] = "unknown command";
    return res;
}

static optional<pos_info> diff(std::string a, std::string b) {
    std::istringstream in_a(a), in_b(b);
    for (unsigned line = 1;; line++) {
        if (in_a.eof() && in_b.eof()) return optional<pos_info>();
        if (in_a.eof() || in_b.eof()) return optional<pos_info>(line, 0);

        std::string line_a, line_b;
        std::getline(in_a, line_a);
        std::getline(in_b, line_b);
        // TODO(gabriel): return column as well
        if (line_a != line_b) return optional<pos_info>(line, 0);
    }
}

json server::handle_sync(json const & req) {
    std::string new_file_name = req["file_name"];
    std::string new_content = req["content"];

    json res;
    res["response"] = "ok";

    if (m_file_name != new_file_name) {
        m_file_name = new_file_name;
        m_content = new_content;
        m_only_checked_until = optional<pos_info>(0, 0);
        res["message"] = "new file name, reloading";
    } else {
        if (auto diff_pos = diff(m_content, new_content)) {
            m_content = new_content;
            // TODO(gabriel): implement min on pos_info
            if (m_only_checked_until && m_only_checked_until->first < diff_pos->first) {
                // we have not yet checked up to the differing position
            } else {
                m_only_checked_until = diff_pos;
            }
            res["message"] = "file partially invalidated";
        } else {
            res["message"] = "no file changes";
        }
    }
    return res;
}

json server::handle_check(json const &) {
    if (imports_have_changed(m_checked_env))
        m_only_checked_until = optional<pos_info>(0, 0);

    if (m_only_checked_until) {
        snapshot_vector new_snapshots;
        for (snapshot const & snap : m_snapshots) {
            if (snap.m_pos.first < m_only_checked_until->first) {
                new_snapshots.push_back(snap);
{'fraction_non_alphanumeric': 0.1348314606741573, 'fraction_numerical': 0.003606602857539187, 'mean_word_length': 2.7474012474012475, 'pattern_counts': {'":': 0, '<': 45, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3908474', 'n_tokens_mistral': 2339, 'n_tokens_neox': 2300, 'n_words': 507}