:- module peano.

% 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.
% created:  June 28, 2004
% author:   Douglas M. Auclair (DMA)

% modified: March 22, 2006, DMA
% changed:  Converted to Mercury.  Added conversions of numbers as
%           strings to their peano equivalents, as well.

:- interface.

:- import_module string, enum.

:- type peano ---> zero; s(peano).
:- instance enum(peano).

        % Converts the natural number in the string to a peano numeral
:- pred to_peano(string::in, peano::out) is semidet.

        % Bidirectionally converts between non-negative integers and
	% their equivalent peano numerals.
:- pred peano(int, peano).
:- mode peano(in, out) is semidet.
:- mode peano(in, in) is semidet.
:- mode peano(out, in) is det.

        % Increments or decrements a peano numeral.
:- pred increment(peano, peano).
:- mode increment(in, in) is semidet.
:- mode increment(in, out) is det.
:- mode increment(out, in) is semidet.

:- implementation.

:- import_module int, peano.nat.

:- instance enum(peano) where [
        to_int(Peano) = fold_to_nat(Peano),
        from_int(Num) = Peano :- peano(Num, Peano)
].

to_peano(String, Peano) :-
  to_int(String, Int),
  guarded_peano(Int, zero, Peano).

:- pragma promise_equivalent_clauses(peano/2).

peano(Number::in, Peano::in) :- fold_to_nat(Peano) = Number.
peano(Number::in, Peano::out) :- guarded_peano(Number, zero, Peano).
peano(Number::out, Peano::in) :- Number = fold_to_nat(Peano).

increment(Peano, s(Peano)).
%    Useful predicate for counting numbers as implied (DCG) arguments.

% -------------------------------------------------------
% INTERNAL IMPLEMENTATION PREDICATES
% -------------------------------------------------------

:- func fold_to_nat(peano) = int.

fold_to_nat(zero) = 0.
fold_to_nat(s(Peano)) = 1 + fold_to_nat(Peano).

:- module nat.
:- interface.

:- pred guarded_peano(int::in, peano::in, peano::out) is semidet.

:- implementation.

guarded_peano(N) --> { N >= 0 }, peano(N).

:- pred peano(int::in, peano::in, peano::out) is det.

peano(N) --> { N > 0 } -> increment, peano(N - 1); [].

:- end_module nat.

:- end_module peano.