(atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$) → (mv block vars)
Function:
(defun atj-gen-shallow-test-code-asgs (arg-exprs arg-types in-types var-base index guards$) (declare (xargs :guard (and (jexpr-listp arg-exprs) (atj-type-listp arg-types) (atj-type-listp in-types) (stringp var-base) (natp index) (booleanp guards$)))) (declare (xargs :guard (and (= (len arg-exprs) (len arg-types)) (= (len arg-types) (len in-types))))) (let ((__function__ 'atj-gen-shallow-test-code-asgs)) (declare (ignorable __function__)) (cond ((endp arg-exprs) (mv nil nil)) (t (b* ((first-var (str::cat var-base (nat-to-dec-string index))) (first-arg-expr (car arg-exprs)) (first-arg-type (car arg-types)) (first-in-type (car in-types)) (first-expr (atj-adapt-expr-to-type first-arg-expr first-arg-type first-in-type guards$)) (first-jtype (atj-type-to-jitype first-in-type)) (first-block (jblock-locvar first-jtype first-var first-expr)) ((mv rest-block rest-vars) (atj-gen-shallow-test-code-asgs (cdr arg-exprs) (cdr arg-types) (cdr in-types) var-base (1+ index) guards$))) (mv (append first-block rest-block) (cons first-var rest-vars)))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-asgs.block (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-atj-gen-shallow-test-code-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (string-listp vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-gen-shallow-test-code-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (equal (len vars) (len arg-exprs))))