		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-to-asg-expr-list

Turn an expression into a list of assignment expressions.

Signature
(expr-to-asg-expr-list expr) → asg-exprs
Arguments: expr — Guard (exprp expr).
Returns: asg-exprs — Type (expr-listp asg-exprs).

In the grammar, an expression is defined as a comma-separated sequence of one or more assignment expressions. If there are no commas, then the expression is an assignment expression.

In abstract syntax, we flatten the expression according to the :commas. We do it for both sub-expressions of each :comma, recursively, regardless of the nesting resulting from the parser.

Definitions and Theorems

Function: expr-to-asg-expr-list

(defun expr-to-asg-expr-list (expr)
  (declare (xargs :guard (exprp expr)))
  (if (expr-case expr :comma)
      (append (expr-to-asg-expr-list (expr-comma->first expr))
              (expr-to-asg-expr-list (expr-comma->next expr)))
    (list (expr-fix expr))))

Theorem: expr-listp-of-expr-to-asg-expr-list

(defthm expr-listp-of-expr-to-asg-expr-list
  (b* ((asg-exprs (expr-to-asg-expr-list expr)))
    (expr-listp asg-exprs))
  :rule-classes :rewrite)

Theorem: expr-to-asg-expr-list-of-expr-fix-expr

(defthm expr-to-asg-expr-list-of-expr-fix-expr
  (equal (expr-to-asg-expr-list (expr-fix expr))
         (expr-to-asg-expr-list expr)))

Theorem: expr-to-asg-expr-list-expr-equiv-congruence-on-expr

(defthm expr-to-asg-expr-list-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-to-asg-expr-list expr)
                  (expr-to-asg-expr-list expr-equiv)))
  :rule-classes :congruence)