		Search-engine friendly clone of the ACL2 documentation.

Value-expressions

Value-expr-to-value

Value denoted by an expression value.

Signature
(value-expr-to-value expr curve) → val
Arguments: expr — Guard (expressionp expr).; curve — Guard (curvep curve).
Returns: val — Type (value-resultp val).

If the expression value is a literal, we evaluate it.

If it is a unary expression, whose operator must be - and whose operand must be a signed integer, there are two cases: (i) if the operand's numeral is the absolute value of the most negative value of the literal's type, the value is the most negative of that type; (ii) otherwise, we evaluate the literal and then we negate it.

If any of these evaluations fails, we return nil.

Theorem: return-type-of-value-expr-to-value.val

(defthm return-type-of-value-expr-to-value.val
  (b* ((?val (value-expr-to-value expr curve)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: return-type-of-value-expr-list-to-value-list.vals

(defthm return-type-of-value-expr-list-to-value-list.vals
  (b* ((?vals (value-expr-list-to-value-list exprs curve)))
    (value-list-resultp vals))
  :rule-classes :rewrite)

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

(defthm value-expr-to-value-of-expression-fix-expr
  (equal (value-expr-to-value (expression-fix expr)
                              curve)
         (value-expr-to-value expr curve)))

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

(defthm value-expr-to-value-of-curve-fix-curve
  (equal (value-expr-to-value expr (curve-fix curve))
         (value-expr-to-value expr curve)))

Theorem: value-expr-list-to-value-list-of-expression-list-fix-exprs

(defthm value-expr-list-to-value-list-of-expression-list-fix-exprs
  (equal (value-expr-list-to-value-list (expression-list-fix exprs)
                                        curve)
         (value-expr-list-to-value-list exprs curve)))

Theorem: value-expr-list-to-value-list-of-curve-fix-curve

(defthm value-expr-list-to-value-list-of-curve-fix-curve
  (equal (value-expr-list-to-value-list exprs (curve-fix curve))
         (value-expr-list-to-value-list exprs curve)))

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

(defthm value-expr-to-value-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (value-expr-to-value expr curve)
                  (value-expr-to-value expr-equiv curve)))
  :rule-classes :congruence)

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

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

Theorem: value-expr-list-to-value-list-expression-list-equiv-congruence-on-exprs

(defthm
 value-expr-list-to-value-list-expression-list-equiv-congruence-on-exprs
 (implies (expression-list-equiv exprs exprs-equiv)
          (equal (value-expr-list-to-value-list exprs curve)
                 (value-expr-list-to-value-list exprs-equiv curve)))
 :rule-classes :congruence)

Theorem: value-expr-list-to-value-list-curve-equiv-congruence-on-curve

(defthm
      value-expr-list-to-value-list-curve-equiv-congruence-on-curve
 (implies (curve-equiv curve curve-equiv)
          (equal (value-expr-list-to-value-list exprs curve)
                 (value-expr-list-to-value-list exprs curve-equiv)))
 :rule-classes :congruence)

Subtopics

Value-expr-list-to-value-list