• 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
        • 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/io
    • Std/osets
    • 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

Istrpos

Case-insensitivly locate the first occurrence of a substring.

(istrpos x y) is like strpos, but the comparisons are done in a case insensitive manner. It returns nil if x never occurs in y, or returns the index of the first character of the first occurrence otherwise.

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 istrprefixp rather than some better algorithm.

The "soundness" and "completness" of strpos are established in the theorems iprefixp-of-istrpos and completeness-of-istrpos.

Definitions and Theorems

Function: istrpos-impl

(defun istrpos-impl (x y n xl yl)
  (declare (type string x y)
           (type (integer 0 *) n xl yl)
           (xargs :guard (and (stringp x)
                              (stringp y)
                              (natp xl)
                              (natp yl)
                              (natp n)
                              (<= n (length y))
                              (= xl (length x))
                              (= yl (length y)))))
  (cond ((mbe :logic (iprefixp (explode x)
                               (nthcdr n (explode y)))
              :exec (istrprefixp-impl (the string x)
                                      (the string y)
                                      (the (integer 0 *) 0)
                                      (the (integer 0 *) n)
                                      (the (integer 0 *) xl)
                                      (the (integer 0 *) yl)))
         (lnfix n))
        ((mbe :logic (zp (- (nfix yl) (nfix n)))
              :exec (int= n yl))
         nil)
        (t (istrpos-impl (the string x)
                         (the string y)
                         (the (integer 0 *)
                              (+ 1 (the (integer 0 *) (lnfix n))))
                         (the (integer 0 *) xl)
                         (the (integer 0 *) yl)))))

Function: istrpos$inline

(defun istrpos$inline (x y)
  (declare (type string x y))
  (let* ((xl (mbe :logic (len (explode x))
                  :exec (length (the string x))))
         (yl (mbe :logic (len (explode y))
                  :exec (length (the string y)))))
    (declare (type (integer 0 *) xl yl))
    (istrpos-impl (the string x)
                  (the string y)
                  (the (integer 0 *) 0)
                  xl yl)))

Theorem: istrpos-type

(defthm istrpos-type
  (or (and (integerp (istrpos x y))
           (<= 0 (istrpos x y)))
      (not (istrpos x y)))
  :rule-classes :type-prescription)

Theorem: iprefixp-of-istrpos

(defthm iprefixp-of-istrpos
  (implies (istrpos x y)
           (iprefixp (explode x)
                     (nthcdr (istrpos x y) (explode y)))))

Theorem: completeness-of-istrpos

(defthm completeness-of-istrpos
  (implies (and (iprefixp (explode x)
                          (nthcdr m (explode y)))
                (force (natp m)))
           (and (natp (istrpos x y))
                (<= (istrpos x y) m))))

Theorem: istreqv-implies-equal-istrpos-impl-1

(defthm istreqv-implies-equal-istrpos-impl-1
  (implies (istreqv x x-equiv)
           (equal (istrpos-impl x y n xl yl)
                  (istrpos-impl x-equiv y n xl yl)))
  :rule-classes (:congruence))

Theorem: istreqv-implies-equal-istrpos-impl-2

(defthm istreqv-implies-equal-istrpos-impl-2
  (implies (istreqv y y-equiv)
           (equal (istrpos-impl x y n xl yl)
                  (istrpos-impl x y-equiv n xl yl)))
  :rule-classes (:congruence))

Theorem: istreqv-implies-equal-istrpos-1

(defthm istreqv-implies-equal-istrpos-1
  (implies (istreqv x x-equiv)
           (equal (istrpos x y)
                  (istrpos x-equiv y)))
  :rule-classes (:congruence))

Theorem: istreqv-implies-equal-istrpos-2

(defthm istreqv-implies-equal-istrpos-2
  (implies (istreqv y y-equiv)
           (equal (istrpos x y)
                  (istrpos x y-equiv)))
  :rule-classes (:congruence))