Last active
November 6, 2016 12:27
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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; | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment