Svex-eval
Evaluate an svex in some environment.
- Signature
(svex-eval x env) → val
- Arguments
- x — Expression to evaluate.
Guard (svex-p x).
- env — Variable bindings. Must be a fast-alist.
Guard (svex-env-p env).
- Returns
- val — Value of x under this environment.
Type (4vec-p val).
svex-eval is a straightforward evaluator for svex
formulas. It takes as arguments an svex object to evaluate, and an
environment mapping variables (svar objects) to 4vec values. It
returns the 4vec value of the formula, under this assignment, in the
obvious way:
- Constants evaluate to themselves.
- Variables are looked up using svex-env-fastlookup. Note that any
unbound variables evaluate to an infinite-width X.
- Functions applications are handled with svex-apply.
We typically expect svexes to be constructed with hons. To
take advantage of this structure sharing, we memoize svex-eval.
Theorem: return-type-of-svex-eval.val
(defthm return-type-of-svex-eval.val
(b* ((?val (svex-eval x env)))
(4vec-p val))
:rule-classes :rewrite)
Theorem: return-type-of-svexlist-eval.vals
(defthm return-type-of-svexlist-eval.vals
(b* ((?vals (svexlist-eval x env)))
(4veclist-p vals))
:rule-classes :rewrite)
Function: svex-eval-memoize-condition
(defun svex-eval-memoize-condition (x env)
(declare (ignorable x env)
(xargs :guard (if (svex-p x) (svex-env-p env) 'nil)))
(eq (svex-kind x) :call))
Subtopics
- Svex-eval-basics
- Very basic lemmas about svex-eval.
