		Search-engine friendly clone of the ACL2 documentation.

Execution

Exec-literal

Execute a literal expression.

Signature
(exec-literal lit env) → evalue+denv
Arguments: lit — Guard (literalp lit).; env — Guard (denvp env).
Returns: evalue+denv — Type (evalue+denv-resultp evalue+denv).

We evaluate the literal, propagating errors. The resulting expression value is a value, not a location. The environment is unchanged.

Definitions and Theorems

Function: exec-literal

(defun exec-literal (lit env)
  (declare (xargs :guard (and (literalp lit) (denvp env))))
  (let ((__function__ 'exec-literal))
    (declare (ignorable __function__))
    (b* ((val (eval-literal lit (denv->curve env)))
         ((unless val)
          (reserrf (list :eval-literal-failed (literal-fix lit))))
         (eval (expr-value-value val)))
      (make-evalue+denv :evalue eval
                        :denv (denv-fix env)))))

Theorem: evalue+denv-resultp-of-exec-literal

(defthm evalue+denv-resultp-of-exec-literal
  (b* ((evalue+denv (exec-literal lit env)))
    (evalue+denv-resultp evalue+denv))
  :rule-classes :rewrite)

Theorem: exec-literal-of-literal-fix-lit

(defthm exec-literal-of-literal-fix-lit
  (equal (exec-literal (literal-fix lit) env)
         (exec-literal lit env)))

Theorem: exec-literal-literal-equiv-congruence-on-lit

(defthm exec-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (exec-literal lit env)
                  (exec-literal lit-equiv env)))
  :rule-classes :congruence)

Theorem: exec-literal-of-denv-fix-env

(defthm exec-literal-of-denv-fix-env
  (equal (exec-literal lit (denv-fix env))
         (exec-literal lit env)))

Theorem: exec-literal-denv-equiv-congruence-on-env

(defthm exec-literal-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-literal lit env)
                  (exec-literal lit env-equiv)))
  :rule-classes :congruence)