		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-plain

Try to match a particular string literal corresponding to some plain token.

Signature
(vl-lex-plain echars breakp string type warnings) → (mv token/nil remainder warnings)
Arguments: echars — Characters we are lexing.
Guard (vl-echarlist-p echars).; breakp — Did we just see a linebreak?.
Guard (booleanp breakp).; string — Exact string we are looking for.
Guard (and (stringp string) (not (equal string ""))).; type — The type of plain token to create, on success.
Guard (vl-plaintokentype-p type).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lex-plain

(defun vl-lex-plain (echars breakp string type warnings)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (booleanp breakp)
                              (and (stringp string)
                                   (not (equal string "")))
                              (vl-plaintokentype-p type)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-lex-plain))
    (declare (ignorable __function__))
    (b* ((string (mbe :logic
                      (if (and (stringp string)
                               (not (equal string "")))
                          string
                        "foo")
                      :exec string))
         (warnings (vl-warninglist-fix warnings))
         ((unless (vl-matches-string-p string echars))
          (mv nil echars warnings))
         (len (length string))
         (etext (first-n len echars)))
      (mv (make-vl-plaintoken :etext etext
                              :type type
                              :breakp breakp)
          (rest-n len echars)
          warnings))))

Theorem: vl-warninglist-p-of-vl-lex-plain.warnings

(defthm vl-warninglist-p-of-vl-lex-plain.warnings
  (b* (((mv ?token/nil ?remainder ?warnings)
        (vl-lex-plain echars breakp string type warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-token-p-of-vl-lex-plain

(defthm vl-token-p-of-vl-lex-plain
 (implies
  (and (force (vl-echarlist-p echars))
       (and (force (vl-plaintokentype-p type))
            (force (booleanp breakp))))
  (equal
    (vl-token-p
         (mv-nth 0
                 (vl-lex-plain echars breakp string type warnings)))
    (if (mv-nth 0
                (vl-lex-plain echars breakp string type warnings))
        t
      nil))))

Theorem: true-listp-of-vl-lex-plain

(defthm true-listp-of-vl-lex-plain
 (equal
    (true-listp
         (mv-nth 1
                 (vl-lex-plain echars breakp string type warnings)))
    (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
       (true-listp echars)
       (true-listp
            (mv-nth 1
                    (vl-lex-plain echars
                                  breakp string type warnings)))))))

Theorem: vl-echarlist-p-of-vl-lex-plain

(defthm vl-echarlist-p-of-vl-lex-plain
 (implies
  (force (vl-echarlist-p echars))
  (equal
    (vl-echarlist-p
         (mv-nth 1
                 (vl-lex-plain echars breakp string type warnings)))
    t)))

Theorem: append-of-vl-lex-plain

(defthm append-of-vl-lex-plain
 (implies
  (and (mv-nth 0
               (vl-lex-plain echars breakp string type warnings))
       (force (vl-echarlist-p echars))
       (and (force (vl-plaintokentype-p type))
            (force (booleanp breakp))))
  (equal
   (append
    (vl-token->etext
         (mv-nth 0
                 (vl-lex-plain echars breakp string type warnings)))
    (mv-nth 1
            (vl-lex-plain echars breakp string type warnings)))
   echars)))

Theorem: no-change-loser-of-vl-lex-plain

(defthm no-change-loser-of-vl-lex-plain
 (implies
   (not (mv-nth 0
                (vl-lex-plain echars breakp string type warnings)))
   (equal (mv-nth 1
                  (vl-lex-plain echars breakp string type warnings))
          echars)))

Theorem: acl2-count-of-vl-lex-plain-weak

(defthm acl2-count-of-vl-lex-plain-weak
 (<=
    (acl2-count
         (mv-nth 1
                 (vl-lex-plain echars breakp string type warnings)))
    (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-plain-strong

(defthm acl2-count-of-vl-lex-plain-strong
 (implies
  (and (mv-nth 0
               (vl-lex-plain echars breakp string type warnings))
       t)
  (<
    (acl2-count
         (mv-nth 1
                 (vl-lex-plain echars breakp string type warnings)))
    (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-lex-plain-token/remainder-thms: Token and remainder theorems for vl-lex-plain, automatically generated by def-token/remainder-thms.