		Search-engine friendly clone of the ACL2 documentation.

Ihs-utilities

Defun-theory

Collects and returns a special set of runes.

(defun-theory names &key (theory '(universal-theory :here)) quiet) searches the theory and collects the :DEFINITION, :INDUCTION, :TYPE-PRESCRIPTION, and :EXECUTABLE-COUNTERPART runes that were put into the theory by (DEFUN name ... ), for each name in names.

The default for the theory argument is (UNIVERSAL-THEORY :HERE). Normally the function will crash if any of the names in names do not have a :DEFINITION in the theory. Call with :QUIET T to avoid this behavior. Note however that limitations in ACL2 make it impossible to produce even a warning message if you specify :QUIET T.

Definitions and Theorems

Function: defun-theory-fn-rec

(defun defun-theory-fn-rec (names theory quiet missing ans)
 (declare (xargs :guard (and (symbol-listp names)
                             (true-listp ans))))
 (cond
  ((endp names)
   (cond
    ((or quiet (null missing))
     (reverse ans))
    (t
     (er
      hard 'defun-theory
      "The following names you supplied to DEFUN-THEORY do ~
                       not have a :DEFINITION in the theory you supplied.  ~
                       Check to make sure that the theory is correct (it ~
                       defaults to (UNIVERSAL-THEORY :HERE)) and that these ~
                       are not the names of macros. To avoid this message ~
                       specify :QUIET T in the call to DEFUN-THEORY. Missing ~
                       names: ~p0"
      missing))))
  (t (let* ((name (car names))
            (defrune (cons ':definition (cons name 'nil)))
            (execrune (cons ':executable-counterpart
                            (cons name 'nil)))
            (inductrune (cons ':induction (cons name 'nil)))
            (typerune (cons ':type-prescription
                            (cons name 'nil)))
            (tail (member-equal defrune theory)))
       (cond ((not tail)
              (defun-theory-fn-rec (cdr names)
                                   theory quiet (cons name missing)
                                   ans))
             (t (defun-theory-fn-rec
                     (cdr names)
                     theory quiet missing
                     (append (if (member-equal typerune tail)
                                 (list typerune)
                               nil)
                             (if (member-equal inductrune tail)
                                 (list inductrune)
                               nil)
                             (if (member-equal execrune tail)
                                 (list execrune)
                               nil)
                             (cons defrune ans)))))))))

Function: defun-theory-fn

(defun defun-theory-fn (names theory quiet missing)
  (declare (xargs :guard (symbol-listp names)))
  (defun-theory-fn-rec names theory quiet missing nil))