		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-add-qconstant

Add (the value of) a quoted constant to a structured collection.

Signature
(atj-add-qconstant value record) → new-record
Arguments: record — Guard (atj-qconstants-p record).
Returns: new-record — Type (atj-qconstants-p new-record), given the guard.

We add the value to the appropriate list, unless it is already present. The process is slightly more complicated for cons pairs, as it involves an alist; if the pair is not already in the alist, we add it, associated with the next index to use, and we increment the next index to use in the record.

Definitions and Theorems

Function: atj-add-qconstant

(defun atj-add-qconstant (value record)
 (declare (xargs :guard (atj-qconstants-p record)))
 (let ((__function__ 'atj-add-qconstant))
  (declare (ignorable __function__))
  (b* (((atj-qconstants record) record))
   (cond
    ((integerp value)
     (change-atj-qconstants
          record
          :integers (add-to-set value record.integers)))
    ((rationalp value)
     (change-atj-qconstants
          record
          :rationals (add-to-set value record.rationals)))
    ((acl2-numberp value)
     (change-atj-qconstants
          record
          :numbers (add-to-set value record.numbers)))
    ((characterp value)
     (change-atj-qconstants record
                            :chars (add-to-set value record.chars)))
    ((stringp value)
     (change-atj-qconstants
          record
          :strings (add-to-set-equal value record.strings)))
    ((symbolp value)
     (change-atj-qconstants
          record
          :symbols (add-to-set-eq value record.symbols)))
    ((consp value)
     (b* ((value+index? (assoc-equal value record.pairs)))
       (if (consp value+index?)
           record
         (change-atj-qconstants
              record
              :pairs (acons value record.next-index record.pairs)
              :next-index (1+ record.next-index)))))
    (t
     (prog2$ (raise "Internal error: ~x0 is not a recognized value."
                    value)
             record))))))

Theorem: atj-qconstants-p-of-atj-add-qconstant

(defthm atj-qconstants-p-of-atj-add-qconstant
  (implies (and (atj-qconstants-p record))
           (b* ((new-record (atj-add-qconstant value record)))
             (atj-qconstants-p new-record)))
  :rule-classes :rewrite)