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