trs-boostfree.cpp

// em++ -std=c++11 -s NO_EXIT_RUNTIME=1 -s ASYNCIFY=1 -s DISABLE_EXCEPTION_CATCHING=0 trs.cpp --bind -o trs.js -O2

#include <algorithm>
#include <vector>
#include <tuple>
#include <functional>
#include <utility>
#include <memory>
#include <map>
#include <cmath>
#include <iostream>
#include <string>
#include <thread>

#ifdef EMSCRIPTEN
#include <emscripten.h>
#include <emscripten/bind.h>
using namespace emscripten;
#endif

template<class TRS>
std::string format_term(const typename TRS::term &t);

template<class ValueType, class Less = std::less<ValueType>>
class term_rewriting_system{
public:
    using type = ValueType;

    template<class Type>
    static bool null(const std::vector<Type> &s){
        return s.empty();
    }

    template<class X, class Y>
    static std::vector<std::pair<X, Y>> zip(const std::vector<X> &xs, const std::vector<Y> &ys){
        std::vector<std::pair<X, Y>> ret;
        auto x = xs.begin();
        auto y = ys.begin();
        while(x != xs.end()){
            ret.push_back(std::make_pair(*x, *y));
            ++x;
            ++y;
        }
        return ret;
    }

    template<class X>
    static bool forall(std::function<bool(const X&)> p, const std::vector<X> &xs){
        bool r = true;
        for(auto &x : xs){
            r = r && p(x);
            if(!r){ break; }
        }
        return r;
    }

    template<class X>
    static bool multi_forall(std::function<bool(const X&, const X&)> p, const std::vector<X> &xs, const std::vector<X> &ys){
        bool r = true;
        auto x = xs.begin(), y = ys.begin();
        while(x != xs.end()){
            r = r && p(*x, *y);
            if(!r){ break; }
            ++x, ++y;
        }
        return r;
    }

    template<class X>
    static bool exists(std::function<bool(const X&)> p, const std::vector<X> &xs){
        bool r = false;
        for(auto &x : xs){
            r = r || p(x);
            if(r){ break; }
        }
        return r;
    }

    template<class X, class Y>
    static std::vector<Y> map(std::function<Y(const X&)> f, const std::vector<X> &xs){
        std::vector<Y> r;
        r.reserve(xs.size());
        for(auto &e : xs){
            r.push_back(f(e));
        }
        return r;
    }

    template<class X, class Y, class Iter>
    static std::vector<Y> map(std::function<Y(const X&)> f, Iter first, Iter last){
        std::vector<Y> r;
        r.reserve(last - first);
        for(; first != last; ++first){
            r.push_back(f(*first));
        }
        return r;
    }

    template<class X>
    static std::vector<X> concat(const std::vector<std::vector<X>> &xs){
        std::vector<X> rs;
        for(auto  &s : xs){
            rs.insert(rs.end(), s.begin(), s.end());
        }
        return rs;
    }

    template<class X>
    static void allapp(std::function<void(const X&)> f, std::function<void(typename std::vector<X>::const_iterator, typename std::vector<X>::const_iterator)> g, const std::vector<X> &xs){
        for(auto iter = xs.begin(); iter != xs.end(); ++iter){
            f(*iter);
            g(iter + 1, xs.end());
        }
    }

    struct vname{
        type str;
        int i = 0;

        bool operator ==(const vname &other) const{
            return str == other.str && i == other.i;
        }
    };

    static vname make_vname(const type &str, int i = 0){
        vname v;
        v.str = str;
        v.i = i;
        return v;
    }

    struct term;

    struct term_list{
        type str;
        std::vector<term> list;

        bool operator ==(const term_list &other) const{
            return str == other.str && list == other.list;
        }
    };

    struct term{
        void *holder = nullptr;
        int which_ = 0;

        vname *&vname_ptr = reinterpret_cast<vname*&>(holder);
        term_list *&term_list_ptr = reinterpret_cast<term_list*&>(holder);

        int which() const{
            return which_;
        }

        enum{
            type_variable = 0,
            type_term_list
        };

        template<class T>
        T &get(){
            return *reinterpret_cast<T*>(holder);
        }

        template<class T>
        const T &get() const{
            return *reinterpret_cast<const T*>(holder);
        }

        term(const vname &v) : holder(reinterpret_cast<void*>(new vname(v))){
            which_ = type_variable;
        }

        term(vname &&v) : holder(reinterpret_cast<void*>(new vname(v))){
            which_ = type_variable;
        }

        term(const term_list &tl) : holder(reinterpret_cast<void*>(new term_list(tl))){
            which_ = type_term_list;
        }

        term(term_list &&tl) : holder(reinterpret_cast<void*>(new term_list(tl))){
            which_ = type_term_list;
        }

        term(){}
        term(const term &other){
            if(!other.holder){
                return;
            }
            which_ = other.which_;

            switch(other.which()){
            case type_variable:
                holder = reinterpret_cast<void*>(new vname(other.template get<vname>()));
                break;

            case type_term_list:
                holder = reinterpret_cast<void*>(new term_list(other.template get<term_list>()));
                break;
            }
        }

        term(term &&other){
            if(!other.holder){
                return;
            }

            holder = other.holder;
            which_ = other.which_;
            other.holder = nullptr;
            other.which_ = 0;
        }

        ~term(){
            switch(which()){
            case type_variable:
                delete reinterpret_cast<vname*>(holder);
                break;

            case type_term_list:
                delete reinterpret_cast<term_list*>(holder);
                break;
            }
        }

        term &operator =(const term &other){
            this->~term();

            if(other.holder){
                switch(other.which()){
                case type_variable:
                    holder = reinterpret_cast<void*>(new vname(other.template get<vname>()));
                    break;

                case type_term_list:
                    holder = reinterpret_cast<void*>(new term_list(other.template get<term_list>()));
                    break;
                }
            }

            which_ = other.which_;

            return *this;
        }

        bool operator ==(const term &other) const{
            if(which() != other.which()){
                return false;
            }else{
                if(!holder && !other.holder){
                    return true;
                }else if(!holder || !other.holder){
                    return false;
                }

                switch(which()){
                case type_variable:
                    return get<vname>() == other.template get<vname>();

                case type_term_list:
                    return get<term_list>() == other.template get<term_list>();
                }
            }
            return false;
        }

        ValueType str() const{
            if(!holder){
                return ValueType();
            }

            switch(which()){
            case type_variable:
                return get<vname>().str();

            case type_term_list:
                return get<term_list>().str();
            }
        }
    };

    using ids = std::vector<std::pair<term, term>>;

    static term make_term_list(const type &str, const std::vector<term> &list){
        return term_list({ str, list });
    }

    static term make_variable(const type &str, int i = 0){
        return make_vname(str, i);
    }

    static term make_constant(const type &str){
        return make_term_list(str, std::vector<term>());
    }

    static term make_function(const type &str, const std::vector<term> &ts){
        return make_term_list(str, ts);
    }

    static term make_variable(const vname &v){
        return v;
    }

    using vname_term = std::pair<vname, term>;
    using subst = std::vector<vname_term>;

    static const vname &get_vname(const vname_term &vt){
        return vt.first;
    }

    static const term &get_term(const vname_term &vt){
        return vt.second;
    }

    static subst add_subst(const subst s, const vname &x, const term &t){
        subst r = { std::make_pair(x, t) };
        r.insert(r.begin(), s.begin(), s.end());
        return r;
    }

    static bool indom(const vname &x, const subst &s){
        std::function<bool(const vname_term&)> f = [&](const vname_term &y){
            return x.str == y.first.str && x.i == y.first.i;
        };
        return exists(f, s);
    }

    static const term &app(const subst &s, const vname &x){
        for(auto &yt : s){
            if(yt.first == x){
                return yt.second;
            }
        }
        throw;
    }

    static term lift(const subst &s, const term &t){
        if(t.which() == term::type_variable){
            const vname &x = t.template get<vname>();
            if(indom(x, s)){
                return app(s, x);
            }else{
                return t;
            }
        }else{
            const term_list &tl = t.template get<term_list>();
            std::function<term(const term&)> f = [&s](const term &a){ return lift(s, a); };
            return make_term_list(tl.str, map(f, tl.list));
        }
    }

    static bool occurs(const vname &x, const term &t){
        if(t.which() == term::type_variable){
            return x == t.template get<vname>();
        }else{
            std::function<bool(const term&)> f = [&x](const term &a){ return occurs(x, a); };
            return exists(f, t.template get<term_list>().list);
        }
    }

    struct unify_exception{};

    static subst solve(typename ids::const_iterator tt_first, typename ids::const_iterator tt_last, const subst &s){
        if(tt_first == tt_last){
            return s;
        }else if(tt_first->first.which() == term::type_variable){
            if(tt_first->second.which() == term::type_variable && tt_first->first.template get<vname>() == tt_first->second.template get<vname>()){
                return solve(tt_first + 1, tt_last, s);
            }else{
                return elim(tt_first->first.template get<vname>(), tt_first->second, tt_first + 1, tt_last, s);
            }
        }else if(tt_first->second.which() == term::type_variable){
            return elim(tt_first->second.template get<vname>(), tt_first->first, tt_first + 1, tt_last, s);
        }else{
            const term_list &ts = tt_first->first.template get<term_list>(), &us = tt_first->second.template get<term_list>();
            if(ts.str == us.str){
                ids ts_us_rest = zip(ts.list, us.list);
                ts_us_rest.insert(ts_us_rest.end(), tt_first + 1, tt_last);
                return solve(ts_us_rest.begin(), ts_us_rest.end(), s);
            }else{
                throw unify_exception();
            }
        }
    }

    static subst elim(const vname &x, const term &t, typename ids::const_iterator rest_first, typename ids::const_iterator rest_last, const subst &s){
        auto xt = [&x, &t](const term &u){
            subst w = { std::make_pair(x, t) };
            return lift(w, u);
        };
        if(occurs(x, t)){
            throw unify_exception();
        }else{
            std::function<std::pair<term, term>(const std::pair<term, term>&)> f = [&xt](const std::pair<term, term> &tt){
                return std::make_pair(xt(tt.first), xt(tt.second));
            };
            ids mapped_rest = map(f, rest_first, rest_last);
            std::function<vname_term(const vname_term&)> g = [&xt](const vname_term &yu){
                return std::make_pair(yu.first, xt(yu.second));
            };
            return solve(mapped_rest.begin(), mapped_rest.end(), add_subst(map(g, s), x, t));
        }
    }

    static subst unify(const std::pair<term, term> &tt){
        ids v = { tt };
        return solve(v.begin(), v.end(), subst());
    }

