• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Defines
      • Define-sk
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
        • Deffixer-implementation
          • Deffixer-fn
          • Deffixer-macro-definition
        • Defconstrained-recognizer-implementation
      • Defmvtypes
      • Defconsts
      • Defthm-unsigned-byte-p
      • Support
      • Defthm-signed-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

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