Last active
May 22, 2021 00:53
-
-
Save marionette-of-u/489118009b80cb17e0b3 to your computer and use it in GitHub Desktop.
Knuth-Bendix Completion Algorithm. (C++)
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
#include <algorithm> | |
#include <vector> | |
#include <tuple> | |
#include <functional> | |
#include <utility> | |
#include <memory> | |
#include <boost/variant.hpp> | |
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 : public boost::variant<vname, term_list>{ | |
using base = boost::variant<vname, term_list>; | |
using base::which; | |
enum{ | |
type_variable = 0, type_term_list | |
}; | |
term(const vname &v) : base(v){} | |
term(vname &&v) : base(v){} | |
term(const term_list &tl) : base(tl){} | |
term(term_list &&tl) : base(tl){} | |
term() : base(vname()){} | |
term(const term &other) : base(vname()){ | |
switch(other.which()){ | |
case type_variable: | |
static_cast<base&>(*this) = boost::get<vname>(other); | |
break; | |
case type_term_list: | |
static_cast<base&>(*this) = boost::get<term_list>(other); | |
break; | |
} | |
} | |
term(term &&other) : base(vname()){ | |
switch(other.which()){ | |
case type_variable: | |
static_cast<base&>(*this) = std::move(boost::get<vname>(other)); | |
break; | |
case type_term_list: | |
static_cast<base&>(*this) = std::move(boost::get<term_list>(other)); | |
break; | |
} | |
} | |
~term() = default; | |
term &operator =(const term &other){ | |
switch(other.which()){ | |
case type_variable: | |
static_cast<base&>(*this) = boost::get<vname>(other); | |
break; | |
case type_term_list: | |
static_cast<base&>(*this) = boost::get<term_list>(other); | |
break; | |
} | |
return *this; | |
} | |
bool operator ==(const term &other) const{ | |
if(which() != other.which()){ | |
return false; | |
}else{ | |
if(which() == type_variable){ | |
return boost::get<vname>(*this) == boost::get<vname>(other); | |
}else{ | |
return boost::get<term_list>(*this) == boost::get<term_list>(other); | |
} | |
} | |
} | |
}; | |
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 = boost::get<vname>(t); | |
if(indom(x, s)){ | |
return app(s, x); | |
}else{ | |
return t; | |
} | |
}else{ | |
const term_list &tl = boost::get<term_list>(t); | |
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 == boost::get<vname>(t); | |
}else{ | |
std::function<bool(const term&)> f = [&x](const term &a){ return occurs(x, a); }; | |
return exists(f, boost::get<term_list>(t).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 && boost::get<vname>(tt_first->first) == boost::get<vname>(tt_first->second)){ | |
return solve(tt_first + 1, tt_last, s); | |
}else{ | |
return elim(boost::get<vname>(tt_first->first), tt_first->second, tt_first + 1, tt_last, s); | |
} | |
}else if(tt_first->second.which() == term::type_variable){ | |
return elim(boost::get<vname>(tt_first->second), tt_first->first, tt_first + 1, tt_last, s); | |
}else{ | |
const term_list &ts = boost::get<term_list>(tt_first->first), &us = boost::get<term_list>(tt_first->second); | |
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 = boost::get<vname>(t1); | |
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 = boost::get<term_list>(t1), &us = boost::get<term_list>(t2); | |
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 term rewrite(typename ids::const_iterator tt_first, typename ids::const_iterator tt_last, const term &t){ | |
for(; tt_first != tt_last; ++tt_first){ | |
try{ | |
const term &l = tt_first->first, &r = tt_first->second; | |
return lift(pattern_match(l, t), r); | |
}catch(unify_exception){ | |
continue; | |
} | |
} | |
throw norm_exception(); | |
} | |
static term norm(const ids &r, const term &t){ | |
if(t.which() == term::type_variable){ | |
return t; | |
}else{ | |
const term_list &ts = boost::get<term_list>(t); | |
std::function<term(const term&)> f = [&r](const term &a){ return norm(r, a); }; | |
term u = make_term_list(ts.str, map(f, ts.list)); | |
try{ | |
return norm(r, rewrite(r.begin(), r.end(), u)); | |
}catch(norm_exception){ | |
return u; | |
} | |
} | |
} | |
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 order lpo(std::function<order(const type&, const type&)> ord, const term &s, const term &t){ | |
if(t.which() == term::type_variable){ | |
if(s == t){ | |
return order::eq; | |
}else{ | |
if(occurs(boost::get<vname>(t), 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 = boost::get<term_list>(s), &ts = boost::get<term_list>(t); | |
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; | |
boost::get<vname>(r).i += n; | |
return r; | |
}else{ | |
const term_list &ts = boost::get<term_list>(t); | |
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 boost::get<vname>(t).i; | |
}else{ | |
int n = 0; | |
for(auto &u : boost::get<term_list>(t).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 = boost::get<term_list>(ts_); | |
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 = boost::get<term_list>(t); | |
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> | |
#include <boost/timer.hpp> | |
template<class TRS> | |
void print_term(const typename TRS::term &t){ | |
switch(t.which()){ | |
case TRS::term::type_variable: | |
std::cout << boost::get<typename TRS::vname>(t).str; | |
break; | |
case TRS::term::type_term_list: | |
std::cout << boost::get<typename TRS::term_list>(t).str; | |
if(!TRS::null(boost::get<typename TRS::term_list>(t).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, boost::get<typename TRS::term_list>(t).list); | |
if(!TRS::null(boost::get<typename TRS::term_list>(t).list)){ | |
std::cout << ")"; | |
} | |
break; | |
} | |
} | |
void group(){ | |
using trs = term_rewriting_system<std::string>; | |
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 }; | |
boost::timer timer; | |
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; | |
} | |
double time = timer.elapsed(); | |
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 << time << "\n" << 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; | |
} | |
int main(){ | |
group(); | |
return 0; | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment