		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-qconst

Generate Java code to build a deeply embedded ACL2 quoted constant.

Signature
(atj-gen-deep-qconst qconst jvar-value-base jvar-value-index) → (mv block expr new-jvar-value-index)
Arguments: qconst — (Unquoted) value of the ACL2 quoted constant.; jvar-value-base — Guard (stringp jvar-value-base).; jvar-value-index — Guard (posp jvar-value-index).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).; new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).

Definitions and Theorems

Function: atj-gen-deep-qconst

(defun atj-gen-deep-qconst (qconst jvar-value-base jvar-value-index)
  (declare (xargs :guard (and (stringp jvar-value-base)
                              (posp jvar-value-index))))
  (let ((__function__ 'atj-gen-deep-qconst))
    (declare (ignorable __function__))
    (b* (((mv value-block value-expr jvar-value-index)
          (atj-gen-value qconst
                         jvar-value-base jvar-value-index t nil))
         (block value-block)
         (expr (jexpr-smethod *aij-type-qconst*
                              "make" (list value-expr))))
      (mv block expr jvar-value-index))))

Theorem: jblockp-of-atj-gen-deep-qconst.block

(defthm jblockp-of-atj-gen-deep-qconst.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-deep-qconst qconst
                             jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-gen-deep-qconst.expr

(defthm jexprp-of-atj-gen-deep-qconst.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-deep-qconst qconst
                             jvar-value-base jvar-value-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-deep-qconst.new-jvar-value-index

(defthm posp-of-atj-gen-deep-qconst.new-jvar-value-index
 (implies
      (posp jvar-value-index)
      (b* (((mv common-lisp::?block
                ?expr ?new-jvar-value-index)
            (atj-gen-deep-qconst qconst
                                 jvar-value-base jvar-value-index)))
        (posp new-jvar-value-index)))
 :rule-classes :rewrite)