%% prelude.rfp
%%
%% The RELFUN prelude

%% Christian Embacher
%% December 1, 1997

%% This module implements the basic library of RELFUN. It makes 
%% common-purpose operations on numbers, lists and other objects 
%% available. 



%% PART I : Numbers
%% ================


%% odd(X) : Bool
%% X : Nat
%% No precondition.
%% Returns true if X is an odd number and false otherwise.

odd(0) :& false.
odd(1) :& true.
odd(X) :- >(X,1) & odd(-[2](X)).


%% even(X) : Bool
%% X : Nat
%% No precondition.
%% Returns true if X is an even number and false otherwise.

even(0) :& true.
even(1) :& false.
even(X) :- >(X,1) & even(-[2](X)).


%% sign(X) : Number
%% X : Number
%% No precondition.
%% Returns -1 if X < 0, 0 if X = 0 and 1 if X > 0.

sign(0) !& 0.
sign(X) :- <(X,0) & -1.
sign(X) :- >(X,0) & 1.


%% -[N](X) : Number
%% N, X : Number
%% No precondition.
%% Returns -(X,N).

-[N](X) :& -(X,N).

%% +[N](X) : Number
%% N, X : Number
%% No precondition.
%% Returns +(X,N).

+[N](X) :& +(X,N).


%% *[N](X) : Number
%% N, X : Number
%% No precondition.
%% Returns *(X,N).

*[N](X) :& *(X,N).


%% /[N](X) : Number
%% N, X : Number
%% Preconditions:
%%   * N /= 0.
%% Returns /(X,N).

/[N](X) :& /(X,N).


%% <[N](X) : Bool
%% N, X : Number
%% No precondition.
%% Returns true if X < N and false otherwise.

<[N](X) :& <(X,N).   


%% <=[N](X) : Bool
%% N, X : Number
%% No precondition.
%% Returns true if X <= N and false otherwise.

<=[N](X) :& <=(X,N).
      
                                                           
%% =[N](X) : Bool
%% N, X : Number
%% No precondition.
%% Returns true if X = N and false otherwise.

=[N](X) :& =(X,N). 


% /=[N](X) : Bool                                                  
%% N, X : Number
%% No precondition.
%% Returns true if X /= N and false otherwise.

/=[N](X) :& /=(X,N).

   
%% >[N](X) : Bool
%% N, X : Number   
%% No precondition.
%% Returns true if X > N and false otherwise.
   
>[N](X) :& >(X,N).

  
%% >=[N](X) : Bool 
%% N, X : Number 
%% No precondition.
%% Returns true if X >= N and false otherwise.

>=[N](X) :& >=(X,N). 
 


%% PART II : Lists
%% ===============


%% listp(X) : Bool
%% X : type
%% No precondition.
%% Returns true if X is a list and false otherwise.

listp([|L]) !& true.
listp(X) :& false.


%% null(L) : Bool
%% L : [type]
%% No precondition.
%% Returns true if L is empty and false otherwise.

null([]) :& true.
null([X|T]) !& false.


%% nth[N](L) : type
%% N : Nat
%% L : [type]
%% Preconditions:
%%   * 0 < N <= length of L
%% Returns the Nth element of L.

nth[1]([H|T]) !& H.
nth[N]([H|T]) :- >(N,1), M.=-(N,1) !& nth[M](T).


%% thn[N](L) : type
%% N : Nat
%% L : [type] 
%% Preconditions:
%%   * 0 < N <= length of L
%% Returns the Nth last element of L.

thn[N](L) :- M.= 1+(-(len(L),N)) & nth[M](L).


%% nrest[N](L) : [type]
%% N : Nat 
%% L : [type]
%% Preconditions:
%%   * N <= length of L.
%% Returns a list M which is built from L by removing the first 
%% N elements of L. The elements of M retain the same order they 
%% possess in L.

nrest[0](L) !& L.
nrest[N]([H|T]) :- >(N,0), M.=-(N,1) & nrest[M](T).


%% restn[N](L) : [type]
%% N : Nat
%% L : [type]
%% Preconditions:
%%   * N <= length of L
%% Returns a list M which is built from L by removing the last 
%% N elements of L. The elements of M retain the same order they 
%% possess in L.

restn[N](L) :- M.= -(len(L),N) & nstart[M](L).


%% nstart[N](L) : [type]
%% N : Nat
%% L : [type]
%% Preconditions:
%%   * N <= length of L.
%% Returns a list consisting of the first N elements of L in 
%% same order.

