module funs.
import List.

type  mapfun   (A -> B) -> list A -> list B -> o.
type  foldr    (A -> B -> B) -> list A -> B -> B -> o.
type  foldl    (A -> B -> A) -> list B -> A -> A -> o.

% Relates a function and two lists if elements of the second list are
% the result of applying (via beta-conversion) the function to the
% corresponding element of the first list.

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

% "fold" a list to the right.  That is, foldr atoms of the
% following form are provable.
%   foldr F (X1 :: X2 :: ... :: Xn :: nil) Init
%            (F X1 (F X2 (... (F Xn Init)))).

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

% "fold" a list to the left.  That is, foldl atoms of the following 
% form are provable.
%   foldl F (X1 :: X2 :: ... :: Xn :: nil) Init
%            (F (F (... (F Init Xn) ... ) X2) X1).

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