Collects and returns a special set of runes.
(defun-type/exec-theory names &key (theory '(universal-theory :here)) quiet) searches the theory and collects the :TYPE-PRESCRIPTION, :EXECUTABLE-COUNTERPART, and :INDUCTION runes that were put into the theory by (DEFUN name ... ), for each name in names. Thus, DEFUN-TYPE/EXEC-THEORY is a "constructive" dual of (DIASBLE . 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 single rune 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-type/exec-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-type/exec-theory "The following names you supplied to ~ DEFUN-TYPE/EXEC-THEORY do not have an :INDUCTION, ~ :EXECUTABLE-COUNTERPART, or any :TYPE-PRESECRIPTIONs ~ 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-TYPE/EXEC-THEORY. Missing ~ names: ~p0" missing)))) (t (let* ((name (car names)) (execrune (cons ':executable-counterpart (cons name 'nil))) (inductrune (cons ':induction (cons name 'nil))) (typerune (cons ':type-prescription (cons name 'nil))) (thy (append (if (member-equal typerune theory) (list typerune) nil) (if (member-equal inductrune theory) (list inductrune) nil) (if (member-equal execrune theory) (list execrune) nil)))) (cond ((null thy) (defun-type/exec-theory-fn-rec (cdr names) theory quiet (cons name missing) ans)) (t (defun-type/exec-theory-fn-rec (cdr names) theory quiet missing (append thy ans))))))))
(defun defun-type/exec-theory-fn (names theory quiet missing) (declare (xargs :guard (symbol-listp names))) (defun-type/exec-theory-fn-rec names theory quiet missing nil))