Generate a list of C expressions from a list of ACL2 terms that must be pure expression terms returning C values.
(atc-gen-expr-pure-list terms gin state) → (mv erp gout)
This lifts atc-gen-expr-pure to lists. However, we do not return the C types of the expressions.
Function:
(defun atc-gen-expr-pure-list (terms gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-term-listp terms) (pexprs-ginp gin)))) (let ((__function__ 'atc-gen-expr-pure-list)) (declare (ignorable __function__)) (b* (((reterr) (irr-pexprs-gout)) ((pexprs-gin gin) gin) ((when (endp terms)) (retok (make-pexprs-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 (pexprs-gout rest)) (atc-gen-expr-pure-list (cdr terms) (change-pexprs-gin gin :thm-index first.thm-index :names-to-avoid first.names-to-avoid) state))) (retok (make-pexprs-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:
(defthm pexprs-goutp-of-atc-gen-expr-pure-list.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-pure-list terms gin state))) (pexprs-goutp gout)) :rule-classes :rewrite)