		Search-engine friendly clone of the ACL2 documentation.

Std/strings

Strtok

Tokenize a string with character delimiters.

(strtok x delimiters) splits the string x into a list of substrings, based on delimiters, a list of characters. This is somewhat similar to repeatedly calling the strtok function in C.

As an example:

(strtok "foo bar, baz!" (list #\Space #\, #\!))
  -->
("foo" "bar" "baz")

Note that all of the characters in delimiters are removed, and no empty strings are ever found in strtok's output.

Definitions and Theorems

Function: strtok$inline

(defun strtok$inline (x delimiters)
  (declare (xargs :guard (and (stringp x)
                              (character-listp delimiters))))
  (let ((rtokens (strtok-aux x 0
                             (mbe :logic (len (explode x))
                                  :exec (length x))
                             delimiters nil nil)))
    (mbe :logic (rev rtokens)
         :exec (reverse rtokens))))

Theorem: string-listp-of-strtok

(defthm string-listp-of-strtok
  (string-listp (strtok x delimiters)))

Theorem: streqv-implies-equal-strtok-1

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

Subtopics

Strtok-aux: Fast implementation of strtok.