		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-transunit

Transform a translation unit.

Signature
(simpadd0-transunit tunit gin) → (mv new-tunit gout)
Arguments: tunit — Guard (transunitp tunit).; gin — Guard (ginp gin).
Returns: new-tunit — Type (transunitp new-tunit).; gout — Type (goutp gout).

The gin passed as input has vartys set to nil (see simpadd0-filepath-transunit-map), but the theorem index and the list of events may be the result of transforming previous translation units.

We generate a comment at the beginning of the translation unit that says that the file was generated by this transformation.

Definitions and Theorems

Function: simpadd0-transunit

(defun simpadd0-transunit (tunit gin)
 (declare (xargs :guard (and (transunitp tunit) (ginp gin))))
 (declare (xargs :guard (and (transunit-unambp tunit)
                             (transunit-annop tunit))))
 (let ((__function__ 'simpadd0-transunit))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    ((transunit tunit) tunit)
    ((mv new-declons (gout gout-decls))
     (simpadd0-ext-declon-list tunit.declons gin))
    (gin (gin-update gin gout-decls))
    (comment
      (acl2::string=>nats "This file is generated by 'simpadd0'.")))
   (mv (make-transunit :comment comment
                       :declons new-declons
                       :info tunit.info)
       (gout-no-thm gin)))))

Theorem: transunitp-of-simpadd0-transunit.new-tunit

(defthm transunitp-of-simpadd0-transunit.new-tunit
  (b* (((mv ?new-tunit ?gout)
        (simpadd0-transunit tunit gin)))
    (transunitp new-tunit))
  :rule-classes :rewrite)

Theorem: goutp-of-simpadd0-transunit.gout

(defthm goutp-of-simpadd0-transunit.gout
  (b* (((mv ?new-tunit ?gout)
        (simpadd0-transunit tunit gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: transunit-unambp-of-simpadd0-transunit

(defthm transunit-unambp-of-simpadd0-transunit
  (b* (((mv ?new-tunit ?gout)
        (simpadd0-transunit tunit gin)))
    (transunit-unambp new-tunit)))

Theorem: transunit-annop-of-simpadd0-transunit

(defthm transunit-annop-of-simpadd0-transunit
  (implies (and (transunit-unambp tunit)
                (transunit-annop tunit))
           (b* (((mv ?new-tunit ?gout)
                 (simpadd0-transunit tunit gin)))
             (transunit-annop new-tunit))))

Theorem: transunit-aidentp-of-simpadd0-transunit

(defthm transunit-aidentp-of-simpadd0-transunit
  (implies (and (transunit-unambp tunit)
                (transunit-aidentp tunit gcc))
           (b* (((mv ?new-tunit ?gout)
                 (simpadd0-transunit tunit gin)))
             (transunit-aidentp new-tunit gcc))))

Theorem: simpadd0-transunit-of-transunit-fix-tunit

(defthm simpadd0-transunit-of-transunit-fix-tunit
  (equal (simpadd0-transunit (c$::transunit-fix tunit)
                             gin)
         (simpadd0-transunit tunit gin)))

Theorem: simpadd0-transunit-transunit-equiv-congruence-on-tunit

(defthm simpadd0-transunit-transunit-equiv-congruence-on-tunit
  (implies (c$::transunit-equiv tunit tunit-equiv)
           (equal (simpadd0-transunit tunit gin)
                  (simpadd0-transunit tunit-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-transunit-of-gin-fix-gin

(defthm simpadd0-transunit-of-gin-fix-gin
  (equal (simpadd0-transunit tunit (gin-fix gin))
         (simpadd0-transunit tunit gin)))

Theorem: simpadd0-transunit-gin-equiv-congruence-on-gin

(defthm simpadd0-transunit-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-transunit tunit gin)
                  (simpadd0-transunit tunit gin-equiv)))
  :rule-classes :congruence)