		Search-engine friendly clone of the ACL2 documentation.

Deffixer-implementation

Deffixer-fn

Event generated by deffixer.

Signature
(deffixer-fn name pred param body-fix parents parents-supplied-p short short-supplied-p long long-supplied-p) → event
Arguments: parents-supplied-p — Guard (booleanp parents-supplied-p).; short-supplied-p — Guard (booleanp short-supplied-p).; long-supplied-p — Guard (booleanp long-supplied-p).
Returns: event — Type (acl2::maybe-pseudo-event-formp event).

Definitions and Theorems

Function: deffixer-fn

(defun deffixer-fn (name pred param body-fix
                         parents parents-supplied-p short
                         short-supplied-p long long-supplied-p)
 (declare (xargs :guard (and (booleanp parents-supplied-p)
                             (booleanp short-supplied-p)
                             (booleanp long-supplied-p))))
 (let ((__function__ 'deffixer-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but it is ~x0 instead."
      name))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp param))
     (raise
      "The :PARAM input must be a symbol, ~
                but it is ~x0 instead."
      param))
    (pkg (symbol-package-name name))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (param (or param
               (intern-in-package-of-symbol "X" pkg-witness)))
    (fixed-param (acl2::packn-pos (list 'fixed- param)
                                  pkg-witness))
    (name-when-pred-thm
     (cons
      'defrule
      (cons
       (acl2::packn-pos (list name '-when- pred)
                        pkg-witness)
       (cons
         (cons 'implies
               (cons (cons pred (cons param 'nil))
                     (cons (cons 'equal
                                 (cons (cons name (cons param 'nil))
                                       (cons param 'nil)))
                           'nil)))
         'nil))))
    (name-fn
     (cons
      'define
      (cons
       name
       (cons
        (cons (cons param (cons pred 'nil))
              'nil)
        (cons
         ':returns
         (cons
          (cons fixed-param (cons pred 'nil))
          (append
           (and parents-supplied-p
                (list :parents parents))
           (append
            (and short-supplied-p (list :short short))
            (append
             (and long-supplied-p (list :long long))
             (cons
              (cons
               'mbe
               (cons
                ':logic
                (cons
                     (cons 'if
                           (cons (cons pred (cons param 'nil))
                                 (cons param (cons body-fix 'nil))))
                     (cons ':exec (cons param 'nil)))))
              (cons
               ':no-function
               (cons
                  't
                  (cons '///
                        (cons name-when-pred-thm 'nil)))))))))))))))
   (cons 'encapsulate
         (cons 'nil
               (cons '(logic) (cons name-fn 'nil)))))))

Theorem: maybe-pseudo-event-formp-of-deffixer-fn

(defthm maybe-pseudo-event-formp-of-deffixer-fn
  (b* ((event (deffixer-fn name pred param body-fix
                           parents parents-supplied-p short
                           short-supplied-p long long-supplied-p)))
    (acl2::maybe-pseudo-event-formp event))
  :rule-classes :rewrite)