List processing

Usage:nonsingle(X)

X is not a singleton.

Test:nonsingle(A)

nonsingle fails.

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[a]
  then the following properties should hold globally:
  (native_props:fails/1)Calls of the form nonsingle(A) fail.

Test:nonsingle(A)

nonsingle succeeds.

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[a,b]

Usage:append(Xs,Ys,Zs)

• Call and exit should be compatible with:
  (basic_props:list/1)Xs is a list.
  (basic_props:list/1)Ys is a list.
  (basic_props:list/1)Zs is a list.

Check:append(Xs,Ys,Zs)

Zs is Ys appended to Xs.

• The following properties should hold upon exit:
  (basic_props:list/1)Xs is a list.

Check:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (basic_props:list/1)Xs is a list.
  (basic_props:list/1)Ys is a list.
  then the following properties should hold upon exit:
  (basic_props:list/1)Zs is a list.

Check:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (basic_props:list/1)Zs is a list.
  then the following properties should hold upon exit:
  (basic_props:list/1)Xs is a list.
  (basic_props:list/1)Ys is a list.

Check:append(Xs,Ys,Zs)

• The following properties should hold upon exit:
  (native_props:mshare/1)The sharing pattern is [[X,Y,Z],[X,Z],[Y,Z]].

Check:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (term_typing:ground/1)Xs is currently ground (it contains no variables).
  (term_typing:ground/1)Ys is currently ground (it contains no variables).
  then the following properties should hold upon exit:
  (term_typing:ground/1)Zs is currently ground (it contains no variables).

Check:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (term_typing:ground/1)Zs is currently ground (it contains no variables).
  then the following properties should hold upon exit:
  (term_typing:ground/1)Xs is currently ground (it contains no variables).
  (term_typing:ground/1)Ys is currently ground (it contains no variables).

True:append(Xs,Ys,Zs)

• The following properties hold globally:
  (basic_props:sideff/2)append(Xs,Ys,Zs) is side-effect free.

True:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (basic_props:list/1)Xs is a list.
  then the following properties hold globally:
  (basic_props:eval/1)append(Xs,Ys,Zs) is evaluable at compile-time.

True:append(Xs,Ys,Zs)

• If the following properties hold at call time:
  (basic_props:list/1)Zs is a list.
  then the following properties hold globally:
  (basic_props:eval/1)append(Xs,Ys,Zs) is evaluable at compile-time.

Test:append(A,B,C)

Simple call to append

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[1,2,3]
  (term_basic:= /2)term_basic:B=[4,5]
  then the following properties should hold upon exit:
  (term_basic:= /2)term_basic:C=[1,2,3,4,5]

Test:append(A,B,X)

Simple append test

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:L=[([1,2],[1,2,4,5,6]),([1,2,3],[1,2,3,4,5,6])]
  (term_basic:= /2)term_basic:B=[4,5,6]
  (basic_props:member/2)A,X2 is an element of L.
  then the following properties should hold upon exit:
  (term_compare:== /2)The terms X and X2 are strictly identical.

Test:append(A,B,X)

Test of reverse call

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:X=[1,2,3]
  then the following properties should hold upon exit:
  (basic_props:member/2)A,B is an element of [([],[1,2,3]),([1],[2,3]),([1,2],[3]),([1,2,3],[])].

Test:append(A,B,X)

Empty test.

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[]
  (term_basic:= /2)term_basic:B=[]
  then the following properties should hold upon exit:
  (term_compare:== /2)The terms X and [] are strictly identical.

Test:append(_A,B,X)

Test of a call that fails

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:B=[2]
  (term_basic:= /2)term_basic:X=[1,2,3]
  then the following properties should hold globally:
  (native_props:fails/1)Calls of the form append(_A,B,X) fail.

Test:append(X,Y,Z)

Test of a reverse call.

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:Y=[2]
  (term_basic:= /2)term_basic:Z=[1,2]
  then the following properties should hold upon exit:
  (term_compare:== /2)The terms X and [1] are strictly identical.

Usage:reverse(Xs,Ys)

Reverses the order of elements in Xs.

• The following properties should hold at call time:
  (basic_props:list/1)Xs is a list.
  (basic_props:term/1)Ys is any term.
• The following properties should hold upon exit:
  (basic_props:list/1)Xs is a list.
  (basic_props:list/1)Ys is a list.

Test:reverse(A,B)