nstart[0](L) !& [].
nstart[N]([H|T]) :- >(N,0), M.=-(N,1) & tup(H|nstart[M](T)).


%% startn[N](L) : [type]
%% N : Nat
%% L : [type]
%% Preconditions:
%%   * N <= length of L
%% Returns a list consisting of the last N elements of L in 
%% same order.

startn[N](L) :- M.=-(len(L),N) & nrest[M](L).


%% sublist[X,Y](L) : [type]
%% X,Y : Nat
%% L : [type]
%% Preconditions:
%%   * 0 < X 
%%   * Y <= length of L.
%% Returns a list consisting of the elements between the Xth and 
%% Yth element of L (inclusive) in same order if X <= Y. If X > Y 
%% the empty list is returned.

sublist[X,Y](L) :- >(X,Y), >=(Y,0) & [].
sublist[X,Y](L) :- N.=1-(X) !& nrest[N](nstart[Y](L)).


%% rev(L) : [type]
%% L : [type]
%% No precondition.
%% Returns a list consisting of the same elements as L but in 
%% reverse order.

rev(L) :& foldl[cns,[]](L).


%% append(L1,...,Ln) : [type]
%% L1, ..., Ln : [type]
%% No precondition.
%% Returns the list that is built from L by appending L1, ..., Ln
%% together in the same order they possess in L.

append(|L) :& foldr[app,[]](L).


%% member[X](L) : Bool
%% X : type
%% L : [type]
%% No precondition.
%% Returns true if X is an element of L and false otherwise.

member[X]([]) :& false.
member[X]([X|T])!.
member[X]([H|T]) :& member[X](T).


%% remove[X](L) : [type]
%% X : type
%% L : [type]
%% No precondition.
%% Returns a list M which is built from L by removing all 
%% occurrences of X in L. The elements of M retain the same relative
%% order they possess in L. 

remove[X]([]) :& [].
remove[X]([X|T]) !& remove[X](T).
remove[X]([H|T]) :& tup(H|remove[X](T)).


%% remove-1th[X](L) : [type]
%% X : type 
%% L : [type]
%% No precondition.
%% Returns a list M which is built from L by removing the first 
%% occurrence of X in L. The elements of M retain the same relative 
%% order they possess in L.
  
remove-1th[X]([]) :& [].
remove-1th[X]([X|T]) !& T.
remove-1th[X]([H|T]) :& tup(H|remove-1th[X](T)).


%% remove-1rest[X](L) : [type]
%% X : type 
%% L : [type]
%% No precondition.
%% Returns a list M which is built from L by removing all 
%% occurrences of X in L but the first. The elements of M retain 
%% the same relative order they possess in L.

remove-1rest[X]([]) :& [].
remove-1rest[X]([X|T]) !& tup(X|remove[X](T)).
remove-1rest[X]([H|T]) :& tup(H|remove-1rest[X](T)).


%% remove-duplicates(L) : [type]
%% L : [type]
%% No precondition.
%% Returns a list M which is built from L by removing all multiple 
%% occcurences of all elements in L. The elements of M retain the 
%% same relative order they possess in L.

remove-duplicates(L) :& remove-duplicates-mem(L,[]).


%% Auxiliary operator for "remove-duplicates".
%% remove-duplicates-mem(L1,L2) : [type]
%% L1,L2 : [type]
%% Preconditions:
%%   * L2 is empty.

remove-duplicates-mem([],L) :& [].
remove-duplicates-mem([H|T],L) 
  :- member[H](L) 
  !& remove-duplicates-mem(T,L).
remove-duplicates-mem([H|T],L) 
  :& tup(H|remove-duplicates-mem(T,tup(H|L))).


%% insert[N,X](L) : [type]
%% N : Nat
%% X : type
%% Preconditions:
%%   + N = 0 if L is empty.
%%   + 0 < N <= length of L if L is not empty.
%% Returns the list [X] if L is empty.. 
%% Otherwise it returns a list which is built from L by inserting X
%% between the (N-1)th and the Nth element of L.

insert[0,X]([]) :& [X].
insert[1,X]([H|L]) :& tup(X,H|L).
insert[N,X]([H|L]) :- >(N,1), M.=1-(N) & tup(H|insert[M,X](L)).


