(atj-gen-shallow-test-code-comps ares-vars jres-vars types comp-var) → block
Function:
(defun atj-gen-shallow-test-code-comps (ares-vars jres-vars types comp-var) (declare (xargs :guard (and (string-listp ares-vars) (string-listp jres-vars) (atj-type-listp types) (stringp comp-var)))) (declare (xargs :guard (and (= (len jres-vars) (len ares-vars)) (= (len types) (len ares-vars))))) (let ((__function__ 'atj-gen-shallow-test-code-comps)) (declare (ignorable __function__)) (cond ((endp ares-vars) nil) (t (b* ((ares-var (car ares-vars)) (jres-var (car jres-vars)) (type (car types)) (comp-expr (atj-type-case type :jprim (jexpr-binary (jbinop-eq) (jexpr-name ares-var) (jexpr-name jres-var)) :jprimarr (jexpr-smethod (jtype-class "Arrays") "equals" (list (jexpr-name ares-var) (jexpr-name jres-var))) :acl2 (b* ((jtype (atj-type-to-jitype type))) (if (jtype-case jtype :prim) (jexpr-binary (jbinop-eq) (jexpr-name ares-var) (jexpr-name jres-var)) (jexpr-method (str::cat ares-var ".equals") (list (jexpr-name jres-var))))))) (comp-block (jblock-expr (jexpr-binary (jbinop-asg-and) (jexpr-name comp-var) comp-expr))) (rest-block (atj-gen-shallow-test-code-comps (cdr ares-vars) (cdr jres-vars) (cdr types) comp-var))) (append comp-block rest-block))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-comps (b* ((block (atj-gen-shallow-test-code-comps ares-vars jres-vars types comp-var))) (jblockp block)) :rule-classes :rewrite)