Reverse a list

• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[1,2,3]
  then the following properties should hold upon exit:
  (term_basic:= /2)term_basic:B=[3,2,1]

True:

• The following properties hold globally:
  (basic_props:sideff/2)reverse(Arg1,Arg2) is side-effect free.

True:reverse(Xs,_Ys)

• If the following properties hold at call time:
  (basic_props:list/1)Xs is a list.
  then the following properties hold globally:
  (basic_props:eval/1)reverse(Xs,_Ys) is evaluable at compile-time.

Usage:reverse(A,B,C)

Reverse the order of elements in A, and append it with B.

Test:reverse(A,B,C)

reverse/3 test

• Call and exit should be compatible with:
  (term_typing:var/1)B is a free variable.
• If the following properties should hold at call time:
  (term_basic:= /2)term_basic:A=[1,2,3]
  then the following properties should hold upon exit:
  (term_basic:= /2)term_basic:C=[3,2,1|B]

Trust:

• The following properties hold globally:
  (basic_props:sideff/2)reverse(Arg1,Arg2,Arg3) is side-effect free.

Trust:reverse(Xs,Ys,Zs)

• If the following properties hold at call time:
  (basic_props:list/1)Xs is a list.
  (basic_props:list/1)Ys is a list.
  then the following properties hold globally:
  (basic_props:eval/1)reverse(Xs,Ys,Zs) is evaluable at compile-time.

Usage:delete(L1,E,L2)

L2 is L1 without the ocurrences of E.

• The following properties should hold upon exit:
  (basic_props:list/1)L1 is a list.
  (basic_props:list/1)L2 is a list.

True:

• The following properties hold globally:
  (basic_props:sideff/2)delete(Arg1,Arg2,Arg3) is side-effect free.

True:delete(L1,E,L2)

• If the following properties hold at call time:
  (term_typing:ground/1)L1 is currently ground (it contains no variables).
  (term_typing:ground/1)L2 is currently ground (it contains no variables).
  then the following properties hold globally:
  (basic_props:eval/1)delete(L1,E,L2) is evaluable at compile-time.

Usage:delete_non_ground(L1,E,L2)

L2 is L1 without the ocurrences of E. E can be a nonground term so that all the elements in L1 it unifies with will be deleted

• The following properties should hold upon exit:
  (basic_props:list/1)L1 is a list.
  (basic_props:list/1)L2 is a list.

True:

• The following properties hold globally:
  (basic_props:sideff/2)delete_non_ground(Arg1,Arg2,Arg3) is side-effect true.

True:delete_non_ground(L1,E,L2)

• If the following properties hold at call time:
  (term_typing:ground/1)L1 is currently ground (it contains no variables).
  (term_typing:ground/1)L2 is currently ground (it contains no variables).
  then the following properties hold globally:
  (basic_props:eval/1)delete_non_ground(L1,E,L2) is evaluable at compile-time.

Usage:select(X,Xs,Ys)

Xs and Ys have the same elements except for one occurrence of X.

True:

• The following properties hold globally:
  (basic_props:sideff/2)select(Arg1,Arg2,Arg3) is side-effect free.

True:select(X,Xs,Ys)

• If the following properties hold at call time:
  (term_typing:ground/1)X is currently ground (it contains no variables).
  (term_typing:ground/1)Xs is currently ground (it contains no variables).
  then the following properties hold globally:
  (basic_props:eval/1)select(X,Xs,Ys) is evaluable at compile-time.

Usage 1:length(L,N)

Computes the length of L.

• The following properties should hold at call time:
  (basic_props:list/1)L is a list.
  (term_typing:var/1)N is a free variable.
• The following properties should hold upon exit:
  (basic_props:list/1)L is a list.
  (basic_props:int/1)N is an integer.

Usage 2:length(L,N)

Outputs L of length N.

• The following properties should hold at call time:
  (term_typing:var/1)L is a free variable.
  (basic_props:int/1)N is an integer.
• The following properties should hold upon exit:
  (basic_props:list/1)L is a list.
  (basic_props:int/1)N is an integer.

Usage 3:length(L,N)

Checks that L is of length N.

• The following properties should hold at call time:
  (basic_props:list/1)L is a list.
  (basic_props:int/1)N is an integer.
• The following properties should hold upon exit:
  (basic_props:list/1)L is a list.
  (basic_props:int/1)N is an integer.

True:length(A,B)

