		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-expr-call-or-pure

Check an expression that must be a function call or a pure expression.

Signature
(check-expr-call-or-pure e funtab vartab tagenv) → type
Arguments: e — Guard (exprp e).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: type — Type (type-resultp 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.

Definitions and Theorems

Function: check-expr-call-or-pure

(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: type-resultp-of-check-expr-call-or-pure

(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: check-expr-call-or-pure-of-expr-fix-e

(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: check-expr-call-or-pure-expr-equiv-congruence-on-e

(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: check-expr-call-or-pure-of-fun-table-fix-funtab

(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: check-expr-call-or-pure-fun-table-equiv-congruence-on-funtab

(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: check-expr-call-or-pure-of-var-table-fix-vartab

(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: check-expr-call-or-pure-var-table-equiv-congruence-on-vartab

(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: check-expr-call-or-pure-of-tag-env-fix-tagenv

(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: check-expr-call-or-pure-tag-env-equiv-congruence-on-tagenv

(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)