		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-everything

Event expansion of the transformation.

Signature
(simpadd0-gen-everything code-old const-new) → (mv erp event)
Arguments: code-old — Guard (code-ensemblep code-old).; const-new — Guard (symbolp const-new).
Returns: event — Type (pseudo-event-formp event).

The vartys component of gin is initialized to nil here, and it applies to the first translation unit (if any): see simpadd0-filepath-transunit-map.

Definitions and Theorems

Function: simpadd0-gen-everything

(defun simpadd0-gen-everything (code-old const-new)
  (declare (xargs :guard (and (code-ensemblep code-old)
                              (symbolp const-new))))
  (declare (xargs :guard (and (code-ensemble-unambp code-old)
                              (code-ensemble-annop code-old))))
  (let ((__function__ 'simpadd0-gen-everything))
    (declare (ignorable __function__))
    (b* (((reterr) '(_))
         (gin (make-gin :ienv (code-ensemble->ienv code-old)
                        :const-new const-new
                        :vartys nil
                        :events nil
                        :thm-index 1))
         ((mv code-new (gout gout))
          (simpadd0-code-ensemble code-old gin))
         (const-event
              (cons 'defconst
                    (cons const-new
                          (cons (cons 'quote (cons code-new 'nil))
                                'nil)))))
      (retok (cons 'encapsulate
                   (cons 'nil
                         (cons const-event (rev gout.events))))))))

Theorem: pseudo-event-formp-of-simpadd0-gen-everything.event

(defthm pseudo-event-formp-of-simpadd0-gen-everything.event
  (b* (((mv acl2::?erp acl2::?event)
        (simpadd0-gen-everything code-old const-new)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)