		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-read-until-literal

Match any characters up until some literal.

Signature
(vl-read-until-literal string echars) → (mv successp prefix remainder)
Arguments: string — The ending string that we're looking for.
Guard (stringp string).; echars — The characters that we're lexing.
Guard (vl-echarlist-p echars).
Returns: successp — Whether we ever found string.; prefix — All characters from echars leading up to but not including the first occurrence of string. When string never occurs in echars, prefix is just the entire list of echars and remainder is its final cdr.

Definitions and Theorems

Function: vl-read-until-literal$inline

(defun vl-read-until-literal$inline (string echars)
  (declare (xargs :guard (and (stringp string)
                              (vl-echarlist-p echars))))
  (declare (xargs :guard (not (equal string ""))))
  (let ((__function__ 'vl-read-until-literal))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (atom echars))
               (mv nil nil echars))
              ((when (vl-matches-string-p string echars))
               (mv t nil echars))
              ((mv successp prefix remainder)
               (vl-read-until-literal string (cdr echars))))
           (mv successp (cons (car echars) prefix)
               remainder))
         :exec
         (b* (((mv successp acc remainder)
               (vl-read-until-literal-impl string echars nil)))
           (mv successp (reverse acc)
               remainder)))))

Theorem: vl-read-until-literal$inline-mvtypes-0

(defthm vl-read-until-literal$inline-mvtypes-0
  (booleanp (mv-nth 0
                    (vl-read-until-literal$inline string echars)))
  :rule-classes :type-prescription)

Theorem: vl-read-until-literal$inline-mvtypes-1

(defthm vl-read-until-literal$inline-mvtypes-1
  (true-listp (mv-nth 1
                      (vl-read-until-literal$inline string echars)))
  :rule-classes :type-prescription)

Theorem: vl-read-until-literal-impl-equiv

(defthm vl-read-until-literal-impl-equiv
  (b* (((mv successp prefix remainder)
        (vl-read-until-literal string echars)))
    (equal (vl-read-until-literal-impl string echars acc)
           (list successp (revappend prefix acc)
                 remainder))))

Theorem: len-of-vl-read-until-literal

(defthm len-of-vl-read-until-literal
  (b* (((mv successp ?prefix remainder)
        (vl-read-until-literal string echars)))
    (implies successp
             (<= (len (explode string))
                 (len remainder))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-matches-string-p-after-vl-read-until-literal

(defthm vl-matches-string-p-after-vl-read-until-literal
  (b* (((mv successp ?prefix remainder)
        (vl-read-until-literal string echars)))
    (implies successp
             (vl-matches-string-p string remainder))))

Theorem: consp-of-remainder-when-successful-vl-read-until-literal

(defthm consp-of-remainder-when-successful-vl-read-until-literal
  (b* (((mv successp ?prefix remainder)
        (vl-read-until-literal string echars)))
    (implies successp (consp remainder))))

Theorem: true-listp-of-remainder-of-vl-read-until-literal

(defthm true-listp-of-remainder-of-vl-read-until-literal
  (equal (true-listp (mv-nth 2
                             (vl-read-until-literal string echars)))
         (true-listp echars)))

Subtopics

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