#include <boost/spirit/core.hpp>

using namespace boost::spirit;

class constraint_grammar : public grammar<constraint_grammar> {

 public:

    static const unsigned long PARAMETER_id = 1;
    static const unsigned long CONSTANT_id = 2;
    static const unsigned long VARIABLE_id = 3;
    static const unsigned long TERM_id = 4;
    static const unsigned long NEG_id = 5;
    static const unsigned long DNEG_id = 6;
    static const unsigned long ATOM_id = 7;
    static const unsigned long JUNC_id = 9;
    static const unsigned long PRED_id = 10;
    static const unsigned long EQ_id = 11;
    static const unsigned long LITERAL_id = 12;
    static const unsigned long LITERALGROUP_id = 13;
    static const unsigned long LITERALSET_id = 14;
    static const unsigned long UPDATE_id = 15;
    static const unsigned long ENTRY_id = 16;

    // s_t is scanner type
    template <typename s_t> struct definition {
        definition(constraint_grammar const&) {

            // ex: ?a
            parameter =
                discard_node_d[ch_p('?')] >>
                lexeme_d[leaf_node_d[+lower_p]]
            ;

            // ex: mary
            constant = lexeme_d[leaf_node_d[+lower_p]];

            // ex: X
            variable = lexeme_d[leaf_node_d[+upper_p]];

            // one of constant, or variable
            term = parameter | constant | variable;

            // negation
            neg = lexeme_d[ch_p('~')];

            // double-negation
            dneg = ch_p('~') >> ch_p('~');

            // possibly negated predicate or (in)equality
            // (because an equality like X=Y is actually
            // an infix form of =(X,Y).
            atom =
                (
                    *(discard_node_d[dneg]) >>
                    !neg >> (pred|eq)
                )
            ;
            
            // con/dis-junction
            junc =
                root_node_d[
                    as_lower_d[str_p("and")]
                    |
                    as_lower_d[str_p("or")]
                ] >> ( literalgroup | literal )
            ;

            // predicate name and list of terms in parens
            pred =
                root_node_d[lexeme_d[leaf_node_d[+lower_p]]] >>
                discard_node_d[ch_p('(')] >>
                term >> *(discard_node_d[ch_p(',')] >> term) >>
                discard_node_d[ch_p(')')]
            ;

            // (in)equality - can be seen as an infix variant of a
            // predicate, i.e. X=Y <-> =(X,Y)
            eq =
                term >> root_node_d[ch_p('=') | str_p("<>")] >> term;

            // atom, possibly connected to a con/disjunction of
            // other stuff
            literal =
                atom >> !junc
            ;

            // one or more literals in parenthesis, possibly with negation(s)
            literalgroup =
                *(discard_node_d[dneg]) >>
                !neg >>
                discard_node_d[ch_p('(')] >>
                ( literal | literalgroup ) >>
                discard_node_d[ch_p(')')] >>
                !junc
            ;

            update = root_node_d[pred];

            entry =
                (literalgroup | literal) >>
                discard_node_d[ch_p(';')] >> update
            ;
        }

        rule<s_t,parser_context<>,parser_tag<PARAMETER_id> >
                                                            parameter;
        rule<s_t,parser_context<>,parser_tag<CONSTANT_id> > constant;
        rule<s_t,parser_context<>,parser_tag<VARIABLE_id> > variable;
        rule<s_t,parser_context<>,parser_tag<TERM_id> >     term;
        rule<s_t,parser_context<>,parser_tag<NEG_id> >      neg;
        rule<s_t,parser_context<>,parser_tag<DNEG_id> >     dneg;
        rule<s_t,parser_context<>,parser_tag<ATOM_id> >     atom;
        rule<s_t,parser_context<>,parser_tag<JUNC_id> >     junc;
        rule<s_t,parser_context<>,parser_tag<PRED_id> >     pred;
        rule<s_t,parser_context<>,parser_tag<EQ_id> >       eq;
        rule<s_t,parser_context<>,parser_tag<LITERAL_id> >  literal;
        rule<s_t,parser_context<>,parser_tag<LITERALGROUP_id> >
                                                            literalgroup;
        rule<s_t,parser_context<>,parser_tag<LITERALSET_id> >
                                                            literalset;
        rule<s_t,parser_context<>,parser_tag<UPDATE_id> >   update;
        rule<s_t,parser_context<>,parser_tag<ENTRY_id> >    entry;

        rule<s_t, parser_context<>, parser_tag<ENTRY_id> > const&
        start() const {
            return entry;
        }
    };
};