• The following properties hold globally:
  (basic_props:native/1)This predicate is understood natively by CiaoPP.

True:

• The following properties hold globally:
  (basic_props:sideff/2)length(Arg1,Arg2) is side-effect free.

True:length(L,N)

• If the following properties hold at call time:
  (basic_props:list/1)L is a list.
  then the following properties hold globally:
  (basic_props:eval/1)length(L,N) is evaluable at compile-time.

True:length(L,N)

• If the following properties hold at call time:
  (term_typing:integer/1)N is currently instantiated to an integer.
  then the following properties hold globally:
  (basic_props:eval/1)length(L,N) is evaluable at compile-time.

N is the position in List of Elem. N counts from one.

Usage 1:

Unifies Elem and the Nth element of List.

• Call and exit should be compatible with:
  (basic_props:list/1)List is a list.
  (basic_props:term/1)Elem is any term.
• The following properties should hold at call time:
  (basic_props:int/1)N is an integer.
• The following properties should hold upon exit:
  (basic_props:list/1)List is a list.
  (basic_props:term/1)Elem is any term.

Usage 2:

Finds the positions where Elem is in List. Positions are found in ascending order.

• Call and exit should be compatible with:
  (basic_props:list/1)List is a list.
  (basic_props:term/1)Elem is any term.
• The following properties should hold at call time:
  (term_typing:var/1)N is a free variable.
• The following properties should hold upon exit:
  (basic_props:int/1)N is an integer.
  (basic_props:list/1)List is a list.
  (basic_props:term/1)Elem is any term.

Trust:

• The following properties hold globally:
  (basic_props:sideff/2)nth(N,List,Elem) is side-effect free.

Trust:nth(N,L,E)

• If the following properties hold at call time:
  (term_typing:integer/1)N is currently instantiated to an integer.
  then the following properties hold globally:
  (basic_props:eval/1)nth(N,L,E) is evaluable at compile-time.

Trust:nth(N,L,E)

• If the following properties hold at call time:
  (basic_props:list/1)L is a list.
  then the following properties hold globally:
  (basic_props:eval/1)nth(N,L,E) is evaluable at compile-time.

Trust:nth(N,L,E)

• If the following properties hold at call time:
  (basic_props:int/1)N is an integer.
  (basic_props:list/1)L is a list.
  then the following properties hold globally:
  (native_props:is_det/1)All calls of the form nth(N,L,E) are deterministic.

Usage:add_after(L0,E0,E,L)

Adds element E after element E0 (or at end) to list L0 returning in L the new list (uses term comparison).

• The following properties should hold at call time:
  (term_typing:nonvar/1)L0 is currently a term which is not a free variable.
  (term_typing:nonvar/1)E0 is currently a term which is not a free variable.
  (term_typing:nonvar/1)E is currently a term which is not a free variable.
  (term_typing:var/1)L is a free variable.

Usage:add_before(L0,E0,E,L)

Adds element E before element E0 (or at start) to list L0 returning in L the new list (uses term comparison).

• The following properties should hold at call time:
  (term_typing:nonvar/1)L0 is currently a term which is not a free variable.
  (term_typing:nonvar/1)E0 is currently a term which is not a free variable.
  (term_typing:nonvar/1)E is currently a term which is not a free variable.
  (term_typing:var/1)L is a free variable.

Usage:list1(X,Y)

X is a list of Ys of at least one element.

Usage:dlist(List,DList,Tail)

List is the result of removing Tail from the end of DList (makes a difference list from a list).

Usage:list_concat(LL,L)

L is the concatenation of all the lists in LL.

• The following properties should hold at call time:
  (basic_props:list/2)LL is a list of lists.
• The following properties should hold upon exit:
  (basic_props:list/1)L is a list.

Usage:list_insert(List,Term)

Adds Term to the end of List if there is no element in List identical to Term.

• The following properties should hold at call time:
  (term_typing:nonvar/1)Term is currently a term which is not a free variable.

Usage:insert_last(L0,E,L)

Adds element E at end of list L0 returning L.

• The following properties should hold at call time:
  (term_typing:nonvar/1)L0 is currently a term which is not a free variable.
  (term_typing:nonvar/1)E is currently a term which is not a free variable.

Usage:

