		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-yul-bytes

Parses the Yul source program bytes into abstract syntax.

Signature
(parse-yul-bytes yul-bytes) → block?
Arguments: yul-bytes — Guard (nat-listp yul-bytes).
Returns: block? — Type (block-resultp block?).

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

Definitions and Theorems

Function: parse-yul-bytes

(defun parse-yul-bytes (yul-bytes)
 (declare (xargs :guard (nat-listp yul-bytes)))
 (let ((__function__ 'parse-yul-bytes))
  (declare (ignorable __function__))
  (b*
   ((tokens (tokenize-yul-bytes yul-bytes))
    ((when (reserrp tokens)) tokens)
    ((mv top-block tokens-after-ast)
     (parse-block tokens))
    ((when (reserrp top-block)) top-block)
    ((unless (null tokens-after-ast))
     (reserrf
      "after parsing top-level yul block, there should be no more tokens")))
   top-block)))

Theorem: block-resultp-of-parse-yul-bytes

(defthm block-resultp-of-parse-yul-bytes
  (b* ((block? (parse-yul-bytes yul-bytes)))
    (block-resultp block?))
  :rule-classes :rewrite)