		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-term-fns

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 :guards input is nil, then all the type annotations consist of the type :avalue of all ACL2 values, i.e. it is as if there were no types.

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.

Definitions and Theorems

Function: atj-gen-shallow-term

(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: atj-gen-shallow-terms

(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: atj-gen-shallow-lambda

(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: atj-gen-shallow-mv-let

(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: return-type-of-atj-gen-shallow-term.block

(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: return-type-of-atj-gen-shallow-term.expr

(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: return-type-of-atj-gen-shallow-term.new-jvar-tmp-index

(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: return-type-of-atj-gen-shallow-terms.blocks

(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: return-type-of-atj-gen-shallow-terms.exprs

(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: return-type-of-atj-gen-shallow-terms.new-jvar-tmp-index

(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: return-type-of-atj-gen-shallow-lambda.block

(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: return-type-of-atj-gen-shallow-lambda.expr

(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: return-type-of-atj-gen-shallow-lambda.new-jvar-tmp-index

(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: return-type-of-atj-gen-shallow-mv-let.successp

(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: return-type-of-atj-gen-shallow-mv-let.block

(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: return-type-of-atj-gen-shallow-mv-let.expr

(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: return-type-of-atj-gen-shallow-mv-let.new-jvar-tmp-index

(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)

Subtopics

Atj-gen-shallow-term: Generate a shallowly embedded ACL2 term.
Atj-gen-shallow-mv-let: Generate a shallowly embedded ACL2 mv-let.
Atj-gen-shallow-lambda: Generate a shallowly embedded ACL2 lambda expression, applied to given Java expressions as arguments.
Atj-gen-shallow-terms: Lift atj-gen-shallow-term to lists.