		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-expr-pure

Check a pure expression.

Signature
(check-expr-pure e vartab tagenv) → etype
Arguments: e — Guard (exprp e).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: etype — Type (expr-type-resultp etype).

More precisely, we check whether an expression is pure and well-formed. If all the checks are satisfied, we return the expression type of the expression (see expr-type).

We disallow function calls and pre/post-increment/decrement, since they are not pure. We only allow pure binary operators.

An identifier must be in the variable table. Its type is looked up there. An identifier is always an lvalue.

Definitions and Theorems

Function: check-expr-pure

(defun check-expr-pure (e vartab tagenv)
 (declare (xargs :guard (and (exprp e)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-expr-pure))
   (declare (ignorable __function__))
   (b* ((e (expr-fix e)))
     (expr-case
          e :ident
          (b* ((info (var-table-lookup e.get vartab))
               ((unless info)
                (reserrf (list :var-not-found e.get))))
            (make-expr-type :type (var-sinfo->type info)
                            :lvalue t))
          :const (check-const e.get)
          :arrsub
          (b* (((okf arr-etype)
                (check-expr-pure e.arr vartab tagenv))
               ((okf sub-etype)
                (check-expr-pure e.sub vartab tagenv)))
            (check-arrsub e.arr arr-etype e.sub sub-etype))
          :call (reserrf (list :expr-non-pure e))
          :member
          (b* (((okf etype)
                (check-expr-pure e.target vartab tagenv)))
            (check-member e.target etype e.name tagenv))
          :memberp
          (b* (((okf etype)
                (check-expr-pure e.target vartab tagenv)))
            (check-memberp e.target etype e.name tagenv))
          :postinc
          (reserrf (list :expr-non-pure e))
          :postdec
          (reserrf (list :expr-non-pure e))
          :preinc
          (reserrf (list :expr-non-pure e))
          :predec
          (reserrf (list :expr-non-pure e))
          :unary
          (b* (((okf arg-etype)
                (check-expr-pure e.arg vartab tagenv)))
            (check-unary e.op e.arg arg-etype))
          :cast
          (b* (((okf arg-etype)
                (check-expr-pure e.arg vartab tagenv)))
            (check-cast e.arg arg-etype e.type tagenv))
          :binary
          (b* (((unless (binop-purep e.op))
                (reserrf (list :binary-non-pure e)))
               ((okf arg1-etype)
                (check-expr-pure e.arg1 vartab tagenv))
               ((okf arg2-etype)
                (check-expr-pure e.arg2 vartab tagenv)))
            (check-binary-pure e.op
                               e.arg1 arg1-etype e.arg2 arg2-etype))
          :cond
          (b* (((okf test-etype)
                (check-expr-pure e.test vartab tagenv))
               ((okf then-etype)
                (check-expr-pure e.then vartab tagenv))
               ((okf else-etype)
                (check-expr-pure e.else vartab tagenv)))
            (check-cond e.test test-etype e.then
                        then-etype e.else else-etype))))))

Theorem: expr-type-resultp-of-check-expr-pure

(defthm expr-type-resultp-of-check-expr-pure
  (b* ((etype (check-expr-pure e vartab tagenv)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-expr-pure-of-expr-fix-e

(defthm check-expr-pure-of-expr-fix-e
  (equal (check-expr-pure (expr-fix e)
                          vartab tagenv)
         (check-expr-pure e vartab tagenv)))

Theorem: check-expr-pure-expr-equiv-congruence-on-e

(defthm check-expr-pure-expr-equiv-congruence-on-e
  (implies (expr-equiv e e-equiv)
           (equal (check-expr-pure e vartab tagenv)
                  (check-expr-pure e-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-expr-pure-of-var-table-fix-vartab

(defthm check-expr-pure-of-var-table-fix-vartab
  (equal (check-expr-pure e (var-table-fix vartab)
                          tagenv)
         (check-expr-pure e vartab tagenv)))

Theorem: check-expr-pure-var-table-equiv-congruence-on-vartab

(defthm check-expr-pure-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-expr-pure e vartab tagenv)
                  (check-expr-pure e vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-expr-pure-of-tag-env-fix-tagenv

(defthm check-expr-pure-of-tag-env-fix-tagenv
  (equal (check-expr-pure e vartab (tag-env-fix tagenv))
         (check-expr-pure e vartab tagenv)))

Theorem: check-expr-pure-tag-env-equiv-congruence-on-tagenv

(defthm check-expr-pure-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-expr-pure e vartab tagenv)
                  (check-expr-pure e vartab tagenv-equiv)))
  :rule-classes :congruence)