mConfiguration.h

#pragma once
 
#include <utils/printer.h>
#include <state/statePattern.h>
#include <utils/messageException.h>
 
#include <numeric>
 
namespace TuringSim::State::MConfiguration {
    template <typename NodeType>
    class MConfiguration :
            public StatePattern<
                    std::shared_ptr<const MConfiguration<NodeType>>,
                    std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>>
            > {
    public:
        typedef std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>> Unification;
    private:
        typedef std::shared_ptr<const MConfiguration<NodeType>> StateType_;
        typedef StatePattern<StateType_, Unification> StatePattern_;
    public:
        using typename StatePattern_::StateType;
        using typename StatePattern_::MatcherType;
 
        typedef std::map<NodeType, NodeType> AlphaRewriting;
 
        typedef std::pair<AlphaRewriting, AlphaRewriting> AlphaRelation;
 
        static_assert(std::is_same_v<StateType, StateType_>);
        static_assert(std::is_same_v<StateType, std::shared_ptr<const MConfiguration<NodeType>>>);
        static_assert(std::is_same_v<MatcherType, std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>>>);
        static_assert(std::is_same_v<MatcherType, Unification>);
 
        constexpr MConfiguration(const NodeType& leaf);
        constexpr MConfiguration(const NodeType& leaf, bool isVar);
        constexpr MConfiguration(const NodeType& node, const std::vector<MConfiguration<NodeType>>& subTrees);
        constexpr MConfiguration(const NodeType& node, std::vector<MConfiguration<NodeType>>&& subTrees);
        constexpr MConfiguration(const NodeType& node, const std::vector<std::shared_ptr<const MConfiguration<NodeType>>>& subTrees);
        constexpr MConfiguration(const NodeType& node, std::vector<std::shared_ptr<const MConfiguration<NodeType>>>&& subTrees);
        constexpr MConfiguration(const MConfiguration<NodeType>& other);
        constexpr MConfiguration(MConfiguration<NodeType>&&);
        constexpr MConfiguration& operator=(const MConfiguration<NodeType>&);
        constexpr MConfiguration& operator=(MConfiguration<NodeType>&&);
        virtual ~MConfiguration() override = default;
        constexpr std::shared_ptr<const MConfiguration<NodeType>> getArg(size_t) const;
        constexpr const NodeType& getNode() const;
        constexpr size_t getArity() const;
        constexpr bool isLeaf() const;
        constexpr bool isVariable() const;
        constexpr bool isPattern() const;
        constexpr bool isMFunction() const;
        static std::shared_ptr<const MConfiguration<NodeType>> applySubstitution(std::shared_ptr<const MConfiguration<NodeType>> pattern, const Unification& subs);
        static std::shared_ptr<const MConfiguration<NodeType>> applySubstitution(std::shared_ptr<const MConfiguration<NodeType>> pattern, const Unification& subs, const std::shared_ptr<const MConfiguration<NodeType>>& def);
        static void unify_state(const std::shared_ptr<const MConfiguration<NodeType>>& state, const MConfiguration<NodeType>& pattern, std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>>& unification);
        static std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>> unify_state(const std::shared_ptr<const MConfiguration<NodeType>>& state, const MConfiguration<NodeType>& pattern);
        constexpr Unification unifyWithMConf(const std::shared_ptr<const MConfiguration<NodeType>>& state) const;
        Unification unify(const std::shared_ptr<const MConfiguration<NodeType>>& state) const;
        std::optional<Unification> unifyWithMConf_opt(const std::shared_ptr<const MConfiguration<NodeType>>& state) const noexcept;
        std::optional<MatcherType> match(const StateType& state) const noexcept override final;
        std::optional<Unification> unify_opt(const std::shared_ptr<const MConfiguration<NodeType>>& state) const;
        template<typename CharT = char, typename Traits = std::char_traits<CharT>, typename Alloc = std::allocator<CharT>>
        std::basic_string<CharT, Traits, Alloc> toString() const;
        constexpr int compare(const MConfiguration<NodeType>& other) const;
        constexpr bool operator!=(const MConfiguration<NodeType>& other) const;
        constexpr bool operator==(const MConfiguration<NodeType>& other) const;
        bool operator<(const MConfiguration<NodeType>& other) const;
        std::optional<AlphaRelation> isAlphaEquivalent(const std::shared_ptr<const MConfiguration<NodeType>>& other) const;
        void isAlphaEquivalent(const std::shared_ptr<const MConfiguration<NodeType>>& other, AlphaRewriting& direct, AlphaRewriting& back) const;
        template <typename CharT = char, typename Traits = std::char_traits<CharT>>
        std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug() const;
 
        template <typename CharT = char, typename Traits = std::char_traits<CharT>>
        static std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug(const Unification& unification);
 
        template <typename CharT = char, typename Traits = std::char_traits<CharT>>
        static std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug(const AlphaRewriting& rewriting);
 
        template <typename CharT = char, typename Traits = std::char_traits<CharT>>
        static std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug(const AlphaRelation& relation);
 
        template <typename U, typename CharT, typename Traits> constexpr friend std::basic_ostream<CharT, Traits>& operator<<(std::basic_ostream<CharT, Traits>& os, const MConfiguration<U>& m_conf) {
            if(m_conf.args.empty()) {
                os << (m_conf.isVar ? "_" : "") << m_conf.node;
                return os;
            }
 
            os << m_conf.node << "(";
            bool first = true;
            for(size_t i = 0; i < m_conf.args.size(); ++i) {
                if(first) {
                    first = false;
                }
                else {
                    os << ", ";
                }
                os << *m_conf.args[i];
            }
            os << ")";
            return os;
        }
 
    protected:
        NodeType node;
        bool isVar;
        std::vector<std::shared_ptr<const MConfiguration<NodeType>>> args;
        bool is_pattern;
    };
 
