Generate Java code to build a deeply embedded ACL2 quoted constant.
(atj-gen-deep-qconst qconst jvar-value-base jvar-value-index) → (mv block expr new-jvar-value-index)
Function:
(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:
(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:
(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:
(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)