		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-everything

Event expansion of the transformation.

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

Definitions and Theorems

Function: simpadd0-gen-everything

(defun simpadd0-gen-everything
       (tunits-old const-old const-new proofs)
 (declare (xargs :guard (and (transunit-ensemblep tunits-old)
                             (symbolp const-old)
                             (symbolp const-new)
                             (booleanp proofs))))
 (declare
      (xargs :guard (and (transunit-ensemble-unambp tunits-old)
                         (transunit-ensemble-annop tunits-old))))
 (let ((__function__ 'simpadd0-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((reterr) '(_))
    (tunits-new (simpadd0-transunit-ensemble tunits-old))
    ((mv erp &)
     (if (not proofs)
         (retok :irrelevant)
       (c$::ldm-transunit-ensemble tunits-old)))
    ((when erp)
     (reterr
      (msg
       "The old translation unit ensemble ~x0 ~
                      is not within the subset of C ~
                      covered by our formal semantics. ~
                      ~@1 ~
                      Thus, proofs cannot be generated: ~
                      re-run the transformation with :PROOFS NIL."
       tunits-old erp)))
    ((mv erp &)
     (if (not proofs)
         (retok :irrelevant)
       (c$::ldm-transunit-ensemble tunits-new)))
    ((when erp)
     (reterr
      (msg
       "The new translation unit ensemble ~x0 ~
                      is not within the subset of C ~
                      covered by our formal semantics. ~
                      ~@1 ~
                      Thus, proofs cannot be generated: ~
                      re-run the transformation with :PROOFS NIL."
       tunits-new erp)))
    (thm-events (and proofs
                     (simpadd0-gen-proofs-for-transunit-ensemble
                          const-old
                          const-new tunits-old tunits-new)))
    (const-event
         (cons 'defconst
               (cons const-new
                     (cons (cons 'quote (cons tunits-new 'nil))
                           'nil)))))
   (retok (cons 'encapsulate
                (cons 'nil
                      (cons const-event thm-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
             tunits-old const-old const-new proofs)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)