Generate the name of the Java field for an ACL2 quoted cons pair.
(atj-gen-shallow-cons-field-name cons qpairs) → 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
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.
Function:
(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:
(defthm stringp-of-atj-gen-shallow-cons-field-name (b* ((name (atj-gen-shallow-cons-field-name cons qpairs))) (stringp name)) :rule-classes :rewrite)