# 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`.

**Other modules used:***System library modules:*`assertions/native_props`.

## Documentation on exports

**General properties:**

`nonsingle(A)`

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

`nonsingle(A)`

*Description:*nonsingle succeeds.*If the following properties should hold at call time:*

(term_basic:= /2)term_basic:A=[a,b]

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

*Description:*X is not a singleton.

**General properties:**

`append(Xs,Ys,Zs)`

*Description:*Zs is Ys appended to Xs.*The following properties should hold upon exit:*

(basic_props:list/1)Xs is a list.

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

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

`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]]`.

`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).

`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).

`append(Xs,Ys,Zs)`

*The following properties hold globally:*

(basic_props:sideff/2)append(Xs,Ys,Zs) is side-effect free.

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

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

`append(A,B,C)`

*Description:*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]

`append(A,B,X)`

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

`append(A,B,X)`

*Description:*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],[])].

`append(A,B,X)`

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

`append(_A,B,X)`

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

`append(X,Y,Z)`

*Description:*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:** `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:**

`reverse(A,B)`

*Description:*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]

*The following properties hold globally:*

(basic_props:sideff/2)reverse(Arg1,Arg2) is side-effect free.

`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(Xs,Ys)`

*Description:*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:**

`reverse(A,B,C)`

*Description:*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]

*The following properties hold globally:*

(basic_props:sideff/2)reverse(Arg1,Arg2,Arg3) is side-effect free.

`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:** `reverse(A,B,C)`

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

**General properties:**

*The following properties hold globally:*

(basic_props:sideff/2)delete(Arg1,Arg2,Arg3) is side-effect free.

`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(L1,E,L2)`

*Description:*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:**

*The following properties hold globally:*

(basic_props:sideff/2)delete_non_ground(Arg1,Arg2,Arg3) is side-effect 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:** `delete_non_ground(L1,E,L2)`

*Description:*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:**

*The following properties hold globally:*

(basic_props:sideff/2)select(Arg1,Arg2,Arg3) is side-effect free.

`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:** `select(X,Xs,Ys)`

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

**General properties:**

`length(A,B)`

*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

*The following properties hold globally:*

(basic_props:sideff/2)length(Arg1,Arg2) is side-effect free.

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

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

**Usage 1:** `length(L,N)`

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

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

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

`nth(N,List,Elem)`

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

**General properties:**

*The following properties hold globally:*

(basic_props:sideff/2)nth(N,List,Elem) is side-effect free.

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

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

`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 1:**

*Description:*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:**

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

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

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

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

*Meta-predicate*with arguments:

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

**Usage:** `list1(X,Y)`

*Description:*X is a list of Ys of at least one element.

**Usage:** `dlist(List,DList,Tail)`

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

**Usage:** `list_concat(LL,L)`

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

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

*Description:*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:**

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

**Usage:** `list_lookup(List,Key,Value)`

*Description:*Same as`list_lookup/4`, but use`-/2`as functor.

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

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

*Description:*Insert the element B in the ordered set of numbers A.

**Usage:** `intset_delete(A,B,Set)`

*Description:*Delete from the ordered set A the element B.

**Usage:** `intset_sequence(N,L1,L2)`

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

**Usage:** `intersection(List1,List2,List)`

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

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

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

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

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

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

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

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

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

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