		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Typecheck-file

Type-check a file.

Signature
(typecheck-file file) → ok
Arguments: file — Guard (filep file).
Returns: ok — Type (senv-resultp ok).

First we go through the file and build the initial static environment, which we use to type-check all the declarations that form the file. In case of success, we return the static environment for the file: this is used as context to check input files.

Definitions and Theorems

Function: typecheck-file

(defun typecheck-file (file)
  (declare (xargs :guard (filep file)))
  (let ((__function__ 'typecheck-file))
    (declare (ignorable __function__))
    (b* (((okf env) (file-to-senv file))
         ((okf &)
          (typecheck-topdecl-list
               (programdecl->items (file->program file))
               env)))
      env)))

Theorem: senv-resultp-of-typecheck-file

(defthm senv-resultp-of-typecheck-file
  (b* ((ok (typecheck-file file)))
    (senv-resultp ok))
  :rule-classes :rewrite)

Theorem: typecheck-file-of-file-fix-file

(defthm typecheck-file-of-file-fix-file
  (equal (typecheck-file (file-fix file))
         (typecheck-file file)))

Theorem: typecheck-file-file-equiv-congruence-on-file

(defthm typecheck-file-file-equiv-congruence-on-file
  (implies (file-equiv file file-equiv)
           (equal (typecheck-file file)
                  (typecheck-file file-equiv)))
  :rule-classes :congruence)