Merge pull request #1692 from aarroyoc/docs-between

Compatible Doclog docs for library(between).
This commit is contained in:
Mark Thom
2023-01-23 04:00:11 +01:00
committed by GitHub

View File

@@ -1,3 +1,10 @@
/** Predicates that generate integers
These predicates can be used to reason about integers in a reduced domain that
follow some property. `library(clpz)` provides another way of reasoning about
integers that may also be interesting.
*/
:- module(between, [between/3, gen_int/1, gen_nat/1, numlist/2, numlist/3, repeat/1]). :- module(between, [between/3, gen_int/1, gen_nat/1, numlist/2, numlist/3, repeat/1]).
%% TODO: numlist/5. %% TODO: numlist/5.
@@ -5,6 +12,24 @@
:- use_module(library(lists), [length/2]). :- use_module(library(lists), [length/2]).
:- use_module(library(error)). :- use_module(library(error)).
%% between(+Lower, +Upper, -X).
%
% Given Lower and Upper are both integer numbers, true iff X is an integer so that _Lower =< X =< Upper_.
% Can be used both to check if X is between Lower and Upper or to generate an integer between
% Lower and Upper.
%
% Examples:
%
% ```
% ?- between(10, 20, 15).
% true.
% ?- between(10, 20, 25).
% false.
% ?- between(3, 5, X).
% X = 3
% ; X = 4
% ; X = 5.
% ```
between(Lower, Upper, X) :- between(Lower, Upper, X) :-
must_be(integer, Lower), must_be(integer, Lower),
must_be(integer, Upper), must_be(integer, Upper),
@@ -30,6 +55,9 @@ enumerate_nats(I0, N) :-
I1 is I0 + 1, I1 is I0 + 1,
enumerate_nats(I1, N). enumerate_nats(I1, N).
%% gen_nat(?N)
%
% True iff N is a natural number.
gen_nat(N) :- gen_nat(N) :-
can_be(integer, N), can_be(integer, N),
( var(N) -> enumerate_nats(0, N) ( var(N) -> enumerate_nats(0, N)
@@ -44,6 +72,9 @@ enumerate_ints(I0, N) :-
I1 is I0 + 1, I1 is I0 + 1,
enumerate_ints(I1, N). enumerate_ints(I1, N).
%% gen_int(?N)
%
% True iff N is an integer.
gen_int(N) :- gen_int(N) :-
can_be(integer, N), can_be(integer, N),
( var(N) -> enumerate_ints(0, N) ( var(N) -> enumerate_ints(0, N)
@@ -55,9 +86,24 @@ repeat_integer(N) :-
repeat_integer(N0) :- repeat_integer(N0) :-
N0 > 0, N1 is N0 - 1, repeat_integer(N1). N0 > 0, N1 is N0 - 1, repeat_integer(N1).
%% repeat(+N)
%
% Succeeds N times. This predicate is only included for compatibility and *should not be used*
% because it lacks a declarative interpretation.
repeat(N) :- repeat(N) :-
must_be(integer, N), repeat_integer(N). must_be(integer, N), repeat_integer(N).
%% numlist(?Upper, ?List)
%
% True iff List is the list of integers _[1, ..., Upper]_. Example:
%
% ```
% ?- numlist(X, Y).
% X = 1, Y = [1],
% ; X = 2, Y = [1,2]
% ; X = 3, Y = [1,2,3]
% ; ... .
% ```
numlist(Upper, List) :- numlist(Upper, List) :-
( integer(Upper) -> findall(X, between(1, Upper, X), List) ( integer(Upper) -> findall(X, between(1, Upper, X), List)
; List = [_|_], length(List, Upper), findall(X, between(1, Upper, X), List) ; List = [_|_], length(List, Upper), findall(X, between(1, Upper, X), List)
@@ -106,5 +152,14 @@ gen_ints(L, U) :-
), ),
L =< U. L =< U.
%% numlist(?Lower, ?Upper, ?List).
%
% True iff List is a list of the form _[Lower, ..., Upper]_.
% Example:
%
% ```
% ?- numlist(5, 10, X).
% X = [5,6,7,8,9,10].
% ```
numlist(Lower, Upper, List) :- numlist(Lower, Upper, List) :-
gen_ints(Lower, Upper), findall(X, between(Lower, Upper, X), List). gen_ints(Lower, Upper), findall(X, between(Lower, Upper, X), List).