		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-value-flat

Generate flat Java code to build an ACL2 value.

Signature
(atj-gen-value-flat value) → expr
Returns: expr — Type (jexprp expr).

This is similar to atj-gen-value, except that we do not generate local variables for the car and cdr sub-expressions of a cons. We generate a single expression, without blocks; in this sense it is ``flat''.

We set the deep$ and guards$ flags to t and nil when we call atj-gen-symbol, atj-gen-char, and atj-gen-string, so that we generate Acl2Symbols for the ACL2 booleans, Acl2Characters for the ACL2 characters, and Acl2Strings for the ACL2 strings. This is because atj-gen-value-flat is only called on conses at the top level; see the documentation of atj-gen-value.

Function: atj-gen-value-flat

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

Function: atj-gen-values-flat

(defun atj-gen-values-flat (values)
  (declare (xargs :guard (true-listp values)))
  (let ((__function__ 'atj-gen-values-flat))
    (declare (ignorable __function__))
    (cond ((endp values) nil)
          (t (cons (atj-gen-value-flat (car values))
                   (atj-gen-values-flat (cdr values)))))))

Function: atj-gen-list-flat

(defun atj-gen-list-flat (list)
  (declare (xargs :guard (true-listp list)))
  (let ((__function__ 'atj-gen-list-flat))
    (declare (ignorable __function__))
    (jexpr-cast *aij-type-cons*
                (jexpr-smethod *aij-type-value* "makeList"
                               (atj-gen-values-flat list)))))

Function: atj-gen-cons-flat

(defun atj-gen-cons-flat (conspair)
  (declare (xargs :guard (consp conspair)))
  (let ((__function__ 'atj-gen-cons-flat))
    (declare (ignorable __function__))
    (b* (((unless (mbt (consp conspair)))
          (jexpr-name "this-is-irrelevant"))
         (car-expr (atj-gen-value-flat (car conspair)))
         (cdr-expr (atj-gen-value-flat (cdr conspair))))
      (jexpr-smethod *aij-type-cons*
                     "make" (list car-expr cdr-expr)))))

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

(defthm return-type-of-atj-gen-value-flat.expr
  (b* ((?expr (atj-gen-value-flat value)))
    (jexprp expr))
  :rule-classes :rewrite)

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

(defthm return-type-of-atj-gen-values-flat.exprs
  (b* ((?exprs (atj-gen-values-flat values)))
    (and (jexpr-listp exprs)
         (equal (len exprs) (len values))))
  :rule-classes :rewrite)

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

(defthm return-type-of-atj-gen-list-flat.expr
  (b* ((?expr (atj-gen-list-flat list)))
    (jexprp expr))
  :rule-classes :rewrite)

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

(defthm return-type-of-atj-gen-cons-flat.expr
  (b* ((?expr (atj-gen-cons-flat conspair)))
    (jexprp expr))
  :rule-classes :rewrite)

Subtopics

Atj-gen-values-flat
Atj-gen-list-flat