		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-cons-field-name

Generate the name of the Java field for an ACL2 quoted cons pair.

Signature
(atj-gen-shallow-cons-field-name cons qpairs) → name
Arguments: cons — Guard (consp cons).; qpairs — Guard (cons-pos-alistp qpairs).
Returns: name — Type (stringp name).

When this function is called, the cons pair in question has already been collected in an atj-qconstants record, whose alist from cons pairs to indices is passed to this function. We prepend $P_ (for `pair') to the index associated to the cons pair in the alist.

Since cons pairs may be potentially large (unlike atoms), there is no easy way to generate a good field name based on the value, unlike in atj-gen-shallow-number-field-name and others. Thus, as we collect cons pairs from terms, we assign unique indices to them, stored in the alist, and we use the index as the name for the field that contains the associated cons pair.

Definitions and Theorems

Function: atj-gen-shallow-cons-field-name

(defun atj-gen-shallow-cons-field-name (cons qpairs)
  (declare (xargs :guard (and (consp cons)
                              (cons-pos-alistp qpairs))))
  (let ((__function__ 'atj-gen-shallow-cons-field-name))
    (declare (ignorable __function__))
    (b* ((cons+index (assoc-equal cons qpairs))
         ((unless (consp cons+index))
          (raise "Internal error: no index for CONS pair ~x0."
                 cons)
          "")
         (index (cdr cons+index)))
      (str::cat "$P_" (nat-to-dec-string index)))))

Theorem: stringp-of-atj-gen-shallow-cons-field-name

(defthm stringp-of-atj-gen-shallow-cons-field-name
  (b* ((name (atj-gen-shallow-cons-field-name cons qpairs)))
    (stringp name))
  :rule-classes :rewrite)