		Search-engine friendly clone of the ACL2 documentation.

Input-execution

Eval-input-file

Evaluate an input file.

Signature
(eval-input-file infile curve) → funargs
Arguments: infile — Guard (input-filep infile).; curve — Guard (curvep curve).
Returns: funargs — Type (funarg-list-resultp funargs).

This reduces to evaluating the input sections.

Definitions and Theorems

Function: eval-input-file

(defun eval-input-file (infile curve)
  (declare (xargs :guard (and (input-filep infile)
                              (curvep curve))))
  (let ((__function__ 'eval-input-file))
    (declare (ignorable __function__))
    (eval-input-section-list (input-file->sections infile)
                             curve)))

Theorem: funarg-list-resultp-of-eval-input-file

(defthm funarg-list-resultp-of-eval-input-file
  (b* ((funargs (eval-input-file infile curve)))
    (funarg-list-resultp funargs))
  :rule-classes :rewrite)

Theorem: eval-input-file-of-input-file-fix-infile

(defthm eval-input-file-of-input-file-fix-infile
  (equal (eval-input-file (input-file-fix infile)
                          curve)
         (eval-input-file infile curve)))

Theorem: eval-input-file-input-file-equiv-congruence-on-infile

(defthm eval-input-file-input-file-equiv-congruence-on-infile
  (implies (input-file-equiv infile infile-equiv)
           (equal (eval-input-file infile curve)
                  (eval-input-file infile-equiv curve)))
  :rule-classes :congruence)

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

(defthm eval-input-file-of-curve-fix-curve
  (equal (eval-input-file infile (curve-fix curve))
         (eval-input-file infile curve)))

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

(defthm eval-input-file-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-input-file infile curve)
                  (eval-input-file infile curve-equiv)))
  :rule-classes :congruence)