		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-yul

Parses a Yul source program string into abstract syntax.

Signature
(parse-yul yul-string) → block?
Arguments: yul-string — Guard (stringp yul-string).
Returns: block? — Type (block-resultp block?).

yul-string must contain the surface syntax of a single Yul block.

Returns either a block or a reserrp. Yul object notation is not supported at this time.

Definitions and Theorems

Function: parse-yul

(defun parse-yul (yul-string)
 (declare (xargs :guard (stringp yul-string)))
 (let ((__function__ 'parse-yul))
  (declare (ignorable __function__))
  (b*
   ((tokens (tokenize-yul yul-string))
    ((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

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