Turn an expression into a list of assignment expressions.
(expr-to-asg-expr-list expr) → 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
Function:
(defun expr-to-asg-expr-list (expr) (declare (xargs :guard (exprp expr))) (let ((__function__ 'expr-to-asg-expr-list)) (declare (ignorable __function__)) (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:
(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:
(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:
(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)