module pairs.

% This module differs from the one given in Figure 4.1 in that
% the type constructor pair is written as pr.  This is because
% elp does not allow a token to be used as both a type and a
% constant.

kind pr      type -> type -> type.
type pair    A -> B -> pr A B.

type assoc   A -> B -> list (pr A B) -> o.
type assok   A -> B -> list (pr A B) -> o.
type domain  list (pr A B) -> list A -> o.
type range   list (pr A B) -> list B -> o.

assoc X Y ((pair X Y)::L).
assoc X Y (P::L) :- assoc X Y L.

assok X Y ((pair X Y)::L) :- !.
assok X Y (P::L) :- assok X Y L.

domain nil nil.
domain ((pair X Y)::Alist) (X::L) :- domain Alist L.

range nil nil.
range ((pair X Y)::Alist) (Y::L)  :- range Alist L.