• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Fty-extensions
      • Defsubtype
      • Defset
      • Deftypes
      • Specific-types
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defomap
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
        • Defunit-implementation
          • Defunit-fn
          • Defunit-macro-definition
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defunit-implementation

Defunit-fn

Event generated by defunit.

Signature

(defunit-fn type value pred fix equiv parents short long) 
  → 
event

Returns

event — A ACL2::pseudo-event-formp.

Definitions and Theorems

Function: defunit-fn

(defun defunit-fn (type value pred fix equiv parents short long)
 (declare (xargs :guard t))
 (let ((__function__ 'defunit-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    ((unless (keywordp value))
     (raise
      "The VALUE input must be a keyword, ~
                but it is ~x0 instead."
      value))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp fix))
     (raise
      "The :FIX input must be a symbol, ~
                but it is ~x0 instead."
      fix))
    ((unless (symbolp equiv))
     (raise
      "The :EQUIV input must be a symbol, ~
                but it is ~x0 instead."
      equiv))
    (x (intern-in-package-of-symbol "X" type))
    (pred (or pred (add-suffix-to-fn type "-P")))
    (fix (or fix (add-suffix-to-fn type "-FIX")))
    (equiv (or equiv (add-suffix-to-fn type "-EQUIV")))
    (type-ref
      (concatenate
           'string
           "@(tsee "
           (common-lisp::string-downcase (symbol-package-name type))
           "::"
           (common-lisp::string-downcase (symbol-name type))
           ")"))
    (pred-event
     (cons
      'define
      (cons
       pred
       (cons
        (cons x 'nil)
        (cons
         ':returns
         (cons
          '(yes/no booleanp)
          (cons
           ':parents
           (cons
            (cons type 'nil)
            (cons ':short
                  (cons (concatenate 'string
                                     "Recognizer for " type-ref ".")
                        (cons (cons 'eq (cons x (cons value 'nil)))
                              '(:no-function t))))))))))))
    (fix-event
     (cons
      'std::deffixer
      (cons
       fix
       (cons
        ':pred
        (cons
         pred
         (cons
          ':param
          (cons
           x
           (cons
            ':body-fix
            (cons
             value
             (cons
              ':parents
              (cons
                 (cons type 'nil)
                 (cons ':short
                       (cons (concatenate 'string
                                          "Fixer for " type-ref ".")
                             'nil)))))))))))))
    (type-event
     (cons
      'defsection
      (cons
       type
       (append
        (and parents (list :parents parents))
        (append
         (and short (list :short short))
         (append
          (and long (list :long long))
          (cons
           (cons
            'deffixtype
            (cons
             type
             (cons
              ':pred
              (cons
               pred
               (cons
                ':fix
                (cons
                   fix
                   (cons ':equiv
                         (cons equiv '(:define t :forward t)))))))))
           'nil))))))))
   (cons
    'encapsulate
    (cons 'nil
          (cons '(logic)
                (cons pred-event
                      (cons fix-event (cons type-event 'nil)))))))))