		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-matches-string-p

See if a string occurs at the front of an vl-echarlist-p.

Signature
(vl-matches-string-p string echars) → bool
Arguments: string — String we're looking for.; echars — Characters we're lexing.
Guard (vl-echarlist-p echars).

This function determines if some string occurs at the front of echars. More exactly, it computes:

(prefixp (explode string)
         (vl-echarlist->chars echars))

But we actually implement the operation with a fast function that does not call explode or build the list of characters.

Definitions and Theorems

Function: vl-matches-string-p$inline

(defun vl-matches-string-p$inline (string echars)
  (declare (type string string))
  (declare (xargs :guard (vl-echarlist-p echars)))
  (declare (xargs :guard (not (equal string ""))))
  (let ((__function__ 'vl-matches-string-p))
    (declare (ignorable __function__))
    (mbe :logic (prefixp (explode string)
                         (vl-echarlist->chars echars))
         :exec (vl-matches-string-p-impl string 0 (length string)
                                         echars))))

Theorem: len-when-vl-matches-string-p-fc

(defthm len-when-vl-matches-string-p-fc
  (implies (vl-matches-string-p string echars)
           (<= (len (explode string))
               (len echars)))
  :rule-classes ((:forward-chaining) (:linear)))

Theorem: consp-when-vl-matches-string-p-fc

(defthm consp-when-vl-matches-string-p-fc
  (implies (and (vl-matches-string-p string echars)
                (stringp string)
                (not (equal string "")))
           (consp echars))
  :rule-classes :forward-chaining)

Theorem: vl-matches-string-p-when-acl2-count-zero

(defthm vl-matches-string-p-when-acl2-count-zero
  (implies (and (equal 0 (acl2-count echars))
                (force (stringp string)))
           (equal (vl-matches-string-p string echars)
                  (equal string ""))))

Subtopics

Vl-matches-string-p-impl