Check an expression that must be a function call or an assignment.
(check-expr-call-or-asg e funtab vartab tagenv) → wf?
If the expression is a function call, we check it as such.
We also ensure that it returns
If the expression is not a function call, it must be an assignment expression, which we resort to check as such.
We retun no type here, because we apply these checks to expressions that form expression statements.
Function:
(defun check-expr-call-or-asg (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-asg)) (declare (ignorable __function__)) (if (expr-case e :call) (b* (((okf type) (check-expr-call (expr-call->fun e) (expr-call->args e) funtab vartab tagenv)) ((unless (type-case type :void)) (reserrf (list :nonvoid-function-result-discarded (expr-fix e))))) :wellformed) (check-expr-asg e funtab vartab tagenv))))
Theorem:
(defthm wellformed-resultp-of-check-expr-call-or-asg (b* ((wf? (check-expr-call-or-asg e funtab vartab tagenv))) (wellformed-resultp wf?)) :rule-classes :rewrite)
Theorem:
(defthm check-expr-call-or-asg-of-expr-fix-e (equal (check-expr-call-or-asg (expr-fix e) funtab vartab tagenv) (check-expr-call-or-asg e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-asg-expr-equiv-congruence-on-e (implies (expr-equiv e e-equiv) (equal (check-expr-call-or-asg e funtab vartab tagenv) (check-expr-call-or-asg e-equiv funtab vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-asg-of-fun-table-fix-funtab (equal (check-expr-call-or-asg e (fun-table-fix funtab) vartab tagenv) (check-expr-call-or-asg e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-asg-fun-table-equiv-congruence-on-funtab (implies (fun-table-equiv funtab funtab-equiv) (equal (check-expr-call-or-asg e funtab vartab tagenv) (check-expr-call-or-asg e funtab-equiv vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-asg-of-var-table-fix-vartab (equal (check-expr-call-or-asg e funtab (var-table-fix vartab) tagenv) (check-expr-call-or-asg e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-asg-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (check-expr-call-or-asg e funtab vartab tagenv) (check-expr-call-or-asg e funtab vartab-equiv tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-expr-call-or-asg-of-tag-env-fix-tagenv (equal (check-expr-call-or-asg e funtab vartab (tag-env-fix tagenv)) (check-expr-call-or-asg e funtab vartab tagenv)))
Theorem:
(defthm check-expr-call-or-asg-tag-env-equiv-congruence-on-tagenv (implies (tag-env-equiv tagenv tagenv-equiv) (equal (check-expr-call-or-asg e funtab vartab tagenv) (check-expr-call-or-asg e funtab vartab tagenv-equiv))) :rule-classes :congruence)