		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.