Collects and returns a special set of runes.
&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
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.
(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)))))))))
(defun defun-theory-fn (names theory quiet missing) (declare (xargs :guard (symbol-listp names))) (defun-theory-fn-rec names theory quiet missing nil))