		Search-engine friendly clone of the ACL2 documentation.

Tokenizer

Tokenize-yul-bytes

Lexes the bytes of a Yul source program into a list of tokens.

Signature
(tokenize-yul-bytes yul-bytes) → yul-lexemes
Arguments: yul-bytes — Guard (nat-listp yul-bytes).
Returns: yul-lexemes — Type (abnf::tree-list-resultp yul-lexemes).

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

Definitions and Theorems

Function: tokenize-yul-bytes

(defun tokenize-yul-bytes (yul-bytes)
 (declare (xargs :guard (nat-listp yul-bytes)))
 (let ((__function__ 'tokenize-yul-bytes))
  (declare (ignorable __function__))
  (b*
   (((mv erp lexeme-trees)
     (lexemeize-yul-bytes yul-bytes))
    ((when erp)
     (reserrf "problem lexing yul-bytes"))
    (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-bytes

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