		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-value

Generate Java code to build an ACL2 value.

Signature
(atj-gen-value value jvar-value-base jvar-value-index deep$ guards$) → (mv block expr new-jvar-value-index)
Arguments: jvar-value-base — Guard (stringp jvar-value-base).; jvar-value-index — Guard (posp jvar-value-index).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).; new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).

For a cons pair that is also a true list, the generated code builds all the elements and then calls Acl2Value.makeList() (a variable arity method) with the elements; the result is cast to Acl2ConsPair. For a cons pair that is not a true list, the generated code builds the car, sets a local variable to it, builds the cdr, sets another local variable to it, and then calls Acl2ConsValue.make() with the two local variables.

The deep$ and guards$ arguments are passed from atj-gen-value to atj-gen-symbol, atj-gen-char, and atj-gen-string only at the top level; this is so that we generate Java boolean, character, and string expressions for ACL2 boolean, character, and string values, in the shallow embedding with guards. But at the non-top levels, these flags are set to t and nil, because ACL2 booleans, characters, and strings are represented as Acl2Symbol, Acl2Character, and Acl2String instances inside other values (conses).

Function: atj-gen-value

(defun atj-gen-value (value jvar-value-base
                            jvar-value-index deep$ guards$)
 (declare (xargs :guard (and (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (booleanp deep$)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-value))
  (declare (ignorable __function__))
  (cond
    ((characterp value)
     (mv nil (atj-gen-char value deep$ guards$)
         jvar-value-index))
    ((stringp value)
     (mv nil (atj-gen-string value deep$ guards$)
         jvar-value-index))
    ((symbolp value)
     (mv nil (atj-gen-symbol value deep$ guards$)
         jvar-value-index))
    ((integerp value)
     (mv nil (atj-gen-integer value)
         jvar-value-index))
    ((rationalp value)
     (mv nil (atj-gen-rational value)
         jvar-value-index))
    ((acl2-numberp value)
     (mv nil (atj-gen-number value)
         jvar-value-index))
    ((true-listp value)
     (atj-gen-list value jvar-value-base jvar-value-index))
    ((consp value)
     (atj-gen-cons value jvar-value-base jvar-value-index))
    (t (prog2$ (raise "Internal error: the value ~x0 is a bad atom."
                      value)
               (mv nil (jexpr-name "this-is-irrelevant")
                   jvar-value-index))))))

Function: atj-gen-values

(defun atj-gen-values (values jvar-value-base jvar-value-index)
 (declare (xargs :guard (and (true-listp values)
                             (stringp jvar-value-base)
                             (posp jvar-value-index))))
 (let ((__function__ 'atj-gen-values))
  (declare (ignorable __function__))
  (cond
    ((endp values)
     (mv nil nil jvar-value-index))
    (t (b* (((mv first-block first-expr jvar-value-index)
             (atj-gen-value (car values)
                            jvar-value-base jvar-value-index t nil))
            ((mv rest-block rest-jexprs jvar-value-index)
             (atj-gen-values (cdr values)
                             jvar-value-base jvar-value-index)))
         (mv (append first-block rest-block)
             (cons first-expr rest-jexprs)
             jvar-value-index))))))

Function: atj-gen-list

(defun atj-gen-list (list jvar-value-base jvar-value-index)
  (declare (xargs :guard (and (true-listp list)
                              (stringp jvar-value-base)
                              (posp jvar-value-index))))
  (declare (xargs :guard (consp list)))
  (let ((__function__ 'atj-gen-list))
    (declare (ignorable __function__))
    (b* (((mv block exprs jvar-value-index)
          (atj-gen-values list jvar-value-base jvar-value-index))
         (expr (jexpr-smethod *aij-type-value* "makeList" exprs)))
      (mv block (jexpr-cast *aij-type-cons* expr)
          jvar-value-index))))

Function: atj-gen-cons

(defun atj-gen-cons (conspair jvar-value-base jvar-value-index)
  (declare (xargs :guard (and (consp conspair)
                              (stringp jvar-value-base)
                              (posp jvar-value-index))))
  (let ((__function__ 'atj-gen-cons))
    (declare (ignorable __function__))
    (b* (((unless (mbt (consp conspair)))
          (mv nil (jexpr-name "this-is-irrelevant")
              jvar-value-index))
         ((mv car-block car-expr jvar-value-index)
          (atj-gen-value (car conspair)
                         jvar-value-base jvar-value-index t nil))
         ((mv car-locvar-block
              car-jvar jvar-value-index)
          (atj-gen-jlocvar-indexed *aij-type-value* jvar-value-base
                                   jvar-value-index car-expr))
         ((mv cdr-block cdr-expr jvar-value-index)
          (atj-gen-value (cdr conspair)
                         jvar-value-base jvar-value-index t nil))
         ((mv cdr-locvar-block
              cdr-jvar jvar-value-index)
          (atj-gen-jlocvar-indexed *aij-type-value* jvar-value-base
                                   jvar-value-index cdr-expr))
         (block (append car-block car-locvar-block
                        cdr-block cdr-locvar-block))
         (expr (jexpr-smethod *aij-type-cons* "make"
                              (list (jexpr-name car-jvar)
                                    (jexpr-name cdr-jvar)))))
      (mv block expr jvar-value-index))))

Theorem: return-type-of-atj-gen-value.block

(defthm return-type-of-atj-gen-value.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-value value jvar-value-base
                       jvar-value-index deep$ guards$)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-value.expr

(defthm return-type-of-atj-gen-value.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-value value jvar-value-base
                       jvar-value-index deep$ guards$)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-value.new-jvar-value-index

(defthm return-type-of-atj-gen-value.new-jvar-value-index
  (implies (posp jvar-value-index)
           (b* (((mv common-lisp::?block
                     ?expr ?new-jvar-value-index)
                 (atj-gen-value value jvar-value-base
                                jvar-value-index deep$ guards$)))
             (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-values.block

(defthm return-type-of-atj-gen-values.block
  (b* (((mv common-lisp::?block
            ?exprs ?new-jvar-value-index)
        (atj-gen-values values
                        jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-values.exprs

(defthm return-type-of-atj-gen-values.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?new-jvar-value-index)
        (atj-gen-values values
                        jvar-value-base jvar-value-index)))
    (and (jexpr-listp exprs)
         (equal (len exprs) (len values))))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-values.new-jvar-value-index

(defthm return-type-of-atj-gen-values.new-jvar-value-index
  (implies (posp jvar-value-index)
           (b* (((mv common-lisp::?block
                     ?exprs ?new-jvar-value-index)
                 (atj-gen-values values
                                 jvar-value-base jvar-value-index)))
             (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.block

(defthm return-type-of-atj-gen-list.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-list list jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.expr

(defthm return-type-of-atj-gen-list.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-list list jvar-value-base jvar-value-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.new-jvar-value-index

(defthm return-type-of-atj-gen-list.new-jvar-value-index
  (implies
       (posp jvar-value-index)
       (b* (((mv common-lisp::?block
                 ?expr ?new-jvar-value-index)
             (atj-gen-list list jvar-value-base jvar-value-index)))
         (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-cons.block

(defthm return-type-of-atj-gen-cons.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-cons conspair
                      jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-cons.expr

(defthm return-type-of-atj-gen-cons.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-cons conspair
                      jvar-value-base jvar-value-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-cons.new-jvar-value-index

(defthm return-type-of-atj-gen-cons.new-jvar-value-index
  (implies (posp jvar-value-index)
           (b* (((mv common-lisp::?block
                     ?expr ?new-jvar-value-index)
                 (atj-gen-cons conspair
                               jvar-value-base jvar-value-index)))
             (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Subtopics

Atj-gen-values
Atj-gen-list