		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-init-fun-env-thm

Generate the theorem asserting that applying init-fun-env to the translation unit gives the corresponding function environment.

Signature
(atc-gen-init-fun-env-thm init-fun-env-thm proofs prog-const fileset) → local-events
Arguments: init-fun-env-thm — Guard (symbolp init-fun-env-thm).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; fileset — Guard (filesetp fileset).
Returns: local-events — Type (pseudo-event-form-listp local-events).

The rationale for generating this theorem is explained in atc-gen-fileset.

Definitions and Theorems

Function: atc-gen-init-fun-env-thm

(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: pseudo-event-form-listp-of-atc-gen-init-fun-env-thm

(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)