    static subst matchs(typename ids::const_iterator tt_first, typename ids::const_iterator tt_last, const subst &s){
        if(tt_first == tt_last){
            return s;
        }else{
            const term &t1 = tt_first->first, &t2 = tt_first->second;
            if(t1.which() == term::type_variable){
                const vname &x = t1.template get<vname>();
                const term &t = t2;
                if(indom(x, s)){
                    if(app(s, x) == t){
                        return matchs(tt_first + 1, tt_last, s);
                    }else{ throw unify_exception(); }
                }else{
                    return matchs(tt_first + 1, tt_last, add_subst(s, x, t));
                }
            }else if(t2.which() == term::type_variable){
                throw unify_exception();
            }else{
                const term_list &ts = t1.template get<term_list>(), &us = t2.template get<term_list>();
                if(ts.str == us.str){
                    ids ts_us_rest = zip(ts.list, us.list);
                    ts_us_rest.insert(ts_us_rest.end(), tt_first + 1, tt_last);
                    return matchs(ts_us_rest.begin(), ts_us_rest.end(), s);
                }else{
                    throw unify_exception();
                }
            }
        }
    }

    static subst pattern_match(const term &pat, const term &obj){
        ids v = { std::make_pair(pat, obj) };
        return matchs(v.begin(), v.end(), subst());
    }

    struct norm_exception{};

    static std::unique_ptr<term> rewrite(typename ids::const_iterator tt_first, typename ids::const_iterator tt_last, const term &t){
        std::unique_ptr<term> s;
        for(; tt_first != tt_last; ++tt_first){
            try{
                const term &l = tt_first->first, &r = tt_first->second;
                s.reset(new term(lift(pattern_match(l, t), r)));
                break;
            }catch(unify_exception){
                continue;
            }
        }
        return s;
    }

    static term norm(const ids &r, const term &t){
        if(t.which() == term::type_variable){
            return t;
        }else{
            const term_list &ts = t.template get<term_list>();
            std::function<term(const term&)> f = [&r](const term &a){ return norm(r, a); };
            std::unique_ptr<term> l;
            {
                std::unique_ptr<term> u(new term(make_term_list(ts.str, map(f, ts.list))));
                std::unique_ptr<term> v(rewrite(r.begin(), r.end(), *u));
                l.swap(v);
                if(!l){
                    return std::move(*u);
                }
            }
            return norm(r, *l.get());
        }
    }

    enum class order : int{
        nge = -1,
        eq = 0,
        gr = 1
    };

    template<class X, class Iter>
    static order lex(std::function<order(const X&, const X&)> f, Iter iter, Iter a_end, Iter jter, Iter b_end){
        for(; iter != a_end && jter != b_end; ++iter, ++jter){
            order ord = f(*iter, *jter);
            if(ord != order::eq){
                return ord;
            }
        }
        if(iter == a_end && jter == b_end){
            return order::eq;
        }
        if(iter != a_end && jter ==b_end){
            return order::gr;
        }else{
            return order::nge;
        }
    }

    static order primitive_compare(const type &a, const type &b){
        bool p = Less()(a, b);
        bool q = Less()(b, a);
        if(!p && !q){
            return order::eq;
        }else if(q){
            return order::gr;
        }else{
            return order::nge;
        }
    }

    static int &lpo_comparison_limit(){
        static int n = 0;
        return n;
    }

    static int &lpo_comparison_counter(){
        static int n = 0;
        return n;
    }

    static void set_lpo_comoparison_limit(int x){
        lpo_comparison_limit() = x;
    }

    static order lpo(std::function<order(const type&, const type&)> ord, const term &s, const term &t){
        //std::this_thread::sleep_for(std::chrono::milliseconds(100));
#ifdef EMSCRIPTEN
        //emscripten_sleep(5);
#endif

        if(lpo_comparison_counter() >= lpo_comparison_limit()){
            std::cout << "lpo comparison counter reached the upper limit." << std::endl;
            lpo_comparison_counter() = 0;
            throw fail_exception();
        }else{
            std::size_t digit = static_cast<std::size_t>(std::ceil(std::log(lpo_comparison_limit()) / std::log(10)));
            std::string n = std::to_string(lpo_comparison_counter());
            std::string z;
            for(std::size_t i = 0; i < digit - n.size(); ++i){
                z += "0";
            }
            std::cout << z + n << " " << format_term<term_rewriting_system>(s) << " : " << format_term<term_rewriting_system>(t) << std::endl;
            ++lpo_comparison_counter();
        }

        if(t.which() == term::type_variable){
            if(s == t){
                return order::eq;
            }else{
                if(occurs(t.template get<vname>(), s)){
                    return order::gr;
                }else{
                    return order::nge;
                }
            }
        }else if(s.which() == term::type_variable && t.which() == term::type_term_list){
            return order::nge;
        }else{
            const term_list &ss = s.template get<term_list>(), &ts = t.template get<term_list>();
            std::function<bool(const term&)> f = [&ord, &t](const term &si){ return lpo(ord, si, t) == order::nge; };
            if(forall(f, ss.list)){
                std::function<bool(const term&)> g = [&ord, &s](const term &a){ return lpo(ord, s, a) == order::gr; };
                switch(ord(ss.str, ts.str)){
                case order::gr:                            
                    if(forall(g, ts.list)){
                        return order::gr;
                    }else{
                        return order::nge;
                    }

                case order::eq:
                    if(forall(g, ts.list)){
                        std::function<order(const term&, const term&)> h = [&ord](const term &a, const term &b){ return lpo(ord, a, b); };
                        return lex(h, ss.list.begin(), ss.list.end(), ts.list.begin(), ts.list.end());
                    }else{
                        return order::nge;
                    }

                case order::nge:
                    return order::nge;
                }
            }
            return order::gr;
        }
    }

