		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemeize-yul-bytes

Lexes the bytes into a list of lexemes.

Signature
(lexemeize-yul-bytes yul-bytes) → (mv erp yul-lexemes)
Arguments: yul-bytes — Guard (nat-listp yul-bytes).
Returns: erp — Type (booleanp erp).; yul-lexemes — Type (abnf::tree-listp yul-lexemes).

This does the same thing as lexemeize-yul, but does not need to convert the string to bytes first.

Definitions and Theorems

Function: lexemeize-yul-bytes

(defun lexemeize-yul-bytes (yul-bytes)
 (declare (xargs :guard (nat-listp yul-bytes)))
 (let ((__function__ 'lexemeize-yul-bytes))
  (declare (ignorable __function__))
  (b*
   (((mv trees rest-input)
     (lex-repetition-*-lexeme yul-bytes))
    ((when (reserrp trees))
     (prog2$ (cw "tokenize-yul: reserrp should not happen here")
             (mv t nil)))
    ((unless (null rest-input))
     (prog2$
      (cw
       "tokenize-yul: bytes given cannot be fully tokenized; returning list of abnf trees found so far")
      (mv t trees))))
   (mv nil trees))))

Theorem: booleanp-of-lexemeize-yul-bytes.erp

(defthm booleanp-of-lexemeize-yul-bytes.erp
  (b* (((mv ?erp ?yul-lexemes)
        (lexemeize-yul-bytes yul-bytes)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: tree-listp-of-lexemeize-yul-bytes.yul-lexemes

(defthm tree-listp-of-lexemeize-yul-bytes.yul-lexemes
  (b* (((mv ?erp ?yul-lexemes)
        (lexemeize-yul-bytes yul-bytes)))
    (abnf::tree-listp yul-lexemes))
  :rule-classes :rewrite)