		Search-engine friendly clone of the ACL2 documentation.

Program-checking

Check-program

Check a program.

Signature
(check-program prg) → api+senv
Arguments: prg — Guard (programp prg).
Returns: api+senv — Type (api+senv-resultp api+senv).

Currently a program consists of a single file in a single file. We type-check the file and we ensure it has no function or struct type recursion. Then we ensure that it has a main function, returning the corresponding API if it does. We also return the static environment for the program.

Definitions and Theorems

Function: check-program

(defun check-program (prg)
  (declare (xargs :guard (programp prg)))
  (let ((__function__ 'check-program))
    (declare (ignorable __function__))
    (b* ((pkg (program->package prg))
         (file (package->file pkg))
         ((okf senv) (typecheck-file file))
         (ok (file-function-recursion-okp file))
         ((unless ok)
          (reserrf :function-recursion))
         (ok (file-struct-recursion-okp file))
         ((unless ok)
          (reserrf :struct-reccursion))
         (decl (lookup-main-function file))
         ((unless decl) (reserrf :no-main))
         (api (make-api :inputs (fundecl->inputs decl)
                        :output (fundecl->output decl))))
      (make-api+senv :api api :senv senv))))

Theorem: api+senv-resultp-of-check-program

(defthm api+senv-resultp-of-check-program
  (b* ((api+senv (check-program prg)))
    (api+senv-resultp api+senv))
  :rule-classes :rewrite)

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

(defthm check-program-of-program-fix-prg
  (equal (check-program (program-fix prg))
         (check-program prg)))

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

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