		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-assignment-statement

Attempts to eat an assignment statement and build a statement AST node of kind :assign-single or :assign-multiple.

Signature
(parse-assignment-statement 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).

Definitions and Theorems

Function: parse-assignment-statement

(defun parse-assignment-statement (tokens)
 (declare (xargs :guard (abnf::tree-listp tokens)))
 (let ((__function__ 'parse-assignment-statement))
  (declare (ignorable __function__))
  (b*
   (((mv path-ast tokens-after-path)
     (parse-path tokens))
    ((when (reserrp path-ast))
     (mv (reserrf (cons "no assignment statement here" tokens))
         nil))
    ((mv additional-paths
         tokens-after-additional-paths)
     (parse-*-comma-path tokens-after-path))
    (tokens-after-assignment-symbol
         (parse-symbol ":=" tokens-after-additional-paths))
    ((when (reserrp tokens-after-assignment-symbol))
     (mv (reserrf (cons "assignment statement requires ':='"
                        tokens))
         nil))
    ((mv init-ast tokens-after-init-form)
     (if (null additional-paths)
         (parse-expression tokens-after-assignment-symbol)
       (parse-function-call tokens-after-assignment-symbol)))
    ((when (reserrp init-ast))
     (mv
      (reserrf (cons "assignment statement does not finish properly"
                     tokens))
      nil)))
   (mv (if (null additional-paths)
           (make-statement-assign-single :target path-ast
                                         :value init-ast)
         (make-statement-assign-multi
              :targets (cons path-ast additional-paths)
              :value init-ast))
       tokens-after-init-form))))

Theorem: statement-resultp-of-parse-assignment-statement.result-ast

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

Theorem: tree-listp-of-parse-assignment-statement.tokens-after-statement

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

Theorem: len-of-parse-assignment-statement-<

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