Functions to generate Java code to build deeply embedded ACL2 terms.
Function:
(defun atj-gen-deep-fnapp (fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$) (declare (xargs :guard (and (pseudo-termfnp fn) (pseudo-term-listp args) (stringp jvar-value-base) (posp jvar-value-index) (stringp jvar-term-base) (posp jvar-term-index) (stringp jvar-lambda-base) (posp jvar-lambda-index) (booleanp guards$)))) (let ((__function__ 'atj-gen-deep-fnapp)) (declare (ignorable __function__)) (b* (((mv fn args) (if (and (eq fn 'if) (= (len args) 3) (equal (first args) (second args))) (mv 'or (list (first args) (third args))) (mv fn args))) ((mv fn-block fn-expr jvar-value-index jvar-term-index jvar-lambda-index) (if (symbolp fn) (mv nil (jexpr-smethod *aij-type-named-fn* "make" (list (atj-gen-symbol fn t nil))) jvar-value-index jvar-term-index jvar-lambda-index) (atj-gen-deep-lambda (lambda-formals fn) (lambda-body fn) jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) ((mv args-block arg-exprs jvar-value-index jvar-term-index jvar-lambda-index) (atj-gen-deep-terms args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$)) (args-expr (jexpr-newarray-init *aij-type-term* arg-exprs)) (fnapp-expr (jexpr-smethod *aij-type-fn-app* "make" (list fn-expr args-expr))) ((mv fnapp-locvar-block fnapp-jvar jvar-term-index) (atj-gen-jlocvar-indexed *aij-type-term* jvar-term-base jvar-term-index fnapp-expr))) (mv (append fn-block args-block fnapp-locvar-block) (jexpr-name fnapp-jvar) jvar-value-index jvar-term-index jvar-lambda-index))))
Function:
(defun atj-gen-deep-lambda (formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$) (declare (xargs :guard (and (symbol-listp formals) (pseudo-termp body) (stringp jvar-value-base) (posp jvar-value-index) (stringp jvar-term-base) (posp jvar-term-index) (stringp jvar-lambda-base) (posp jvar-lambda-index) (booleanp guards$)))) (let ((__function__ 'atj-gen-deep-lambda)) (declare (ignorable __function__)) (b* ((formals-expr (atj-gen-deep-formals formals)) ((mv body-block body-expr jvar-value-index jvar-term-index jvar-lambda-index) (atj-gen-deep-term body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$)) (lambda-expr (jexpr-smethod *aij-type-lambda* "make" (list formals-expr body-expr))) ((mv lambda-locvar-block lambda-jvar jvar-lambda-index) (atj-gen-jlocvar-indexed *aij-type-lambda* jvar-lambda-base jvar-lambda-index lambda-expr))) (mv (append body-block lambda-locvar-block) (jexpr-name lambda-jvar) jvar-value-index jvar-term-index jvar-lambda-index))))
Function:
(defun atj-gen-deep-term (term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$) (declare (xargs :guard (and (pseudo-termp term) (stringp jvar-value-base) (posp jvar-value-index) (stringp jvar-term-base) (posp jvar-term-index) (stringp jvar-lambda-base) (posp jvar-lambda-index) (booleanp guards$)))) (let ((__function__ 'atj-gen-deep-term)) (declare (ignorable __function__)) (cond ((variablep term) (mv nil (atj-gen-deep-var term) jvar-value-index jvar-term-index jvar-lambda-index)) ((fquotep term) (b* (((mv block expr jvar-value-index) (atj-gen-deep-qconst (unquote term) jvar-value-base jvar-value-index))) (mv block expr jvar-value-index jvar-term-index jvar-lambda-index))) (t (atj-gen-deep-fnapp (ffn-symb term) (fargs term) jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$)))))
Function:
(defun atj-gen-deep-terms (terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$) (declare (xargs :guard (and (pseudo-term-listp terms) (stringp jvar-value-base) (posp jvar-value-index) (stringp jvar-term-base) (posp jvar-term-index) (stringp jvar-lambda-base) (posp jvar-lambda-index) (booleanp guards$)))) (let ((__function__ 'atj-gen-deep-terms)) (declare (ignorable __function__)) (if (endp terms) (mv nil nil jvar-value-index jvar-term-index jvar-lambda-index) (b* (((mv first-block expr jvar-value-index jvar-term-index jvar-lambda-index) (atj-gen-deep-term (car terms) jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$)) ((mv rest-block exprs jvar-value-index jvar-term-index jvar-lambda-index) (atj-gen-deep-terms (cdr terms) jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (mv (append first-block rest-block) (cons expr exprs) jvar-value-index jvar-term-index jvar-lambda-index)))))
Theorem:
(defthm return-type-of-atj-gen-deep-fnapp.block (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-fnapp fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-fnapp.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-fnapp fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-fnapp.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-fnapp fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-fnapp.new-jvar-term-index (implies (posp jvar-term-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-fnapp fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-term-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-fnapp.new-jvar-lambda-index (implies (posp jvar-lambda-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-fnapp fn args jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-lambda-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-lambda.block (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-lambda formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-lambda.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-lambda formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-lambda.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-lambda formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-lambda.new-jvar-term-index (implies (posp jvar-term-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-lambda formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-term-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-lambda.new-jvar-lambda-index (implies (posp jvar-lambda-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-lambda formals body jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-lambda-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-term.block (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-term term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-term.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-term term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-term.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-term term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-term.new-jvar-term-index (implies (posp jvar-term-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-term term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-term-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-term.new-jvar-lambda-index (implies (posp jvar-lambda-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-term term jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-lambda-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-terms.block (b* (((mv common-lisp::?block ?exprs ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-terms terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-terms.exprs (b* (((mv common-lisp::?block ?exprs ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-terms terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (jexpr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-terms.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?exprs ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-terms terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-terms.new-jvar-term-index (implies (posp jvar-term-index) (b* (((mv common-lisp::?block ?exprs ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-terms terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-term-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-deep-terms.new-jvar-lambda-index (implies (posp jvar-lambda-index) (b* (((mv common-lisp::?block ?exprs ?new-jvar-value-index ?new-jvar-term-index ?new-jvar-lambda-index) (atj-gen-deep-terms terms jvar-value-base jvar-value-index jvar-term-base jvar-term-index jvar-lambda-base jvar-lambda-index guards$))) (posp new-jvar-lambda-index))) :rule-classes :rewrite)