List processing

Author(s): The CLIP Group.

This module provides a set of predicates for list processing.

Documentation on exports

PREDICATE

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]

    PREDICATE

    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.

    PREDICATE

    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.

    PREDICATE

    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.

      PREDICATE

      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.

      PREDICATE

      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.

      PREDICATE

      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.

        PREDICATE

        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.

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

        PREDICATE

        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.

        PREDICATE

        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.

        PROPERTY

        Usage:list1(X,Y)

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

          Meta-predicate with arguments: list1(?,(pred 1)).

          PREDICATE

          Usage:dlist(List,DList,Tail)

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

            PREDICATE

            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.

            PREDICATE

            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.

            PREDICATE

            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.

            PREDICATE

            Usage:

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

              PREDICATE

              Usage:

              First membership.

                PREDICATE

                Usage:nocontainsx(L,X)

                X is not identical to any element of L.

                  PREDICATE

                  Usage:last(L,X)

                  X is the last element of list L.

                    PREDICATE

                    Usage:list_lookup(List,Key,Value)

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

                      PREDICATE

                      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.

                        PREDICATE

                        Usage:intset_insert(A,B,Set)

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

                          PREDICATE

                          Usage:intset_delete(A,B,Set)

                          Delete from the ordered set A the element B.

                            PREDICATE

                            Usage:intset_in(E,Set)

                            Succeds iff E is element of Set

                              PREDICATE

                              Usage:intset_sequence(N,L1,L2)

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

                                PREDICATE

                                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.

                                PREDICATE

                                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.

                                PREDICATE

                                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.

                                PROPERTY

                                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.

                                PROPERTY

                                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.

                                PREDICATE

                                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.

                                PREDICATE

                                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.

                                PREDICATE

                                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)

                                PREDICATE

                                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)

                                PREDICATE

                                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.

                                  REGTYPE
                                  A regular type, defined as follows:
                                  list_of_lists([]).
                                  list_of_lists([L|Xs]) :-
                                          list(L),
                                          list_of_lists(Xs).