		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemeize-yul

Lexes the bytes of yul-string into a list of lexemes.

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

A lexeme is a token, comment, or whitespace. Lexemize-yul returns two values: an error flag and a list of these lexemes in abnf::tree form. Lexemes are further separated into keyword, literal, identifier, or symbol. Recombining these lexemes is done in the parser.

Definitions and Theorems

Function: lexemeize-yul

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

Theorem: booleanp-of-lexemeize-yul.erp

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

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

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