    static order lpo_functor(const term &t, const term &u){
        return lpo(primitive_compare, t, u);
    }

    class term_comparetor{
    public:
        bool operator()(const term &t, const term &u) const{
            return lpo_functor(t, u) == order::nge;
        }
    };

    static term rename(int n, const term &t){
        if(t.which() == term::type_variable){
            term r = t;
            r.template get<vname>().i += n;
            return r;
        }else{
            const term_list &ts = t.template get<term_list>();
            std::function<term(const term&)> f = [n](const term &a){ return rename(n, a); };
            return make_term_list(ts.str, map(f, ts.list));
        }
    }

    static int maxs(const std::vector<int> &s){
        int n = 0;
        for(auto &a : s){
            n = std::max(a, n);
        }
        return n;
    }

    static int maxindex(const term &t){
        if(t.which() == term::type_variable){
            return t.template get<vname>().i;
        }else{
            int n = 0;
            for(auto &u : t.template get<term_list>().list){
                n = (std::max)(maxindex(u), n);
            }
            return n;
        }
    }

    static ids ccp(
        std::function<term(const term&)> c,
        const term &t,
        const term &r,
        const term &l2,
        const term &r2
    ){
        try{
            return ids({std::make_pair(
                lift(unify(std::make_pair(t, l2)), r),
                lift(unify(std::make_pair(t, l2)), c(r2))
            )});
        }catch(unify_exception){
            return ids();
        }
    }

    static ids ccps(const ids &ttlist, const term &l, const term &r){
        std::function<ids(std::function<term(const term&)>, const term&, const term&)> cps;
        cps = [&](std::function<term(const term&)> c, const term &ts_, const term &r){
            if(ts_.which() == term::type_variable){
                return ids();
            }else{
                const term_list &ts = ts_.template get<term_list>();
                std::function<ids(const std::pair<term, term>&)> f = [&](const std::pair<term, term> &l2r2){
                    return ccp(c, ts_, r, l2r2.first, l2r2.second);
                };
                std::function<
                    ids(
                        std::function<term(const term&)>,
                        const type&,
                        const term_list&,
                        typename std::vector<term>::const_iterator,
                        typename std::vector<term>::const_iterator,
                        const term&
                    )
                > inner_cps = [&](
                    std::function<term(const term&)> c,
                    const type &f,
                    const term_list &ts0,
                    typename std::vector<term>::const_iterator ts1_first,
                    typename std::vector<term>::const_iterator ts1_last,
                    const term &r
                    ){
                    if(ts1_first == ts1_last){
                        return ids();
                    }else{
                        std::function<term(const term&)> cf = [&](const term &s){
                            std::vector<term> v = ts0.list;
                            v.reserve(v.size() + (ts1_last - ts1_first));
                            v.push_back(s);
                            v.insert(v.end(), ts1_first + 1, ts1_last);
                            return c(make_term_list(f, v));
                        };
                        term_list ts0_t = ts0;
                        ts0_t.list.push_back(*ts1_first);
                        ids
                            tmp1 = cps(cf, *ts1_first, r),
                            tmp2 = inner_cps(c, f, ts0_t, ts1_first + 1, ts1_last, r);
                        tmp1.insert(tmp1.end(), tmp2.begin(), tmp2.end());
                        return tmp1;
                    }
                };
                std::function<ids(const std::pair<term, term>&)> wrapped_ccp = [&](const std::pair<term, term> &l2r2){
                    return ccp(c, ts, r, l2r2.first, l2r2.second);
                };
                std::vector<ids> ccp_ttlist_result = map(wrapped_ccp, ttlist);
                {
                    ids inner_cps_result = inner_cps(c, ts.str, term_list(), ts.list.begin(), ts.list.end(), r);
                    ccp_ttlist_result.push_back(inner_cps_result);
                }
                return concat(ccp_ttlist_result);
            }
        };
        auto m = [&](const term &t){
            int mtu = 0;
            for(auto &p : ttlist){
                mtu = (std::max)(maxindex(p.first), mtu);
                mtu = (std::max)(maxindex(p.second), mtu);
            }
            return rename(mtu + 1, t);
        };
        std::function<term(const term&)> identity = [](const term &a){ return a; };
        return cps(identity, m(l), m(r));
    }

    static ids critical_pairs2(const ids &r1, const ids &r2){
        ids ttlist;
        for(auto &iter : r2){
            ids tt = ccps(r1, iter.first, iter.second);
            ttlist.insert(ttlist.end(), tt.begin(), tt.end());
        }
        return ttlist;
    }

    static ids critical_pairs(const ids &r){
        return critical_pairs2(r, r);
    }

    struct context_element{
        type str;
        std::vector<term> ts, us;
    };

    using context = std::vector<context_element>;

    static term replace(const context &cs, term t){
        for(auto &c : cs){
            std::vector<term> ts_t_us = c.ts;
            ts_t_us.reserve(ts_t_us.size() + c.us.size() + 1);
            ts_t_us.push_back(t);
            ts_t_us.insert(ts_t_us.end(), c.us.begin(), c.us.end());
            t = make_term_list(c.str, ts_t_us);
        }
        return t;
    }

