Functions to generate shallowly embedded ACL2 terms.
These code generation functions assume that the ACL2 terms
have been type-annotated via atj-type-annotate-term.
They also assume that all the variables of the ACL2 terms have been marked
via atj-mark-var-new and atj-mark-var-old,
and renamed via atj-rename-term.
If the
Our code generation strategy involves generating temporary Java local variables to store results of arguments of ACL2's non-strict if. The base name to use for these variables is an argument of these code generation functions; the index to make these variables unique is threaded through the code generation functions.
Function:
(defun atj-gen-shallow-term (term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld) (declare (xargs :guard (and (pseudo-termp term) (stringp jvar-tmp-base) (posp jvar-tmp-index) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (stringp curr-pkg) (cons-pos-alistp qpairs) (booleanp guards$) (plist-worldp wrld)))) (declare (xargs :guard (not (equal curr-pkg "")))) (let ((__function__ 'atj-gen-shallow-term)) (declare (ignorable __function__)) (b* (((mv mv-let-p block expr jvar-tmp-index) (atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld)) ((when mv-let-p) (mv block expr jvar-tmp-index)) ((mv uterm src-types dst-types) (atj-type-unwrap-term term)) ((unless (< (pseudo-term-count uterm) (pseudo-term-count term))) (mv nil (jexpr-name "dummy") jvar-tmp-index)) (term uterm) ((when (pseudo-term-case term :null)) (raise "Internal error: null unwrapped term.") (mv nil (jexpr-name "dummy") jvar-tmp-index)) ((when (pseudo-term-case term :var)) (b* (((mv var &) (atj-unmark-var (pseudo-term-var->name term))) ((mv var &) (atj-type-unannotate-var var)) (expr (jexpr-name (symbol-name var))) (expr (atj-adapt-expr-to-type expr (atj-type-list-to-type src-types) (atj-type-list-to-type dst-types) guards$))) (mv nil expr jvar-tmp-index))) ((when (pseudo-term-case term :quote)) (b* ((value (pseudo-term-quote->val term)) (expr (atj-gen-shallow-value value qpairs pkg-class-names curr-pkg guards$)) (expr (atj-adapt-expr-to-type expr (atj-type-list-to-type src-types) (atj-type-list-to-type dst-types) guards$))) (mv nil expr jvar-tmp-index))) ((when (pseudo-term-case term :fncall)) (b* ((fn (pseudo-term-fncall->fn term)) (args (pseudo-term-fncall->args term)) ((mv arg-blocks arg-exprs jvar-tmp-index) (atj-gen-shallow-terms args jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (atj-gen-shallow-fn-call fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$))) ((mv arg-blocks arg-exprs jvar-tmp-index) (atj-gen-shallow-terms (pseudo-term-lambda->args term) jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (atj-gen-shallow-lambda (pseudo-term-lambda->formals term) (pseudo-term-lambda->body term) arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))))
Function:
(defun atj-gen-shallow-terms (terms jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (stringp jvar-tmp-base) (posp jvar-tmp-index) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (stringp curr-pkg) (cons-pos-alistp qpairs) (booleanp guards$) (plist-worldp wrld)))) (declare (xargs :guard (not (equal curr-pkg "")))) (let ((__function__ 'atj-gen-shallow-terms)) (declare (ignorable __function__)) (if (endp terms) (mv nil nil jvar-tmp-index) (b* (((mv first-block first-expr jvar-tmp-index) (atj-gen-shallow-term (car terms) jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld)) ((mv rest-blocks rest-exprs jvar-tmp-index) (atj-gen-shallow-terms (cdr terms) jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (mv (cons first-block rest-blocks) (cons first-expr rest-exprs) jvar-tmp-index)))))
Function:
(defun atj-gen-shallow-lambda (formals body arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld) (declare (xargs :guard (and (symbol-listp formals) (pseudo-termp body) (jblock-listp arg-blocks) (jexpr-listp arg-exprs) (atj-type-listp src-types) (atj-type-listp dst-types) (stringp jvar-tmp-base) (posp jvar-tmp-index) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (stringp curr-pkg) (cons-pos-alistp qpairs) (booleanp guards$) (plist-worldp wrld)))) (declare (xargs :guard (and (consp src-types) (consp dst-types) (int= (len arg-blocks) (len formals)) (int= (len arg-exprs) (len formals)) (not (equal curr-pkg ""))))) (let ((__function__ 'atj-gen-shallow-lambda)) (declare (ignorable __function__)) (b* ((let-block (atj-gen-shallow-let-bindings formals arg-blocks arg-exprs)) ((mv body-block body-expr jvar-tmp-index) (atj-gen-shallow-term body jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld)) ((unless (= (len src-types) (len dst-types))) (raise "Internal error: ~ the source types ~x0 and destination types ~x1 ~ differ in number." src-types dst-types) (mv nil (jexpr-name "irrelevant") jvar-tmp-index)) ((mv adapt-block expr jvar-tmp-index) (atj-adapt-expr-to-types body-expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$))) (mv (append let-block body-block adapt-block) expr jvar-tmp-index))))
Function:
(defun atj-gen-shallow-mv-let (term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld) (declare (xargs :guard (and (pseudo-termp term) (stringp jvar-tmp-base) (posp jvar-tmp-index) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (stringp curr-pkg) (cons-pos-alistp qpairs) (booleanp guards$) (plist-worldp wrld)))) (declare (xargs :guard (not (equal curr-pkg "")))) (let ((__function__ 'atj-gen-shallow-mv-let)) (declare (ignorable __function__)) (b* (((mv yes/no mv-var mv-term vars indices body-term) (atj-check-marked-annotated-mv-let-call term)) ((unless yes/no) (mv nil nil (jexpr-name "dummy") jvar-tmp-index)) ((unless (and (< (pseudo-term-count mv-term) (pseudo-term-count term)) (< (pseudo-term-count body-term) (pseudo-term-count term)))) (mv nil nil (jexpr-name "dummy") jvar-tmp-index)) ((mv mv-block mv-expr jvar-tmp-index) (atj-gen-shallow-term mv-term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld)) (mv-block (atj-gen-shallow-let-bindings (list mv-var) (list mv-block) (list mv-expr))) (mv-expr (b* (((mv mv-var &) (atj-unmark-var mv-var)) ((mv mv-var &) (atj-type-unannotate-var mv-var))) (jexpr-name (symbol-name mv-var)))) (exprs (atj-gen-shallow-mv-let-aux mv-expr indices)) (vars-block (atj-gen-shallow-let-bindings vars (repeat (len vars) nil) exprs)) ((mv body-block body-expr jvar-tmp-index) (atj-gen-shallow-term body-term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (mv t (append mv-block vars-block body-block) body-expr jvar-tmp-index))))
Theorem:
(defthm return-type-of-atj-gen-shallow-term.block (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-term term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-term.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-term term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-term.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-term term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-terms.blocks (b* (((mv ?blocks ?exprs ?new-jvar-tmp-index) (atj-gen-shallow-terms terms jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (and (jblock-listp blocks) (equal (len blocks) (len terms)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-terms.exprs (b* (((mv ?blocks ?exprs ?new-jvar-tmp-index) (atj-gen-shallow-terms terms jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (and (jexpr-listp exprs) (equal (len exprs) (len terms)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-terms.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv ?blocks ?exprs ?new-jvar-tmp-index) (atj-gen-shallow-terms terms jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-lambda.block (implies (jblock-listp arg-blocks) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-lambda formals body arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jblockp block))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-lambda.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-lambda formals body arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-lambda.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-lambda formals body arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-mv-let.successp (b* (((mv ?successp common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (booleanp successp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-mv-let.block (b* (((mv ?successp common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-mv-let.expr (b* (((mv ?successp common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-mv-let.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv ?successp common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg qpairs guards$ wrld))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)