• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
        • Std/util-extensions
        • Std/basic-extensions
        • Std/strings-extensions
          • Strtok!
          • Character-kinds
        • Std/system-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Std/strings-extensions
• Std/strings

Strtok!

Variant of strtok that does not treat contiguous delimiters as one.

Signature

(strtok! string delimiters) → strings

Arguments

string — Guard (stringp string).

delimiters — Guard (character-listp delimiters).

Returns

strings — Type (string-listp strings).

The function strtok treats contiguous delimiters as one, and thus it never returns empty strings, e.g.:

(strtok "abc.de..f" (list #\.)) --> ("abc" "de" "f")

In contrast, strtok! considers each delimiter separately, possibly returning empty string between contiguous delimiters:

(strtok! "abc.de..f" (list #\.)) --> ("abc" "de" "" "f")

The implementation of strtok! is very similar to strtok, aside from some parameter name changes. The main difference is that strtok! omits some tests about the (reversed) current token being non-empty: in this way, empty tokens are considered and returned.

Note that strtok! returns the singleton list ("") when given the empty string "" as argument. This seems to make sense because the beginning and end of the string are considered like delimiters, and strtok! considers and returns empty strings between delimiters.

Definitions and Theorems

Function: strtok!-aux

(defun
 strtok!-aux
 (string pos len delimiters rev-curr-tok acc)
 (declare (type string string)
          (type (integer 0 *) pos)
          (type (integer 0 *) len))
 (declare (xargs :guard (and (stringp string)
                             (natp pos)
                             (natp len)
                             (character-listp delimiters)
                             (character-listp rev-curr-tok)
                             (string-listp acc))))
 (declare (xargs :guard (and (<= pos len)
                             (<= len (length string)))))
 (let
   ((acl2::__function__ 'strtok!-aux))
   (declare (ignorable acl2::__function__))
   (if (mbe :logic (zp (- (nfix len) (nfix pos)))
            :exec (int= pos len))
       (cons (rchars-to-string rev-curr-tok)
             acc)
       (b* ((char (char string pos))
            (matchp (member char delimiters)))
           (strtok!-aux (the string string)
                        (the (integer 0 *)
                             (1+ (mbe :logic (nfix pos) :exec pos)))
                        (the (integer 0 *) len)
                        delimiters
                        (if matchp nil (cons char rev-curr-tok))
                        (if matchp
                            (cons (rchars-to-string rev-curr-tok)
                                  acc)
                            acc))))))

Theorem: string-listp-of-strtok!-aux

(defthm
 string-listp-of-strtok!-aux
 (implies
    (string-listp acc)
    (b* ((result (strtok!-aux string
                              pos len delimiters rev-curr-tok acc)))
        (string-listp result)))
 :rule-classes :rewrite)

Theorem: streqv-implies-equal-strtok!-aux-1

(defthm
 streqv-implies-equal-strtok!-aux-1
 (implies (streqv string string-equiv)
          (equal (strtok!-aux string
                              pos len delimiters rev-curr-tok acc)
                 (strtok!-aux string-equiv
                              pos len delimiters rev-curr-tok acc)))
 :rule-classes (:congruence))

Function: strtok!

(defun
 strtok! (string delimiters)
 (declare (xargs :guard (and (stringp string)
                             (character-listp delimiters))))
 (let
    ((acl2::__function__ 'strtok!))
    (declare (ignorable acl2::__function__))
    (b* ((rev-tokens (strtok!-aux string 0
                                  (mbe :logic (len (explode string))
                                       :exec (length string))
                                  delimiters nil nil)))
        (mbe :logic (rev rev-tokens)
             :exec (reverse rev-tokens)))))

Theorem: string-listp-of-strtok!

(defthm string-listp-of-strtok!
        (b* ((strings (strtok! string delimiters)))
            (string-listp strings))
        :rule-classes :rewrite)

Theorem: streqv-implies-equal-strtok!-1

(defthm streqv-implies-equal-strtok!-1
        (implies (streqv string string-equiv)
                 (equal (strtok! string delimiters)
                        (strtok! string-equiv delimiters)))
        :rule-classes (:congruence))