		Search-engine friendly clone of the ACL2 documentation.

Execution

Expr-value-to-value

Turn an expression value into a value.

Signature
(expr-value-to-value eval env) → val
Arguments: eval — Guard (expr-valuep eval).; env — Guard (denvp env).
Returns: val — Type (value-resultp val).

As explained in expr-value, an expression may evaluate to a location or to a value. When the expression is a sub-expression of a larger one, in some cases the location and value cases are treated differently, but in other cases the value of the expression is needed, whether it denotes a value or a location: if it denotes a location, the value stored in it is read; this way, expressions can be uniformly treated as returning values, when needed in the context of certain larger expressions.

This ACL2 function performs this conversion. If the expression value is just a value, it is returned. If the expression value is a location, the value is read from the location. The latter requires a dynamic environment, which is an additional parameter of this ACL2 function.

We return an error if the location cannot be read, but this should never be the case when we call this ACL2 function. We plan to look into formalizing and proving this invariant, e.g. via suitable guards.

Definitions and Theorems

Function: expr-value-to-value

(defun expr-value-to-value (eval env)
  (declare (xargs :guard (and (expr-valuep eval) (denvp env))))
  (let ((__function__ 'expr-value-to-value))
    (declare (ignorable __function__))
    (expr-value-case eval
                     :location (read-location eval.get env)
                     :value eval.get)))

Theorem: value-resultp-of-expr-value-to-value

(defthm value-resultp-of-expr-value-to-value
  (b* ((val (expr-value-to-value eval env)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: expr-value-to-value-of-expr-value-fix-eval

(defthm expr-value-to-value-of-expr-value-fix-eval
  (equal (expr-value-to-value (expr-value-fix eval)
                              env)
         (expr-value-to-value eval env)))

Theorem: expr-value-to-value-expr-value-equiv-congruence-on-eval

(defthm expr-value-to-value-expr-value-equiv-congruence-on-eval
  (implies (expr-value-equiv eval eval-equiv)
           (equal (expr-value-to-value eval env)
                  (expr-value-to-value eval-equiv env)))
  :rule-classes :congruence)

Theorem: expr-value-to-value-of-denv-fix-env

(defthm expr-value-to-value-of-denv-fix-env
  (equal (expr-value-to-value eval (denv-fix env))
         (expr-value-to-value eval env)))

Theorem: expr-value-to-value-denv-equiv-congruence-on-env

(defthm expr-value-to-value-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (expr-value-to-value eval env)
                  (expr-value-to-value eval env-equiv)))
  :rule-classes :congruence)