		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Exec-program

Execute a program.

Signature
(exec-program prg input curve limit) → result
Arguments: prg — Guard (programp prg).; input — Guard (input-filep input).; curve — Guard (curvep curve).; limit — Guard (natp limit).
Returns: result — Type (value-resultp result).

We execute the input file, obtaining arguments. We find the main function, and match the arguments to its parameters. We call he main function with the resulting values.

Definitions and Theorems

Function: exec-program

(defun exec-program (prg input curve limit)
  (declare (xargs :guard (and (programp prg)
                              (input-filep input)
                              (curvep curve)
                              (natp limit))))
  (let ((__function__ 'exec-program))
    (declare (ignorable __function__))
    (b* (((okf args)
          (eval-input-file input curve))
         (pkg (program->package prg))
         (file (package->file pkg))
         (main (lookup-main-function file))
         ((unless main)
          (reserrf :no-main-function))
         (params (fundecl->inputs main))
         ((okf vals)
          (funparams-match-funargs params args)))
      (exec-file-main file vals curve limit))))

Theorem: value-resultp-of-exec-program

(defthm value-resultp-of-exec-program
  (b* ((result (exec-program prg input curve limit)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: exec-program-of-program-fix-prg

(defthm exec-program-of-program-fix-prg
  (equal (exec-program (program-fix prg)
                       input curve limit)
         (exec-program prg input curve limit)))

Theorem: exec-program-program-equiv-congruence-on-prg

(defthm exec-program-program-equiv-congruence-on-prg
  (implies (program-equiv prg prg-equiv)
           (equal (exec-program prg input curve limit)
                  (exec-program prg-equiv input curve limit)))
  :rule-classes :congruence)

Theorem: exec-program-of-input-file-fix-input

(defthm exec-program-of-input-file-fix-input
  (equal (exec-program prg (input-file-fix input)
                       curve limit)
         (exec-program prg input curve limit)))

Theorem: exec-program-input-file-equiv-congruence-on-input

(defthm exec-program-input-file-equiv-congruence-on-input
  (implies (input-file-equiv input input-equiv)
           (equal (exec-program prg input curve limit)
                  (exec-program prg input-equiv curve limit)))
  :rule-classes :congruence)

Theorem: exec-program-of-curve-fix-curve

(defthm exec-program-of-curve-fix-curve
  (equal (exec-program prg input (curve-fix curve)
                       limit)
         (exec-program prg input curve limit)))

Theorem: exec-program-curve-equiv-congruence-on-curve

(defthm exec-program-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (exec-program prg input curve limit)
                  (exec-program prg input curve-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-program-of-nfix-limit

(defthm exec-program-of-nfix-limit
  (equal (exec-program prg input curve (nfix limit))
         (exec-program prg input curve limit)))

Theorem: exec-program-nat-equiv-congruence-on-limit

(defthm exec-program-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-program prg input curve limit)
                  (exec-program prg input curve limit-equiv)))
  :rule-classes :congruence)