		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-declon

Generate a C block item that consists of an object declaration.

Signature
(atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state) → (mv item item-limit item-events item-thm new-inscope new-context thm-index names-to-avoid)
Arguments: var — Guard (symbolp var).; type — Guard (typep type).; expr — Guard (exprp expr).; expr-term — Guard (pseudo-termp expr-term).; expr-limit — Guard (pseudo-termp expr-limit).; expr-events — Guard (pseudo-event-form-listp expr-events).; expr-thm — Guard (symbolp expr-thm).; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; item-limit — Type (pseudo-termp item-limit), given (pseudo-termp expr-limit).; item-events — Type (pseudo-event-form-listp item-events), given (pseudo-event-form-listp expr-events).; item-thm — Type (symbolp item-thm).; new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope).; new-context — Type (atc-contextp new-context).; thm-index — Type (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid).

We get the (ACL2) variable, the type, and the expressions as inputs. We return not only the block item, and also a symbol table updated with the variable.

We generate a theorem about executing the initializer, and a theorem about executing the block item.

The limit for the block item is 3 more than the expression, because we need 1 to go from exec-block-item to its :declon case and to exec-obj-declon, 1 to go from there to exec-initer, and 1 to go from there to its :single case and to exec-expr.

Definitions and Theorems

Function: atc-gen-block-item-declon

