		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-plain-alist

Signature
(vl-lex-plain-alist echars breakp alist warnings) → (mv token/nil remainder warnings)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).; 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 breakp alist warnings)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (booleanp breakp)
                              (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 breakp (caar alist)
                        (cdar alist)
                        warnings))
         ((when token)
          (mv token remainder warnings)))
      (vl-lex-plain-alist echars breakp (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 breakp 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))
       (and (force (vl-plaintoken-alistp alist))
            (force (booleanp breakp))))
  (equal
    (vl-token-p
         (mv-nth 0
                 (vl-lex-plain-alist echars breakp alist warnings)))
    (if (mv-nth 0
                (vl-lex-plain-alist echars breakp 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 breakp 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 breakp 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 breakp 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 breakp alist warnings))
       (force (vl-echarlist-p echars))
       (and (force (vl-plaintoken-alistp alist))
            (force (booleanp breakp))))
  (equal
   (append
    (vl-token->etext
         (mv-nth 0
                 (vl-lex-plain-alist echars breakp alist warnings)))
    (mv-nth 1
            (vl-lex-plain-alist echars breakp 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 breakp alist warnings)))
   (equal (mv-nth 1
                  (vl-lex-plain-alist echars breakp 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 breakp 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 breakp alist warnings))
       t)
  (<
    (acl2-count
         (mv-nth 1
                 (vl-lex-plain-alist echars breakp 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.