		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-list-cons

Generate a list of block items by consing a block item to a list of block items.

Signature
(atc-gen-block-item-list-cons term item item-limit item-events item-thm items items-limit items-events items-thm items-type new-context new-inscope gin state) → gout
Arguments: term — Guard (pseudo-termp term).; item — Guard (block-itemp item).; item-limit — Guard (pseudo-termp item-limit).; item-events — Guard (pseudo-event-form-listp item-events).; item-thm — Guard (symbolp item-thm).; items — Guard (block-item-listp items).; items-limit — Guard (pseudo-termp items-limit).; items-events — Guard (pseudo-event-form-listp items-events).; items-thm — Guard (symbolp items-thm).; items-type — Guard (typep items-type).; new-context — Guard (atc-contextp new-context).; new-inscope — Guard (atc-symbol-varinfo-alist-listp new-inscope).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

We need a limit that suffices for both item and items. We take their sum (instead of the maximum), so the term remains linear. We also need to add 1, because it takes 1 to go from the execution of (cons item items) to the execution of item and items.

The context in gin is the one before all the items, while the context new-context is the one after all the items. The former should be always a prefix of the latter. In order to calculate the computation state after all the items, we take the ``difference'' between the two contexts and use it to contextualize the computation state variable, obtaining the computation state after all the items; note that, at that spot in the generated theorem, the computation state variable already accumulates the contextual premises in gin.

The new-inscope input is the variable table after all the items.

Currently this function is only called on a term that returns a single value, which is either the returned C value (if the C type is not void), or a side-effected variables (if the C type is void). Thus, if the type if not void, we can take the whole term as the first result of exec-block-item-list. In the future, this will need to be generalized to be (mv-nth 0 term) when the term returns multiple results and the type is not void.

Definitions and Theorems

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

(defun atc-gen-block-item-list-cons
       (term item item-limit
             item-events item-thm items items-limit
             items-events items-thm items-type
             new-context new-inscope gin state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (pseudo-termp term)
                        (block-itemp item)
                        (pseudo-termp item-limit)
                        (pseudo-event-form-listp item-events)
                        (symbolp item-thm)
                        (block-item-listp items)
                        (pseudo-termp items-limit)
                        (pseudo-event-form-listp items-events)
                        (symbolp items-thm)
                        (typep items-type)
                        (atc-contextp new-context)
                        (atc-symbol-varinfo-alist-listp new-inscope)
                        (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-list-cons))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((stmt-gin gin) gin)
    (all-items (cons item items))
    (all-items-limit
     (cons
        '+
        (cons ''1
              (cons (cons '+
                          (cons item-limit (cons items-limit 'nil)))
                    'nil))))
    ((when (not gin.proofs))
     (make-stmt-gout :items all-items
                     :type items-type
                     :term term
                     :context gin.context
                     :inscope gin.inscope
                     :limit all-items-limit
                     :events (append item-events items-events)
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (new-compst (atc-contextualize-compustate
                     gin.compst-var gin.context new-context))
    ((mv stmt-value type-formula &)
     (atc-gen-stmt-value-term-and-type-formula
          (untranslate$ term nil state)
          items-type
          gin.affect gin.inscope gin.prec-tags))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-block-item-list
                     (cons (cons 'quote (cons all-items 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons stmt-value (cons new-compst 'nil)))
                     'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var all-items-limit t wrld))
    (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-when-consp
            (cons
             'not-zp-of-limit-variable
             (cons
              item-thm
              (cons
               'mv-nth-of-cons
               (cons
                '(:e zp)
                (cons
                 '(:e value-optionp)
                 (cons
                  '(:e value-option-fix)
                  (cons
                   'not-zp-of-limit-minus-const
                   (cons
                    'return-type-of-stmt-value-return
                    (cons
                     'return-type-of-stmt-value-none
                     (cons
                      'stmt-value-return->value?-of-stmt-value-return
                      (cons
                       'stmt-value-return-of-value-option-fix-value?
                       (cons
                        '(:e valuep)
                        (cons
                         items-thm
                         '(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)))))))))))))))
           'nil))
         'nil)))
      'nil))
    (thm-name (pack gin.fn '-correct- gin.thm-index))
    (thm-index (1+ gin.thm-index))
    ((mv thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          thm-name nil gin.names-to-avoid wrld))
    ((mv event &)
     (evmac-generate-defthm thm-name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (make-stmt-gout
        :items all-items
        :type items-type
        :term term
        :context new-context
        :inscope new-inscope
        :limit all-items-limit
        :events (append item-events items-events (list event))
        :thm-name thm-name
        :thm-index thm-index
        :names-to-avoid names-to-avoid))))

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

(defthm stmt-goutp-of-atc-gen-block-item-list-cons
  (b* ((gout (atc-gen-block-item-list-cons
                  term item item-limit
                  item-events item-thm items items-limit
                  items-events items-thm items-type
                  new-context new-inscope gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)