# List processing

**Author(s):**The CLIP Group.

This module provides a set of predicates for list processing.

## Usage and interface

**Library usage:**`:- use_module(library(lists)).`**Exports:***Predicates:*`nonsingle/1`,`append/3`,`reverse/2`,`reverse/3`,`delete/3`,`delete_non_ground/3`,`select/3`,`length/2`,`nth/3`,`add_after/4`,`add_before/4`,`dlist/3`,`list_concat/2`,`list_insert/2`,`insert_last/3`,`contains_ro/2`,`contains1/2`,`nocontainsx/2`,`last/2`,`list_lookup/3`,`list_lookup/4`,`intset_insert/3`,`intset_delete/3`,`intset_in/2`,`intset_sequence/3`,`intersection/3`,`union/3`,`difference/3`,`equal_lists/2`,`list_to_list_of_lists/2`,`powerset/2`,`cross_product/2`,`sequence_to_list/2`.*Properties:*`list1/2`,`sublist/2`,`subordlist/2`.*Regular Types:*`list_of_lists/1`.

**Imports:***System library modules:*`assertions/native_props`.*Packages:*`prelude`,`nonpure`,`assertions`,`isomodes`,`metatypes`,`hiord`,`nativeprops`.

## Documentation on exports

**Usage:**`nonsingle(X)`

X is not a singleton.

**General properties:**

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

**General properties:**

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

**General properties:**

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

**General properties:**

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

**General properties:**

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

**General properties:**

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

**General properties:**

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

**General properties:**

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

`nth(N,List,Elem)`

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.

**General properties:**

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

*Meta-predicate*with arguments:

`list1(?,(pred 1))`.

**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:**`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_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).