		Search-engine friendly clone of the ACL2 documentation.

Tokenizer

Tokenize-yul

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

Signature
(tokenize-yul yul-string) → yul-lexemes
Arguments: yul-string — Guard (stringp yul-string).
Returns: yul-lexemes — Type (abnf::tree-list-resultp yul-lexemes).

The returned trees are for rulenames keyword, literal, identifier, or symbol. Each token is represented by an abnf::tree. Discards comments and whitespace. If the input structure from any lexeme down to the specific token type is incorrect, returns an error result value of type reserr instead of a list of tokens. Also, if the input string ends in the middle of a token, returns reserr.

Definitions and Theorems

Function: tokenize-yul

(defun tokenize-yul (yul-string)
 (declare (xargs :guard (stringp yul-string)))
 (let ((__function__ 'tokenize-yul))
  (declare (ignorable __function__))
  (b*
   (((mv erp lexeme-trees)
     (lexemeize-yul yul-string))
    ((when erp)
     (reserrf "problem lexing yul-string"))
    (subtoken-trees
     (filter-and-reduce-lexeme-tree-to-subtoken-trees lexeme-trees))
    ((when (reserrp subtoken-trees))
     (reserrf "problem with structure of lexeme tree")))
   subtoken-trees)))

Theorem: tree-list-resultp-of-tokenize-yul

(defthm tree-list-resultp-of-tokenize-yul
  (b* ((yul-lexemes (tokenize-yul yul-string)))
    (abnf::tree-list-resultp yul-lexemes))
  :rule-classes :rewrite)