    static std::tuple<ids, ids, ids> add_rule(const term &l,  const term &r, typename ids::const_iterator ids_e_first, typename ids::const_iterator ids_e_last, const ids &ids_s, const ids &ids_r){
        std::function<
            std::tuple<ids, ids>(
                typename ids::const_iterator,
                typename ids::const_iterator,
                typename ids::const_iterator,
                typename ids::const_iterator,
                const ids&
                )
        > simpl = [&](
            typename ids::const_iterator u_first,
            typename ids::const_iterator u_last,
            typename ids::const_iterator e_prime_first,
            typename ids::const_iterator e_prime_last,
            const ids &u_prime
            ){
            if(u_first == u_last){
                return make_tuple(ids(e_prime_first, e_prime_last), u_prime);
            }else{
                const term &g = u_first->first, &d = u_first->second;
                ids lr = { std::make_pair(l, r) };
                term g_prime = norm(lr, g);
                if(g_prime == g){
                    term d_prime;
                    {
                        ids lr_r_s;
                        lr_r_s.reserve(ids_r.size() + ids_s.size() + 1);
                        lr_r_s.push_back(std::make_pair(l, r));
                        lr_r_s.insert(lr_r_s.end(), ids_r.begin(), ids_r.end());
                        lr_r_s.insert(lr_r_s.end(), ids_s.begin(), ids_s.end());
                        d_prime = norm(lr_r_s, d);
                    }
                    ids g_d_prime_u_prime;
                    g_d_prime_u_prime.reserve(u_prime.size() + 1);
                    g_d_prime_u_prime.push_back(std::make_pair(g, d_prime));
                    g_d_prime_u_prime.insert(g_d_prime_u_prime.end(), u_prime.begin(), u_prime.end());
                    return simpl(u_first + 1, u_last, e_prime_first, e_prime_last, g_d_prime_u_prime);
                }else{
                    ids g_prime_d_e;
                    g_prime_d_e.reserve(ids_e_last - ids_e_first + 1);
                    g_prime_d_e.push_back(std::make_pair(g_prime, d));
                    g_prime_d_e.insert(g_prime_d_e.end(), ids_e_first, ids_e_last);
                    return simpl(u_first + 1, u_last, g_prime_d_e.begin(), g_prime_d_e.end(), u_prime);
                }
            }
        };
        std::tuple<ids, ids> e_prime_s_prime = simpl(ids_s.begin(), ids_s.end(), ids_e_first, ids_e_last, ids());
        ids &e_prime = std::get<0>(e_prime_s_prime), &s_prime = std::get<1>(e_prime_s_prime);
        std::tuple<ids, ids> e_wprime_r_prime = simpl(ids_r.begin(), ids_r.end(), e_prime.begin(), e_prime.end(), ids());
        ids &e_wprime = std::get<0>(e_wprime_r_prime), r_prime = std::get<1>(e_wprime_r_prime);
        ids lr_s_prime;
        lr_s_prime.reserve(s_prime.size() + 1);
        lr_s_prime.push_back(std::make_pair(l, r));
        lr_s_prime.insert(lr_s_prime.end(), s_prime.begin(), s_prime.end());
        return make_tuple(e_wprime, lr_s_prime, r_prime);
    }

    struct fail_exception{
        term t, u;
    };

    struct ori{
        std::function<order(const term&, const term&)> ord;
        std::pair<ids, ids> operator ()(typename ids::const_iterator e_first, typename ids::const_iterator e_last, ids ids_s, ids ids_r) const{
            term s_prime, t_prime;
            std::tuple<ids, ids, ids> tmp;
            while(true){
                if(e_first == e_last){
                    break;
                }else{
                    const term &s = e_first->first, &t = e_first->second;
                    {
                        ids rs;
                        rs.reserve(ids_r.size() + ids_s.size());
                        rs.insert(rs.end(), ids_r.begin(), ids_r.end());
                        rs.insert(rs.end(), ids_s.begin(), ids_s.end());
                        s_prime = norm(rs, s), t_prime = norm(rs, t);
                    }
                    if(ord(s_prime, t_prime) == order::eq){
                        ++e_first;
                        continue;
                    }else if(ord(s_prime, t_prime) == order::gr){
                        tmp = add_rule(s_prime, t_prime, e_first + 1, e_last, ids_s, ids_r);
                        e_first = std::get<0>(tmp).begin();
                        e_last = std::get<0>(tmp).end();
                        ids_s = std::move(std::get<1>(tmp));
                        ids_r = std::move(std::get<2>(tmp));
                        continue;
                    }else if(ord(t_prime, s_prime) == order::gr){
                        tmp = add_rule(t_prime, s_prime, e_first + 1, e_last, ids_s, ids_r);
                        e_first = std::get<0>(tmp).begin();
                        e_last = std::get<0>(tmp).end();
                        ids_s = std::move(std::get<1>(tmp));
                        ids_r = std::move(std::get<2>(tmp));
                        continue;
                    }
                    throw fail_exception({ s_prime, t_prime });
                }
            }
            return std::make_pair(ids_s, ids_r);
        }
    };

    static std::function<std::pair<ids, ids>(typename ids::const_iterator, typename ids::const_iterator, ids, ids)> orient(std::function<order(const term&, const term&)> ord){
        return ori{ ord };
    }