    template <typename NodeType>
    class NoUnificationException : public Utils::MessageException {
    public:
        NoUnificationException() = delete;
 
        NoUnificationException(
                std::string message,
                const MConfiguration<NodeType>& pattern,
                const MConfiguration<NodeType>& state,
                const typename MConfiguration<NodeType>::Unification& unification) :
                MessageException(message),
                pattern(pattern),
                state(state),
                unification(unification)
        {}
 
    protected:
        virtual std::string makeFullMessage() const override {
            using Utils::Debug::operator<<;
            std::ostringstream ss;
            ss << this->msg << std::endl;
            ss << "  pattern: " << pattern.debug() << std::endl;
            ss << "  state: " << state.debug() << std::endl;
            ss << "  unification: " << Utils::Debug::debug(unification) << std::endl;
            return ss.str();
        }
 
        MConfiguration<NodeType> pattern;
 
        MConfiguration<NodeType> state;
 
        typename MConfiguration<NodeType>::Unification unification;
    };
 
    template <typename NodeType>
    class NoAlphaEquivalenceException : public Utils::MessageException {
    public:
        NoAlphaEquivalenceException() = delete;
 
        NoAlphaEquivalenceException(
                std::string message,
                const MConfiguration<NodeType>& lhs,
                const MConfiguration<NodeType>& rhs,
                const typename MConfiguration<NodeType>::AlphaRewriting& direct,
                const typename MConfiguration<NodeType>::AlphaRewriting& back) :
                MessageException(message),
                lhs(lhs),
                rhs(rhs),
                direct(direct),
                back(back)
        {}
 
    protected:
        virtual std::string makeFullMessage() const override {
            using Utils::Debug::operator<<;
            std::ostringstream ss;
            ss << this->msg << std::endl;
            ss << "  lhs: " << lhs.debug() << std::endl;
            ss << "  rhs: " << rhs.debug() << std::endl;
            ss << "  direct: " << Utils::Debug::debug(direct) << std::endl;
            ss << "  back: " << Utils::Debug::debug(back) << std::endl;
            return ss.str();
        }
 
        MConfiguration<NodeType> lhs;
 
        MConfiguration<NodeType> rhs;
 
        typename MConfiguration<NodeType>::AlphaRewriting direct;
 
        typename MConfiguration<NodeType>::AlphaRewriting back;
    };
 
