		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-fn-call

Generate a shallowly embedded ACL2 named function call.

Signature
(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 block expr new-jvar-tmp-index)
Arguments: fn — Guard (symbolp fn).; args — Guard (pseudo-term-listp args).; arg-blocks — Guard (jblock-listp arg-blocks).; arg-exprs — Guard (jexpr-listp arg-exprs).; src-types — Guard (atj-type-listp src-types).; dst-types — Guard (atj-type-listp dst-types).; jvar-tmp-base — Guard (stringp jvar-tmp-base).; jvar-tmp-index — Guard (posp jvar-tmp-index).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; curr-pkg — Guard (stringp curr-pkg).; guards$ — Guard (booleanp guards$).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).; new-jvar-tmp-index — Type (posp new-jvar-tmp-index), given (posp jvar-tmp-index).

Calls of if are handled via a separate function, non-strictly. We only pass one of src-types or dst-types to this separate function, because those two types are always equal for if (see atj-type-annotate-term).

Calls of and are also handled via a separate function. Recall that and calls are if calls of the form (if a b nil). As in any if call, src-types and dst-types are equal, and in addition they are equal to the destination types of b (see atj-type-annotate-term); so, it suffices to pass the destination types of b to the separate code generation function. But we also need to pass the type of the first operand, in order to check whether it is boolean or not (see atj-gen-shallow-and-call).

Calls of or are also handled via a separate function. Recall that or calls are if calls of the form (if a a b). As in any if call, src-types and dst-types are equal, and in addition they are equal to the destination types of both a and b (see atj-type-annotate-term); so, it suffices to pass the destination types of b to the separate code generation function. Unlike the case of and, there is no need to pass the destination type of the first operand, because it is the same as the second operand's.

If :guards is t, calls of not, and calls of ACL2 functions that model Java primitive and primitive array operations, are handled via separate functions.

In all other cases, in which the call is always strict, we generate a call of the method that corresponds to the function, and finally we wrap that into a Java conversion if needed. (We treat the Java abstract syntax somewhat improperly here, by using a generic method call with a possibly qualified method name, which should be therefore a static method call; this still produces correct Java code, but it should be handled more properly in a future version of this implementation.) Note that, because of the type annotations of the ACL2 terms, the actual argument expressions will have types appropriate to the method's formal argument types.

Definitions and Theorems

Function: atj-gen-shallow-fn-call