    static std::size_t size(const term &t){
        if(t.which() == term::type_variable){
            return 1;
        }else{
            const term_list &ts = t.template get<term_list>();
            std::size_t s = 1;
            for(auto &iter : ts.list){
                s += size(iter);
            }
            return s;
        }
    }

    static std::tuple<const term*, const term*, ids> min_rule(const term &t, const term &u, std::size_t n, typename ids::const_iterator r_first, typename ids::const_iterator r_last, const ids &r_prime){
        if(r_first == r_last){
            return make_tuple(&t, &u, r_prime);
        }else{
            const term &l = r_first->first, &r = r_first->second;
            std::size_t m = size(l) + size(r);
            ids nr;
            nr.reserve(r_prime.size() + 1);
            if(m < n){
                nr.push_back(std::make_pair(t, u));
                nr.insert(nr.end(), r_prime.begin(), r_prime.end());
                return min_rule(l, r, m, r_first + 1, r_last, nr);
            }else{
                nr.push_back(std::make_pair(l, r));
                nr.insert(nr.end(), r_prime.begin(), r_prime.end());
                return min_rule(t, u, n, r_first + 1, r_last, nr);
            }
        }
    }

    static std::tuple<const term*, const term*, ids> choose(typename ids::const_iterator r_first, typename ids::const_iterator r_last){
        return min_rule(r_first->first, r_first->second, size(r_first->first) + size(r_first->second), r_first + 1, r_last, ids());
    }

    static ids complete(std::function<order(const term&, const term&)> ord, const ids &e, std::size_t break_count = 0){
        std::function<ids(ids, ids, ids)> inner_completion = [&](ids ids_e, ids ids_s, ids ids_r){
            std::pair<ids, ids> sr;
            std::size_t count = 0;
            while(break_count == 0 || count < break_count){
                std::function<std::pair<ids, ids>(typename ids::const_iterator, typename ids::const_iterator, const ids&, const ids&)> f = orient(ord);
                sr = f(ids_e.begin(), ids_e.end(), ids_s, ids_r);
                if(sr.first.empty()){
                    break;
                }else{
                    const ids &s_prime = sr.first, &r_prime = sr.second;
                    std::tuple<const term*, const term*, ids> rl_s_wprime = choose(s_prime.begin(), s_prime.end());
                    ids cps, cps_tmp, rl = { std::make_pair(*std::get<0>(rl_s_wprime), *std::get<1>(rl_s_wprime)) };
                    cps = critical_pairs2(rl, r_prime);
                    cps_tmp = critical_pairs2(r_prime, rl);
                    cps.insert(cps.begin(), cps_tmp.begin(), cps_tmp.end());
                    cps_tmp = critical_pairs2(rl, rl);
                    cps.insert(cps.begin(), cps_tmp.begin(), cps_tmp.end());
                    cps_tmp = ids();
                    ids rl_r_prime;
                    rl_r_prime.reserve(r_prime.size() + 1);
                    rl_r_prime.push_back(std::make_pair(*std::get<0>(rl_s_wprime), *std::get<1>(rl_s_wprime)));
                    rl_r_prime.insert(rl_r_prime.begin(), r_prime.begin(), r_prime.end());
                    ids_e = std::move(cps);
                    ids_s = std::move(std::get<2>(rl_s_wprime));
                    ids_r = std::move(rl_r_prime);
                }
                ++count;
            }
            return sr.second;
        };
        return inner_completion(e, ids(), ids());
    }
};

#include <iostream>
#include <string>
#include <memory>

template<class TRS>
void print_term(const typename TRS::term &t){
    switch(t.which()){
    case TRS::term::type_variable:
        std::cout << t.template get<typename TRS::vname>().str;
        break;

    case TRS::term::type_term_list:
        std::cout << t.template get<typename TRS::vname>().str;
        if(!TRS::null(t.template get<typename TRS::term_list>().list)){
            std::cout << "(";
        }
        std::function<void(const typename TRS::term&)> f = [](const typename TRS::term &t){
            print_term<TRS>(t);
        };
        std::function<void(typename std::vector<typename TRS::term>::const_iterator, typename std::vector<typename TRS::term>::const_iterator)>
            g = [](typename std::vector<typename TRS::term>::const_iterator beg, typename std::vector<typename TRS::term>::const_iterator end){
            if(beg != end){ std::cout << ", "; }
        };
        TRS::allapp(f, g, t.template get<typename TRS::term_list>().list);
        if(!TRS::null(t.template get<typename TRS::term_list>().list)){
            std::cout << ")";
        }
        break;
    }
}

template<class TRS>
std::string format_term(const typename TRS::term &t){
    std::string str;
    switch(t.which()){
    case TRS::term::type_variable:
        str += t.template get<typename TRS::vname>().str;
        break;

    case TRS::term::type_term_list:
        str += t.template get<typename TRS::vname>().str;
        if(!TRS::null(t.template get<typename TRS::term_list>().list)){
            str += "(";
        }
        std::function<void(const typename TRS::term&)> f = [&str](const typename TRS::term &t){
            str += format_term<TRS>(t);
        };
        std::function<void(typename std::vector<typename TRS::term>::const_iterator, typename std::vector<typename TRS::term>::const_iterator)>
            g = [&str](typename std::vector<typename TRS::term>::const_iterator beg, typename std::vector<typename TRS::term>::const_iterator end){
                if(beg != end){ str += ", "; }
            };
        TRS::allapp(f, g, t.template get<typename TRS::term_list>().list);
        if(!TRS::null(t.template get<typename TRS::term_list>().list)){
            str += ")";
        }
        break;
    }
    return str;
}