    template <typename NodeType> MConfiguration(const NodeType&) -> MConfiguration<NodeType>;
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& leaf) :
            StatePattern_(),
            node(leaf),
            isVar(false),
            args(std::vector<std::shared_ptr<const MConfiguration<NodeType>>>()),
            is_pattern(false)
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& leaf, bool isVariable) :
            StatePattern_(),
            node(leaf),
            isVar(isVariable),
            args(std::vector<std::shared_ptr<const MConfiguration<NodeType>>>()),
            is_pattern(isVariable)
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& nodeContent, const std::vector<MConfiguration<NodeType>>& subTrees) :
            StatePattern_(),
            node(nodeContent),
            isVar(false),
            args(),
            is_pattern(std::accumulate(subTrees.begin(), subTrees.end(), false, [](bool acc, const MConfiguration<NodeType>& b) -> bool { return acc || b.is_pattern; }))
    {
        for(const MConfiguration<NodeType>& subTree: subTrees) {
            args.push_back(std::make_shared<MConfiguration<NodeType>>(subTree));
        }
    }
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& nodeContent, std::vector<MConfiguration<NodeType>>&& subTrees) :
            StatePattern_(),
            node(nodeContent),
            isVar(false),
            args(),
            is_pattern(std::accumulate(subTrees.begin(), subTrees.end(), false, [](bool acc, const MConfiguration<NodeType>& b) -> bool { return acc || b.is_pattern; }))
    {
        for(const MConfiguration<NodeType>& subTree: subTrees) {
            args.push_back(std::make_shared<MConfiguration<NodeType>>(std::move(subTree)));
        }
    }
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& nodeContent, const std::vector<std::shared_ptr<const MConfiguration<NodeType>>>& subTrees) :
            StatePattern_(),
            node(nodeContent),
            isVar(false),
            args(subTrees),
            is_pattern(std::accumulate(subTrees.begin(), subTrees.end(), false, [](bool acc, const std::shared_ptr<const MConfiguration<NodeType>>& b) -> bool { return acc || b->is_pattern; }))
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const NodeType& nodeContent, std::vector<std::shared_ptr<const MConfiguration<NodeType>>>&& subTrees) :
            StatePattern_(),
            node(nodeContent),
            isVar(false),
            args(std::move(subTrees)),
            is_pattern(std::accumulate(subTrees.begin(), subTrees.end(), false, [](bool acc, const std::shared_ptr<const MConfiguration<NodeType>>& b) -> bool { return acc || b->is_pattern; }))
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(const MConfiguration<NodeType>& other) :
            StatePattern_(other),
            node(other.node),
            isVar(other.isVar),
            args(other.args),
            is_pattern(other.is_pattern)
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>::MConfiguration(MConfiguration<NodeType>&& other) :
            StatePattern_(std::move(other)),
            node(std::move(other.node)),
            isVar(other.isVar),
            args(std::move(other.args)),
            is_pattern(other.is_pattern)
    {}
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>& MConfiguration<NodeType>::operator=(const MConfiguration<NodeType>& other) {
        if(this != &other) {
            StatePattern_::operator=(other);
            node = other.node;
            isVar = other.isVar;
            args = other.args;
            is_pattern = other.is_pattern;
        }
        return *this;
    }
 
    template <typename NodeType>
    constexpr MConfiguration<NodeType>& MConfiguration<NodeType>::operator=(MConfiguration<NodeType>&& other) {
        if(this != &other) {
            StatePattern_::operator=(std::move(other));
            node = std::move(other.node);
            isVar = other.isVar;
            args = std::move(other.args);
            is_pattern = other.is_pattern;
        }
        return *this;
    }
 
    template <typename NodeType>
    constexpr std::shared_ptr<const MConfiguration<NodeType>> MConfiguration<NodeType>::getArg(size_t i) const {
        return args.at(i);
    }
 
    template <typename NodeType>
    constexpr const NodeType& MConfiguration<NodeType>::getNode() const {
        return node;
    }
 
    template <typename NodeType>
    constexpr size_t MConfiguration<NodeType>::getArity() const {
        return args.size();
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::isLeaf() const {
        return args.empty();
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::isVariable() const {
        return isVar;
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::isPattern() const {
        return is_pattern;
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::isMFunction() const {
        return !is_pattern;
    }
 
    template <typename NodeType>
    std::shared_ptr<const MConfiguration<NodeType>> MConfiguration<NodeType>::applySubstitution(std::shared_ptr<const MConfiguration<NodeType>> pattern, const Unification& subs) {
        if(pattern->isLeaf() && pattern->isVariable()) {
            if(subs.count(pattern->node))
                return subs.at(pattern->node);
            else
                return pattern;
        }
 
        std::vector<std::shared_ptr<const MConfiguration<NodeType>>> outputArgs;
 
        for(std::shared_ptr<const MConfiguration<NodeType>> arg : pattern->args) {
            if(arg->is_pattern) {
                outputArgs.push_back(applySubstitution(arg, subs));
            }
            else {
                outputArgs.push_back(arg);
            }
        }
 
        return std::make_shared<const MConfiguration<NodeType>>(pattern->node, std::move(outputArgs));
    }
 
    template <typename NodeType>
    std::shared_ptr<const MConfiguration<NodeType>> MConfiguration<NodeType>::applySubstitution(std::shared_ptr<const MConfiguration<NodeType>> pattern, const Unification& subs, const std::shared_ptr<const MConfiguration<NodeType>>& def) {
        if(pattern->isLeaf() && pattern->isVariable()) {
            if(subs.count(pattern->node))
                return subs.at(pattern->node);
            else
                return def;
        }
 
        std::vector<std::shared_ptr<const MConfiguration<NodeType>>> outputArgs;
 
        for(std::shared_ptr<const MConfiguration<NodeType>> arg : pattern->args) {
            if(arg->is_pattern) {
                outputArgs.push_back(applySubstitution(arg, subs, def));
            }
            else {
                outputArgs.push_back(arg);
            }
        }
 
        return std::make_shared<const MConfiguration<NodeType>>(pattern->node, std::move(outputArgs));
    }
 
    template <typename NodeType>
    void MConfiguration<NodeType>::unify_state(const std::shared_ptr<const MConfiguration<NodeType>>& state, const MConfiguration<NodeType>& pattern, std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>>& unification) {
        std::function<NoUnificationException<NodeType>(const std::string&)> make_exception =
                [&state, &pattern, &unification = std::as_const(unification)](const std::string& message) {
                    return NoUnificationException(message, pattern, *state, unification);
                };
 
        if(pattern.isLeaf()) {
            if(pattern.isVariable()) {
                NodeType node = pattern.getNode();
                typename std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>>::const_iterator it = unification.find(node);
                if(it == unification.end()) {
                    unification.insert({node, state});
                }
                else if(*it->second != *state) {
                    std::ostringstream ss;
                    ss << "Unable to unify: incompatible variables. At node " << node << "." << std::endl
                       << "  Known unification: " << it->second;
                    throw make_exception(ss.str());
                }
                else {
                    return;
                }
            }
            else if(pattern.getNode() == state->getNode())
                return;
            else {
                std::ostringstream ss;
                ss << "Unable to unify: incompatible leaves: " << state->getNode() << "(state) vs " << pattern.getNode() << "(pattern)";
                throw make_exception(ss.str());
            }
        } else {
            if(state->getArity() != pattern.getArity()) {
                std::ostringstream ss;
                ss << "Unable to unify: arities does not match: "
                   << state->getArity() << "(state) vs "
                   << pattern.getArity() << "(pattern)";
                throw make_exception(ss.str());
            }
            if(state->getNode() != pattern.getNode()) {
                std::ostringstream ss;
                ss << "Unable to unify: m-function name does not match: " << state->getNode() << "(state) vs "
                   << pattern.getNode() << "(pattern)";
                throw make_exception(ss.str());
            }
            size_t args_size = state->getArity();
            for(size_t i=0; i < args_size; ++i) {
                unify_state(state->args[i], *pattern.args[i], unification);
            }
        }
    }
 
    template <typename NodeType>
    std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>> MConfiguration<NodeType>::unify_state(const std::shared_ptr<const MConfiguration<NodeType>>& state, const MConfiguration<NodeType>& pattern) {
        std::function<NoUnificationException<NodeType>(const std::string&)> make_exception =
                [&state, &pattern](const std::string& message) {
                    using Utils::Debug::operator<<;
                    std::ostringstream ss;
                    ss << message << std::endl;
                    ss << "  state: " << state->debug() << std::endl;
                    ss << "  pattern: " << pattern.debug() << std::endl;
                    return NoUnificationException<NodeType>(message, pattern, *state, {});
                };
 
        if(state->isPattern()) {
            throw make_exception("first argument of unify_state must not be a pattern.");
        }
        std::map<NodeType, std::shared_ptr<const MConfiguration<NodeType>>> unification;
        unify_state(state, pattern, unification);
        return unification;
    }
 
    template <typename NodeType>
    constexpr typename MConfiguration<NodeType>::Unification MConfiguration<NodeType>::unifyWithMConf(const std::shared_ptr<const MConfiguration<NodeType>>& state) const {
        return unify_state(state, *this);
    }
 
    template <typename NodeType>
    typename MConfiguration<NodeType>::Unification MConfiguration<NodeType>::unify(const std::shared_ptr<const MConfiguration<NodeType>>& other) const {
        std::function<NoUnificationException<NodeType>(const std::string&)> make_exception =
                [this, &other](const std::string& message) {
                    return NoUnificationException(message, *this, *other, {});
                };
 
        if(isPattern()) {
            if(other->isMFunction()) {
                return unifyWithMConf(other);
            }
            throw make_exception("Two patterns in MConfiguration<T>::unify");
        }
        else {
            throw make_exception("'this' should be a pattern for MConfiguration<T>::unify");
        }
    }
 
    template <typename NodeType>
    std::optional<typename MConfiguration<NodeType>::Unification> MConfiguration<NodeType>::unifyWithMConf_opt(const std::shared_ptr<const MConfiguration<NodeType>>& m_conf) const noexcept {
        try {
            return std::make_optional(unify_state(m_conf, *this));
        }
        catch (NoUnificationException<NodeType>) {
            return std::nullopt;
        }
    }
 
    template <typename NodeType>
    std::optional<typename MConfiguration<NodeType>::MatcherType> MConfiguration<NodeType>::match(const StateType& state) const noexcept {
        return unifyWithMConf_opt(state);
    }
 
    template <typename NodeType>
    std::optional<typename MConfiguration<NodeType>::Unification> MConfiguration<NodeType>::unify_opt(const std::shared_ptr<const MConfiguration<NodeType>>& state) const {
        std::function<NoUnificationException<NodeType>(const std::string&)> make_exception =
                [this, &state](const std::string& message) {
                    return NoUnificationException(message, *this, *state, {});
                };
 
        if(isPattern()) {
            if(state->isMFunction()) {
                return unifyWithMConf_opt(state);
            }
            throw make_exception("Two patterns in MConfiguration<T>::unify");
        }
        else {
            throw make_exception("'this' should be a pattern for MConfiguration<T>::unify_opt");
        }
    }
 
    template <typename NodeType>
    template <typename CharT, typename Traits, typename Alloc>
    std::basic_string<CharT, Traits, Alloc> MConfiguration<NodeType>::toString() const {
        std::basic_ostringstream<CharT, Traits, Alloc> ss;
        ss << *this;
        return ss.str();
    }
 
    template <typename NodeType>
    constexpr int MConfiguration<NodeType>::compare(const MConfiguration<NodeType>& other) const {
        if(node != other.node) {
            // return node <=> other.node;
            if(node < other.node) {
                return -1;
            }
            return 1;
        }
 
        if(isVar != other.isVar) {
            // return isVar <=> other.isVar;
            if(isVar < other.isVar) {
                return -1;
            }
            return 1;
        }
 
        if(args.size() != other.args.size()) {
            // return args.size() <=> other.args.size();
            if(args.size() < other.args.size()) {
                return -1;
            }
            return 1;
        }
 
        const size_t args_size = args.size();
 
        for(size_t i = 0; i < args_size; ++i) {
            // int cmp = args[i] <=> other.args[i];
            // if(cmp) return cmp;
            int cmp = args[i]->compare(*other.args[i]);
            if (cmp) {
                return cmp;
            }
        }
 
        return 0;
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::operator!=(const MConfiguration<NodeType>& other) const {
        return compare(other) != 0;
    }
 
    template <typename NodeType>
    constexpr bool MConfiguration<NodeType>::operator==(const MConfiguration<NodeType>& other) const {
        return compare(other) == 0;
    }
 
    template<typename NodeType>
    bool MConfiguration<NodeType>::operator<(const MConfiguration<NodeType>& other) const {
        return compare(other) < 0;
    }
 
    template <typename NodeType>
    std::optional<typename MConfiguration<NodeType>::AlphaRelation> MConfiguration<NodeType>::isAlphaEquivalent(const std::shared_ptr<const MConfiguration<NodeType>>& other) const {
        AlphaRewriting direct, back;
        try {
            isAlphaEquivalent(other, direct, back);
        }
        catch (NoAlphaEquivalenceException<NodeType>) {
            return std::nullopt;
        }
        return {{direct, back}};
    }
 
    template <typename NodeType>
    void MConfiguration<NodeType>::isAlphaEquivalent(const std::shared_ptr<const MConfiguration<NodeType>>& other, AlphaRewriting& direct, AlphaRewriting& back) const {
        std::function<NoAlphaEquivalenceException<NodeType>(const std::string&)> make_exception =
                [this, &other, &direct = std::as_const(direct), &back = std::as_const(back)](const std::string& message) {
                    return NoAlphaEquivalenceException<NodeType>(message, *this, *other, direct, back);
                };
        if(isVar != other->isVar) {
            throw make_exception("One variable and one constant node");
        }
        if(!isVar) {
            if(node != other->node) {
                throw make_exception("Two unequal nodes");
            }
            if(args.size() != other->args.size()) {
                throw make_exception("Two nodes with unequal arity");
            }
 
            const size_t args_size = args.size();
            for(size_t i = 0; i < args_size; ++i) {
                args[i]->isAlphaEquivalent(other->args[i], direct, back);
            }
        }
        else {
            if(direct.count(node) > 0 && back.count(other->node) == 0) {
                throw make_exception("Left node does not point to right node");
            }
            else if(direct.count(node) == 0 && back.count(other->node) > 0) {
                throw make_exception("Right node does not point to left node");
            }
            else if(direct.count(node) == 0 && back.count(other->node) == 0) {
                direct[node] = other->node;
                back[other->node] = node;
            }
            else if(direct[node] != other->node || back[other->node] != node) {
                throw make_exception("Incompatible relation");
            }
            else {
                return;
            }
 
        }
    }
 
    template <typename NodeType>
    template <typename CharT, typename Traits>
    std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> MConfiguration<NodeType>::debug() const {
        return [this](std::basic_ostream<CharT, Traits>& out) -> std::basic_ostream<CharT, Traits>& {
            if (args.empty()) {
                out << std::string(isVar ? "_" : "") << node;
                return out;
            }
 
            out << "{" << node << "}(";
            for (size_t i = 0; i < args.size() - 1; ++i)
                out << "{" << *args[i] << "}, ";
            out << "{" << *args.back() << "})";
            return out;
        };
    }
 
    template<typename NodeType>
    template <typename CharT, typename Traits>
    std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> MConfiguration<NodeType>::debug(const MConfiguration::Unification& u) {
        return Utils::Debug::debug(u);
    }
 
    template<typename NodeType>
    template <typename CharT, typename Traits>
    std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> MConfiguration<NodeType>::debug(const MConfiguration::AlphaRewriting& rew) {
        return Utils::Debug::debug(rew);
    }
 
    template<typename NodeType>
    template <typename CharT, typename Traits>
    std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> MConfiguration<NodeType>::debug(const MConfiguration::AlphaRelation& rel) {
        return Utils::Debug::debug(rel);
    }
}