		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-list-none

Generate an empty list of block items.

Signature
(atc-gen-block-item-list-none term gin state) → gout
Arguments: term — Guard (pseudo-termp term).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

The empty list of block items itself is trivial of course, but we also generate a theorem about exec-block-item-list applied to the empty list of block items. This provide uniformity with non-empty lists of block items, when lists of block items that may be empty or not are involved within larger constructs.

We return 1 as the limit, which is needed in exec-block-item-list to not return an error due to the limit being exhausted.

Definitions and Theorems

Function: atc-gen-block-item-list-none

(defun atc-gen-block-item-list-none (term gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-list-none))
  (declare (ignorable __function__))
  (b*
   (((stmt-gin gin) gin)
    (wrld (w state))
    (limit (pseudo-term-quote 1))
    ((when (not gin.proofs))
     (make-stmt-gout :items nil
                     :type (type-void)
                     :term term
                     :context gin.context
                     :inscope gin.inscope
                     :limit limit
                     :events nil
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (name (pack gin.fn '-correct- gin.thm-index))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil gin.names-to-avoid wrld))
    (thm-index (1+ gin.thm-index))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-block-item-list
                     (cons 'nil
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons '(stmt-value-none)
                                 (cons gin.compst-var 'nil)))
                     'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var limit t wrld))
    ((mv type-formula type-thms)
     (atc-gen-term-type-formula
          (untranslate$ term nil state)
          (type-void)
          gin.affect gin.inscope gin.prec-tags))
    (type-formula
         (atc-contextualize type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (formula (cons 'and
                   (cons exec-formula (cons type-formula 'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-block-item-list-of-nil
            (cons
             'not-zp-of-limit-variable
             (cons
              'compustatep-of-add-frame
              (cons
               'compustatep-of-enter-scope
               (cons
                'compustatep-of-exit-scope
                (cons
                 'compustatep-of-add-var
                 (cons
                  'compustatep-of-update-var
                  (cons
                   'compustatep-of-update-object
                   (cons
                    'compustatep-of-update-static-var
                    (cons
                     'compustatep-of-if*-when-both-compustatep
                     (append
                      type-thms
                      '(uchar-array-length-of-uchar-array-write
                           schar-array-length-of-schar-array-write
                           ushort-array-length-of-ushort-array-write
                           sshort-array-length-of-sshort-array-write
                           uint-array-length-of-uint-array-write
                           sint-array-length-of-sint-array-write
                           ulong-array-length-of-ulong-array-write
                           slong-array-length-of-slong-array-write
                           ullong-array-length-of-ullong-array-write
                           sllong-array-length-of-sllong-array-write
                           mv-nth-of-cons (:e zp)))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (make-stmt-gout :items nil
                   :type (type-void)
                   :term term
                   :context gin.context
                   :inscope gin.inscope
                   :limit limit
                   :events (list event)
                   :thm-name name
                   :thm-index thm-index
                   :names-to-avoid names-to-avoid))))

Theorem: stmt-goutp-of-atc-gen-block-item-list-none

(defthm stmt-goutp-of-atc-gen-block-item-list-none
  (b* ((gout (atc-gen-block-item-list-none term gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)