%% Relfun-Batchfile "classic-funlib.bat"
%%
%% Illustration of the RELFUN-Prelude (classic-funlib.rfp)

%% 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. 


destroy

consult "classic-funlib"


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


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

odd(0)
odd(3)
odd(4)
odd(27)
odd(3.5)
odd(-2)

pause()


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

even(0)
even(3)
even(4)
even(27)
even(3.5)
even(-2)

pause()


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

sign(-3)
sign(-0.5)
sign(0)
sign(11)
sign(1.75)

pause()


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

-[-4](6)
-[11](3.5)

pause()


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

+[-4](6)
+[11](3.5)


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

*[-4](6)
*[11](3.5)

pause()


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

/[-4](6)
/[11](3.5)
/[0](4)

pause()


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

<[3.5](8)

<[8](3.5)

<[2](-1)

<[3](3)

pause()


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

<=[3.5](8)

<=[8](3.5)

<=[2](-1)

<=[3](3)

pause()


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

=[3.5](8)

=[8](3.5)

=[2](-1)

=[3](3)

pause()


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

/=[3.5](8)

/=[8](3.5)

/=[2](-1)

/=[3](3)

pause()


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

>[3.5](8)

>[8](3.5)

>[2](-1)

>[3](3)

pause()


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

>=[3.5](8)

>=[8](3.5)

>=[2](-1)

>=[3](3)

pause()



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


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

listp([])
listp([1,2,3])
listp(a)
listp(ctr[1,2])

pause()


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

null([])
null([1,2])

pause()


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

nth[2]([a,b,c,d,e,f,g])
nth[1]([a,b,c,d,e,f,g])
nth[7]([a,b,c,d,e,f,g])
nth[2]([])
nth[0]([a,b,c,d,e,f,g])
nth[8]([a,b,c,d,e,f,g])
nth[-2]([a,b,c,d,e,f,g])

pause()


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

thn[3]([a,b,c,d,e,f,g])
thn[1]([a,b,c,d,e,f,g])
thn[7]([a,b,c,d,e,f,g])
thn[2]([])
thn[0]([a,b,c,d,e,f,g])
thn[8]([a,b,c,d,e,f,g])
thn[-2]([a,b,c,d,e,f,g])

pause()


%% 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[3]([a,b,c,d,e,f,g])
nrest[1]([a,b,c,d,e,f,g])
nrest[7]([a,b,c,d,e,f,g])
nrest[0]([a,b,c,d,e,f,g])
nrest[0]([])
nrest[2]([])
nrest[8]([a,b,c,d,e,f,g])
nrest[-2]([a,b,c,d,e,f,g])

pause()


%% 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[3]([a,b,c,d,e,f,g])
restn[1]([a,b,c,d,e,f,g])
restn[7]([a,b,c,d,e,f,g])
restn[0]([a,b,c,d,e,f,g])
restn[0]([])
restn[2]([])
restn[8]([a,b,c,d,e,f,g])
restn[-2]([a,b,c,d,e,f,g])

pause()


%% 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[3]([a,b,c,d,e,f,g])
nstart[1]([a,b,c,d,e,f,g])
nstart[7]([a,b,c,d,e,f,g])
nstart[0]([a,b,c,d,e,f,g])
nstart[0]([])
nstart[2]([])
nstart[8]([a,b,c,d,e,f,g])
nstart[-2]([a,b,c,d,e,f,g])

pause()


%% 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[3]([a,b,c,d,e,f,g])
startn[1]([a,b,c,d,e,f,g])
startn[7]([a,b,c,d,e,f,g])
startn[0]([a,b,c,d,e,f,g])
startn[0]([])
startn[2]([])
startn[8]([a,b,c,d,e,f,g])
startn[-2]([a,b,c,d,e,f,g])

pause()


%% 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[2,5]([a,b,c,d,e,f,g])
sublist[1,7]([a,b,c,d,e,f,g])
sublist[2,2]([a,b,c,d,e,f,g])
sublist[5,2]([a,b,c,d,e,f,g])
sublist[5,0]([a,b,c,d,e,f,g])
sublist[0,2]([a,b,c,d,e,f,g])
sublist[1,8]([a,b,c,d,e,f,g])
sublist[-2,2]([a,b,c,d,e,f,g])
sublist[2,-2]([a,b,c,d,e,f,g])

pause()


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

rev([])
rev([a])
rev([a,b,c,d,e,f,g])

pause()


%% 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([])
append([a],[b,c,d],[e,f])
append([a],[b,c,d],[],[e,f],[])

pause()


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

member[2]([])
member[2]([1,3,4])
member[2]([1,2,3,4])

pause()


%% 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[2]([1,3,4])
remove[2]([1,2,3,4])
remove[2]([1,2,2,3,4])
remove[2]([2,1,2,3,2,4,2])

pause()


%% 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[2]([1,3,4])
remove-1th[2]([1,2,3,4])
remove-1th[2]([1,2,2,3,4])
remove-1th[2]([2,1,2,3,2,4,2])

pause()


