% module:   peano.pl
% date:     June 28, 2004
% author:   Douglas M. Auclair (DMA)

% copyright (c) 2005, Cotillion Group, Inc.  All rights reserved.

% synopsis: The Peano series is a logical approach to
%           counting/iterating over things; it converts
%           non-deterministic loops over a number range to
%           deterministic loops over the series.

:- module(peano, [peano/2, increment/2]).

% modified: November 17, 2005, DMA
% changed:  Added guards to peano/2 to ensure that only non-negative
%           integrals are permitted for Number.  To do this we need
%           the semantics of the syntax symbols.

:- use_module(library(syntax), [(~)/1, (<=)/2]).

:- op(900,   fy, ~).
:- op(920,  xfy, <= ).

peano(Number, Peano) :-
%    peano/2 converts between integers and Peano terms.  We use this
%    indirect call to allow the bidirectional conversion to work
%    without descending to var/1 hackery.  But, unfortunately, we do
%    need the cut (!/0) in order to avoid infinite regression on
%    backtracking.
  peano(Peano, 0, Number).

increment(Peano, s(Peano)).
%    Useful predicate for counting numbers as implicit DCG parameters.

% -------------------------------------------------------
% INTERNAL IMPLEMENTATION PREDICATE
% -------------------------------------------------------

peano(zero) --> [].
peano(s(Peano), Accum, Ans) :-
  New is Accum + 1,
  ((integer(Ans), Ans > -1, Ans >= New) <= ~(Ans = '_|_')),
  peano(Peano, New, Ans).