%% exchange[N,X](L) : [type]
%% N : Nat
%% X : type 
%% L : [type]
%% Preconditions:
%%   * L is not empty
%%   * 0 < N <= length of L
%% Returns a list which is built from L by replacing the Nth 
%% element of L by X.

exchange[1,X]([H|T]) :& tup(X|T).
exchange[N,X]([H|T]) :- >(N,1), M.=-(N,1) & tup(H|exchange[M,X](T)). 


%% substitute[X,Y](L) : [type]
%% X,Y : type
%% L : [type]
%% No precondition.
%% Returns a list which is built from L by replacing all occurrences
%% of X in L by Y.

substitute[X,Y]([]) :& [].
substitute[X,Y]([X|T]) !& tup(Y|substitute[X,Y](T)).
substitute[X,Y]([H|T]) :& tup(H|substitute[X,Y](T)). 


%% zip(L1,L2) : [<type1,type2>]
%% L1 : [type1]
%% L2 : [type2]
%% Preconditions:
%%   * L1 and L2 are both of the same length.
%% Returns a list M of length of L1 and L2. For every i the ith 
%% element of M is [X,Y] iff the ith element of L1 is X and the ith 
%% element of L2 is Y.

zip([],[]) :& [].
zip([H1|T1],[H2|T2]) :& tup([H1,H2]|zip(T1,T2)).


%% unzip(L) : <[type1],[type2]>
%% L : [<type1,type2>]
%% No precondition.
%% Returns a Pair [L1,L2] of lists that has the same length as L. 
%% For every i the ith element of L1 is X and the ith element of L2 
%% is Y iff the ith element of L is [X,Y].

unzip(L) :& foldr[unzip-foldr-F,[[],[]]](L).


%% Auxiliary operator for "unzip".
%% unzip-foldr-F(Pair,L) : <[type1],[type2]>
%% Pair : <type1,type2>
%% L : <[type1],[type2]>

unzip-foldr-F([X,Y],[L1,L2]) 
  :- M1.=tup(X|L1), M2.=tup(Y|L2) 
  & [M1,M2]. 


%% mapping[F](L) : [type2]
%% F : type1 --> type2
%% L : [type1] 
%% No precondition.
%% Returns a list M of length of L such that for every i the ith 
%% element of M is the result F(X) of applying F to the ith element 
%% X of L.

mapping[F](L) :& foldr[mapping-cns[F],[]](L).


%% Auxiliary operator for "mapping".
%% mapping-cns[F](X,L) : [type2]
%% F : type1 --> type2
%% X : type1
%% L : [type2]
 
mapping-cns[F](X,L) :& tup(F(X)|L).


%% tabulate[F](X,Y) : [type]
%% F : Integer --> type
%% X,Y : Integer
%% No precondition.
%% Returns the list [F(X), F(X+1), ..., F(Y)] if X <= Y 
%% and [] otherwise.

tabulate[F](X,Y) :- >(X,Y) !& [].
tabulate[F](X,Y) :& tup(F(X)|tabulate[F](1+(X),Y)).


%% iterate[F,N](X) : [type]
%% F : type --> type
%% N : Nat
%% X : type
%% No preconditions
%% Returns a list M consisiting of the first N+1 Iterations of F 
%% over X, i.e. M:=[X,F^1(X),...,F^N(X)].

iterate[F,0](X) :& [X].
iterate[F,N](X) :- >(N,0), M.=1-(N) & tup(X|iterate[F,M](F(X))).


%% filter[P](L) : [type]
%% P : type --> Bool 
%% L : [type]
%% No precondition.
%% Returns a list M which consists of exactly those elements X of L
%% for which P(X) evaluates true. The elements of M retain the same 
%% relative order they possess in L.

filter[P]([]) :& [].
filter[P]([H|T]) :- P(H) !& tup(H|filter[P](T)).
filter[P]([H|T]) :& filter[P](T).


%% partition[P](L) : <[type],[type]>
%% P : type --> bool
%% L : [type]
%% Applies P to each element of L, from left to right, and returns a
%% pair [Pos, Neg] where Pos is the list of those X of L for which 
%% P(X) evaluated to true, and Neg is the list of those X in L for 
%% which P(X) evaluated to false. The elements of Pos and Neg retain
%% the same relative order they possess in L.

partition[P]([]) :& [[],[]].
partition[P]([H|T]) 
  :- P(H), [L1,L2].=partition[P](T), M.=tup(H|L1) 
  !& [M,L2].
