SEARCH

Major Section:  ACL2-BUILT-INS

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.

o The two arguments much both satisfy true-listp or else must both be strings, which must consist of standard characters (see standard-char-p) if the :test is char-equal.

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

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

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