Check an expression that must be a function call or a pure expression.
(check-expr-call-or-pure e funtab vartab tagenv) → type
If the expression is a function call, we check it as such.
If the expression is not a function call, it must be a pure expression, which we resort to check it as such.
We return a plain type, not an expression type, because the caller of this function do not need to differentiate between lvalues and not lvalues.
Function:
(defun check-expr-call-or-pure (e funtab vartab tagenv) (declare (xargs :guard (and (exprp e) (fun-tablep funtab) (var-tablep vartab) (tag-envp tagenv)))) (let ((__function__ 'check-expr-call-or-pure)) (declare (ignorable __function__)) (if (expr-case e :call) (check-expr-call (expr-call->fun e) (expr-call->args e) funtab vartab tagenv) (b* (((okf etype) (check-expr-pure e vartab tagenv))) (expr-type->type etype)))))
Theorem:
(defthm type-resultp-of-check-expr-call-or-pure (b* ((type (check-expr-call-or-pure e funtab vartab tagenv))) (type-resultp type)) :rule-classes :rewrite)
Theorem:
(defthm check-expr-call-or-pure-of-expr-fix-e (equal (check-expr-call-or-pure (expr-fix e) funtab vartab tagenv) (check-expr-call-or-pure e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-pure-expr-equiv-congruence-on-e (implies (expr-equiv e e-equiv) (equal (check-expr-call-or-pure e funtab vartab tagenv) (check-expr-call-or-pure e-equiv funtab vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-pure-of-fun-table-fix-funtab (equal (check-expr-call-or-pure e (fun-table-fix funtab) vartab tagenv) (check-expr-call-or-pure e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-pure-fun-table-equiv-congruence-on-funtab (implies (fun-table-equiv funtab funtab-equiv) (equal (check-expr-call-or-pure e funtab vartab tagenv) (check-expr-call-or-pure e funtab-equiv vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-pure-of-var-table-fix-vartab (equal (check-expr-call-or-pure e funtab (var-table-fix vartab) tagenv) (check-expr-call-or-pure e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-pure-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (check-expr-call-or-pure e funtab vartab tagenv) (check-expr-call-or-pure e funtab vartab-equiv tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-pure-of-tag-env-fix-tagenv (equal (check-expr-call-or-pure e funtab vartab (tag-env-fix tagenv)) (check-expr-call-or-pure e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-pure-tag-env-equiv-congruence-on-tagenv (implies (tag-env-equiv tagenv tagenv-equiv) (equal (check-expr-call-or-pure e funtab vartab tagenv) (check-expr-call-or-pure e funtab vartab tagenv-equiv))) :rule-classes :congruence)