rfi-p> exec classic-funlib

relfun
rfi-p> %% Relfun-Batchfile "classic-funlib.bat"
rfi-p> %%
rfi-p> %% Illustration of the RELFUN-Prelude (classic-funlib.rfp)
rfi-p> 
rfi-p> %% Christian Embacher
rfi-p> %% December 1, 1997
rfi-p> 
rfi-p> %% This module implements the basic library of RELFUN. It makes 
rfi-p> %% common-purpose operations on numbers, lists and other objects 
rfi-p> %% available. 
rfi-p> 
rfi-p> 
rfi-p> destroy
rfi-p> 
rfi-p> consult "classic-funlib"
Reading file "./classic-funlib.rfp"
rfi-p> 
rfi-p> 
rfi-p> %% PART I : Numbers
rfi-p> %% ================
rfi-p> 
rfi-p> 
rfi-p> %% odd(X) : Bool
rfi-p> %% X : Nat
rfi-p> %% No precondition.
rfi-p> %% Returns true if X is an odd number and false otherwise.
rfi-p> 
rfi-p> odd(0)
false
rfi-p> odd(3)
true
rfi-p> odd(4)
false
rfi-p> odd(27)
true
rfi-p> odd(3.5)
unknown
rfi-p> odd(-2)
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% even(X) : Bool
rfi-p> %% X : Nat
rfi-p> %% No precondition.
rfi-p> %% Returns true if X is an even number and false otherwise.
rfi-p> 
rfi-p> even(0)
true
rfi-p> even(3)
false
rfi-p> even(4)
true
rfi-p> even(27)
false
rfi-p> even(3.5)
unknown
rfi-p> even(-2)
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% sign(X) : Number
rfi-p> %% X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns -1 if X < 0, 0 if X = 0 and 1 if X > 0.
rfi-p> 
rfi-p> sign(-3)
-1
rfi-p> sign(-0.5)
-1
rfi-p> sign(0)
0
rfi-p> sign(11)
1
rfi-p> sign(1.75)
1
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% -[N](X) : Number
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns -(X,N).
rfi-p> 
rfi-p> -[-4](6)
10
rfi-p> -[11](3.5)
-7.5
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% +[N](X) : Number
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns +(X,N).
rfi-p> 
rfi-p> +[-4](6)
2
rfi-p> +[11](3.5)
14.5
rfi-p> 
rfi-p> 
rfi-p> %% *[N](X) : Number
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns *(X,N).
rfi-p> 
rfi-p> *[-4](6)
-24
rfi-p> *[11](3.5)
38.5
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% /[N](X) : Number
rfi-p> %% N, X : Number
rfi-p> %% Preconditions:
rfi-p> %%   * N /= 0.
rfi-p> %% Returns /(X,N).
rfi-p> 
rfi-p> /[-4](6)
-3/2
rfi-p> /[11](3.5)
0.3181818
rfi-p> /[0](4)
error - attempt to divide 4 by zero.
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% <[N](X) : Bool
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns true if X < N and false otherwise.
rfi-p> 
rfi-p> <[3.5](8)
false
rfi-p> 
rfi-p> <[8](3.5)
true
rfi-p> 
rfi-p> <[2](-1)
true
rfi-p> 
rfi-p> <[3](3)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% <=[N](X) : Bool
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns true if X <= N and false otherwise.
rfi-p> 
rfi-p> <=[3.5](8)
false
rfi-p> 
rfi-p> <=[8](3.5)
true
rfi-p> 
rfi-p> <=[2](-1)
true
rfi-p> 
rfi-p> <=[3](3)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% =[N](X) : Bool
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns true if X = N and false otherwise.
rfi-p> 
rfi-p> =[3.5](8)
false
rfi-p> 
rfi-p> =[8](3.5)
false
rfi-p> 
rfi-p> =[2](-1)
false
rfi-p> 
rfi-p> =[3](3)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% /=[N](X) : Bool
rfi-p> %% N, X : Number
rfi-p> %% No precondition.
rfi-p> %% Returns true if X /= N and false otherwise.
rfi-p> 
rfi-p> /=[3.5](8)
true
rfi-p> 
rfi-p> /=[8](3.5)
true
rfi-p> 
rfi-p> /=[2](-1)
true
rfi-p> 
rfi-p> /=[3](3)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% >[N](X) : Bool
rfi-p> %% N, X : Number   
rfi-p> %% No precondition.
rfi-p> %% Returns true if X > N and false otherwise.
rfi-p> 
rfi-p> >[3.5](8)
true
rfi-p> 
rfi-p> >[8](3.5)
false
rfi-p> 
rfi-p> >[2](-1)
false
rfi-p> 
rfi-p> >[3](3)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% >=[N](X) : Bool 
rfi-p> %% N, X : Number 
rfi-p> %% No precondition.
rfi-p> %% Returns true if X >= N and false otherwise.
rfi-p> 
rfi-p> >=[3.5](8)
true
rfi-p> 
rfi-p> >=[8](3.5)
false
rfi-p> 
rfi-p> >=[2](-1)
false
rfi-p> 
rfi-p> >=[3](3)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %% PART II : Lists
rfi-p> %% ===============
rfi-p> 
rfi-p> 
rfi-p> %% listp(X) : Bool
rfi-p> %% X : type
rfi-p> %% No precondition.
rfi-p> %% Returns true if X is a list and false otherwise.
rfi-p> 
rfi-p> listp([])
true
rfi-p> listp([1,2,3])
true
rfi-p> listp(a)
false
rfi-p> listp(ctr[1,2])
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% null(L) : Bool
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns true if L is empty and false otherwise.
rfi-p> 
rfi-p> null([])
true
rfi-p> null([1,2])
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% nth[N](L) : type
rfi-p> %% N : Nat
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * 0 < N <= length of L
rfi-p> %% Returns the Nth element of L.
rfi-p> 
rfi-p> nth[2]([a,b,c,d,e,f,g])
b
rfi-p> nth[1]([a,b,c,d,e,f,g])
a
rfi-p> nth[7]([a,b,c,d,e,f,g])
g
rfi-p> nth[2]([])
unknown
rfi-p> nth[0]([a,b,c,d,e,f,g])
unknown
rfi-p> nth[8]([a,b,c,d,e,f,g])
unknown
rfi-p> nth[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% thn[N](L) : type
rfi-p> %% N : Nat
rfi-p> %% L : [type] 
rfi-p> %% Preconditions:
rfi-p> %%   * 0 < N <= length of L
rfi-p> %% Returns the Nth last element of L.
rfi-p> 
rfi-p> thn[3]([a,b,c,d,e,f,g])
e
rfi-p> thn[1]([a,b,c,d,e,f,g])
g
rfi-p> thn[7]([a,b,c,d,e,f,g])
a
rfi-p> thn[2]([])
unknown
rfi-p> thn[0]([a,b,c,d,e,f,g])
unknown
rfi-p> thn[8]([a,b,c,d,e,f,g])
unknown
rfi-p> thn[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% nrest[N](L) : [type]
rfi-p> %% N : Nat 
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * N <= length of L.
rfi-p> %% Returns a list M which is built from L by removing the first 
rfi-p> %% N elements of L. The elements of M retain the same order they 
rfi-p> %% possess in L.
rfi-p> 
rfi-p> nrest[3]([a,b,c,d,e,f,g])
[d,e,f,g]
rfi-p> nrest[1]([a,b,c,d,e,f,g])
[b,c,d,e,f,g]
rfi-p> nrest[7]([a,b,c,d,e,f,g])
[]
rfi-p> nrest[0]([a,b,c,d,e,f,g])
[a,b,c,d,e,f,g]
rfi-p> nrest[0]([])
[]
rfi-p> nrest[2]([])
unknown
rfi-p> nrest[8]([a,b,c,d,e,f,g])
unknown
rfi-p> nrest[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% restn[N](L) : [type]
rfi-p> %% N : Nat
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * N <= length of L
rfi-p> %% Returns a list M which is built from L by removing the last 
rfi-p> %% N elements of L. The elements of M retain the same order they 
rfi-p> %% possess in L.
rfi-p> 
rfi-p> restn[3]([a,b,c,d,e,f,g])
[a,b,c,d]
rfi-p> restn[1]([a,b,c,d,e,f,g])
[a,b,c,d,e,f]
rfi-p> restn[7]([a,b,c,d,e,f,g])
[]
rfi-p> restn[0]([a,b,c,d,e,f,g])
[a,b,c,d,e,f,g]
rfi-p> restn[0]([])
[]
rfi-p> restn[2]([])
unknown
rfi-p> restn[8]([a,b,c,d,e,f,g])
unknown
rfi-p> restn[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% nstart[N](L) : [type]
rfi-p> %% N : Nat
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * N <= length of L.
rfi-p> %% Returns a list consisting of the first N elements of L in 
rfi-p> %% same order.
rfi-p> 
rfi-p> nstart[3]([a,b,c,d,e,f,g])
[a,b,c]
rfi-p> nstart[1]([a,b,c,d,e,f,g])
[a]
rfi-p> nstart[7]([a,b,c,d,e,f,g])
[a,b,c,d,e,f,g]
rfi-p> nstart[0]([a,b,c,d,e,f,g])
[]
rfi-p> nstart[0]([])
[]
rfi-p> nstart[2]([])
unknown
rfi-p> nstart[8]([a,b,c,d,e,f,g])
unknown
rfi-p> nstart[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% startn[N](L) : [type]
rfi-p> %% N : Nat
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * N <= length of L
rfi-p> %% Returns a list consisting of the last N elements of L in 
rfi-p> %% same order.
rfi-p> 
rfi-p> startn[3]([a,b,c,d,e,f,g])
[e,f,g]
rfi-p> startn[1]([a,b,c,d,e,f,g])
[g]
rfi-p> startn[7]([a,b,c,d,e,f,g])
[a,b,c,d,e,f,g]
rfi-p> startn[0]([a,b,c,d,e,f,g])
[]
rfi-p> startn[0]([])
[]
rfi-p> startn[2]([])
unknown
rfi-p> startn[8]([a,b,c,d,e,f,g])
unknown
rfi-p> startn[-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% sublist[X,Y](L) : [type]
rfi-p> %% X,Y : Nat
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * 0 < X 
rfi-p> %%   * Y <= length of L.
rfi-p> %% Returns a list consisting of the elements between the Xth and 
rfi-p> %% Yth element of L (inclusive) in same order if X <= Y. If X > Y 
rfi-p> %% the empty list is returned.
rfi-p> 
rfi-p> sublist[2,5]([a,b,c,d,e,f,g])
[b,c,d,e]
rfi-p> sublist[1,7]([a,b,c,d,e,f,g])
[a,b,c,d,e,f,g]
rfi-p> sublist[2,2]([a,b,c,d,e,f,g])
[b]
rfi-p> sublist[5,2]([a,b,c,d,e,f,g])
[]
rfi-p> sublist[5,0]([a,b,c,d,e,f,g])
[]
rfi-p> sublist[0,2]([a,b,c,d,e,f,g])
unknown
rfi-p> sublist[1,8]([a,b,c,d,e,f,g])
unknown
rfi-p> sublist[-2,2]([a,b,c,d,e,f,g])
unknown
rfi-p> sublist[2,-2]([a,b,c,d,e,f,g])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% rev(L) : [type]
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list consisting of the same elements as L but in 
rfi-p> %% reverse order.
rfi-p> 
rfi-p> rev([])
[]
rfi-p> rev([a])
[a]
rfi-p> rev([a,b,c,d,e,f,g])
[g,f,e,d,c,b,a]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% append(L1,...,Ln) : [type]
rfi-p> %% L1, ..., Ln : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns the list that is built from L by appending L1, ..., Ln
rfi-p> %% together in the same order they possess in L.
rfi-p> 
rfi-p> append([])
[]
rfi-p> append([a],[b,c,d],[e,f])
[a,b,c,d,e,f]
rfi-p> append([a],[b,c,d],[],[e,f],[])
[a,b,c,d,e,f]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% member[X](L) : Bool
rfi-p> %% X : type
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns true if X is an element of L and false otherwise.
rfi-p> 
rfi-p> member[2]([])
false
rfi-p> member[2]([1,3,4])
false
rfi-p> member[2]([1,2,3,4])
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% remove[X](L) : [type]
rfi-p> %% X : type
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list M which is built from L by removing all 
rfi-p> %% occurrences of X in L. The elements of M retain the same relative
rfi-p> %% order they possess in L.
rfi-p> 
rfi-p> remove[2]([1,3,4])
[1,3,4]
rfi-p> remove[2]([1,2,3,4])
[1,3,4]
rfi-p> remove[2]([1,2,2,3,4])
[1,3,4]
rfi-p> remove[2]([2,1,2,3,2,4,2])
[1,3,4]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% remove-1th[X](L) : [type]
rfi-p> %% X : type 
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list M which is built from L by removing the first 
rfi-p> %% occurrence of X in L. The elements of M retain the same relative 
rfi-p> %% order they possess in L.
rfi-p> 
rfi-p> remove-1th[2]([1,3,4])
[1,3,4]
rfi-p> remove-1th[2]([1,2,3,4])
[1,3,4]
rfi-p> remove-1th[2]([1,2,2,3,4])
[1,2,3,4]
rfi-p> remove-1th[2]([2,1,2,3,2,4,2])
[1,2,3,2,4,2]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% remove-1rest[X](L) : [type]
rfi-p> %% X : type 
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list M which is built from L by removing all 
rfi-p> %% occurrences of X in L but the first. The elements of M retain 
rfi-p> %% the same relative order they possess in L.
rfi-p> 
rfi-p> remove-1rest[2]([1,3,4])
[1,3,4]
rfi-p> remove-1rest[2]([1,2,3,4])
[1,2,3,4]
rfi-p> remove-1rest[2]([1,2,2,3,4])
[1,2,3,4]
rfi-p> remove-1rest[2]([2,1,2,3,2,4,2])
[2,1,3,4]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% remove-duplicates(L) : [type]
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list M which is built from L by removing all multiple 
rfi-p> %% occcurences of all elements in L. The elements of M retain the 
rfi-p> %% same relative order they possess in L.
rfi-p> 
rfi-p> remove-duplicates([1,2,1,3,1,2,3])
[1,2,3]
rfi-p> remove-duplicates([])
[]
rfi-p> remove-duplicates([1,2,3])
[1,2,3]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% insert[N,X](L) : [type]
rfi-p> %% N : Nat
rfi-p> %% X : type
rfi-p> %% Preconditions:
rfi-p> %%   + N = 0 if L is empty.
rfi-p> %%   + 0 < N <= length of L if L is not empty.
rfi-p> %% Returns the list [X] if L is empty.. 
rfi-p> %% Otherwise it returns a list which is built from L by inserting X
rfi-p> %% between the (N-1)th and the Nth element of L.
rfi-p> 
rfi-p> insert[0,a]([])
[a]
rfi-p> insert[1,a]([1,2,3,4,5])
[a,1,2,3,4,5]
rfi-p> insert[5,a]([1,2,3,4,5])
[1,2,3,4,a,5]
rfi-p> insert[3,a]([1,2,3,4,5])
[1,2,a,3,4,5]
rfi-p> insert[2,a]([])
unknown
rfi-p> insert[6,a]([1,2,3,4,5])
unknown
rfi-p> insert[0,a]([1,2,3,4,5])
unknown
rfi-p> insert[-1,a]([1,2,3,4,5])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% exchange[N,X](L) : [type]
rfi-p> %% N : Nat
rfi-p> %% X : type 
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * L is not empty
rfi-p> %%   * 0 < N <= length of L
rfi-p> %% Returns a list which is built from L by replacing the Nth 
rfi-p> %% element of L by X.
rfi-p> 
rfi-p> exchange[2,100]([a,b,c,d])
[a,100,c,d]
rfi-p> exchange[1,100]([a,b,c,d])
[100,b,c,d]
rfi-p> exchange[4,100]([a,b,c,d])
[a,b,c,100]
rfi-p> exchange[2,100]([])
unknown
rfi-p> exchange[2,100]([a])
unknown
rfi-p> exchange[0,100]([a,b,c,d])
unknown
rfi-p> exchange[5,100]([a,b,c,d])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% substitute[X,Y](L) : [type]
rfi-p> %% X,Y : type 
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list which is built from L by replacing all occurrences
rfi-p> %% of X in L by Y.
rfi-p> 
rfi-p> substitute[a,100]([])
[]
rfi-p> substitute[a,100]([b,c,d])
[b,c,d]
rfi-p> substitute[a,100]([a,b,c,d])
[100,b,c,d]
rfi-p> substitute[a,100]([a,b,a,c,a,d,a])
[100,b,100,c,100,d,100]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% zip(L1,L2) : [<type1,type2>]
rfi-p> %% L1 : [type1]
rfi-p> %% L2 : [type2]
rfi-p> %% Preconditions:
rfi-p> %%   * L1 and L2 are both of the same length.
rfi-p> %% Returns a list M of length of L1 and L2. For every i the ith 
rfi-p> %% element of M is [X,Y] iff the ith element of L1 is X and the ith 
rfi-p> %% element of L2 is Y.
rfi-p> 
rfi-p> zip([],[])
[]
rfi-p> zip([1,2,3,4],[a,b,c,d])
[[1,a],[2,b],[3,c],[4,d]]
rfi-p> zip([1,2],[a,b,c,d])
unknown
rfi-p> zip([1,2,3,4],[a,b])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% unzip(L) : <[type1],[type2]>
rfi-p> %% L : [<type1,type2>]
rfi-p> %% No precondition.
rfi-p> %% Returns a Pair [L1,L2] of lists that has the same length as L. 
rfi-p> %% For every i the ith element of L1 is X and the ith element of L2 
rfi-p> %% is Y iff the ith element of L is [X,Y].
rfi-p> 
rfi-p> unzip([])
[[],[]]
rfi-p> unzip([[1,a],[2,b],[3,c],[4,d]])
[[1,2,3,4],[a,b,c,d]]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% mapping[F](L) : [type2]
rfi-p> %% F : type1 --> type2
rfi-p> %% L : [type1] 
rfi-p> %% No precondition.
rfi-p> %% Returns a list M of length of L such that for every i the ith 
rfi-p> %% element of M is the result F(X) of applying F to the ith element 
rfi-p> %% X of L.
rfi-p> 
rfi-p> mapping[1+]([])
[]
rfi-p> mapping[1+]([0])
[1]
rfi-p> mapping[1+]([0,10,20,30])
[1,11,21,31]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% tabulate[F](X,Y) : [type]
rfi-p> %% F : Integer --> type
rfi-p> %% X,Y : Integer
rfi-p> %% No precondition.
rfi-p> %% Returns the list [F(X), F(X+1), ..., F(Y)] if X <= Y 
rfi-p> %% and [] otherwise.
rfi-p> 
rfi-p> tabulate[1+](4,8)
[5,6,7,8,9]
rfi-p> tabulate[1+](4,4)
[5]
rfi-p> tabulate[1+](8,4)
[]
rfi-p> tabulate[identity](-2,8)
[-2,-1,0,1,2,3,4,5,6,7,8]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% iterate[F,N](X) : [type]
rfi-p> %% F : type --> type
rfi-p> %% N : Nat
rfi-p> %% X : type
rfi-p> %% No preconditions
rfi-p> %% Returns a list M consisiting of the first N+1 Iterations of F 
rfi-p> %% over X, i.e. M:=[X,F^1(X),...,F^N(X)].
rfi-p> 
rfi-p> iterate[1+,4](10)
[10,11,12,13,14]
rfi-p> iterate[1+,0](10)
[10]
rfi-p> iterate[1+,-3](10)
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% filter[P](L) : [type]
rfi-p> %% P : type --> Bool 
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a list M which consists of exactly those elements X of L
rfi-p> %% for which P(X) evaluates true. The elements of M retain the same 
rfi-p> %% relative order they possess in L.
rfi-p> 
rfi-p> filter[<[10]]([])
[]
rfi-p> filter[<[10]]([12,15,-3,9,10,0,2])
[-3,9,0,2]
rfi-p> filter[even]([12,6,21,0,3,2,88])
[12,6,0,2,88]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% partition[P](L) : <[type],[type]>
rfi-p> %% P : type --> bool
rfi-p> %% L : [type]
rfi-p> %% Applies P to each element of L, from left to right, and returns a
rfi-p> %% pair [Pos, Neg] where Pos is the list of those X of L for which 
rfi-p> %% P(X) evaluated to true, and Neg is the list of those X in L for 
rfi-p> %% which P(X) evaluated to false. The elements of Pos and Neg retain
rfi-p> %% the same relative order they possess in L.
rfi-p> 
rfi-p> partition[<[10]]([12,15,-3,9,10,0,2])
[[-3,9,0,2],[12,15,10]]
rfi-p> partition[<[10]]([])
[[],[]]
rfi-p> partition[<[10]]([1,2,3,4])
[[1,2,3,4],[]]
rfi-p> partition[<[10]]([10,11,12,13])
[[],[10,11,12,13]]
rfi-p> partition[even]([12,6,21,0,3,2,88])
[[12,6,0,2,88],[21,3]]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% split[P](L) : <[type],[type]>
rfi-p> %% P : type --> bool
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns a pair [Only-pos,With-neg]. Only-pos is the longest 
rfi-p> %% prefix of L that contains only elements X of L for which P(X) 
rfi-p> %% evaluates true. With-neg is the suffix of L which starts with 
rfi-p> %% the first element Y of L for which P(Y) evaluates false. 
rfi-p> %% It is L = Only-pos ++ With-neg.     
rfi-p> 
rfi-p> split[<[10]]([9,3,5,14,2])
[[9,3,5],[14,2]]
rfi-p> split[<[10]]([12,15,-3,9,10,0,2])
[[],[12,15,-3,9,10,0,2]]
rfi-p> split[<[10]]([1,2,3,4])
[[1,2,3,4],[]]
rfi-p> split[<[10]]([])
[[],[]]
rfi-p> split[even]([12,6,21,0,3,2,88])
[[12,6],[21,0,3,2,88]]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% some[P](L) : Bool
rfi-p> %% P : type --> Bool 
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns true if P(X) evaluates true for (at least) one element of
rfi-p> %% L and false otherwise.
rfi-p> 
rfi-p> some[<[10]]([12,15,-3,9,10,0,2])
true
rfi-p> some[<[10]]([10,11,12,13])
false
rfi-p> some[<[10]]([])
false
rfi-p> some[even]([12,6,21,0,3,2,88])
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% every[P](L) : Bool
rfi-p> %% P : type --> Bool
rfi-p> %% L : [type]
rfi-p> %% No precondition.
rfi-p> %% Returns true if P(X) evaluates true for each element of L and 
rfi-p> %% false otherwise.
rfi-p> 
rfi-p> every[<[10]]([12,15,-3,9,10,0,2])
false
rfi-p> every[<[10]]([1,2,3,4])
true
rfi-p> every[<[10]]([])
true
rfi-p> every[even]([12,6,21,0,3,2,88])
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% find[P](L) : type
rfi-p> %% P : type --> Bool
rfi-p> %% L : [type]
rfi-p> %% Applies P to each element X of the L, from left to right, and 
rfi-p> %% returns the first X for which P(X) evaluates true. Returns 'none' 
rfi-p> %% if F(X) evaluates false for each element X of L.
rfi-p> 
rfi-p> find[<[10]]([12,15,-3,9,10,0,2])
-3
rfi-p> find[<[10]]([])
none
rfi-p> find[<[10]]([10,11,12,13])
none
rfi-p> find[even]([12,6,21,0,3,2,88])
12
rfi-p> find[odd]([12,6,21,0,3,2,88])
21
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% mcompose[F_1,F_2,...,F_N](X) : type_1
rfi-p> %% F_1  : type_2 --> type_1
rfi-p> %% F_2  : type_3 --> type_2
rfi-p> %% ...
rfi-p> %% F_N-1: type_N --> type_N-1
rfi-p> %% F_N  : type_X --> type_N
rfi-p> %% X   : type_X
rfi-p> %% Preconditions:
rfi-p> %%   * N > 0
rfi-p> %% Returns F_1(F_2(...F_N(X)...))
rfi-p> 
rfi-p> mcompose[1-,1+,1+](3)
4
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% sort[P](L) : [type]
rfi-p> %% P : type type --> Bool
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * P is a total order.
rfi-p> %% Sorts L in ascending order w.r.t. P, i.e. returns a list 
rfi-p> %% consisting of exactly the elements of L in ascending order 
rfi-p> %% w.r.t. P.
rfi-p> 
rfi-p> sort[<]([])
[]
rfi-p> sort[>]([5,-1,4,7,3])
[7,5,4,3,-1]
rfi-p> sort[<]([5,-1,4,7,3])
[-1,3,4,5,7]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% sorted-p[P](L) : Bool
rfi-p> %% P : type type --> Bool
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * P is a total order.
rfi-p> %% Returns true if the elements of L are in ascending order w.r.t. P.
rfi-p> 
rfi-p> sorted-p[<]([])
true
rfi-p> sorted-p[<]([1,3,5,11])
true
rfi-p> sorted-p[<]([1,5,3,11])
false
rfi-p> sorted-p[>]([1,3,5,11])
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% min[P](L) : type
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * P is a total order.
rfi-p> %%   * L is not empty.
rfi-p> %% Returns the P-minimum of L, i.e. the element X of L for which
rfi-p> %% P(X,Y) holds true for every other Y of L.
rfi-p> 
rfi-p> min[<]([5,11,-3,6,-2])
-3
rfi-p> min[>]([5,11,-3,6,-2])
11
rfi-p> min[>]([])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% max[P](L) : type
rfi-p> %% L : [type]
rfi-p> %% Preconditions:
rfi-p> %%   * P is a total order.
rfi-p> %%   * L is not empty.
rfi-p> %% Returns the P-maximum of L, i.e. the element Y of L for which
rfi-p> %% P(X,Y) holds true for every other X of L.
rfi-p> 
rfi-p> max[>]([5,11,-3,6,-2])
-3
rfi-p> max[<]([5,11,-3,6,-2])
11
rfi-p> max[>]([])
unknown
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% foldl[F,X](L) : type2
rfi-p> %% F : (type1 type2) --> type2
rfi-p> %% X : type2
rfi-p> %% L : [type1]
rfi-p> %% No precondition.
rfi-p> %% Returns F(Xn,...,F(X2, F(X1, X))...) if L=[X1,X2,...,Xn] is not 
rfi-p> %% empty and X if L is empty. 
rfi-p> 
rfi-p> foldl[-,0]([5,3,-7,2])  
7
rfi-p> foldl[max,0]([3,2,7,0,-1])
7
rfi-p> foldl[-,0]([])
0
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% foldr[F,X](L) : type2
rfi-p> %% F : (type1 type2) --> type2
rfi-p> %% X : type2
rfi-p> %% L : [type1]
rfi-p> %% No precondition.
rfi-p> %% Returns F(X1, F(X2,...,F(Xn,X)...)) if L=[X1,X2,...,Xn] is not 
rfi-p> %% empty and X if L is empty. 
rfi-p> 
rfi-p> foldr[-,0]([5,3,-7,2])  
-7
rfi-p> foldr[max,0]([3,2,7,0,-1])
7
rfi-p> foldr[-,0]([])
0
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %% PART III : Strings
rfi-p> %% ==================
rfi-p> 
rfi-p> 
rfi-p> %% string=[St1](St2) : Bool
rfi-p> %% St1,St2 : String
rfi-p> %% Returns true if St1 and St2 are the same strings and false 
rfi-p> %% otherwise.
rfi-p> 
rfi-p> string=["aa"]("aa")  
true
rfi-p> string=["aa"]("bb")  
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %% PART IV : Boolean algebra
rfi-p> %% =========================
rfi-p> 
rfi-p> 
rfi-p> %% not(X) : Bool
rfi-p> %% X : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (not X).
rfi-p> 
rfi-p> not(true)
false
rfi-p> not(false)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% and(X,Y) : Bool
rfi-p> %% X,Y : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X and Y).
rfi-p> 
rfi-p> and(false,false) 
false
rfi-p> and(false,true)
false
rfi-p> and(true,false)
false
rfi-p> and(true,true) 
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% or(X,Y) : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X or Y).
rfi-p> %% X,Y : Bool
rfi-p> 
rfi-p> or(false,false) 
false
rfi-p> or(false,true) 
true
rfi-p> or(true,false)
true
rfi-p> or(true,true)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% xor(X,Y) : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X xor Y).
rfi-p> %% X,Y : Bool
rfi-p> 
rfi-p> xor(false,false) 
false
rfi-p> xor(false,true) 
true
rfi-p> xor(true,false)
true
rfi-p> xor(true,true)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% equiv(X,Y) : Bool
rfi-p> %% X,Y : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X equiv Y).
rfi-p> 
rfi-p> equiv(false,false)
true
rfi-p> equiv(false,true)
false
rfi-p> equiv(true,false)
false
rfi-p> equiv(true,true)
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% nand(X,Y) : Bool
rfi-p> %% X,Y : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X nand Y).
rfi-p> 
rfi-p> nand(false,false)
true
rfi-p> nand(false,true)
true
rfi-p> nand(true,false)
true
rfi-p> nand(true,true)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% nor(X,Y) : Bool
rfi-p> %% X,Y : Bool
rfi-p> %% No precondition.
rfi-p> %% Returns the value of (X nor Y).
rfi-p> 
rfi-p> nor(false,false)
true
rfi-p> nor(false,true)
false
rfi-p> nor(true,false)
false
rfi-p> nor(true,true)
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %% PART V : Misc
rfi-p> %% =============
rfi-p> 
rfi-p> 
rfi-p> %% identity(X) : type
rfi-p> %% X : type
rfi-p> %% No precondition.
rfi-p> %% Returns X.
rfi-p> 
rfi-p> identity(a)
a
rfi-p> identity([a])
[a]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% const[X](Y) : type1
rfi-p> %% X : type1
rfi-p> %% Y : type2
rfi-p> %% No precondition.
rfi-p> %% Returns X.
rfi-p> 
rfi-p> const[3]([a,b])
3
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% eq(X,Y) : Bool
rfi-p> %% X : type1
rfi-p> %% Y : type2
rfi-p> %% No precondition.
rfi-p> %% Returns true if X and Y are identical and false otherwise.
rfi-p> 
rfi-p> eq(1,1)
true
rfi-p> eq(1,2)
false
rfi-p> eq(1,[a,b])
false
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% neq(X,Y) : Bool
rfi-p> %% X : type1
rfi-p> %% Y : type2
rfi-p> %% No precondition.
rfi-p> %% Returns false if X and Y are identical and true otherwise.
rfi-p> 
rfi-p> neq(1,1)
false
rfi-p> neq(1,2)
true
rfi-p> neq(1,[a,b])
true
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% tup
rfi-p> 
rfi-p> tup(1|[])
[1]
rfi-p> tup(1,2|[3,4,5])
[1,2,3,4,5]
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% mgu(X,Y) : type1 | type2 
rfi-p> %% X : type1
rfi-p> %% Y : type2
rfi-p> 
rfi-p> mgu([a,b],[a,b]) 
[a,b]
rfi-p> mgu([a,b],X)
[a,b]
X=[a,b]
rfi-p> mgu(ctr[a,X],ctr[Y,b])
ctr[a,b]
Y=a
X=b
rfi-p> 
rfi-p> pause()
true
rfi-p> 
rfi-p> 
rfi-p> %% pause()
rfi-p> 
rfi-p> pause() 
true
rfi-p> bye

relfun