		Search-engine friendly clone of the ACL2 documentation.

Search

Search for a string or list in another string or list

Example Forms:
(search "cd" "Cdabcdefcde")                   ; = 4, index of first match
(search "cd" "Cdabcdefcde" :test 'equal)      ; same as above
(search "cd" "Cdabcdefcde" :from-end t)       ; = 8, index of last match
(search "cd" "Cdabcdefcde" :start1 1)         ; = 1
(search "cd" "Cdabcdefcde" :start2 5)         ; = 8
(search "cd" "Cdabcdefcde" :test 'char-equal) ; = 0 (case-insensitive)
(search "ac" "Cdabcdefcde")                   ; = nil
(search '(a b) '(9 8 a b 7 6))                    ; = 2

General Form:
(search seq1 seq2 &key from-end test start1 start2 end1 end2)

Search indicates whether one string or list occurs as a (contiguous) subsequence of another string or list, respectively. It returns nil if no such match is found; otherwise it returns the (zero-based) index of the first match by default, but a non-nil value of keyword argument :from-end causes it to return the last match. The :test is equal by default. The other legal value for :test is char-equal, which can be given only for two strings, in which case the match is case-insensitive. Finally, values of :start1 and :end1 for the first sequence, and of :start2 and :end2 for the second sequence, bound the portion of the respective sequence used for deciding on a match, though the index returned is always an index into the second sequence as a whole.

The guard for calls of search is given by a function, search-fn-guard, which has the following requirements.

The two arguments much both satisfy true-listp or else must both be strings.
The :test must evaluate to one of the symbols equal or char-equal, where the latter is only allowed if the (first) two arguments are strings.
The values of :start1, :start2, :end1, and :end2 must all be natural numbers, where if omitted they default to 0, 0, the length len1 of the first argument, and the length len2 of the second argument, respectively.
If start1 is the value of :start1, defaulting as described just above, and similarly for the other start and end keywords and for lengths len1 and len2 as described just above, then: start1 <= end1 <= len1 and start2 <= end2 <= len2.

Search is a Common Lisp function (actually, a macro in ACL2). See any Common Lisp documentation for more information.

Definition

Macro: search

(defmacro search (seq1 seq2 &key from-end (test ''equal)
                       (start1 '0)
                       (start2 '0)
                       (end1 'nil end1p)
                       (end2 'nil end2p))
 (cons
  'search-fn
  (cons
   seq1
   (cons
    seq2
    (cons
     from-end
     (cons
      test
      (cons
          start1
          (cons start2
                (cons end1
                      (cons end2
                            (cons end1p (cons end2p 'nil))))))))))))

Function: search-fn

(defun search-fn (seq1 seq2 from-end test
                       start1 start2 end1 end2 end1p end2p)
 (declare
  (xargs
      :guard (search-fn-guard seq1 seq2 from-end test
                              start1 start2 end1 end2 end1p end2p)))
 (let* ((end1 (if end1p end1 (length seq1)))
        (end2 (if end2p end2 (length seq2)))
        (seq1 (subseq seq1 start1 end1)))
  (mv-let (seq1 seq2)
          (cond ((eq test 'char-equal)
                 (mv (string-downcase seq1)
                     (string-downcase seq2)))
                (t (mv seq1 seq2)))
   (and (<= (- end1 start1) (- end2 start2))
        (cond (from-end (search-from-end seq1 seq2 start2 end2 nil))
              (t (search-from-start seq1 seq2 start2 end2)))))))

Function: search-from-end

(defun search-from-end (seq1 seq2 start2 end2 acc)
  (declare (xargs :guard (and (or (true-listp seq1) (stringp seq1))
                              (or (true-listp seq2) (stringp seq2))
                              (integerp start2)
                              (<= 0 start2)
                              (integerp end2)
                              (<= end2 (length seq2))
                              (<= (+ start2 (length seq1)) end2))))
  (cond ((or (not (integerp end2))
             (not (integerp start2)))
         nil)
        (t (let* ((bound2 (+ start2 (length seq1)))
                  (matchp (equal seq1 (subseq seq2 start2 bound2)))
                  (new-acc (if matchp start2 acc)))
             (cond ((>= bound2 end2) new-acc)
                   (t (search-from-end seq1 seq2 (1+ start2)
                                       end2 new-acc)))))))

Function: search-from-start

(defun search-from-start (seq1 seq2 start2 end2)
  (declare (xargs :guard (and (or (true-listp seq1) (stringp seq1))
                              (or (true-listp seq2) (stringp seq2))
                              (integerp start2)
                              (<= 0 start2)
                              (integerp end2)
                              (<= end2 (length seq2))
                              (<= (+ start2 (length seq1)) end2))))
  (let ((bound2 (+ start2 (length seq1))))
    (cond ((or (not (integerp end2))
               (not (integerp start2)))
           nil)
          ((equal seq1 (subseq seq2 start2 bound2))
           start2)
          ((>= bound2 end2) nil)
          (t (search-from-start seq1 seq2 (1+ start2)
                                end2)))))

Subtopics

Index-of: (index-of k x) returns the index of the first occurrence of element k in list x if it exists, NIL otherwise.
Sublistp: (sublistp x y) checks whether the list x ever occurs within the list y.