%   Predicates in Lambda Prolog that define some of the `higher-order'
%   mapping operations

module	maps.
import List.

	type	mapfun		(A -> B) -> (list A) -> (list B) -> o.
	% mapfun F (X1::X2::...::Xn) ((F X1)::(F X2)::...::(F Xn))

	mapfun F nil nil.
	mapfun F (X :: L) ((F X) :: K) :- mapfun F L K.

	type	mappred		(A -> B -> o) -> (list A) -> (list B) -> o.
	% mappred P (X1::X2::...::Xn) (Y1::Y2::...::Yn)
	%	Succeeds if the predicate P relates Xi to Yi.

	mappred P nil nil.
	mappred P (X :: L) (Y :: K) :- P X Y, mappred P L K.

	type	reduce		(A -> B -> B) -> (list A) -> B -> B -> o.
	% reduce F (X1::X2::...::Xn) Init (F X1 (F X2 (... (F Xn Init)))).

	reduce F nil X X.
	reduce F (W :: L) X (F W Y) :-  reduce F L X Y.

	type	forevery	(A -> o) -> (list A) -> o.
	% forevery P (X1::X2::...::Xn)
	%	Succeeds if P holds for every Xi.

	forevery P nil.
	forevery P (X :: L) :- P X, forevery P L.

	type	forsome		(A -> o) -> (list A) -> o.
	% forsome P (X1::X2::...::Xn).
	%	Succeeds if P holds for some Xi.

	forsome P (X :: L) :- P X.
	forsome P (X :: L) :- forsome P L.