		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-mbt-block-items

Generate a list of block items from an ACL2 conditional with an mbt test.

Signature
(atc-gen-mbt-block-items test-term then-term else-term then-items then-type then-limit then-events then-thm new-context new-inscope gin state) → (mv erp gout)
Arguments: test-term — Guard (pseudo-termp test-term).; then-term — Guard (pseudo-termp then-term).; else-term — Guard (pseudo-termp else-term).; then-items — Guard (block-item-listp then-items).; then-type — Guard (typep then-type).; then-limit — Guard (pseudo-termp then-limit).; then-events — Guard (pseudo-event-form-listp then-events).; then-thm — Guard (symbolp then-thm).; 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).

A statement term may be an ACL2 if with an mbt test. This represents the same C code as the `then' branch. Thus, atc-gen-stmt, when encountering an if of this form, processes the `then' branch, obtaining a list of block items and other related pieces of information, which are all passed to this function, along with the three argument terms of the if.

Here we generate two theorems.

The first one is a lemma that says that the ACL2 conditional is equal to its `then' branch under the guard and under all the contextual assumptions that involve ACL2 terms (i.e. not involving computation states). We use if* for the ACL2 conditional, consistently with other ACL2 conditionals that we translate to C, to avoid unwanted case splits. This lemma is proved using the guard theorem, and enabling the guard function, if*, test*, declar, and assign, just like in the okp theorems generated for expressions (e.g. see atc-gen-expr-unary).

The second one is the correctness theorem for the ACL2 conditional. It is just like the one for the `then' branch, except that it has the conditional (with if*) instead of the `then' term. It is proved using the correctness theorem for the `then' branch, and enabling the lemma described just above.

Since atc-gen-fn-def* replaces every if with if* in the whole body of the function, we need to perform this replacement in both the test and `else' branch, because these are not recursively processed to generate code.

The new-context parameter is the context just after the `then' branch, which is also the context after the whole if.

The generation of modular proofs in this code currently assumes that then-term returns a single value, which is either a returned C value or a side-effected C variable (the distinction is based on then-type). This is reflected in the generated modular theorems. This will need to be generalized to the case in which the term returns multiple values.

Definitions and Theorems

Function: atc-gen-mbt-block-items

(defun atc-gen-mbt-block-items
       (test-term then-term else-term then-items then-type
                  then-limit then-events then-thm
                  new-context new-inscope gin state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (pseudo-termp test-term)
                        (pseudo-termp then-term)
                        (pseudo-termp else-term)
                        (block-item-listp then-items)
                        (typep then-type)
                        (pseudo-termp then-limit)
                        (pseudo-event-form-listp then-events)
                        (symbolp then-thm)
                        (atc-contextp new-context)
                        (atc-symbol-varinfo-alist-listp new-inscope)
                        (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-mbt-block-items))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-stmt-gout))
    ((stmt-gin gin) gin)
    (wrld (w state))
    (test-term (cons 'mbt
                     (cons (fty-if-to-if* test-term) 'nil)))
    (else-term (fty-if-to-if* else-term))
    (term (cons 'if*
                (cons test-term
                      (cons then-term (cons else-term 'nil)))))
    ((when (not gin.proofs))
     (retok (make-stmt-gout :items then-items
                            :type then-type
                            :term term
                            :context gin.context
                            :inscope gin.inscope
                            :limit then-limit
                            :events then-events
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid)))
    (lemma-name (pack gin.fn '-if-mbt- 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))
    (lemma-formula (cons 'equal
                         (cons term (cons then-term 'nil))))
    (lemma-formula (untranslate$ lemma-formula nil state))
    (lemma-formula
         (atc-contextualize lemma-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (lemma-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
          (cons 'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
          (cons ':use
                (cons (cons ':guard-theorem
                            (cons gin.fn '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))
    (uterm (untranslate$ term nil state))
    (formula1
     (cons
         'equal
         (cons (cons 'exec-block-item-list
                     (cons (cons 'quote (cons then-items 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons (if (type-case then-type :void)
                                     nil
                                   uterm)
                                 (cons gin.compst-var 'nil)))
                     'nil))))
    (formula1 (atc-contextualize formula1 gin.context
                                 gin.fn gin.fn-guard gin.compst-var
                                 gin.limit-var then-limit t wrld))
    (formula
     (if (type-case then-type :void)
         formula1
      (b*
       ((type-pred (atc-type-to-recognizer then-type gin.prec-tags))
        (formula2 (cons type-pred (cons term 'nil)))
        (formula2
             (atc-contextualize formula2 gin.context gin.fn
                                gin.fn-guard nil nil nil nil wrld)))
       (cons 'and
             (cons formula1 (cons formula2 'nil))))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
         ':use
         (cons then-thm
               (cons ':in-theory
                     (cons (cons 'quote
                                 (cons (cons lemma-name 'nil) 'nil))
                           'nil)))))
      'nil))
    ((mv thm-event &)
     (evmac-generate-defthm thm-name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (retok
       (make-stmt-gout :items then-items
                       :type then-type
                       :term term
                       :context new-context
                       :inscope new-inscope
                       :limit then-limit
                       :events (append then-events
                                       (list lemma-event thm-event))
                       :thm-name thm-name
                       :thm-index thm-index
                       :names-to-avoid names-to-avoid)))))

Theorem: stmt-goutp-of-atc-gen-mbt-block-items.gout

(defthm stmt-goutp-of-atc-gen-mbt-block-items.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-mbt-block-items
             test-term
             then-term else-term then-items then-type
             then-limit then-events then-thm
             new-context new-inscope gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)