template<class TRS>
std::string format_rules(const typename TRS::ids &rules){
    std::string str = "(RULES\n";
    const std::string indent = "  ";
    for(auto &pair : rules){
        str += indent + format_term<TRS>(pair.first) + " -> " + format_term<TRS>(pair.second) + "\n";
    }
    str += ")";
    return str;
}

//auto print_rules = [&](const trs::ids &rules){
//    for(auto &iter : rules){
//        print_term<trs>(iter.first);
//        std::cout << " -> ";
//        print_term<trs>(iter.second);
//        std::cout << std::endl;
//    }
//};

using trs = term_rewriting_system<std::string>;

std::size_t skip_blank(const std::string &target, std::size_t pos){
    if(pos >= target.size()){
        return pos;
    }

    while(
        pos < target.size() &&
        target[pos] == ' ' || target[pos] == '\t' || target[pos] == '\n'
    ){
        ++pos;
    }

    return pos;
}

std::size_t char_match(const std::string &target, std::size_t pos, char c){
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return pos;
    }

    j = skip_blank(target, i);
    if(j != i){
        i = j;
    }

    if(i >= target.size()){
        return pos;
    }

    if(target[i] == c){
        ++i;
    }else{
        return pos;
    }

    return i;
}

std::tuple<std::size_t, std::string> str(const std::string &target, std::size_t pos){
    const std::tuple<std::size_t, std::string> fail = std::make_tuple(pos, "");
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return fail;
    }

    j = skip_blank(target, i);
    if(j != i){
        i = j;
    }

    std::string s;
    while(
        i < target.size() &&
        target[i] != ' ' && target[i] != '\t' && target[i] != '\n' &&
        target[i] != '(' && target[i] != ')' && target[i] != '<' && target[i] != '>' &&
        target[i] != ','
    ){
        s += target[i];
        ++i;
    }

    return std::make_tuple(i, s);
}

std::size_t message(const std::string &target, std::size_t pos){
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return pos;
    }

    i = skip_blank(target, i);

    j = char_match(target, i, '<');
    if(j == i){
        return pos;
    }
    i = j;

    while(true){
        std::string s;
        std::tie(j, s) = str(target, i);
        if(j == i){
            j = message(target, i);
            if(j == i){
                j = char_match(target, i, '>');
                if(j == i){
                    return pos;
                }else{
                    i = j;
                    break;
                }
            }
        }
        i = j;
    }

    return i;
}

#include <set>

std::tuple<std::size_t, std::set<std::string>> variable_set(const std::string &target, std::size_t pos){
    const std::tuple<std::size_t, std::set<std::string>> fail = std::make_tuple(pos, std::set<std::string>{ std::string("") });
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return fail;
    }

    j = char_match(target, i, '(');
    if(j == i){
        return fail;
    }
    i = j;

    std::string keyword_var;
    std::tie(j, keyword_var) = str(target, i);
    if(j == i || keyword_var != "VAR"){
        return fail;
    }
    i = j;

    std::set<std::string> set;
    while(true){
        if(i >= target.size()){
            return fail;
        }
        std::string s;
        std::tie(j, s) = str(target, i);
        if(j == i){
            break;
        }
        i = j;
        set.insert(s);
    }

    j = char_match(target, i, ')');
    if(j == i){
        return fail;
    }
    i = j;

    return std::make_tuple(i, set);
}

std::tuple<std::size_t, trs::term> term(const std::string &target, std::size_t pos, const std::set<std::string> &set){
    std::tuple<std::size_t, trs::term> fail = std::make_tuple(pos, trs::term());
    std::size_t i = pos, j = i;

    std::string s;
    std::tie(j, s) = str(target, i);
    if(j == i){
        return fail;
    }
    i = j;

    if(set.find(s) != set.end()){
        return std::make_tuple(i, trs::make_variable(s));
    }

    j = char_match(target, i, '(');
    if(j == i){
        return std::make_tuple(i, trs::make_constant(s));
    }
    i = j;

    std::vector<trs::term> list;
    while(true){
        trs::term nested;
        std::tie(j, nested) = term(target, i, set);
        if(j == i){
            return fail;
        }
        i = j;
        list.push_back(nested);

        j = char_match(target, i, ',');
        if(j != i){
            i = j;
            continue;
        }else{
            j = char_match(target, i, ')');
            if(j == i){
                return fail;
            }
            i = j;
            break;
        }
    }

    return std::make_pair(i, trs::make_term_list(s, list));
}

std::tuple<std::size_t, std::pair<trs::term, trs::term>> rule(const std::string &target, std::size_t pos, const std::set<std::string> &set){
    std::tuple<std::size_t, std::pair<trs::term, trs::term>> fail = std::make_tuple(pos, std::make_pair(trs::term(), trs::term()));
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return fail;
    }

    trs::term a, b;
    std::tie(j, a) = term(target, i, set);
    if(j == i){
        return fail;
    }
    i = j;

    j = char_match(target, i, '-');
    if(j == i){
        return fail;
    }
    i = j;

    j = char_match(target, i, '>');
    if(j == i){
        return fail;
    }
    i = j;

    std::tie(j, b) = term(target, i, set);
    if(j == i){
        return fail;
    }
    i = j;

    return std::make_tuple(i, std::make_pair(a, b));
}

