		Search-engine friendly clone of the ACL2 documentation.

Position

Position of an item in a string or a list

General Forms:
(position x seq)
(position x seq :test 'eql)   ; same as above (eql as equality test)
(position x seq :test 'eq)    ; same, but eq is equality test
(position x seq :test 'equal) ; same, but equal is equality test

(Position x seq) is the least index (zero-based) of the element x in the string or list seq, if x is an element of seq. Otherwise (position x seq) is nil. The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing x with items of seq.

The guard for a call of position depends on the test. In all cases, the second argument must satisfy stringp or true-listp. If the test is eql, then either the first argument must be suitable for eql (see eqlablep) or the second argument must satisfy eqlable-listp. If the test is eq, then either the first argument must be a symbol or the second argument must satisfy symbol-listp.

See equality-variants for a discussion of the relation between position and its variants:

(position-eq x seq) is equivalent to (position x seq :test 'eq);

(position-equal x seq) is equivalent to (position x seq :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function position-equal.

Position is defined by Common Lisp. See any Common Lisp documentation for more information.

Macro: position

(defmacro position (x seq &key (test ''eql))
  (declare (xargs :guard (or (equal test ''eq)
                             (equal test ''eql)
                             (equal test ''equal))))
  (cond ((equal test ''eq)
         (cons 'let-mbe
               (cons (cons (cons 'x (cons x 'nil))
                           (cons (cons 'seq (cons seq 'nil)) 'nil))
                     '(:logic (position-equal x seq)
                              :exec (position-eq-exec x seq)))))
        ((equal test ''eql)
         (cons 'let-mbe
               (cons (cons (cons 'x (cons x 'nil))
                           (cons (cons 'seq (cons seq 'nil)) 'nil))
                     '(:logic (position-equal x seq)
                              :exec (position-eql-exec x seq)))))
        (t (cons 'position-equal
                 (cons x (cons seq 'nil))))))

Function: position-equal

(defun position-equal (x seq)
  (declare (xargs :guard (or (stringp seq) (true-listp seq))))
  (if (stringp seq)
      (position-ac x (coerce seq 'list) 0)
    (position-equal-ac x seq 0)))

Function: position-equal-ac

(defun position-equal-ac (item lst acc)
  (declare (xargs :guard (and (true-listp lst)
                              (acl2-numberp acc))))
  (cond ((endp lst) nil)
        ((equal item (car lst))
         (mbe :exec acc :logic (fix acc)))
        (t (position-equal-ac item (cdr lst)
                              (1+ acc)))))

Macro: position-ac

(defmacro position-ac (item lst acc &key (test ''eql))
 (declare (xargs :guard (or (equal test ''eq)
                            (equal test ''eql)
                            (equal test ''equal))))
 (cond
  ((equal test ''eq)
   (cons 'let-mbe
         (cons (cons (cons 'item (cons item 'nil))
                     (cons (cons 'lst (cons lst 'nil))
                           (cons (cons 'acc (cons acc 'nil))
                                 'nil)))
               '(:logic (position-equal-ac item lst acc)
                        :exec (position-ac-eq-exec item lst acc)))))
  ((equal test ''eql)
   (cons
        'let-mbe
        (cons (cons (cons 'item (cons item 'nil))
                    (cons (cons 'lst (cons lst 'nil))
                          (cons (cons 'acc (cons acc 'nil))
                                'nil)))
              '(:logic (position-equal-ac item lst acc)
                       :exec (position-ac-eql-exec item lst acc)))))
  (t (cons 'position-equal-ac
           (cons item (cons lst (cons acc 'nil)))))))

Subtopics

Listpos: (listpos x y) returns the starting position of the first occurrence of the sublist x within the list y, or NIL if there is no such occurrence.