• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
        • Reserr
        • Reserr-option
        • Patbind-ok
        • Reserrf-push
        • Defresult-macro-definition
        • Reserrf
        • Patbind-okf
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Defomap
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • 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

• Defresult

Defresult-macro-definition

Definition of defresult.

Macro: defresult

(defmacro defresult (type &key ok
                          pred fix equiv (parents 'nil parents?)
                          short long prepwork)
 (cons
  'make-event
  (cons
   (cons
    'defresult-fn
    (cons
     (cons 'quote (cons type 'nil))
     (cons
      (cons 'quote (cons ok 'nil))
      (cons
       (cons 'quote (cons pred 'nil))
       (cons
        (cons 'quote (cons fix 'nil))
        (cons
         (cons 'quote (cons equiv 'nil))
         (cons
          (cons 'quote (cons parents 'nil))
          (cons (cons 'quote (cons parents? 'nil))
                (cons (cons 'quote (cons short 'nil))
                      (cons (cons 'quote (cons long 'nil))
                            (cons (cons 'quote (cons prepwork 'nil))
                                  '((w state)))))))))))))
   'nil)))

Definitions and Theorems

Function: defresult-fn

(defun defresult-fn (type ok pred fix equiv parents
                          parents? short long prepwork wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defresult-fn))
  (declare (ignorable __function__))
  (b* ((fty-table (get-fixtypes-alist wrld))
       (fty-info (find-fixtype ok fty-table))
       (ok-pred (fixtype->pred fty-info))
       (type-pred (or pred (add-suffix type "-P")))
       (type-fix (or fix (add-suffix type "-FIX")))
       (type-equiv (or equiv (add-suffix type "-EQUIV")))
       (not-reserrp-when-ok-pred
            (acl2::packn-pos (list 'not-reserrp-when- ok-pred)
                             type))
       (ok-pred-when-type-pred-and-not-reserrp
            (acl2::packn-pos (list ok-pred '-when-
                                   type-pred '-and-not-reserrp)
                             type)))
   (cons
    'encapsulate
    (cons
     'nil
     (append
      prepwork
      (cons
       (cons
        'defflatsum
        (cons
         type
         (append
          (and parents? (list :parents parents))
          (append
           (and short (list :short short))
           (append
            (and long (list :long long))
            (cons
             (cons ':ok (cons ok 'nil))
             (cons
              '(:err reserr)
              (cons
               ':pred
               (cons
                type-pred
                (cons ':fix
                      (cons type-fix
                            (cons ':equiv
                                  (cons type-equiv 'nil)))))))))))))
       (cons
        (cons 'defruled
              (cons not-reserrp-when-ok-pred
                    (cons (cons 'implies
                                (cons (cons ok-pred '(x))
                                      '((not (reserrp x)))))
                          (cons ':enable
                                (cons (cons ok-pred '(reserrp))
                                      'nil)))))
        (cons
         (cons
          'defruled
          (cons ok-pred-when-type-pred-and-not-reserrp
                (cons (cons 'implies
                            (cons (cons 'and
                                        (cons (cons type-pred '(x))
                                              '((not (reserrp x)))))
                                  (cons (cons ok-pred '(x)) 'nil)))
                      (cons ':enable (cons type-pred 'nil)))))
         'nil)))))))))