• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
          • Ihs-utilities
            • Defun-type/exec-theory
            • Defun-theory
            • Definition-free-theory
            • Rewrite-theory
            • Rewrite-free-theory
            • Definition-theory
            • Mlambda
            • Enable-theory
            • Disable-theory
        • Logops
      • Rtl
    • Algebra

• Ihs-utilities

Defun-type/exec-theory

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.

Definitions and Theorems

Function: defun-type/exec-theory-fn-rec

(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))))))))

Function: defun-type/exec-theory-fn

(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))