		Search-engine friendly clone of the ACL2 documentation.

Errors

Defresult

Introduce a fixtype of result types.

This is a flat sum of the specified fixtype and the error fixtype. Thus, the specified fixtype must be disjoint from the error fixtype, which is easily satisfied if values of the specified fixtype do not start with :error.

We also generate a theorem to conclude that a value is of the original type when it is of the new type and not an error. We disable it by default so that we do not always backchain to the result type when trying to prove the base type, in contexts where the result type is not used at all.

Definitions and Theorems

Function: defresult-fn

(defun defresult-fn (type desc name enable wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defresult-fn))
  (declare (ignorable __function__))
  (b* ((fty-table (fty::get-fixtypes-alist wrld))
       (fty-info (fty::find-fixtype type fty-table))
       (typep (fty::fixtype->pred fty-info))
       (name (or name type))
       (name-result (add-suffix name "-RESULT"))
       (name-resultp (add-suffix name "-RESULTP"))
       (short (str::cat "Fixtype of " desc " and errors."))
       (typep-when-name-resultp-and-not-errorp
            (packn-pos (list typep '-when-
                             name-resultp '-and-not-errorp)
                       name)))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      (cons
       'fty::defflatsum
       (cons
        name-result
        (cons
         ':short
         (cons
          short
          (cons
           (cons ':ok (cons type 'nil))
           (cons
            '(:err error)
            (cons
             ':pred
             (cons
              name-resultp
              (and
               enable
               (cons
                ':prepwork
                (cons
                 (cons
                  (cons
                   'defrulel
                   (cons
                    'disjoint
                    (cons
                     (cons
                      'implies
                      (cons
                          '(errorp x)
                          (cons (cons 'not
                                      (cons (cons typep '(x)) 'nil))
                                'nil)))
                     (cons ':enable (cons enable 'nil)))))
                  'nil)
                 'nil)))))))))))
      (cons
       (cons
        'defruled
        (cons typep-when-name-resultp-and-not-errorp
              (cons (cons 'implies
                          (cons (cons 'and
                                      (cons (cons name-resultp '(x))
                                            '((not (errorp x)))))
                                (cons (cons typep '(x)) 'nil)))
                    (cons ':enable
                          (cons name-resultp 'nil)))))
       'nil)))))))