		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-mv-asgs

Generate the assignments in the factory method of the mv class for the given types.

Signature
(atj-gen-shallow-mv-asgs types) → block
Arguments: types — Guard (atj-type-listp types).
Returns: block — Type (jblockp block).

As explained in atj-gen-shallow-mv-class-name, we generate Java classes that represent mv values. Each such class has a static factory method that re-uses a singleton instance of the class. The body of this method assigns the parameters to the corresponding fields of the singleton instance, which is stored in a private static field.

Definitions and Theorems

Function: atj-gen-shallow-mv-asgs-aux

(defun atj-gen-shallow-mv-asgs-aux (types index)
 (declare (xargs :guard (and (atj-type-listp types)
                             (natp index))))
 (let ((__function__ 'atj-gen-shallow-mv-asgs-aux))
   (declare (ignorable __function__))
   (b*
     (((when (endp types)) nil)
      (param-name (atj-gen-shallow-mv-field-name index))
      (field-var (jexpr-name (str::cat *atj-mv-singleton-field-name*
                                       "." param-name)))
      (asg (jstatem-expr
                (jexpr-binary (jbinop-asg)
                              field-var (jexpr-name param-name))))
      (asgs (atj-gen-shallow-mv-asgs-aux (cdr types)
                                         (1+ index))))
     (cons asg asgs))))

Theorem: jblockp-of-atj-gen-shallow-mv-asgs-aux

(defthm jblockp-of-atj-gen-shallow-mv-asgs-aux
  (b* ((block (atj-gen-shallow-mv-asgs-aux types index)))
    (jblockp block))
  :rule-classes :rewrite)

Function: atj-gen-shallow-mv-asgs

(defun atj-gen-shallow-mv-asgs (types)
  (declare (xargs :guard (atj-type-listp types)))
  (let ((__function__ 'atj-gen-shallow-mv-asgs))
    (declare (ignorable __function__))
    (atj-gen-shallow-mv-asgs-aux types 0)))

Theorem: jblockp-of-atj-gen-shallow-mv-asgs

(defthm jblockp-of-atj-gen-shallow-mv-asgs
  (b* ((block (atj-gen-shallow-mv-asgs types)))
    (jblockp block))
  :rule-classes :rewrite)