% converts a grammar rule into a normal clause:

dcg_rule(Rule, Clause) :-
    dcg_rule(Rule, S0, S, Expansion),
    dcg_simplify(Expansion, S0, S, Clause).


dcg_rule((RHead --> _), _, _, _) :-
    var(RHead),
    throw(instantiation_error).

dcg_rule((RHead, _ --> _), _, _, _) :-
    var(RHead),
    throw(instantiation_error).

dcg_rule((_, Terminals --> _), _, _, _) :-
    var(Terminals),
    throw(instantiation_error).

dcg_rule((_, Terminals --> _), _, _, _) :-
    \+ is_list(Terminals),
    throw(type_error(list, Terminals)).

dcg_rule((NonTerminal, Terminals --> GRBody), S0, S, (Head :- Body)) :-
    !,
    dcg_non_terminal(NonTerminal, S0, S, Head),
    dcg_body(GRBody, S0, S1, Goal1),
    dcg_terminals(Terminals, S, S1, Goal2),
    Body = (Goal1, Goal2).

dcg_rule((NonTerminal --> GRBody), S0, S, (Head :- Body)) :-
    !,
    dcg_non_terminal(NonTerminal, S0, S, Head),
    dcg_body(GRBody, S0, S, Body).

dcg_rule(Term, _, _, _) :-
    throw(type_error(grammar_rule, Term)).


% translates a grammar goal non-terminal:

dcg_non_terminal(NonTerminal, _, _, _) :-
    \+ callable(NonTerminal),
    throw(type_error(callable, NonTerminal)).

dcg_non_terminal(NonTerminal, S0, S, Goal) :-
    NonTerminal =.. NonTerminalUniv,
    append(NonTerminalUniv, [S0, S], GoalUniv),
    Goal =.. GoalUniv.


% translates a list of terminals:

dcg_terminals(Terminals, _, _, _) :-
    \+ is_list(Terminals),
    throw(type_error(list, Terminals)).

dcg_terminals(Terminals, S0, S, S0 = List) :-
    append(Terminals, S, List).


% translates a grammar rule body:

dcg_body(Var, S0, S, phrase(Var, S0, S)) :-
    var(Var),
    !.

dcg_body((GRIf -> GRThen), S0, S, (If -> Then)) :-
    !,
    dcg_body(GRIf, S0, S1, If),
    dcg_body(GRThen, S1, S, Then).

dcg_body((GREither; GROr), S0, S, (Either; Or)) :-
    !,
    dcg_body(GREither, S0, S, Either),
    dcg_body(GROr, S0, S, Or).

dcg_body((GRFirst, GRSecond), S0, S, (First, Second)) :-
    !,
    dcg_body(GRFirst, S0, S1, First),
    dcg_body(GRSecond, S1, S, Second).

dcg_body(!, S0, S, (!, S0 = S)) :-
    !.

dcg_body({Goal}, S0, S, (call(Goal), S0 = S)) :-
    var(Goal),
    !.

dcg_body({Goal}, _, _, _) :-
    \+ callable(Goal),
    throw(type_error(callable, Goal)).

dcg_body({Goal}, S0, S, (Goal, S0 = S)) :-
    !.

dcg_body(\+ GRBody, S0, S, (\+ Goal, S0 = S)) :-
    !,
    dcg_body(GRBody, S0, S, Goal).

dcg_body([], S0, S, (S0=S)) :-
    !.

dcg_body([T| Ts], S0, S, Goal) :-
    !,
    dcg_terminals([T| Ts], S0, S, Goal).

dcg_body(NonTerminal, S0, S, Goal) :-
    dcg_non_terminal(NonTerminal, S0, S, Goal).


% tries to simplify the resulting clause:

dcg_simplify((Head :- true), _, _, Head) :-
    !.

dcg_simplify((Head :- Body), _, _, Head) :-
    dcg_conj_unifications(Body),
    dcg_fold_unifications(Body),
    !.

dcg_simplify((Head :- Body), _, _, (Head :- Simplified)) :-
    dcg_simplify_and(Body, Simplified),
    !.

dcg_simplify(Clause, _, _, Clause).


% folds unifications when the clause body only contains calls to =/2:

dcg_conj_unifications(_ = _) :-
    !.

dcg_conj_unifications(((_ = _), Goal)) :-
    !,
    dcg_conj_unifications(Goal).

dcg_conj_unifications((Goal, (_ = _))) :-
    !,
    dcg_conj_unifications(Goal).


dcg_fold_unifications(Term1 = Term2) :-
    !,
    Term1 = Term2.

dcg_fold_unifications(((Term1 = Term2), Goal)) :-
    !,
    Term1 = Term2,
    dcg_fold_unifications(Goal).

dcg_fold_unifications((Goal, (Term1 = Term2))) :-
    Term1 = Term2,
    dcg_fold_unifications(Goal).


% removes redundant calls to true/0 and flats conjunction of goals:

dcg_simplify_and((Goal1 -> Goal2), (SGoal1 -> SGoal2)) :-
    !,
    dcg_simplify_and(Goal1, SGoal1),
    dcg_simplify_and(Goal2, SGoal2).

dcg_simplify_and((Goal1;Goal2), (SGoal1;SGoal2)) :-
    !,
    dcg_simplify_and(Goal1, SGoal1),
    dcg_simplify_and(Goal2, SGoal2).

dcg_simplify_and(((Goal1,Goal2),Goal3), Body) :-
    !,
    dcg_simplify_and((Goal1,(Goal2,Goal3)), Body).

dcg_simplify_and((true,Goal), Body) :-
    !,
    dcg_simplify_and(Goal, Body).

dcg_simplify_and((Goal,true), Body) :-
    !,
    dcg_simplify_and(Goal, Body).

dcg_simplify_and((Goal1,Goal2), (Goal1,Goal3)) :-
    !,
    dcg_simplify_and(Goal2, Goal3).

dcg_simplify_and(\+ Goal, \+ SGoal) :-
    !,
    dcg_simplify_and(Goal, SGoal).

dcg_simplify_and(Goal, Goal).


% auxiliary predicates:

append([], List, List).
append([Head| Tail], List, [Head| Tail2]) :-
    append(Tail, List, Tail2).

callable(Term) :-
    nonvar(Term),
    functor(Term, Functor, _),
    atom(Functor).

is_list([]).
is_list([_| Tail]) :-
    is_list(Tail).