		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Macro-add

Add a macro to the macro table.

Signature
(macro-add name info table) → (mv erp new-table)
Arguments: name — Guard (identp name).; info — Guard (macro-infop info).; table — Guard (macro-tablep table).
Returns: new-table — Type (macro-tablep new-table).

If the table already contains a macro with the given name, the associated information must be the same: this realizes the requirement in [C17:6.10.3/2], namely that multiple definitions are allowed so long as they are of the same kind (both object-like or both function-like), they have the same parameters if both function-like, and they have identical replacement list. The latter notion [C17:6.10.3/1] amounts to equality for us, because, as explained in macro-info, we normalize all whitespace to single spaces. If all these conditions are satisfied, the table does not change; otherwise, we return an error.

If the table does not already contain a macro with the given name, it is added to the table.

Definitions and Theorems

Function: macro-add

(defun macro-add (name info table)
 (declare (xargs :guard (and (identp name)
                             (macro-infop info)
                             (macro-tablep table))))
 (b* (((reterr) (irr-macro-table))
      (name (ident-fix name))
      (info (macro-info-fix info))
      (alist (macro-table->alist table))
      (name+info (assoc-equal name alist)))
  (if name+info
   (if (equal info (cdr name+info))
       (retok (macro-table-fix table))
    (reterr
     (msg
      "Duplicate macro ~x0 ~
                        with incompatible definitions ~x1 and ~x2."
      name info (cdr name+info))))
   (retok (macro-table (acons name info alist))))))

Theorem: macro-tablep-of-macro-add.new-table

(defthm macro-tablep-of-macro-add.new-table
  (b* (((mv acl2::?erp ?new-table)
        (macro-add name info table)))
    (macro-tablep new-table))
  :rule-classes :rewrite)

Theorem: macro-add-of-ident-fix-name

(defthm macro-add-of-ident-fix-name
  (equal (macro-add (ident-fix name) info table)
         (macro-add name info table)))

Theorem: macro-add-ident-equiv-congruence-on-name

(defthm macro-add-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (macro-add name info table)
                  (macro-add name-equiv info table)))
  :rule-classes :congruence)

Theorem: macro-add-of-macro-info-fix-info

(defthm macro-add-of-macro-info-fix-info
  (equal (macro-add name (macro-info-fix info)
                    table)
         (macro-add name info table)))

Theorem: macro-add-macro-info-equiv-congruence-on-info

(defthm macro-add-macro-info-equiv-congruence-on-info
  (implies (macro-info-equiv info info-equiv)
           (equal (macro-add name info table)
                  (macro-add name info-equiv table)))
  :rule-classes :congruence)

Theorem: macro-add-of-macro-table-fix-table

(defthm macro-add-of-macro-table-fix-table
  (equal (macro-add name info (macro-table-fix table))
         (macro-add name info table)))

Theorem: macro-add-macro-table-equiv-congruence-on-table

(defthm macro-add-macro-table-equiv-congruence-on-table
  (implies (macro-table-equiv table table-equiv)
           (equal (macro-add name info table)
                  (macro-add name info table-equiv)))
  :rule-classes :congruence)