		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-list-append

Generate a list of block items by appending two lists of block items.

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

Besides concatenating the two lists, which is easy, we also generate a theorem about exec-block-item-list applied to the concatenation, given theorems about exec-block-item-list applied to each of the two lists.

The generated theorem applies exec-block-item-list to a quoted list of block items that is the concatenation. Thus, we cannot just use a rule about exec-block-item-list applied to append. Instead, we need a rule that backchains to two applications of exec-block-item-list to sublists of the quoted list, obtained via take and nthcdr. We generate this rule as a lemma before the theorem.

We need a limit that suffices for all items. We take the sum of the limits of the two lists of items (instead of the maximum), so the term remains linear. That suffices to execute the items from the first list, but we also need to add 1 to the limit because it takes 1 step to go from the end of the first list to starting the second list.

Definitions and Theorems

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

(defun atc-gen-block-item-list-append
       (term items1 items2
             items1-limit items2-limit items1-events
             items2-events items1-thm items2-thm
             type new-context new-inscope gin state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (pseudo-termp term)
                        (block-item-listp items1)
                        (block-item-listp items2)
                        (pseudo-termp items1-limit)
                        (pseudo-termp items2-limit)
                        (pseudo-event-form-listp items1-events)
                        (pseudo-event-form-listp items2-events)
                        (symbolp items1-thm)
                        (symbolp items2-thm)
                        (typep type)
                        (atc-contextp new-context)
                        (atc-symbol-varinfo-alist-listp new-inscope)
                        (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-list-append))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((stmt-gin gin) gin)
    (items (append items1 items2))
    (items-limit
     (cons
      '+
      (cons
           ''1
           (cons (cons '+
                       (cons items1-limit (cons items2-limit 'nil)))
                 'nil))))
    ((when (not gin.proofs))
     (make-stmt-gout :items items
                     :type type
                     :term term
                     :context gin.context
                     :inscope gin.inscope
                     :limit items-limit
                     :events (append items1-events items2-events)
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (lemma-name (pack gin.fn
                      '-exec-block-item-list-concatenation-
                      gin.thm-index))
    ((mv lemma-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          lemma-name nil gin.names-to-avoid wrld))
    (thm-index (1+ gin.thm-index))
    (n (len items1))
    (m (+ n (len items2)))
    (lemma-formula
     (cons
      'implies
      (cons
       (cons
        'and
        (cons
         (cons
             'syntaxp
             (cons (cons 'and
                         (cons '(quotep items)
                               (cons (cons 'equal
                                           (cons '(len (cadr items))
                                                 (cons m 'nil)))
                                     'nil)))
                   'nil))
         (cons
          (cons 'equal
                (cons '(len items) (cons m 'nil)))
          (cons
           '(not (zp limit))
           (cons
            (cons
              'equal
              (cons 'sval+compst1
                    (cons (cons 'exec-block-item-list
                                (cons (cons 'take (cons n '(items)))
                                      '(compst fenv limit)))
                          'nil)))
            '((equal sval (mv-nth 0 sval+compst1))
              (stmt-valuep sval)
              (equal compst1 (mv-nth 1 sval+compst1))))))))
       (cons
        (cons
         'equal
         (cons
          '(exec-block-item-list items compst fenv limit)
          (cons
           (cons
            'if
            (cons
             '(equal (stmt-value-kind sval) :return)
             (cons
              '(mv sval compst1)
              (cons
               (cons
                'exec-block-item-list
                (cons
                 (cons 'nthcdr (cons n '(items)))
                 (cons
                   'compst1
                   (cons 'fenv
                         (cons (cons '- (cons 'limit (cons n 'nil)))
                               'nil)))))
               'nil))))
           'nil)))
        'nil))))
    (lemma-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''(stmt-value-return-of-fields
                stmt-value-fix-when-stmt-valuep
                valuep-when-value-optionp
                value-optionp-of-stmt-value-return->value?
                (:e valuep)
                append-of-take-and-nthcdr (:e nfix)
                value-optionp
                not-errorp-when-stmt-valuep (:e errorp)
                len-of-take commutativity-of-+)
         (cons
          ':use
          (cons
           (cons
            ':instance
            (cons
             'exec-block-item-list-of-append
             (cons
                  (cons 'items1
                        (cons (cons 'take (cons n '(items)))
                              'nil))
                  (cons (cons 'items2
                              (cons (cons 'nthcdr (cons n '(items)))
                                    'nil))
                        'nil))))
           'nil)))))
      'nil))
    ((mv lemma-event &)
     (evmac-generate-defthm lemma-name
                            :formula lemma-formula
                            :hints lemma-hints
                            :enable nil))
    (thm-name (pack gin.fn '-correct- thm-index))
    ((mv thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          thm-name nil names-to-avoid wrld))
    (thm-index (1+ thm-index))
    (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)
          type
          gin.affect gin.inscope gin.prec-tags))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-block-item-list
                     (cons (cons 'quote (cons 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 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
            lemma-name
            (cons
             '(:e len)
             (cons
              '(:e take)
              (cons
               '(:e nthcdr)
               (cons
                'not-zp-of-limit-variable
                (cons
                 items1-thm
                 (cons
                  'mv-nth-of-cons
                  (cons
                   '(:e zp)
                   (cons
                    '(:e value-optionp)
                    (cons
                     items2-thm
                     '((:e valuep)
                       (:e value-option-fix)
                       return-type-of-stmt-value-return
                       return-type-of-stmt-value-none
                       stmt-value-return->value?-of-stmt-value-return
                       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))
    ((mv event &)
     (evmac-generate-defthm thm-name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (make-stmt-gout
        :items items
        :type type
        :term term
        :context new-context
        :inscope new-inscope
        :limit items-limit
        :events (append items1-events
                        items2-events (list lemma-event event))
        :thm-name thm-name
        :thm-index thm-index
        :names-to-avoid names-to-avoid))))

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

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