• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
        • Istrpos
        • Strrpos
        • Strpos
          • Strpos-fast
        • Collect-syms-with-isubstr
        • Istrprefixp
        • Collect-strs-with-isubstr
        • Iprefixp
        • Strsuffixp
        • Firstn-chars
        • Strprefixp
        • Isubstrp
        • Substrp
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Substrings

Strpos

Locate the first occurrence of a substring.

(strpos x y) searches through the string y for the first occurrence of the substring x. If x occurs somewhere in y, it returns the starting index of the first occurrence. Otherwise, it returns nil to indicate that x never occurs in y.

The function is "efficient" in the sense that it does not coerce its arguments into lists, but rather traverses both strings with char. On the other hand, it is a naive string search which operates by repeatedly calling strprefixp, rather than some better algorithm.

Corner case: we say that the empty string is a prefix of any other string. That is, (strpos "" x) is 0 for all x.

Definitions and Theorems

Function: strpos$inline

(defun strpos$inline (x y)
  (declare (type string x y))
  (mbe :logic (listpos (explode x) (explode y))
       :exec (strpos-fast (the string x)
                          (the string y)
                          (the integer 0)
                          (the integer (length (the string x)))
                          (the integer (length (the string y))))))

Theorem: streqv-implies-equal-strpos-1

(defthm streqv-implies-equal-strpos-1
  (implies (streqv x x-equiv)
           (equal (strpos x y) (strpos x-equiv y)))
  :rule-classes (:congruence))

Theorem: streqv-implies-equal-strpos-2

(defthm streqv-implies-equal-strpos-2
  (implies (streqv y y-equiv)
           (equal (strpos x y) (strpos x y-equiv)))
  :rule-classes (:congruence))

Subtopics

Strpos-fast

Fast implementation of strpos.