		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-test-values

Lift atj-gen-test-value to lists.

Signature
(atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$) → (mv block exprs types new-jvar-value-index)
Arguments: tvalues — Guard (atj-test-value-listp tvalues).; jvar-value-base — Guard (stringp jvar-value-base).; jvar-value-index — Guard (posp jvar-value-index).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).
Returns: block — Type (jblockp block).; exprs — Type (jexpr-listp exprs).; types — Type (atj-type-listp types).; new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).

Definitions and Theorems

Function: atj-gen-test-values

(defun atj-gen-test-values (tvalues jvar-value-base
                                    jvar-value-index deep$ guards$)
  (declare (xargs :guard (and (atj-test-value-listp tvalues)
                              (stringp jvar-value-base)
                              (posp jvar-value-index)
                              (booleanp deep$)
                              (booleanp guards$))))
  (let ((__function__ 'atj-gen-test-values))
    (declare (ignorable __function__))
    (b* (((when (endp tvalues))
          (mv nil nil nil jvar-value-index))
         ((mv first-block
              first-expr first-type jvar-value-index)
          (atj-gen-test-value (car tvalues)
                              jvar-value-base
                              jvar-value-index deep$ guards$))
         ((mv rest-block
              rest-exprs rest-types jvar-value-index)
          (atj-gen-test-values (cdr tvalues)
                               jvar-value-base
                               jvar-value-index deep$ guards$)))
      (mv (append first-block rest-block)
          (cons first-expr rest-exprs)
          (cons first-type rest-types)
          jvar-value-index))))

Theorem: jblockp-of-atj-gen-test-values.block

(defthm jblockp-of-atj-gen-test-values.block
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexpr-listp-of-atj-gen-test-values.exprs

(defthm jexpr-listp-of-atj-gen-test-values.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (jexpr-listp exprs))
  :rule-classes :rewrite)

Theorem: atj-type-listp-of-atj-gen-test-values.types

(defthm atj-type-listp-of-atj-gen-test-values.types
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (atj-type-listp types))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-test-values.new-jvar-value-index

(defthm posp-of-atj-gen-test-values.new-jvar-value-index
  (implies
       (posp jvar-value-index)
       (b* (((mv common-lisp::?block
                 ?exprs ?types ?new-jvar-value-index)
             (atj-gen-test-values tvalues jvar-value-base
                                  jvar-value-index deep$ guards$)))
         (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Theorem: len-of-atj-gen-test-values.exprs

(defthm len-of-atj-gen-test-values.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (equal (len exprs) (len tvalues))))

Theorem: len-of-atj-gen-test-values.types

(defthm len-of-atj-gen-test-values.types
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (equal (len types) (len tvalues))))

Theorem: consp-of-atj-gen-test-values.exprs

(defthm consp-of-atj-gen-test-values.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (implies (consp tvalues) (consp exprs)))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-gen-test-values.types

(defthm consp-of-atj-gen-test-values.types
  (b* (((mv common-lisp::?block
            ?exprs ?types ?new-jvar-value-index)
        (atj-gen-test-values tvalues jvar-value-base
                             jvar-value-index deep$ guards$)))
    (implies (consp tvalues) (consp types)))
  :rule-classes :type-prescription)