		Search-engine friendly clone of the ACL2 documentation.

Svex-alist-eval

Evaluate every expression in an svex-alist under the same environment.

Signature
(svex-alist-eval x env) → result
Arguments: x — Alist of variables to svex expressions to evaluate. Need not be fast.
Guard (svex-alist-p x).; env — Environment to evaluate the expressions under. Should be a fast-alist.
Guard (svex-env-p env).
Returns: result — New (slow) alist, binds the variables to their expressions' values.
Type (svex-env-p result).

Definitions and Theorems

Function: svex-alist-eval

(defun svex-alist-eval (x env)
  (declare (xargs :guard (and (svex-alist-p x)
                              (svex-env-p env))))
  (let ((__function__ 'svex-alist-eval))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (if (mbt (and (consp (car x)) (svar-p (caar x))))
               (cons (cons (caar x) (svex-eval (cdar x) env))
                     (svex-alist-eval (cdr x) env))
             (svex-alist-eval (cdr x) env)))
         :exec (with-fast-alist env (svex-alist-eval-aux x env)))))

Theorem: svex-env-p-of-svex-alist-eval

(defthm svex-env-p-of-svex-alist-eval
  (b* ((result (svex-alist-eval x env)))
    (svex-env-p result))
  :rule-classes :rewrite)

Theorem: svex-alist-eval-of-svex-alist-fix-x

(defthm svex-alist-eval-of-svex-alist-fix-x
  (equal (svex-alist-eval (svex-alist-fix x) env)
         (svex-alist-eval x env)))

Theorem: svex-alist-eval-svex-alist-equiv-congruence-on-x

(defthm svex-alist-eval-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-eval x env)
                  (svex-alist-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svex-alist-eval-of-svex-env-fix-env

(defthm svex-alist-eval-of-svex-env-fix-env
  (equal (svex-alist-eval x (svex-env-fix env))
         (svex-alist-eval x env)))

Theorem: svex-alist-eval-svex-env-equiv-congruence-on-env

(defthm svex-alist-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-alist-eval x env)
                  (svex-alist-eval x env-equiv)))
  :rule-classes :congruence)

Theorem: svex-env-lookup-of-svex-alist-eval

(defthm svex-env-lookup-of-svex-alist-eval
  (equal (svex-env-lookup k (svex-alist-eval x env))
         (let ((xk (svex-lookup k x)))
           (if xk (svex-eval xk env) (4vec-x)))))

Theorem: svex-env-boundp-of-svex-alist-eval

(defthm svex-env-boundp-of-svex-alist-eval
  (iff (svex-env-boundp k (svex-alist-eval x env))
       (svex-lookup k x)))

Theorem: svex-alist-eval-of-append

(defthm svex-alist-eval-of-append
  (equal (svex-alist-eval (append a b) env)
         (append (svex-alist-eval a env)
                 (svex-alist-eval b env))))

Theorem: alist-keys-of-svex-alist-eval

(defthm alist-keys-of-svex-alist-eval
  (equal (alist-keys (svex-alist-eval x env))
         (svex-alist-keys x)))

Subtopics

Svex-alist-eval-aux