		Search-engine friendly clone of the ACL2 documentation.

Input-execution

Eval-input-item

Evaluate an input item.

Signature
(eval-input-item initem intitle curve) → funarg
Arguments: initem — Guard (input-itemp initem).; intitle — Guard (input-titlep intitle).; curve — Guard (curvep curve).
Returns: funarg — Type (funarg-resultp funarg).

We evaluate the input item to a function argument, which has the same name as the input item, whose sort is determined by the input title under which the item appears, and whose value is obtained by evaluating the input expression.

Definitions and Theorems

Function: eval-input-item

(defun eval-input-item (initem intitle curve)
  (declare (xargs :guard (and (input-itemp initem)
                              (input-titlep intitle)
                              (curvep curve))))
  (let ((__function__ 'eval-input-item))
    (declare (ignorable __function__))
    (b* (((input-item initem) initem)
         (expr (input-expression->get initem.value))
         ((unless (expression-valuep expr))
          (reserrf (list :not-value-expression expr)))
         ((okf val)
          (value-expr-to-value expr curve)))
      (make-funarg :name initem.name
                   :sort (input-title->sort intitle)
                   :value val))))

Theorem: funarg-resultp-of-eval-input-item

(defthm funarg-resultp-of-eval-input-item
  (b* ((funarg (eval-input-item initem intitle curve)))
    (funarg-resultp funarg))
  :rule-classes :rewrite)

Theorem: eval-input-item-of-input-item-fix-initem

(defthm eval-input-item-of-input-item-fix-initem
  (equal (eval-input-item (input-item-fix initem)
                          intitle curve)
         (eval-input-item initem intitle curve)))

Theorem: eval-input-item-input-item-equiv-congruence-on-initem

(defthm eval-input-item-input-item-equiv-congruence-on-initem
  (implies (input-item-equiv initem initem-equiv)
           (equal (eval-input-item initem intitle curve)
                  (eval-input-item initem-equiv intitle curve)))
  :rule-classes :congruence)

Theorem: eval-input-item-of-input-title-fix-intitle

(defthm eval-input-item-of-input-title-fix-intitle
  (equal (eval-input-item initem (input-title-fix intitle)
                          curve)
         (eval-input-item initem intitle curve)))

Theorem: eval-input-item-input-title-equiv-congruence-on-intitle

(defthm eval-input-item-input-title-equiv-congruence-on-intitle
  (implies (input-title-equiv intitle intitle-equiv)
           (equal (eval-input-item initem intitle curve)
                  (eval-input-item initem intitle-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-input-item-of-curve-fix-curve

(defthm eval-input-item-of-curve-fix-curve
  (equal (eval-input-item initem intitle (curve-fix curve))
         (eval-input-item initem intitle curve)))

Theorem: eval-input-item-curve-equiv-congruence-on-curve

(defthm eval-input-item-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-input-item initem intitle curve)
                  (eval-input-item initem intitle curve-equiv)))
  :rule-classes :congruence)