		Search-engine friendly clone of the ACL2 documentation.

Program-and-input-checking

Check-program-and-input

Check a program and an input file together.

Signature
(check-program-and-input prg infile) → env
Arguments: prg — Guard (programp prg).; infile — Guard (input-filep infile).
Returns: env — Type (senv-resultp env).

We first check the program, obtaining an API and a static environment. We use the static environment to check the input file. We match the program API to the result of checking the input file.

We temporarily allow the parameters of the main function to be a subset, as opposed to a permutation, of the input items in the input file. We plan to tighten this check to be a permutation instead.

If all the checks are successful, we return the static environment of the program.

Definitions and Theorems

Function: check-program-and-input

(defun check-program-and-input (prg infile)
  (declare (xargs :guard (and (programp prg)
                              (input-filep infile))))
  (let ((__function__ 'check-program-and-input))
    (declare (ignorable __function__))
    (b* (((okf api+senv) (check-program prg))
         (api (api+senv->api api+senv))
         (env (api+senv->senv api+senv))
         ((okf params)
          (check-input-file infile env))
         ((unless (subsetp-equal (api->inputs api)
                                 params))
          (reserrf (list :mismatched-inputs
                         :main (api->inputs api)
                         :file params))))
      env)))

Theorem: senv-resultp-of-check-program-and-input

(defthm senv-resultp-of-check-program-and-input
  (b* ((env (check-program-and-input prg infile)))
    (senv-resultp env))
  :rule-classes :rewrite)

Theorem: check-program-and-input-of-program-fix-prg

(defthm check-program-and-input-of-program-fix-prg
  (equal (check-program-and-input (program-fix prg)
                                  infile)
         (check-program-and-input prg infile)))

Theorem: check-program-and-input-program-equiv-congruence-on-prg

(defthm check-program-and-input-program-equiv-congruence-on-prg
  (implies (program-equiv prg prg-equiv)
           (equal (check-program-and-input prg infile)
                  (check-program-and-input prg-equiv infile)))
  :rule-classes :congruence)

Theorem: check-program-and-input-of-input-file-fix-infile

(defthm check-program-and-input-of-input-file-fix-infile
  (equal (check-program-and-input prg (input-file-fix infile))
         (check-program-and-input prg infile)))

Theorem: check-program-and-input-input-file-equiv-congruence-on-infile

(defthm
      check-program-and-input-input-file-equiv-congruence-on-infile
  (implies (input-file-equiv infile infile-equiv)
           (equal (check-program-and-input prg infile)
                  (check-program-and-input prg infile-equiv)))
  :rule-classes :congruence)