Generate the theorem asserting that applying init-fun-env to the translation unit gives the corresponding function environment.
(atc-gen-init-fun-env-thm init-fun-env-thm proofs prog-const fileset) → local-events
The rationale for generating this theorem is explained in atc-gen-fileset.
Function:
(defun atc-gen-init-fun-env-thm (init-fun-env-thm proofs prog-const fileset) (declare (xargs :guard (and (symbolp init-fun-env-thm) (booleanp proofs) (symbolp prog-const) (filesetp fileset)))) (let ((__function__ 'atc-gen-init-fun-env-thm)) (declare (ignorable __function__)) (b* (((unless proofs) nil) (tunit (preprocess fileset)) ((when (reserrp tunit)) (raise "Internal error: preprocessing of ~x0 fails with error ~x1." fileset tunit)) (fenv (init-fun-env tunit)) ((when (errorp fenv)) (raise "Internal error: ~ function environment initialization of ~x0 ~ fails with error ~x1." tunit fenv)) (formula (cons 'equal (cons (cons 'init-fun-env (cons (cons 'preprocess (cons prog-const 'nil)) 'nil)) (cons (cons 'quote (cons fenv 'nil)) 'nil)))) (hints '(("Goal" :in-theory '((:e preprocess) (:e init-fun-env))))) ((mv event &) (evmac-generate-defthm init-fun-env-thm :formula formula :hints hints :enable nil))) (list event))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-init-fun-env-thm (b* ((local-events (atc-gen-init-fun-env-thm init-fun-env-thm proofs prog-const fileset))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)