		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-plain-alist

Signature
(vl-lex-plain-alist echars alist warnings) → (mv token/nil remainder warnings)
Arguments: echars — Guard (vl-echarlist-p echars).; alist — Guard (vl-plaintoken-alistp alist).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

We walk through the alist, looking for the first string that matches the beginning of echars. If we find one, we build a plaintoken using the matching echars and the corresponding type. Since the alist is searched in order, you can search for long prefixes first, e.g., >>> before >>.

Definitions and Theorems

Function: vl-lex-plain-alist

(defun vl-lex-plain-alist (echars alist warnings)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (vl-plaintoken-alistp alist)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-lex-plain-alist))
    (declare (ignorable __function__))
    (b* (((when (atom alist))
          (mv nil echars (ok)))
         ((mv token remainder warnings)
          (vl-lex-plain echars (caar alist)
                        (cdar alist)
                        warnings))
         ((when token)
          (mv token remainder warnings)))
      (vl-lex-plain-alist echars (cdr alist)
                          warnings))))

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

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

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

(defthm vl-token-p-of-vl-lex-plain-alist
 (implies
  (and (force (vl-echarlist-p echars))
       (force (vl-plaintoken-alistp alist)))
  (equal
    (vl-token-p (mv-nth 0
                        (vl-lex-plain-alist echars alist warnings)))
    (if (mv-nth 0
                (vl-lex-plain-alist echars alist warnings))
        t
      nil))))

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

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

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

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

Theorem: append-of-vl-lex-plain-alist

(defthm append-of-vl-lex-plain-alist
 (implies
  (and (mv-nth 0
               (vl-lex-plain-alist echars alist warnings))
       (force (vl-echarlist-p echars))
       (force (vl-plaintoken-alistp alist)))
  (equal
   (append (vl-token->etext
                (mv-nth 0
                        (vl-lex-plain-alist echars alist warnings)))
           (mv-nth 1
                   (vl-lex-plain-alist echars alist warnings)))
   echars)))

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

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

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

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

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

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

Subtopics

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