		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-declon-declon

Equality lifting transformation of a non-static-assert declaration.

Signature
(xeq-declon-declon extension specs specs-new specs-thm-name ideclors ideclors-new ideclors-thm-name vartys-post gin) → (mv declon gout)
Arguments: extension — Guard (booleanp extension).; specs — Guard (decl-spec-listp specs).; specs-new — Guard (decl-spec-listp specs-new).; specs-thm-name — Guard (symbolp specs-thm-name).; ideclors — Guard (init-declor-listp ideclors).; ideclors-new — Guard (init-declor-listp ideclors-new).; ideclors-thm-name — Guard (symbolp ideclors-thm-name).; vartys-post — Guard (c::ident-type-mapp vartys-post).; gin — Guard (ginp gin).
Returns: declon — Type (declonp declon).; gout — Type (goutp gout).

We combine the (untransformed) extension flag with the possibly transformed declaration specifiers and initializer declarators.

Currently we do not generate theorems for lists of declaration specifiers. We double-check that here.

Definitions and Theorems

Function: xeq-declon-declon

(defun xeq-declon-declon
       (extension specs specs-new
                  specs-thm-name ideclors ideclors-new
                  ideclors-thm-name vartys-post gin)
 (declare (xargs :guard (and (booleanp extension)
                             (decl-spec-listp specs)
                             (decl-spec-listp specs-new)
                             (symbolp specs-thm-name)
                             (init-declor-listp ideclors)
                             (init-declor-listp ideclors-new)
                             (symbolp ideclors-thm-name)
                             (c::ident-type-mapp vartys-post)
                             (ginp gin))))
 (declare
      (xargs :guard (and (decl-spec-list-unambp specs)
                         (decl-spec-list-annop specs)
                         (decl-spec-list-unambp specs-new)
                         (decl-spec-list-annop specs-new)
                         (init-declor-list-unambp ideclors)
                         (init-declor-list-annop ideclors)
                         (init-declor-list-unambp ideclors-new)
                         (init-declor-list-annop ideclors-new))))
 (let ((__function__ 'xeq-declon-declon))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (declon (make-declon-declon :extension extension
                                :specs specs
                                :declors ideclors))
    (declon-new (make-declon-declon :extension extension
                                    :specs specs-new
                                    :declors ideclors-new))
    (gout-no-thm (change-gout (gout-no-thm gin)
                              :vartys vartys-post))
    ((when specs-thm-name)
     (raise
      "Internal error: ~
                new list of initializer declarators ~x0 ~
                is not in the formalized subset."
      ideclors)
     (mv declon-new (irr-gout)))
    ((unless (and ideclors-thm-name
                  (declon-block-formalp declon)))
     (mv declon-new gout-no-thm))
    ((unless (declon-block-formalp declon-new))
     (raise
      "Internal error: ~
                new declaration ~x0 is not in the formalized subset ~
                while old declaration ~x1 is."
      declon-new declon)
     (mv declon-new (irr-gout)))
    (initdeclor (car ideclors))
    (var (dirdeclor-ident->ident
              (declor->direct (init-declor->declor initdeclor))))
    (initer (init-declor->initer? initdeclor))
    (initdeclor-new (car ideclors-new))
    ((unless
      (equal
       var
       (dirdeclor-ident->ident
            (declor->direct (init-declor->declor initdeclor-new)))))
     (raise
      "Internal error: ~
                new variable ~x0 differs from old variable ~x1."
      (dirdeclor-ident->ident
           (declor->direct (init-declor->declor initdeclor-new)))
      var)
     (mv declon-new (irr-gout)))
    (initer-new (init-declor->initer? initdeclor-new))
    ((unless (equal specs specs-new))
     (raise
      "Internal error: ~
                new declaration specifiers ~x0 differ from ~
                old declaration specifiers ~x1."
      specs-new specs)
     (mv declon-new (irr-gout)))
    ((mv & tyspecs)
     (check-decl-spec-list-all-typespec specs))
    ((mv & ctyspecs)
     (ldm-type-spec-list tyspecs))
    (ctype (c::tyspecseq-to-type ctyspecs))
    ((unless (c::type-nonchar-integerp ctype))
     (mv declon-new gout-no-thm))
    ((mv & cvar) (ldm-ident var))
    ((mv & old-initer) (ldm-initer initer))
    ((mv & new-initer)
     (ldm-initer initer-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::obj-declon->scspec)
            (:e c::obj-declon->tyspec)
            (:e c::obj-declon->declor)
            (:e c::obj-declon->init?)
            (:e c::obj-declon)
            (:e c::obj-declor-kind)
            (:e c::obj-declor-ident->get)
            (:e c::obj-declor-ident)
            (:e c::scspecseq-none)
            (:e c::tyspecseq-to-type)
            (:e c::identp)
            c::compustate-frames-number-of-exec-initer
            c::compustatep-when-compustate-resultp-and-not-errorp
            declon-declon-compustate-vars-old
            declon-declon-compustate-vars-new)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons ideclors-thm-name
                        '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'declon-declon-congruence
               (cons
                (cons 'var
                      (cons (cons 'quote (cons cvar 'nil))
                            'nil))
                (cons
                 (cons 'tyspecs
                       (cons (cons 'quote (cons ctyspecs 'nil))
                             'nil))
                 (cons
                  (cons 'old-initer
                        (cons (cons 'quote (cons old-initer 'nil))
                              'nil))
                  (cons
                    (cons 'new-initer
                          (cons (cons 'quote (cons new-initer 'nil))
                                'nil))
                    'nil))))))
             (cons
              (cons
               ':instance
               (cons
                'declon-declon-errors
                (cons
                 (cons 'var
                       (cons (cons 'quote (cons cvar 'nil))
                             'nil))
                 (cons
                  (cons 'tyspecs
                        (cons (cons 'quote (cons ctyspecs 'nil))
                              'nil))
                  (cons
                    (cons 'initer
                          (cons (cons 'quote (cons old-initer 'nil))
                                'nil))
                    '((fenv old-fenv)))))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-declon-thm declon declon-new gin.vartys vartys-post
                     gin.const-new gin.thm-index hints)))
   (mv declon-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys vartys-post)))))

Theorem: declonp-of-xeq-declon-declon.declon

(defthm declonp-of-xeq-declon-declon.declon
  (b* (((mv c$::?declon ?gout)
        (xeq-declon-declon extension specs specs-new
                           specs-thm-name ideclors ideclors-new
                           ideclors-thm-name vartys-post gin)))
    (declonp declon))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-declon-declon.gout

(defthm goutp-of-xeq-declon-declon.gout
  (b* (((mv c$::?declon ?gout)
        (xeq-declon-declon extension specs specs-new
                           specs-thm-name ideclors ideclors-new
                           ideclors-thm-name vartys-post gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: declon-unambp-of-xeq-declon-declon

(defthm declon-unambp-of-xeq-declon-declon
  (implies
       (and (decl-spec-list-unambp specs-new)
            (init-declor-list-unambp ideclors-new))
       (b* (((mv c$::?declon ?gout)
             (xeq-declon-declon extension specs specs-new
                                specs-thm-name ideclors ideclors-new
                                ideclors-thm-name vartys-post gin)))
         (declon-unambp declon))))

Theorem: declon-annop-of-xeq-declon-declon

(defthm declon-annop-of-xeq-declon-declon
  (implies
       (and (decl-spec-list-annop specs-new)
            (init-declor-list-annop ideclors-new))
       (b* (((mv c$::?declon ?gout)
             (xeq-declon-declon extension specs specs-new
                                specs-thm-name ideclors ideclors-new
                                ideclors-thm-name vartys-post gin)))
         (declon-annop declon))))

Theorem: declon-aidentp-of-xeq-declon-declon

(defthm declon-aidentp-of-xeq-declon-declon
  (implies
       (and (decl-spec-list-aidentp specs-new gcc)
            (init-declor-list-aidentp ideclors-new gcc))
       (b* (((mv c$::?declon ?gout)
             (xeq-declon-declon extension specs specs-new
                                specs-thm-name ideclors ideclors-new
                                ideclors-thm-name vartys-post gin)))
         (declon-aidentp declon gcc))))