partition[P]([H|T]) 
  :- [L1,L2].=partition[P](T), M.=tup(H|L2) 
  & [L1,M].


%% split[P](L) : <[type],[type]>
%% P : type --> bool
%% L : [type]
%% No precondition.
%% Returns a pair [Only-pos,With-neg]. Only-pos is the longest 
%% prefix of L that contains only elements X of L for which P(X) 
%% evaluates to true. With-neg is the suffix of L which starts with 
%% the first element Y of L for which P(Y) evaluates false. 
%% It is L = Only-pos ++ With-neg.   

split[P]([]) :& [[],[]].
split[P]([H|T]) 
  :- P(H), [L1,L2].=split[P](T), M.=tup(H|L1) 
  !& [M,L2].
split[P]([H|T]) :& [[],[H|T]]. 


%% some[P](L) : Bool
%% P : type --> Bool 
%% L : [type]
%% No precondition.
%% Returns true if P(X) evaluates true for (at least) one element of
%% L and false otherwise.

some[P]([]) :& false.
some[P]([H|T]) :- P(H) !& true.
some[P]([H|T]) :& some[P](T).


%% every[P](L) : Bool
%% P : type --> Bool
%% L : [type]
%% No precondition.
%% Returns true if P(X) evaluates true for each element of L and 
%% false otherwise.

every[P]([]) :& true.
every[P]([H|T]) :- P(H) !& every[P](T).
every[P]([H|T]) :& false.


%% find[P](L) : type
%% P : type --> Bool
%% L : [type]
%% Applies P to each element X of the L, from left to right, and 
%% returns the first X for which P(X) evaluates true. Returns 'none' 
%% if F(X) evaluates false for each element X of L.

find[P]([]) :& none.
find[P]([H|T]) :- P(H) !& H.
find[P]([H|T]) :& find[P](T).


%% mcompose[F_1,F_2,...,F_N](X) : type_1
%% F_1  : type_2 --> type_1
%% F_2  : type_3 --> type_2
%% ...
%% F_N-1: type_N --> type_N-1
%% F_N  : type_X --> type_N
%% X   : type_X
%% Preconditions:
%%   * N > 0
%% Returns F_1(F_2(...F_N(X)...))

mcompose[F](X) :& F(X).
mcompose[F|Fr](X) :& F(mcompose[|Fr](X)).


%% sort[P](L) : [type]
%% P : type type --> Bool
%% L : [type]
%% Preconditions:
%%   * P is a total order.
%% Sorts L in ascending order w.r.t. P, i.e. returns a list 
%% consisting of exactly the elements of L in ascending order 
%% w.r.t. P.

sort[P]([]) :& [].
sort[P]([H|T]) 
  :- [L,G].=partition[comp[P,H]](T), 
     L-sorted.=sort[P](L), 
     G-sorted.=sort[P](G)
  & app(L-sorted,[H|G-sorted]).


%% Auxiliary operator for sort.
%% comp[P,X](Y) : Bool
%% P : type type --> Bool
%% X,Y : type

comp[P,X](Y) :& P(Y,X).


%% sorted-p[P](L) : Bool
%% P : type type --> Bool
%% L : [type]
%% Preconditions:
%%   * P is a total order.
%% Returns true if the elements of L are in ascending order w.r.t. P.

sorted-p[P]([]) :& true.
sorted-p[P]([X]) :& true.
sorted-p[P]([X,Y|L]) :- P(X,Y) !& sorted-p[P]([Y|L]).
sorted-p[P]([X,Y|L]) :& false.


%% min[P](L) : type
%% L : [type]
%% Preconditions:
%%   * P is a total order.
%%   * L is not empty.
%% Returns the P-minimum of L, i.e. the element X of L for which
%% P(X,Y) holds true for every other Y of L.

min[P]([H|L]) :& foldr[bin-min[P],H](L).


%% Auxiliary operator for "min".
%% bin-min[P](X,Y) : type
%% P : type type --> Bool
%% X,Y : type
%% No precondition.
%% Returns X if X=Y or if P(X,Y) is evaluated true and false otherwise.

bin-min[P](X,X) !& X.
bin-min[P](X,Y) :- P(X,Y) !& X.
bin-min[P](X,Y) :& Y.


%% max[P](L) : type
%% L : [type]
%% Preconditions:
%%   * P is a total order.
%%   * L is not empty.
%% Returns the P-maximum of L, i.e. the element Y of L for which
%% P(X,Y) holds true for every other X of L.

