		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-pure-list

Generate a list of C expressions from a list of ACL2 terms that must be pure expression terms returning C values.

Signature
(atc-gen-expr-pure-list terms gin state) → (mv erp gout)
Arguments: terms — Guard (pseudo-term-listp terms).; gin — Guard (exprs-ginp gin).
Returns: gout — Type (exprs-goutp gout).

This lifts atc-gen-expr-pure to lists. However, we do not return the C types of the expressions.

Definitions and Theorems

Function: atc-gen-expr-pure-list

(defun atc-gen-expr-pure-list (terms gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-term-listp terms)
                             (exprs-ginp gin))))
 (let ((__function__ 'atc-gen-expr-pure-list))
  (declare (ignorable __function__))
  (b*
    (((reterr) (irr-exprs-gout))
     ((exprs-gin gin) gin)
     ((when (endp terms))
      (retok (make-exprs-gout :exprs nil
                              :types nil
                              :terms nil
                              :events nil
                              :thm-names nil
                              :thm-index gin.thm-index
                              :names-to-avoid gin.names-to-avoid)))
     ((erp (expr-gout first))
      (atc-gen-expr-pure
           (car terms)
           (make-expr-gin :context gin.context
                          :inscope gin.inscope
                          :prec-tags gin.prec-tags
                          :fn gin.fn
                          :fn-guard gin.fn-guard
                          :compst-var gin.compst-var
                          :thm-index gin.thm-index
                          :names-to-avoid gin.names-to-avoid
                          :proofs gin.proofs)
           state))
     ((erp (exprs-gout rest))
      (atc-gen-expr-pure-list
           (cdr terms)
           (change-exprs-gin gin
                             :thm-index first.thm-index
                             :names-to-avoid first.names-to-avoid)
           state)))
   (retok
    (make-exprs-gout :exprs (cons first.expr rest.exprs)
                     :types (cons first.type rest.types)
                     :terms (cons first.term rest.terms)
                     :events (append first.events rest.events)
                     :thm-names (cons first.thm-name rest.thm-names)
                     :thm-index rest.thm-index
                     :names-to-avoid rest.names-to-avoid)))))

Theorem: exprs-goutp-of-atc-gen-expr-pure-list.gout

(defthm exprs-goutp-of-atc-gen-expr-pure-list.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-expr-pure-list terms gin state)))
    (exprs-goutp gout))
  :rule-classes :rewrite)