		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-read-through-literal

Match any characters until and through some literal.

Signature
(vl-read-through-literal string echars) → (mv successp prefix remainder)
Arguments: echars — Guard (vl-echarlist-p echars).
Returns: successp — Whether we ever found string.; prefix — On success, all characters from echars leading up to and including the first occurrence of string. When string never occurs in echars, then prefix is the entire list of echars and remainder is its final cdr.

Definitions and Theorems

Function: vl-read-through-literal

(defun vl-read-through-literal (string echars)
  (declare (type string string))
  (declare (xargs :guard (vl-echarlist-p echars)))
  (declare (xargs :guard (not (equal string ""))))
  (let ((__function__ 'vl-read-through-literal))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((string (string-fix string))
              ((mv successp prefix remainder)
               (vl-read-until-literal string echars))
              ((unless successp)
               (mv nil prefix remainder)))
           (mv t
               (append prefix (take (length string) remainder))
               (nthcdr (length string) remainder)))
         :exec
         (b* (((mv successp prefix remainder)
               (vl-read-until-literal-impl string echars nil))
              ((unless successp)
               (mv nil (reverse prefix) remainder))
              (strlen (length string)))
           (mv t
               (reverse (revappend-of-take strlen remainder prefix))
               (rest-n strlen remainder))))))

Theorem: prefix-of-vl-read-through-literal-under-iff

(defthm prefix-of-vl-read-through-literal-under-iff
  (b* (((mv ?successp prefix ?remainder)
        (vl-read-through-literal string echars)))
    (implies (and (stringp string)
                  (not (equal string "")))
             (iff prefix (consp echars)))))

Subtopics

Vl-read-through-literal-prefix/remainder-thms: Prefix and remainder theorems for vl-read-through-literal, automatically generated by def-prefix/remainder-thms.