Check a list of pure expressions.
(check-expr-pure-list es vartab tagenv) → types
This is used for arguments of function calls. The expression types returned by the expressions are subjected to lvalue conversion and array-to-pointer conversion.
Function:
(defun check-expr-pure-list (es vartab tagenv) (declare (xargs :guard (and (expr-listp es) (var-tablep vartab) (tag-envp tagenv)))) (let ((__function__ 'check-expr-pure-list)) (declare (ignorable __function__)) (b* (((when (endp es)) nil) ((okf etype) (check-expr-pure (car es) vartab tagenv)) (type (expr-type->type etype)) (type (apconvert-type type)) ((okf types) (check-expr-pure-list (cdr es) vartab tagenv))) (cons type types))))
Theorem:
(defthm type-list-resultp-of-check-expr-pure-list (b* ((types (check-expr-pure-list es vartab tagenv))) (type-list-resultp types)) :rule-classes :rewrite)
Theorem:
(defthm check-expr-pure-list-of-expr-list-fix-es (equal (check-expr-pure-list (expr-list-fix es) vartab tagenv) (check-expr-pure-list es vartab tagenv)))
Theorem:
(defthm check-expr-pure-list-expr-list-equiv-congruence-on-es (implies (expr-list-equiv es es-equiv) (equal (check-expr-pure-list es vartab tagenv) (check-expr-pure-list es-equiv vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-pure-list-of-var-table-fix-vartab (equal (check-expr-pure-list es (var-table-fix vartab) tagenv) (check-expr-pure-list es vartab tagenv)))
Theorem:
(defthm check-expr-pure-list-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (check-expr-pure-list es vartab tagenv) (check-expr-pure-list es vartab-equiv tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-pure-list-of-tag-env-fix-tagenv (equal (check-expr-pure-list es vartab (tag-env-fix tagenv)) (check-expr-pure-list es vartab tagenv)))
Theorem:
(defthm check-expr-pure-list-tag-env-equiv-congruence-on-tagenv (implies (tag-env-equiv tagenv tagenv-equiv) (equal (check-expr-pure-list es vartab tagenv) (check-expr-pure-list es vartab tagenv-equiv))) :rule-classes :congruence)