Execute a list of pure expression.
(exec-expr-pure-list es compst) → result
Given that the expression have no side effects (if there is no error), the order of evaluation does not matter. Thus, we proceed left to right.
This ACL2 function is only used in situations in which we are interested in the values of the expressions, not their expression values (i.e. object designators, if any). Thus, we just return lists of values here.
In the situations in which this ACL2 function is used, we also need to perform array-to-pointer conversion [C:6.3.2.1/3].
Function:
(defun exec-expr-pure-list (es compst) (declare (xargs :guard (and (expr-listp es) (compustatep compst)))) (let ((__function__ 'exec-expr-pure-list)) (declare (ignorable __function__)) (b* (((when (endp es)) nil) (eval (exec-expr-pure (car es) compst)) ((when (errorp eval)) eval) (eval (apconvert-expr-value eval)) ((when (errorp eval)) eval) (val (expr-value->value eval)) (vals (exec-expr-pure-list (cdr es) compst)) ((when (errorp vals)) vals)) (cons val vals))))
Theorem:
(defthm value-list-resultp-of-exec-expr-pure-list (b* ((result (exec-expr-pure-list es compst))) (value-list-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm exec-expr-pure-list-of-expr-list-fix-es (equal (exec-expr-pure-list (expr-list-fix es) compst) (exec-expr-pure-list es compst)))
Theorem:
(defthm exec-expr-pure-list-expr-list-equiv-congruence-on-es (implies (expr-list-equiv es es-equiv) (equal (exec-expr-pure-list es compst) (exec-expr-pure-list es-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm exec-expr-pure-list-of-compustate-fix-compst (equal (exec-expr-pure-list es (compustate-fix compst)) (exec-expr-pure-list es compst)))
Theorem:
(defthm exec-expr-pure-list-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (exec-expr-pure-list es compst) (exec-expr-pure-list es compst-equiv))) :rule-classes :congruence)