%% 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[2]([1,3,4])
remove-1rest[2]([1,2,3,4])
remove-1rest[2]([1,2,2,3,4])
remove-1rest[2]([2,1,2,3,2,4,2])

pause()


%% 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([1,2,1,3,1,2,3])
remove-duplicates([])
remove-duplicates([1,2,3])

pause()


%% 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,a]([])
insert[1,a]([1,2,3,4,5])
insert[5,a]([1,2,3,4,5])
insert[3,a]([1,2,3,4,5])
insert[2,a]([])
insert[6,a]([1,2,3,4,5])
insert[0,a]([1,2,3,4,5])
insert[-1,a]([1,2,3,4,5])

pause()


%% 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[2,100]([a,b,c,d])
exchange[1,100]([a,b,c,d])
exchange[4,100]([a,b,c,d])
exchange[2,100]([])
exchange[2,100]([a])
exchange[0,100]([a,b,c,d])
exchange[5,100]([a,b,c,d])

pause()


%% 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[a,100]([])
substitute[a,100]([b,c,d])
substitute[a,100]([a,b,c,d])
substitute[a,100]([a,b,a,c,a,d,a])

pause()


%% 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([1,2,3,4],[a,b,c,d])
zip([1,2],[a,b,c,d])
zip([1,2,3,4],[a,b])

pause()


%% 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([])
unzip([[1,a],[2,b],[3,c],[4,d]])

pause()


%% 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[1+]([])
mapping[1+]([0])
mapping[1+]([0,10,20,30])

pause()


%% 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[1+](4,8)
tabulate[1+](4,4)
tabulate[1+](8,4)
tabulate[identity](-2,8)

pause()


%% 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[1+,4](10)
iterate[1+,0](10)
iterate[1+,-3](10)

pause()


%% 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[<[10]]([])
filter[<[10]]([12,15,-3,9,10,0,2])
filter[even]([12,6,21,0,3,2,88])

pause()


%% 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[<[10]]([12,15,-3,9,10,0,2])
partition[<[10]]([])
partition[<[10]]([1,2,3,4])
partition[<[10]]([10,11,12,13])
partition[even]([12,6,21,0,3,2,88])

pause()


%% 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 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[<[10]]([9,3,5,14,2])
split[<[10]]([12,15,-3,9,10,0,2])
split[<[10]]([1,2,3,4])
split[<[10]]([])
split[even]([12,6,21,0,3,2,88])

pause()


%% 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[<[10]]([12,15,-3,9,10,0,2])
some[<[10]]([10,11,12,13])
some[<[10]]([])
some[even]([12,6,21,0,3,2,88])

pause()


%% 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[<[10]]([12,15,-3,9,10,0,2])
every[<[10]]([1,2,3,4])
every[<[10]]([])
every[even]([12,6,21,0,3,2,88])

pause()


%% 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[<[10]]([12,15,-3,9,10,0,2])
find[<[10]]([])
find[<[10]]([10,11,12,13])
find[even]([12,6,21,0,3,2,88])
find[odd]([12,6,21,0,3,2,88])

pause()


%% 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[1-,1+,1+](3)

pause()


%% 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[<]([])
sort[>]([5,-1,4,7,3])
sort[<]([5,-1,4,7,3])

pause()


%% 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[<]([])
sorted-p[<]([1,3,5,11])
sorted-p[<]([1,5,3,11])
sorted-p[>]([1,3,5,11])

pause()


%% 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[<]([5,11,-3,6,-2])
min[>]([5,11,-3,6,-2])
min[>]([])

pause()


%% 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[>]([5,11,-3,6,-2])
max[<]([5,11,-3,6,-2])
max[>]([])

pause()


%% 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[-,0]([5,3,-7,2])  
foldl[max,0]([3,2,7,0,-1])
foldl[-,0]([])

pause()


%% 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[-,0]([5,3,-7,2])  
foldr[max,0]([3,2,7,0,-1])
foldr[-,0]([])

pause()



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


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

string=["aa"]("aa")  
string=["aa"]("bb")  

pause()



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


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

not(true)
not(false)

pause()


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

and(false,false) 
and(false,true)
and(true,false)
and(true,true) 

pause()


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

or(false,false) 
or(false,true) 
or(true,false)
or(true,true)

pause()


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

xor(false,false) 
xor(false,true) 
xor(true,false)
xor(true,true)

pause()


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

equiv(false,false)
equiv(false,true)
equiv(true,false)
equiv(true,true)

pause()


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

nand(false,false)
nand(false,true)
nand(true,false)
nand(true,true)

pause()


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

nor(false,false)
nor(false,true)
nor(true,false)
nor(true,true)

pause()



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


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

identity(a)
identity([a])

pause()


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

const[3]([a,b])

pause()


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

eq(1,1)
eq(1,2)
eq(1,[a,b])

pause()


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

neq(1,1)
neq(1,2)
neq(1,[a,b])

pause()


%% tup

tup(1|[])
tup(1,2|[3,4,5])

pause()


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

mgu([a,b],[a,b]) 
mgu([a,b],X)
mgu(ctr[a,X],ctr[Y,b])

pause()


%% pause()

pause()