		Search-engine friendly clone of the ACL2 documentation.

Type-checking

File-to-senv

Build a static environment from a file.

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

Starting with the initial (empty) static environment, we extend it with all the top-level declarations in the file.

Definitions and Theorems

Function: file-to-senv

(defun file-to-senv (file)
  (declare (xargs :guard (filep file)))
  (let ((__function__ 'file-to-senv))
    (declare (ignorable __function__))
    (extend-senv-with-topdecl-list
         (programdecl->items (file->program file))
         (init-senv))))

Theorem: senv-resultp-of-file-to-senv

(defthm senv-resultp-of-file-to-senv
  (b* ((env (file-to-senv file)))
    (senv-resultp env))
  :rule-classes :rewrite)

Theorem: file-to-senv-of-file-fix-file

(defthm file-to-senv-of-file-fix-file
  (equal (file-to-senv (file-fix file))
         (file-to-senv file)))

Theorem: file-to-senv-file-equiv-congruence-on-file

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