		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation

Atj-pre-translate

Pre-translate the formal parameters and body of an ACL2 function definition.

Signature
(atj-pre-translate fn formals body in-types out-types out-arrays mv-typess deep$ guards$ no-aij-types$ wrld) → (mv new-formals new-body new-mv-typess)
Arguments: fn — Guard (symbolp fn).; formals — Guard (symbol-listp formals).; body — Guard (pseudo-termp body).; in-types — Guard (atj-type-listp in-types).; out-types — Guard (atj-type-listp out-types).; out-arrays — Guard (symbol-listp out-arrays).; mv-typess — Guard (atj-type-list-listp mv-typess).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; wrld — Guard (plist-worldp wrld).
Returns: new-formals — Type (symbol-listp new-formals), given the guard.; new-body — Type (pseudo-termp new-body), given the guard.; new-mv-typess — Type (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)).

This is done before the translation from ACL2 to Java proper. The pre-translation steps are described in atj-pre-translation.

We collect all the mv types in the body for which we will need to generate mv classes. This is only relevant to the shallow embedding.

Definitions and Theorems

Function: atj-pre-translate

(defun atj-pre-translate (fn formals body
                             in-types out-types out-arrays mv-typess
                             deep$ guards$ no-aij-types$ wrld)
  (declare (xargs :guard (and (symbolp fn)
                              (symbol-listp formals)
                              (pseudo-termp body)
                              (atj-type-listp in-types)
                              (atj-type-listp out-types)
                              (symbol-listp out-arrays)
                              (atj-type-list-listp mv-typess)
                              (booleanp deep$)
                              (booleanp guards$)
                              (booleanp no-aij-types$)
                              (plist-worldp wrld))))
  (declare (xargs :guard (and (= (len formals) (len in-types))
                              (consp out-types)
                              (cons-listp mv-typess))))
  (let ((__function__ 'atj-pre-translate))
    (declare (ignorable __function__))
    (b* ((body (atj-remove-return-last body guards$))
         (body (remove-dead-if-branches body))
         (body (remove-unused-vars body))
         ((when deep$) (mv formals body nil))
         (body (remove-trivial-vars body))
         (body (atj-restore-mv-calls-in-body body out-types wrld))
         ((run-when no-aij-types$)
          (atj-check-no-aij-types+body in-types out-types body fn))
         ((mv formals body mv-typess)
          (atj-type-annotate-formals+body
               formals body in-types
               out-types mv-typess guards$ wrld))
         ((run-when guards$)
          (atj-analyze-arrays-in-formals+body
               formals body out-arrays wrld))
         ((mv formals body)
          (atj-mark-formals+body formals body))
         ((mv formals body)
          (atj-rename-formals+body
               formals body (symbol-package-name fn)))
         (body (atj-restore-and-calls-in-term body))
         (body (atj-restore-or-calls-in-term body)))
      (mv formals body mv-typess))))

Theorem: symbol-listp-of-atj-pre-translate.new-formals

(defthm symbol-listp-of-atj-pre-translate.new-formals
 (implies
    (and (symbolp fn)
         (symbol-listp formals)
         (pseudo-termp body)
         (atj-type-listp in-types)
         (atj-type-listp out-types)
         (symbol-listp out-arrays)
         (atj-type-list-listp mv-typess)
         (booleanp deep$)
         (booleanp guards$)
         (booleanp no-aij-types$)
         (plist-worldp wrld)
         (= (len formals) (len in-types))
         (consp out-types)
         (cons-listp mv-typess))
    (b* (((mv ?new-formals ?new-body ?new-mv-typess)
          (atj-pre-translate fn formals body
                             in-types out-types out-arrays mv-typess
                             deep$ guards$ no-aij-types$ wrld)))
      (symbol-listp new-formals)))
 :rule-classes :rewrite)

Theorem: pseudo-termp-of-atj-pre-translate.new-body

(defthm pseudo-termp-of-atj-pre-translate.new-body
 (implies
    (and (symbolp fn)
         (symbol-listp formals)
         (pseudo-termp body)
         (atj-type-listp in-types)
         (atj-type-listp out-types)
         (symbol-listp out-arrays)
         (atj-type-list-listp mv-typess)
         (booleanp deep$)
         (booleanp guards$)
         (booleanp no-aij-types$)
         (plist-worldp wrld)
         (= (len formals) (len in-types))
         (consp out-types)
         (cons-listp mv-typess))
    (b* (((mv ?new-formals ?new-body ?new-mv-typess)
          (atj-pre-translate fn formals body
                             in-types out-types out-arrays mv-typess
                             deep$ guards$ no-aij-types$ wrld)))
      (pseudo-termp new-body)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-pre-translate.new-mv-typess

(defthm return-type-of-atj-pre-translate.new-mv-typess
  (b* (((mv ?new-formals ?new-body ?new-mv-typess)
        (atj-pre-translate fn formals body
                           in-types out-types out-arrays mv-typess
                           deep$ guards$ no-aij-types$ wrld)))
    (and (atj-type-list-listp new-mv-typess)
         (cons-listp new-mv-typess)))
  :rule-classes :rewrite)

Theorem: len-of-atj-pre-translate.new-formals

(defthm len-of-atj-pre-translate.new-formals
  (b* (((mv ?new-formals ?new-body ?new-mv-typess)
        (atj-pre-translate fn formals body
                           in-types out-types out-arrays mv-typess
                           deep$ guards$ no-aij-types$ wrld)))
    (equal (len new-formals)
           (len formals))))