• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
        • Defsurj
        • Defiso
        • Defmapping-implementation
          • Defmapping-event-generation
          • Defmapping-check-redundancy
          • Defmapping-table
          • Defmapping-fn
          • Defmapping-input-processing
            • Defmapping-process-thm-names
            • Defmapping-process-inputs
            • Defmapping-process-function
            • Defmapping-process-functions
            • Defmapping-process-thm-enable
            • Defmapping-thm-keywords
            • Defmapping-process-name
          • Defmapping-macro-definition
        • Definj
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Defines
      • Define-sk
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Defthm-unsigned-byte-p
      • Support
      • Defthm-signed-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmapping-input-processing

Defmapping-process-thm-names

Process the :thm-names input.

Signature

(defmapping-process-thm-names thm-names name$ 
                              beta-of-alpha-thm$ alpha-of-beta-thm$ 
                              guard-thms$ ctx state) 
 
  → 
(mv erp thm-names$ state)

Arguments

name$ — Guard (symbolp name$).

beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).

alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).

guard-thms$ — Guard (booleanp guard-thms$).

Returns

thm-names$ — A symbol-symbol-alistp.

We compute the names of all the theorems to generate, and we return them as a complete alist from the keywords that identify the theorems to the corresponding theorem names. The alist has unique keys.

If an explicit theorem name is supplied in the :thm-names input, it is used; otherwise, the theorem name is generated as explained in the documentation. The theorem names, whether generated or supplied, must be valid fresh theorem names. They must also be all distinct; this is always the case if the theorem names are all generated, because the keywords used in their names are all distinct.

Definitions and Theorems

Function: defmapping-process-thm-names-aux

(defun defmapping-process-thm-names-aux
       (thm-keywords thm-names-alist name$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp thm-keywords)
                             (symbol-symbol-alistp thm-names-alist)
                             (symbolp name$))))
 (let ((__function__ 'defmapping-process-thm-names-aux))
  (declare (ignorable __function__))
  (if (endp thm-keywords)
      (value nil)
   (b*
    ((thm-keyword (car thm-keywords))
     (pair (assoc-eq thm-keyword thm-names-alist))
     (thm-name (if pair (cdr pair)
                 (add-suffix-to-fn
                      name$
                      (concatenate 'string
                                   "." (symbol-name thm-keyword)))))
     (description (msg "The name ~x0 of the ~x1 theorem, ~@2,"
                       thm-name thm-keyword
                       (if pair "supplied in the :THM-NAMES input"
                         "automatically generated")))
     ((er &)
      (ensure-value-is-symbol$ thm-name description t nil))
     ((er &)
      (ensure-symbol-new-event-name$ thm-name description t nil))
     ((er alist)
      (defmapping-process-thm-names-aux
           (cdr thm-keywords)
           thm-names-alist name$ ctx state)))
    (value (acons thm-keyword thm-name alist))))))

Function: defmapping-process-thm-names

(defun defmapping-process-thm-names
       (thm-names name$
                  beta-of-alpha-thm$ alpha-of-beta-thm$
                  guard-thms$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name$)
                             (booleanp beta-of-alpha-thm$)
                             (booleanp alpha-of-beta-thm$)
                             (booleanp guard-thms$))))
 (let ((__function__ 'defmapping-process-thm-names))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-keyword-value-list$
          thm-names "The :THM-NAMES input" t nil))
    (thm-names-alist (keyword-value-list-to-alist thm-names))
    (keys (strip-cars thm-names-alist))
    (description
         (msg "The list ~x0 of keywords of the :THM-NAMES input"
              keys))
    ((er &)
     (ensure-list-has-no-duplicates$ keys description t nil))
    (thm-keywords
         (defmapping-thm-keywords beta-of-alpha-thm$
                                  alpha-of-beta-thm$ guard-thms$))
    ((er &)
     (ensure-list-subset$ keys thm-keywords description t nil))
    ((er thm-names$)
     (defmapping-process-thm-names-aux
          thm-keywords
          thm-names-alist name$ ctx state))
    (names (strip-cdrs thm-names$))
    (description
     (msg
      "The list ~x0 of theorem names, ~
                          some of which may be supplied ~
                          in the :THM-NAMES input,"
      names))
    ((er &)
     (ensure-list-has-no-duplicates$ names description t nil)))
   (value thm-names$))))