std::tuple<std::size_t, trs::ids> rules(const std::string &target, std::size_t pos, const std::set<std::string> &set){
    const std::tuple<std::size_t, trs::ids> fail = std::tuple<std::size_t, trs::ids>(pos, trs::ids());
    std::size_t i = pos, j = i;

    if(i >= target.size()){
        return fail;
    }

    j = char_match(target, i, '(');
    if(j == i){
        return fail;
    }
    i = j;

    std::string keyword_var;
    std::tie(j, keyword_var) = str(target, i);
    if(j == i || keyword_var != "RULES"){
        return fail;
    }
    i = j;

    bool first = true;
    trs::ids ids;
    while(true){
        std::pair<trs::term, trs::term> r;
        std::tie(j, r) = rule(target, i, set);
        if(j == i){
            if(first){
                return fail;
            }else{
                break;
            }
        }
        i = j;
        ids.push_back(r);
        first = false;
    }

    j = char_match(target, i, ')');
    if(j == i){
        return fail;
    }
    i = j;

    return std::make_tuple(i, ids);
}

std::tuple<std::size_t, std::size_t> rows_cols(const std::string &target, std::size_t pos){
    std::tuple<std::size_t, std::size_t> ret;
    std::size_t i = 0;
    for(; i < pos; ++i){
        if(target[i] == '\n'){
            std::get<0>(ret) = 0;
            ++std::get<1>(ret);
        }else if(target[i] == '\t'){
            std::get<0>(ret) += 8;
        }else{
            ++std::get<0>(ret);
        }
    }
    return ret;
}

std::string format_variable_set(const std::set<std::string> &set){
    std::string str = "(VAR";
    auto iter = set.begin();
    for(std::size_t i = 0; i < set.size(); ++i, ++iter){
        str += " " + *iter;
    }
    str += ")\n";
    return str;
}

std::string completion(std::string target, int limit){
    trs::lpo_comparison_limit() = limit;
    trs::lpo_comparison_counter() = 0;

    std::size_t pos = message(target, 0);
    std::size_t i = pos, j = i;
    std::set<std::string> var_set;
    std::tie(j, var_set) = variable_set(target, i);
    if(j == i){
        auto point = rows_cols(target, j);
        std::cout << "parsing error: " << std::to_string(std::get<1>(point) + 1) << ":" << std::to_string(std::get<0>(point) + 1) << std::endl;
        return target;
    }
    i = j;
    trs::ids ids;
    std::tie(j, ids) = rules(target, i, var_set);
    if(j == i){
        auto point = rows_cols(target, j);
        std::cout << "parsing error: " << std::to_string(std::get<1>(point) + 1) << ":" << std::to_string(std::get<0>(point) + 1) << std::endl;
        return target;
    }
    i = j;

    std::string str;
    try{
        trs::ids result = trs::complete(trs::lpo_functor, ids);
        str = "<kb completion success.>\n" + format_variable_set(var_set) + "\n" + format_rules<trs>(result);
    }catch(...){
        str = "<kb completion failed.>\n" + target.substr(pos, target.size() - pos);
    }

    return str;
}

#ifdef EMSCRIPTEN
int global = 0;

int increment_global(){
    global += 2;
    return 0;
}

int print_global(){
    std::cout << global << std::endl;
    return 0;
}

EMSCRIPTEN_BINDINGS(mod){
    function("completion", &completion);
    function("increment_global", &increment_global);
    function("print_global", &print_global);
}

#endif

trs::ids group(){
    auto f = [&](const trs::term &a, const trs::term &b){ return trs::make_function("f", { a, b }); };
    auto i = [&](const trs::term &a){ return trs::make_function("i", { a }); };
    auto e = trs::make_constant("e");
    auto var = [&](const std::string &str){ return trs::make_variable(str); };

    std::pair<trs::term, trs::term> rule_1 = std::make_pair(f(f(var("x"), var("y")), var("z")), f(var("x"), f(var("y"), var("z"))));
    std::pair<trs::term, trs::term> rule_2 = std::make_pair(f(i(var("x")), var("x")), e);
    std::pair<trs::term, trs::term> rule_3 = std::make_pair(f(e, var("x")), var("x"));
    trs::ids rules = { rule_1, rule_2, rule_3 };
    trs::ids result;
    try{
        result = trs::complete(trs::lpo_functor, rules);
    }catch(trs::fail_exception e){
        print_term<trs>(e.t);
        std::cout << std::endl;
        print_term<trs>(e.u);
        return result;
    }

    auto print_rules = [&](const trs::ids &rules){
        for(auto &iter : rules){
            print_term<trs>(iter.first);
            std::cout << " -> ";
            print_term<trs>(iter.second);
            std::cout << std::endl;
        }
    };

    std::cout << "group:" <<  std::endl;
    print_rules(rules);
    std::cout << std::endl;

    std::cout << "completed group:" <<  std::endl;
    print_rules(result);
    std::cout << std::endl;

    return result;
}

int main(){
    //completion(
    //    "<test>\n"
    //    "(VAR x y z)\n"
    //    "(RULES\n"
    //    "  f(f(x, y), z) -> f(x, f(y, z))\n"
    //    "  f(e, x)       -> x\n"
    //    "  f(i(x), x)    -> e\n"
    //    ")",
    //    5000
    //);
    return 0;
}