		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-decl-decl

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

Signature
(xeq-decl-decl extension specs specs-new specs-thm-name init init-new init-thm-name vartys-post gin) → (mv decl 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).; init — Guard (initdeclor-listp init).; init-new — Guard (initdeclor-listp init-new).; init-thm-name — Guard (symbolp init-thm-name).; vartys-post — Guard (c::ident-type-mapp vartys-post).; gin — Guard (ginp gin).
Returns: decl — Type (declp decl).; 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-decl-decl

(defun xeq-decl-decl
       (extension specs specs-new specs-thm-name init
                  init-new init-thm-name vartys-post gin)
 (declare (xargs :guard (and (booleanp extension)
                             (decl-spec-listp specs)
                             (decl-spec-listp specs-new)
                             (symbolp specs-thm-name)
                             (initdeclor-listp init)
                             (initdeclor-listp init-new)
                             (symbolp init-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)
                             (initdeclor-list-unambp init)
                             (initdeclor-list-annop init)
                             (initdeclor-list-unambp init-new)
                             (initdeclor-list-annop init-new))))
 (let ((__function__ 'xeq-decl-decl))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (decl (make-decl-decl :extension extension
                          :specs specs
                          :init init))
    (decl-new (make-decl-decl :extension extension
                              :specs specs-new
                              :init init-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."
      init)
     (mv decl-new (irr-gout)))
    ((unless (and init-thm-name
                  (decl-block-formalp decl)))
     (mv decl-new gout-no-thm))
    ((unless (decl-block-formalp decl-new))
     (raise
      "Internal error: ~
                new declaration ~x0 is not in the formalized subset ~
                while old declaration ~x1 is."
      decl-new decl)
     (mv decl-new (irr-gout)))
    (initdeclor (car init))
    (var (dirdeclor-ident->ident
              (declor->direct (initdeclor->declor initdeclor))))
    (initer (initdeclor->init? initdeclor))
    (initdeclor-new (car init-new))
    ((unless
      (equal
        var
        (dirdeclor-ident->ident
             (declor->direct (initdeclor->declor initdeclor-new)))))
     (raise
      "Internal error: ~
                new variable ~x0 differs from old variable ~x1."
      (dirdeclor-ident->ident
           (declor->direct (initdeclor->declor initdeclor-new)))
      var)
     (mv decl-new (irr-gout)))
    (initer-new (initdeclor->init? initdeclor-new))
    ((unless (equal specs specs-new))
     (raise
      "Internal error: ~
                new declaration specifiers ~x0 differ from ~
                old declaration specifiers ~x1."
      specs-new specs)
     (mv decl-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 decl-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
            decl-decl-compustate-vars-old
            decl-decl-compustate-vars-new)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons init-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'decl-decl-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
                'decl-decl-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-decl-thm decl decl-new gin.vartys vartys-post
                   gin.const-new gin.thm-index hints)))
   (mv decl-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys vartys-post)))))

Theorem: declp-of-xeq-decl-decl.decl

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

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

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

Theorem: decl-unambp-of-xeq-decl-decl

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

Theorem: decl-annop-of-xeq-decl-decl

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

Theorem: decl-aidentp-of-xeq-decl-decl

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