Impure membership (does not instantiate a variable in its first argument.

Usage:

First membership.

Usage:nocontainsx(L,X)

X is not identical to any element of L.

Usage:last(L,X)

X is the last element of list L.

Usage:list_lookup(List,Key,Value)

Same as list_lookup/4, but use -/2 as functor.

Usage:list_lookup(List,Functor,Key,Value)

Look up Functor(Key,Value) pair in variable ended key-value pair list L or else add it at the end.

Usage:intset_insert(A,B,Set)

Insert the element B in the ordered set of numbers A.

Usage:intset_delete(A,B,Set)

Delete from the ordered set A the element B.

Usage:intset_in(E,Set)

Succeds iff E is element of Set

Usage:intset_sequence(N,L1,L2)

Generates an ordered set of numbers from 0 to N-1, and append it to L1.

Usage:intersection(List1,List2,List)

List has the elements which are both in List1 and List2.

• The following properties should hold at call time:
  (term_typing:nonvar/1)List1 is currently a term which is not a free variable.
  (term_typing:nonvar/1)List2 is currently a term which is not a free variable.
  (basic_props:list/1)List1 is a list.
  (basic_props:list/1)List2 is a list.
• The following properties should hold upon exit:
  (basic_props:list/1)List is a list.

Usage:union(List1,List2,List)

List has the elements which are in List1 followed by the elements which are in List2 but not in List1.

• The following properties should hold at call time:
  (term_typing:nonvar/1)List1 is currently a term which is not a free variable.
  (term_typing:nonvar/1)List2 is currently a term which is not a free variable.
  (term_typing:var/1)List is a free variable.
  (basic_props:list/1)List1 is a list.
  (basic_props:list/1)List2 is a list.
• The following properties should hold upon exit:
  (basic_props:list/1)List is a list.

Usage:difference(List1,List2,List)

List has the elements which are in List1 but not in List2.

• The following properties should hold at call time:
  (term_typing:nonvar/1)List1 is currently a term which is not a free variable.
  (term_typing:nonvar/1)List2 is currently a term which is not a free variable.
  (term_typing:var/1)List is a free variable.
  (basic_props:list/1)List1 is a list.
  (basic_props:list/1)List2 is a list.
• The following properties should hold upon exit:
  (basic_props:list/1)List is a list.

Usage:sublist(List1,List2)

List2 contains all the elements of List1.

• If the following properties should hold at call time:
  (term_typing:nonvar/1)List2 is currently a term which is not a free variable.

Usage:subordlist(List1,List2)

List2 contains all the elements of List1 in the same order.

• If the following properties should hold at call time:
  (term_typing:nonvar/1)List2 is currently a term which is not a free variable.

Usage:equal_lists(List1,List2)

List1 has all the elements of List2, and vice versa.

• The following properties should hold at call time:
  (basic_props:list/1)List1 is a list.
  (basic_props:list/1)List2 is a list.

Usage 1:list_to_list_of_lists(List,LList)

• The following properties should hold at call time:
  (basic_props:list/1)List is a list.
• The following properties should hold upon exit:
  (lists:list_of_lists/1)lists:list_of_lists(LList)

Usage 2:list_to_list_of_lists(List,LList)

LList is the list of one element lists with elements of List.

• The following properties should hold at call time:
  (lists:list_of_lists/1)lists:list_of_lists(LList)
• The following properties should hold upon exit:
  (basic_props:list/1)List is a list.

Usage:powerset(List,LList)

LList is the powerset of List, i.e., the list of all lists which have elements of List. If List is ordered, LList and all its elements are ordered.

• The following properties should hold at call time:
  (term_typing:nonvar/1)List is currently a term which is not a free variable.
  (basic_props:list/1)List is a list.
• The following properties should hold upon exit:
  (lists:list_of_lists/1)lists:list_of_lists(LList)

Usage:cross_product(LList,List)

List is the cartesian product of the lists in LList, that is, the list of lists formed with one element of each list in LList, in the same order.

• The following properties should hold at call time:
  (term_typing:nonvar/1)LList is currently a term which is not a free variable.
  (lists:list_of_lists/1)lists:list_of_lists(LList)
• The following properties should hold upon exit:
  (lists:list_of_lists/1)lists:list_of_lists(List)

Usage:sequence_to_list(Sequence,List)

List is the list of all elements in the (comma-separated) sequence Sequence. The use of this predicate is reversible.

list_of_lists([]).
list_of_lists([L|Xs]) :-
        list(L),
        list_of_lists(Xs).