		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-variable-declaration

Attempts to eat a variable declaration and build a statement AST node of kind :variable-single or :variable-multi.

Signature
(parse-variable-declaration tokens) → (mv result-ast tokens-after-statement)
Arguments: tokens — Guard (abnf::tree-listp tokens).
Returns: result-ast — Type (statement-resultp result-ast).; tokens-after-statement — Type (abnf::tree-listp tokens-after-statement).

The syntax diagram for `yul-variable-declaration' allows two ways of parsing a variable declaration with a single identifier and an initialization of a function call.For example, let x := s(0).

The initialization can be a yul-expression which can be a yul-function-call, or the initialization can be a yul-function-call directly.Although the syntax does not differ, and a grammar does not dictate the AST that is built, we still must decide what to build.We decided to build an expression of kind :funcall containing a funcall object whenever there is a single identifier.

This treatment is consistent with the handling of single and muli-assignmebnts, but in that case the syntax diagram dictates at least two yul-path instances prior to a direct yul-function-call.

Definitions and Theorems

Function: parse-variable-declaration

(defun parse-variable-declaration (tokens)
  (declare (xargs :guard (abnf::tree-listp tokens)))
  (let ((__function__ 'parse-variable-declaration))
    (declare (ignorable __function__))
    (b* (((mv ?key1 tokens-after-let)
          (parse-keyword "let" tokens))
         ((when (reserrp tokens-after-let))
          (mv (reserrf (cons "no variable decl here" tokens))
              nil))
         ((mv let-var-1 tokens-after-let-var-1)
          (parse-identifier tokens-after-let))
         ((when (null let-var-1))
          (mv (reserrf (cons "no variable decl here 2" tokens))
              nil))
         ((when (reserrp tokens-after-let-var-1))
          (mv (reserrf (cons "no variable decl here 3" tokens))
              nil))
         ((mv rest-identifiers
              tokens-after-rest-identifiers)
          (parse-*-comma-identifier tokens-after-let-var-1))
         (tokens-after-init-symbol
              (parse-symbol ":=" tokens-after-rest-identifiers))
         ((mv init-ast tokens-final)
          (if (reserrp tokens-after-init-symbol)
              (mv nil tokens-after-rest-identifiers)
            (b* (((mv init-ast tokens-after-init)
                  (if (null rest-identifiers)
                      (parse-expression tokens-after-init-symbol)
                    (parse-function-call tokens-after-init-symbol)))
                 ((when (reserrp init-ast))
                  (mv nil tokens-after-rest-identifiers)))
              (mv init-ast tokens-after-init)))))
      (mv (if (null rest-identifiers)
              (make-statement-variable-single :name let-var-1
                                              :init init-ast)
            (make-statement-variable-multi
                 :names (cons let-var-1 rest-identifiers)
                 :init init-ast))
          tokens-final))))

Theorem: statement-resultp-of-parse-variable-declaration.result-ast

(defthm statement-resultp-of-parse-variable-declaration.result-ast
  (b* (((mv ?result-ast ?tokens-after-statement)
        (parse-variable-declaration tokens)))
    (statement-resultp result-ast))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-variable-declaration.tokens-after-statement

(defthm
    tree-listp-of-parse-variable-declaration.tokens-after-statement
  (b* (((mv ?result-ast ?tokens-after-statement)
        (parse-variable-declaration tokens)))
    (abnf::tree-listp tokens-after-statement))
  :rule-classes :rewrite)

Theorem: len-of-parse-variable-declaration-<

(defthm len-of-parse-variable-declaration-<
  (b* (((mv ?result-ast ?tokens-after-statement)
        (parse-variable-declaration tokens)))
    (implies (not (reserrp result-ast))
             (< (len tokens-after-statement)
                (len tokens))))
  :rule-classes :linear)