(defun 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$)
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-term-listp args)
                             (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)
                             (booleanp guards$))))
 (declare (xargs :guard (and (= (len args) (len arg-blocks))
                             (= (len args) (len arg-exprs))
                             (consp src-types)
                             (consp dst-types)
                             (not (equal curr-pkg "")))))
 (let ((__function__ 'atj-gen-shallow-fn-call))
  (declare (ignorable __function__))
  (b*
   (((when (and (eq fn 'if) (int= (len args) 3)))
     (b* (((mv test-block then-block else-block)
           (atj-jblock-list-to-3-jblocks arg-blocks))
          ((mv test-expr then-expr else-expr)
           (atj-jexpr-list-to-3-jexprs arg-exprs)))
       (atj-gen-shallow-if-call test-block
                                then-block else-block test-expr
                                then-expr else-expr (first args)
                                dst-types
                                jvar-tmp-base jvar-tmp-index)))
    ((when (and (eq fn 'and) (int= (len args) 2)))
     (b* (((mv left-block right-block)
           (atj-jblock-list-to-2-jblocks arg-blocks))
          ((mv left-expr right-expr)
           (atj-jexpr-list-to-2-jexprs arg-exprs))
          ((mv & & left-types)
           (atj-type-unwrap-term (first args)))
          ((mv & & right-types)
           (atj-type-unwrap-term (second args))))
       (atj-gen-shallow-and-call left-block right-block left-expr
                                 right-expr left-types right-types
                                 jvar-tmp-base jvar-tmp-index)))
    ((when (and (eq fn 'or) (int= (len args) 2)))
     (b* (((mv left-block right-block)
           (atj-jblock-list-to-2-jblocks arg-blocks))
          ((mv left-expr right-expr)
           (atj-jexpr-list-to-2-jexprs arg-exprs))
          ((mv & & types)
           (atj-type-unwrap-term (second args))))
      (atj-gen-shallow-or-call left-block
                               right-block left-expr right-expr
                               types jvar-tmp-base jvar-tmp-index)))
    ((when (and guards$ (eq fn 'not)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-not-call (car arg-blocks)
                                     (car arg-exprs)
                                     (car args)
                                     src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprim-constr-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprim-constr-call fn (car arg-blocks)
                                              (car arg-exprs)
                                              (car args)
                                              src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprim-deconstr-fn-p fn)
                (int= (len args) 1)))
     (b*
      (((mv block expr)
        (atj-gen-shallow-jprim-deconstr-call fn (car arg-blocks)
                                             (car arg-exprs)
                                             src-types dst-types)))
      (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprim-unop-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprim-unop-call fn (car arg-blocks)
                                            (car arg-exprs)
                                            src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprim-binop-fn-p fn)
                (int= (len args) 2)))
     (b* (((mv left-block right-block)
           (atj-jblock-list-to-2-jblocks arg-blocks))
          ((mv left-expr right-expr)
           (atj-jexpr-list-to-2-jexprs arg-exprs))
          ((mv block expr)
           (atj-gen-shallow-jprim-binop-call
                fn left-block right-block left-expr
                right-expr src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprim-conv-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprim-conv-call fn (car arg-blocks)
                                            (car arg-exprs)
                                            src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprimarr-read-fn-p fn)
                (int= (len args) 2)))
     (b* (((mv array-block index-block)
           (atj-jblock-list-to-2-jblocks arg-blocks))
          ((mv array-expr index-expr)
           (atj-jexpr-list-to-2-jexprs arg-exprs))
          ((mv block expr)
           (atj-gen-shallow-jprimarr-read-call
                array-block index-block array-expr
                index-expr src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprimarr-length-fn-p fn)
                (int= (len args) 1)))
     (b*
      (((mv block expr)
        (atj-gen-shallow-jprimarr-length-call (car arg-blocks)
                                              (car arg-exprs)
                                              src-types dst-types)))
      (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprimarr-write-fn-p fn)
                (int= (len args) 3)))
     (b* (((mv array-block index-block component-block)
           (atj-jblock-list-to-3-jblocks arg-blocks))
          ((mv array-expr index-expr component-expr)
           (atj-jexpr-list-to-3-jexprs arg-exprs))
          ((mv block expr)
           (atj-gen-shallow-jprimarr-write-call
                fn array-block index-block
                component-block array-expr index-expr
                component-expr src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$ (atj-jprimarr-new-len-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprimarr-new-len-call
                fn (car arg-blocks)
                (car arg-exprs)
                src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$
                (atj-jprimarr-new-init-fn-p fn)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprimarr-new-init-call
                fn arg-blocks
                arg-exprs src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$
                (atj-jprimarr-conv-fromlist-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprimarr-conv-fromlist-call
                fn (car arg-blocks)
                (car arg-exprs)
                src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (and guards$
                (atj-jprimarr-conv-tolist-fn-p fn)
                (int= (len args) 1)))
     (b* (((mv block expr)
           (atj-gen-shallow-jprimarr-conv-tolist-call
                fn (car arg-blocks)
                (car arg-exprs)
                src-types dst-types)))
       (mv block expr jvar-tmp-index)))
    ((when (eq fn 'mv))
     (b* (((mv block expr)
           (atj-gen-shallow-mv-call
                arg-blocks
                arg-exprs src-types dst-types guards$)))
       (mv block expr jvar-tmp-index)))
    (expr
     (jexpr-method (atj-gen-shallow-fnname fn pkg-class-names
                                           fn-method-names curr-pkg)
                   arg-exprs))
    ((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
          expr src-types dst-types
          jvar-tmp-base jvar-tmp-index guards$)))
   (mv (append (flatten (jblock-list-fix arg-blocks))
               adapt-block)
       expr jvar-tmp-index))))

Theorem: jblockp-of-atj-gen-shallow-fn-call.block

(defthm jblockp-of-atj-gen-shallow-fn-call.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-tmp-index)
        (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$)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-gen-shallow-fn-call.expr

(defthm jexprp-of-atj-gen-shallow-fn-call.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-tmp-index)
        (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$)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-shallow-fn-call.new-jvar-tmp-index

(defthm posp-of-atj-gen-shallow-fn-call.new-jvar-tmp-index
 (implies
  (posp jvar-tmp-index)
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-tmp-index)
        (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$)))
    (posp new-jvar-tmp-index)))
 :rule-classes :rewrite)