max[P]([H|L]) :& foldr[bin-max[P],H](L).


%% Auxiliary operator for "max".
%% bin-max[P](X,Y) : type
%% P : type type --> Bool
%% X,Y : type
%% No precondition.
%% Returns Y if X=Y or if  P(X,Y) is evaluated false and true otherwise.

bin-max[P](X,X) !& X.
bin-max[P](X,Y) :- P(X,Y) !& Y.
bin-max[P](X,Y) :& X.


%% foldl[F,X](L) : type2
%% F : (type1 type2) --> type2
%% X : type2
%% L : [type1]
%% No precondition.
%% Returns F(Xn,...,F(X2, F(X1, X))...) if L=[X1,X2,...,Xn] is not 
%% empty and X if L is empty. 

foldl[F,X]([]) :& X.
foldl[F,X]([H|T]) :- Y.=F(H,X) & foldl[F,Y](T).


%% foldr[F,X](L) : type2
%% F : (type1 type2) --> type2
%% X : type2
%% L : [type1]
%% No precondition.
%% Returns F(X1, F(X2,...,F(Xn,X)...)) if L=[X1,X2,...,Xn] is not 
%% empty and X if L is empty. 

foldr[F,X]([]) :& X.
foldr[F,X]([H|T]) :- Y.= foldr[F,X](T) & F(H,Y).



%% PART III : Strings
%% ==================


%% string=[St1](St2) : Bool
%% St1,St2 : String
%% Returns true if St1 and St2 are the same strings and false 
%% otherwise.

string=[St1](St2) :& string=(St1,St2).



%% PART IV : Boolean algebra
%% =========================


%% not(X) : Bool
%% X : Bool
%% No precondition.
%% Returns the value of (not X).

not(true) :& false.
not(false) :& true.


%% and(X,Y) : Bool
%% X,Y : Bool
%% No precondition.
%% Returns the value of (X and Y).

and(false,false) :& false.
and(false,true) :& false.
and(true,false) :& false.
and(true,true) :& true.


%% or(X,Y) : Bool
%% No precondition.
%% Returns the value of (X or Y).
%% X,Y : Bool

or(false,false) :& false.
or(false,true) :& true.
or(true,false) :& true.
or(true,true) :& true.


%% xor(X,Y) : Bool
%% No precondition.
%% Returns the value of (X xor Y).
%% X,Y : Bool

xor(false,false) :& false.
xor(false,true) :& true.
xor(true,false) :& true.
xor(true,true) :& false.


%% equiv(X,Y) : Bool
%% X,Y : Bool
%% No precondition.
%% Returns the value of (X equiv Y).

equiv(false,false) :& true.
equiv(false,true) :& false.
equiv(true,false) :& false.
equiv(true,true) :& true.


%% nand(X,Y) : Bool
%% X,Y : Bool
%% No precondition.
%% Returns the value of (X nand Y).

nand(false,false) :& true.
nand(false,true) :& true.
nand(true,false) :& true.
nand(true,true) :& false.


%% nor(X,Y) : Bool
%% X,Y : Bool
%% No precondition.
%% Returns the value of (X nor Y).

nor(false,false) :& true.
nor(false,true) :& false.
nor(true,false) :& false.
nor(true,true) :& false.



%% PART V : Misc
%% =============


%% identity(X) : type
%% X : type
%% No precondition.
%% Returns X.

identity(X) :& X.


%% const[X](Y) : type1
%% X : type1
%% Y : type2
%% No precondition.
%% Returns X.

const[X](Y) :& X.


%% eq(X,Y) : Bool
%% X : type1
%% Y : type2
%% No precondition.
%% Returns true if X and Y are identical and false otherwise.

eq(X,Y) :& not(neq(X,Y)).


%% neq(X,Y) : Bool
%% X : type1
%% Y : type2
%% No precondition.
%% Returns false if X and Y are identical and true otherwise.

neq(X,X) !& false.
neq(_,_).


%% tup

tup() :& [].
tup(First|Rest) :& [First|Rest].


%% mgu(X,Y) : type1 | type2 
%% X : type1
%% Y : type2

mgu(X,X) :& X.


%% pause()

pause() :- relfun().



%% =================================

%% Nur vorlaeufig: Das aktive "cns"

%% cns(X,L) : [type]
%% X : type
%% L : [type]

cns(X,L) :& tup(X|L).