(defun atc-gen-block-item-declon
       (var type expr expr-term expr-limit
            expr-events expr-thm gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp var)
                             (typep type)
                             (exprp expr)
                             (pseudo-termp expr-term)
                             (pseudo-termp expr-limit)
                             (pseudo-event-form-listp expr-events)
                             (symbolp expr-thm)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-declon))
  (declare (ignorable __function__))
  (b*
   (((stmt-gin gin) gin)
    (wrld (w state))
    ((mv tyspec declor)
     (ident+type-to-tyspec+declor
          (make-ident :name (symbol-name var))
          type))
    (initer (initer-single expr))
    (declon (make-obj-declon :scspec (scspecseq-none)
                             :tyspec tyspec
                             :declor declor
                             :init? initer))
    (item (block-item-declon declon))
    (item-limit (cons '+
                      (cons ''3 (cons expr-limit 'nil))))
    (varinfo (make-atc-var-info :type type
                                :thm nil
                                :externalp nil))
    ((when (not gin.proofs))
     (mv item item-limit expr-events nil
         (atc-add-var var varinfo gin.inscope)
         gin.context
         gin.thm-index gin.names-to-avoid))
    (new-compst
        (cons 'add-var
              (cons (cons 'ident
                          (cons (cons 'quote
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons expr-term (cons gin.compst-var 'nil)))))
    (item-thm-name (pack gin.fn '-correct- gin.thm-index))
    (thm-index (1+ gin.thm-index))
    ((mv item-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          item-thm-name
          nil gin.names-to-avoid wrld))
    (item-formula
     (cons
      'equal
      (cons
         (cons 'exec-block-item
               (cons (cons 'quote (cons item 'nil))
                     (cons gin.compst-var
                           (cons gin.fenv-var
                                 (cons gin.limit-var 'nil)))))
         (cons (cons 'mv
                     (cons '(stmt-value-none)
                           (cons (untranslate$ new-compst nil state)
                                 'nil)))
               'nil))))
    (item-formula
         (atc-contextualize item-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var item-limit t wrld))
    (valuep-when-type-pred
         (atc-type-to-valuep-thm type gin.prec-tags))
    (value-kind-when-type-pred
         (atc-type-to-value-kind-thm type gin.prec-tags))
    (type-of-value-when-type-pred
         (atc-type-to-type-of-value-thm type gin.prec-tags))
    (e-type (cons ':e
                  (cons (car (type-to-maker type)) 'nil)))
    (item-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-block-item-when-declon
            (cons
             'exec-obj-declon-open
             (cons
              'exec-initer-when-single
              (cons
               '(:e block-item-kind)
               (cons
                '(:e initer-kind)
                (cons
                 '(:e initer-single->get)
                 (cons
                  'not-zp-of-limit-variable
                  (cons
                   'not-zp-of-limit-minus-const
                   (cons
                    '(:e block-item-declon->get)
                    (cons
                     '(:e obj-declon-to-ident+scspec+tyname+init)
                     (cons
                      'mv-nth-of-cons
                      (cons
                       '(:e zp)
                       (cons
                        '(:e scspecseq-kind)
                        (cons
                         '(:e tyname-to-type)
                         (cons
                          '(:e type-kind)
                          (cons
                           'return-type-of-init-value-single
                           (cons
                            'init-value-to-value-when-single
                            (cons
                             expr-thm
                             (cons
                              valuep-when-type-pred
                              (cons
                               type-of-value-when-type-pred
                               (cons
                                e-type
                                (cons
                                 'create-var-of-const-identifier
                                 (cons
                                  '(:e identp)
                                  (cons
                                   '(:e ident->name)
                                   (cons
                                    'create-var-to-add-var
                                    (cons
                                     'create-var-okp-of-add-var
                                     (cons
                                      'create-var-okp-of-enter-scope
                                      (cons
                                       'create-var-okp-of-add-frame
                                       (cons
                                        'create-var-okp-of-update-var
                                        (cons
                                         'create-var-okp-of-update-object
                                         (cons
                                          'ident-fix-when-identp
                                          (cons
                                           'equal-of-ident-and-ident
                                           (cons
                                            '(:e str-fix)
                                            (cons
                                             'identp-of-ident
                                             (cons
                                              'compustate-frames-number-of-add-var-not-zero
                                              (cons
                                               'compustate-frames-number-of-enter-scope-not-zero
                                               (cons
                                                'compustate-frames-number-of-add-frame-not-zero
                                                (cons
                                                 'compustate-frames-number-of-update-var
                                                 (cons
                                                  'compustate-frames-number-of-update-object
                                                  (cons
                                                   'compustatep-of-add-var
                                                   (cons
                                                    'expr-valuep-of-expr-value
                                                    (cons
                                                     'expr-value->value-of-expr-value
                                                     (cons
                                                      'value-fix-when-valuep
                                                      (cons
                                                       'apconvert-expr-value-when-not-value-array
                                                       (cons
                                                        value-kind-when-type-pred
                                                        'nil)))))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv item-thm-event &)
     (evmac-generate-defthm item-thm-name
                            :formula item-formula
                            :hints item-hints
                            :enable nil))
    ((mv new-inscope
         new-context new-inscope-events
         thm-index names-to-avoid)
     (atc-gen-vardecl-inscope
          gin.fn
          gin.fn-guard gin.inscope gin.context var
          type (untranslate$ expr-term nil state)
          expr-thm gin.compst-var gin.prec-tags
          thm-index names-to-avoid wrld)))
   (mv item item-limit
       (append expr-events (list item-thm-event)
               new-inscope-events)
       item-thm-name new-inscope
       new-context thm-index names-to-avoid))))

Theorem: block-itemp-of-atc-gen-block-item-declon.item

(defthm block-itemp-of-atc-gen-block-item-declon.item
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (block-itemp item))
 :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-declon.item-limit

(defthm pseudo-termp-of-atc-gen-block-item-declon.item-limit
 (implies
   (pseudo-termp expr-limit)
   (b*
     (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
     (pseudo-termp item-limit)))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-block-item-declon.item-events

(defthm
   pseudo-event-form-listp-of-atc-gen-block-item-declon.item-events
 (implies
   (pseudo-event-form-listp expr-events)
   (b*
     (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
     (pseudo-event-form-listp item-events)))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-block-item-declon.item-thm

(defthm symbolp-of-atc-gen-block-item-declon.item-thm
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (symbolp item-thm))
 :rule-classes :rewrite)

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-declon.new-inscope

(defthm
 atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-declon.new-inscope
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (atc-symbol-varinfo-alist-listp new-inscope))
 :rule-classes :rewrite)

Theorem: atc-contextp-of-atc-gen-block-item-declon.new-context

(defthm atc-contextp-of-atc-gen-block-item-declon.new-context
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (atc-contextp new-context))
 :rule-classes :rewrite)

Theorem: posp-of-atc-gen-block-item-declon.thm-index

(defthm posp-of-atc-gen-block-item-declon.thm-index
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (posp thm-index))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-block-item-declon.names-to-avoid

(defthm symbol-listp-of-atc-gen-block-item-declon.names-to-avoid
 (b* (((mv ?item ?item-limit
           ?item-events ?item-thm ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-declon var type expr expr-term expr-limit
                                  expr-events expr-thm gin state)))
   (symbol-listp names-to-avoid))
 :rule-classes :rewrite)