DCG-ification of mi_list3

[GeoffChurch]

Hi Markus, I really liked the simple but effective mi_list3 from the acomip chapter. It's already in difference list form, so it can of course be rewritten using DCGs (and called with phrase/2 to force reduction to [] i.e. true):

mi_dcg_clause, [] --> [natnum(0)].
mi_dcg_clause, [natnum(X)] --> [natnum(s(X))].
mi_dcg_clause, [always_infinite] --> [always_infinite].

mi_dcg --> [].
mi_dcg --> mi_dcg_clause, mi_dcg.

Here's the original for reference:

mi_ldclause(natnum(0), Rest, Rest).
mi_ldclause(natnum(s(X)), [natnum(X)|Rest], Rest).
mi_ldclause(always_infinite, [always_infinite|Rest], Rest).

mi_list3([]).
mi_list3([G0|Gs0]) :- mi_ldclause(G0, Remaining, Gs0), mi_list3(Remaining).

I think this DCG form has several really nice features:

1. Pedagogically, I think it's a beautiful example of semicontext notation, which I'd found confusing.
2. The optional empty list semicontext (, []) in the first mi_dcg_clause conveniently corresponds to the optional :- true., and the --> corresponds to implication in the usual direction. And it makes it clear that the interpreter itself is just the reflexive transitive closure of some rewriting rules.
3. It's a nice basis for experimenting with meta-interpreters which make non-trivial use of DCG capabilities. For example, using seq and ... we can write some basic rules in a very readable way:

mi_dcg_clause, A, [X], B, C --> seq(A), [X], seq(B), [Y], seq(C), {X == Y}. % idempotence
mi_dcg_clause, [false] --> ..., [X], ..., [\+ Y], {X == Y}, ... . % contradiction
mi_dcg_clause, [false] --> ..., [\+ X], ..., [Y], {X == Y}, ... .
mi_dcg_clause, L, R --> seq(L), [true], seq(R). % everything absorbs true
mi_dcg_clause, [false] --> ..., [false, _], ... . % false absorbs everything
mi_dcg_clause, [false] --> ..., [_, false], ... .

I thought this might be a fun addition to the DCG or meta-interpreter chapters, or at least worth sharing!