Filtering...

returnspecs

books/std/util/returnspecs
other
(in-package "STD")
other
(include-book "da-base")
other
(include-book "look-up")
other
(program)
other
(defxdoc returns-specifiers
  :parents (std/util define)
  :short "A concise way to name, document, and prove basic type-like theorems
about a function's return values."
  :long "<p>The @(see define) macro and some other @(see std/util) macros
support a @(':returns') option.  This option provides a concise way to name,
document, and prove basic type-like theorems about the return values of your
functions.  Named return values also allow your function to be used with the
special <see topic='@(url acl2::patbind-ret)'>ret</see> binder for @(see
b*).</p>

<p>The general form is:</p>

@({
    :returns return-spec       ;; for single-value functions
 or :returns (mv return-spec*) ;; for multiple-valued functions
})

<p>There should be exactly one @('return-spec') per return value.  Each
return-spec has the form:</p>

@({
     name               ;; just for naming return values
  or (name [option]*)   ;; for naming, documenting, and proving theorems
})

<p>where @('name') is a symbol and the options can come in any order.  To
distinguish between the two forms of @(':returns'), it is not legal to use
@('mv') as the name of a return value.  The options are:</p>

<dl>

<dt>@('<xdoc>'), any string literal</dt>

<dd>You can document each return value with a string literal.  The string may
make use of @(see xdoc::markup) and @(see xdoc::preprocessor) directives.
Typically these descriptions should be short and not include
document-structuring tags like @('<p>'), @('<ul>'), @('<h3>'), and so forth.
See the section on xdoc integration, below, for more details.</dd>

<dt>@('<return-type>'), a symbol or term</dt>

<dd>When provided, the return type is used to generate a basic type-like
theorems about the return values.  A default hint is provided if no @(':hints')
keyword is present; see the discussion of @(':hints') below.</dd>

<dd><b>Important Note</b> in the multiple-valued case, this approach assumes
you are using the @('tools/mv-nth') book.  The theorems we prove target terms
like @('(mv-nth 0 (f ...))') and @('(mv-nth 1 (f ...))').  This will not work
well if @(see mv-nth) is enabled, especially about the 0th return value. For
your convenience, @('define') automatically includes the @('tools/mv-nth')
book.  You really should be using it, you know.</dd>

<dd>As a convenient shorthand, you can use a single symbol like @('evenp').
The theorem to be proven in this case might be, e.g., @('(evenp (f x))') for a
single-valued function, or @('(evenp (mv-nth 3 (f x)))') if this is the
fourth (because of zero-indexing) return value of a multiply-valued function.
The symbol @('t') is explicitly allowed and results in no theorem.  The symbol
@('nil') and keyword symbols are explicitly invalid as return types.</dd>

<dd>In certain cases, you may wish to prove a more complex theorem, e.g., say
we want to prove this return value is always greater than 5.  To support this,
you can write a return type like @('(< 5 ans)'), where @('ans') is the
@('name') of this return value.  You can also refer to the names of other
return values in this term.  To make it easy to distinguish return types from
other options, the return type term must be a cons and must not begin with
@('quote').</dd>

<dt>@(':hyp hyp-term')</dt>

<dd>This option only makes sense when there is a return-type term.  By default,
the return-type theorem is unconditional.  If the theorem needs a hypothesis,
you can put it here.</dd>

<dd>Frequently, the hypothesis you want for a type-like theorem is for the
guards of the function to be met.  As a convenient shorthand, @('hyp-term') may
be:

<ul>
<li>@(':guard') -- use the function's guard as the hypothesis</li>
<li>@(':fguard') -- like @(':guard'), but @(see force) the entire guard</li>
</ul>

If neither of these is what you want, you can provide an arbitrary
@('hyp-term').  Typically this term should mention only the formals of your
function.  The return values of the theorem will not be bound in scope of the
hyp, so trying to refer to them in a hypothesis is generally an error.</dd>

<dt>@(':hints hints-term')</dt>

<dd>This option only makes sense when there is a return-type term; when
specified, the given hints are passed to the proof attempt for the associated
return-type.  When no @(':hints') keyword is present, a default hint is taken
from the @('std::returnspec') entry of the @('std::default-hints-table') table,
but this is overridden if the @(':hints') keyword is present, even for
@(':hints nil').  To change the default hints, you may use
@('set-returnspec-default-hints').  The setting for this provided in the
std/util books provides an induction and expand hint when the
function introduced is singly-recursive.</dd>

<dd>A few special symbols (and even substrings of symbols) are substituted into
hints; see the section "Substitutions" below.</dd>

<dt>@(':rule-classes classes')</dt>

<dd>This option only makes sense when there is a return-type term.  By default,
the return-type theorem is added as a @(':rewrite') rule.  If you want to use
other @(see acl2::rule-classes), then you will want to override this default.</dd>

<dd>A few special symbols (and even substrings of symbols) are substituted into
hints; see the section "Substitutions" below.</dd>

<dt>@(':name name')</dt>

<dd>This allows you to control the name of the associated theorem.</dd>

<dd>The default value of @('name') is <it>type</it>-of-<it>your-function</it>.
For example, @('natp-of-foo').</dd>

<dt>@(':hints-sub-returnnames')</dt>

<dd>This option determines whether the
return-name substitution is applied to the hints. See "Substitutions"
below.</dd>

</dl>

<h3>Substitutions</h3>

<p>Certain symbols and certain substrings of symbols are
replaced in the theorem body, hints, and rule-classes.</p>

<p>The following substitutions replace any symbol matching the given name in
all three places (body, hints, and rule-classes):</p>

<ul>
<li>@('<CALL>') is replaced by the function applied to the formals.</li>
<li>@('<FN>') is replaced by the function's macro alias, if it has one, or else its name.  That is, for a form that introduces @('foo') with macro arguments, creating a function named @('foo-fn'), this produces @('foo').</li>
<li>@('<FN!>') is replaced by the functions name, strictly, i.e. @('foo-fn') in the example above.</li>
<li>@('<VALUES>') is replaced by the list of return value names.</li>
</ul>

<p>In the hints, the substrings @('<FN>') and @('<FN!>') of symbol names are
also substituted as above.  This allows hints to refer to @(see defret)-style
theorem names.</p>

<p>In the rule-classes, the return value names are substituted for appropriate
terms; i.e., if the second return value of @('foo') is named @('bar'), then
@('bar') becomes @('(mv-nth 1 (foo ...))').  This substitution may also
optionally be applied to the hints by setting the @(':hints-sub-returnnames') option.
This return name substitution is not applied to the theorem body, but the let-binding
of the return names to the function call has a similar effect.</p>

<h3>Configuration Object</h3>

<p>Similar to @(see define), a configuration object can be set up to set some
options globally (local to a book).  At the moment only the
@(':hints-sub-returnnames') option is read from this configuration object.  The
following form sets that option:</p>

@({
 (make-returnspec-config :hints-sub-returnnames t)
 })

")
other
(def-primitive-aggregate returnspec
  (name doc
    return-type
    hyp
    hints
    hintsp
    rule-classes
    thm-name
    opts)
  :tag :return-spec)
other
(defconst *default-returnspec*
  (make-returnspec :name 'ret
    :doc ""
    :return-type t
    :hyp t
    :hints nil
    :hintsp nil
    :rule-classes :rewrite :thm-name nil))
returnspeclist-pfunction
(defun returnspeclist-p
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    t
    (and (returnspec-p (car x))
      (returnspeclist-p (cdr x)))))
returnspeclist->namesfunction
(defun returnspeclist->names
  (x)
  (declare (xargs :guard (returnspeclist-p x)))
  (if (atom x)
    nil
    (cons (returnspec->name (car x))
      (returnspeclist->names (cdr x)))))
parse-returnspec-itemfunction
(defun parse-returnspec-item
  (fnname varname item terms docs)
  "Returns (mv terms docs)"
  (declare (xargs :guard t))
  (b* ((__function__ 'parse-returnspec-item) ((when (eq item t)) (mv (cons item terms) docs))
      ((when (or (eq item nil) (keywordp item))) (raise "Error in ~x0: return type for ~x1 is ~x2, which is not ~
                allowed."
          fnname
          varname
          item)
        (mv terms docs))
      ((when (symbolp item)) (mv (cons `(,STD::ITEM ,STD::VARNAME) terms)
          docs))
      ((when (and (consp item) (not (eq (car item) 'quote)))) (mv (cons item terms) docs))
      ((when (stringp item)) (mv terms (cons item docs))))
    (raise "Error in ~x0, return type for ~x1: expected return type terms or ~
            documentation strings, but found ~x2."
      fnname
      varname
      item)
    (mv terms docs)))
parse-returnspec-itemsfunction
(defun parse-returnspec-items
  (fnname varname items terms docs)
  "Returns (mv terms docs)"
  (declare (xargs :guard t))
  (b* ((__function__ 'parse-returnspec-items) ((when (not items)) (mv terms docs))
      ((when (atom items)) (raise "Error in ~x0: expected returnspec-items for ~x1 to be ~
                nil-terminated, but found ~x2 as the final cdr."
          fnname
          varname
          items)
        (mv terms docs))
      ((mv terms docs) (parse-returnspec-item fnname
          varname
          (car items)
          terms
          docs)))
    (parse-returnspec-items fnname
      varname
      (cdr items)
      terms
      docs)))
parse-returnspecfunction
(defun parse-returnspec
  (fnname x world)
  "Returns a returnspec-p."
  (declare (xargs :guard (plist-worldp world)))
  (b* ((__function__ 'parse-returnspec) ((when (eq x 'mv)) (raise "Error in ~x0: return values may not be named MV."
          fnname)
        *default-returnspec*)
      ((when (symbolp x)) (b* ((look (getprop x
               'formals
               :bad 'current-acl2-world
               world)) ((unless (eq look :bad)) (raise "Error in ~x0: you named a return value ~x1, which is ~
                      the name of a defined function, but you don't have any ~
                      return type associated with this value.  There's a good ~
                      chance this you meant this to be the return value's ~
                      type instead of its name.~%~%If you really want to name ~
                      this return value ~x1 and not prove anything about it, ~
                      you can use syntax like ~x2.~%"
                fnname
                x
                (list x t))
              *default-returnspec*))
          (make-returnspec :name x
            :doc ""
            :return-type t
            :rule-classes :rewrite :hyp nil
            :hints nil
            :thm-name nil)))
      ((when (atom x)) (raise "Error in ~x0: return specifiers must be symbols or lists, but ~
                found: ~x1"
          fnname
          x)
        *default-returnspec*)
      ((cons varname options) x)
      ((unless (symbolp varname)) (raise "Error in ~x0: return specifiers must start with a symbol ~
                name, so this return specifier is not valid: ~x1"
          fnname
          x)
        *default-returnspec*)
      ((when (eq varname 'mv)) (raise "Error in ~x0: return values may not be named MV."
          fnname)
        *default-returnspec*)
      ((mv kwd-alist other-opts) (extract-keywords fnname
          '(:hyp :hints :rule-classes :name :props :hints-sub-returnnames)
          options
          nil))
      (hyp (if (assoc :hyp kwd-alist)
          (cdr (assoc :hyp kwd-alist))
          t))
      ((when (and (keywordp hyp)
           (not (eq hyp :guard))
           (not (eq hyp :fguard)))) (raise "Error in ~x0: invalid keyword ~x1 used as a :hyp."
          fnname
          hyp)
        *default-returnspec*)
      ((mv hints hintsp) (if (assoc :hints kwd-alist)
          (mv (cdr (assoc :hints kwd-alist)) t)
          (mv nil nil)))
      (rule-classes (if (assoc :rule-classes kwd-alist)
          (cdr (assoc :rule-classes kwd-alist))
          :rewrite))
      (thm-name (if (assoc :name kwd-alist)
          (cdr (assoc :name kwd-alist))
          nil))
      ((mv terms docs) (parse-returnspec-items fnname
          varname
          other-opts
          nil
          nil))
      (return-type (cond ((atom terms) t)
          ((atom (cdr terms)) (car terms))
          (t (raise "Error in ~x0: return specifier ~x1 has multiple return ~
                       type terms, but at most one is allowed: ~&2"
              fnname
              varname
              terms))))
      (xdoc (cond ((atom docs) "")
          ((atom (cdr docs)) (car docs))
          (t (progn$ (raise "Error in ~x0: return specifier ~x1 has multiple xdoc ~
                        strings, but at most one is allowed: ~x2."
                fnname
                varname
                terms)
              "")))))
    (make-returnspec :name varname
      :doc xdoc
      :return-type return-type
      :rule-classes rule-classes
      :hyp hyp
      :hints hints
      :hintsp hintsp
      :thm-name thm-name
      :opts kwd-alist)))
parse-returnspecs-auxfunction
(defun parse-returnspecs-aux
  (fnname x world)
  "Returns a returnspeclist-p"
  (declare (xargs :guard (plist-worldp world)))
  (if (atom x)
    nil
    (cons (parse-returnspec fnname (car x) world)
      (parse-returnspecs-aux fnname
        (cdr x)
        world))))
normalize-returnspecsfunction
(defun normalize-returnspecs
  (fnname x)
  (declare (xargs :guard t))
  (b* ((__function__ 'normalize-returnspecs) ((unless x) nil)
      ((when (eq x 'mv)) (raise "Error in ~x0: :returns may not be just MV."
          fnname))
      ((when (symbolp x)) (list x))
      ((when (atom x)) (raise "Error in ~x0: :returns may not be ~x1."
          fnname
          x))
      ((when (eq (car x) 'mv)) (if (true-listp (cdr x))
          (cdr x)
          (raise "Error in ~x0: :returns must be nil-terminated, but ~x1 is not."
            fnname
            x))))
    (list x)))
parse-returnspecsfunction
(defun parse-returnspecs
  (fnname x world)
  "Returns a returnspeclist-p"
  (declare (xargs :guard (plist-worldp world)))
  (parse-returnspecs-aux fnname
    (normalize-returnspecs fnname x)
    world))
arity-check-returnsfunction
(defun arity-check-returns
  (name name-fn specs world)
  (declare (xargs :guard (and (symbolp name)
        (symbolp name-fn)
        (returnspeclist-p specs)
        (plist-worldp world))))
  (b* (((when (atom specs)) t) (stobjs-out (look-up-return-vals name-fn world))
      ((when (equal (len stobjs-out) (len specs))) t)
      ((when (getprop name-fn
           'non-executablep
           nil
           'current-acl2-world
           world)) t))
    (er hard?
      'arity-check-returns
      "Error in ~x0: ACL2 thinks this function has ~x1 return ~
         values, but :returns has ~x2 entries!"
      name
      (len stobjs-out)
      (len specs))))
other
(defsection untranslate-and
  (defun untranslate-and
    (x)
    (declare (xargs :guard t))
    (cond ((atom x) (list x))
      ((and (consp x)
         (eq (first x) 'if)
         (equal (len x) 4)
         (equal (fourth x) ''nil)) (cons (second x) (untranslate-and (third x))))
      (t (list x)))))
force-eachfunction
(defun force-each
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    nil
    (cons `(force ,(CAR STD::X))
      (force-each (cdr x)))))
fancy-force-hypfunction
(defun fancy-force-hyp
  (x)
  (declare (xargs :guard t))
  (b* ((hyp-list (untranslate-and x)))
    (cons 'and (force-each hyp-list))))
fancy-hypfunction
(defun fancy-hyp
  (x)
  (declare (xargs :guard t))
  (b* ((hyp-list (untranslate-and x)))
    (cons 'and hyp-list)))
returnspec-thm-bodyfunction
(defun returnspec-thm-body
  (fnname binds x world)
  (declare (xargs :guard (and (symbolp fnname)
        (returnspec-p x)
        (plist-worldp world))))
  (b* (((returnspec x) x) ((when (equal x.return-type t)) t)
      (hyp (cond ((eq x.hyp :guard) (fancy-hyp (look-up-guard fnname world)))
          ((eq x.hyp :fguard) (fancy-force-hyp (look-up-guard fnname world)))
          (t x.hyp)))
      (concl `(b* (,STD::BINDS) ,STD::X.RETURN-TYPE)))
    (if (eq hyp t)
      concl
      `(implies ,STD::HYP ,STD::CONCL))))
returnspec-generate-namefunction
(defun returnspec-generate-name
  (name x singlep badname-okp)
  (b* (((returnspec x) x) ((when x.thm-name) x.thm-name)
      (multi-suffix (if singlep
          ""
          (concatenate 'string "." (symbol-name x.name))))
      ((when (and (tuplep 2 x.return-type)
           (symbolp (first x.return-type))
           (equal (second x.return-type) x.name))) (intern-in-package-of-symbol (concatenate 'string
            (symbol-name (first x.return-type))
            "-OF-"
            (symbol-name name)
            multi-suffix)
          name))
      ((unless badname-okp) (er hard?
          'returnspec-generate-name
          "Return spec for ~x0, ~x1, must be given an explicit name."
          name
          x.return-type)))
    (intern-in-package-of-symbol (concatenate 'string
        "RETURN-TYPE-OF-"
        (symbol-name name)
        multi-suffix)
      name)))
returnspec-default-default-hintfunction
(defun returnspec-default-default-hint
  (fnname id world)
  (and (eql (len (recursivep fnname t world)) 1)
    (let* ((pool-lst (access clause-id id :pool-lst)))
      (and (eql 0 (access clause-id id :forcing-round))
        (cond ((not pool-lst) (let ((formals (look-up-formals fnname world)))
              `(:induct (,STD::FNNAME . ,STD::FORMALS)
                :in-theory (disable (:d ,STD::FNNAME)))))
          ((equal pool-lst '(1)) `(:computed-hint-replacement ((and stable-under-simplificationp
                 (expand-calls ,STD::FNNAME)))
              :in-theory (disable (:d ,STD::FNNAME)))))))))
returnspec-default-hintsfunction
(defun returnspec-default-hints
  (fnname world)
  (let ((entry (cdr (assoc 'returnspec
           (table-alist 'default-hints-table world)))))
    (subst fnname 'fnname entry)))
set-returnspec-default-hintsmacro
(defmacro set-returnspec-default-hints
  (hint)
  `(table default-hints-table
    'returnspec
    ',STD::HINT))
other
(set-returnspec-default-hints ((returnspec-default-default-hint 'fnname
     id
     world)))
returnspec-sublisfunction
(defun returnspec-sublis
  (subst str-subst x)
  "Like sublis, but only substitutes symbols, and looks them up both by value and by name."
  (if (atom x)
    (if (symbolp x)
      (let ((look (assoc-equal x subst)))
        (if look
          (cdr look)
          (let ((look (assoc-equal (symbol-name x) subst)))
            (if look
              (cdr look)
              (let ((subst (dumb-str-sublis str-subst (symbol-name x))))
                (if (equal subst (symbol-name x))
                  x
                  (intern-in-package-of-symbol subst x)))))))
      x)
    (cons-with-hint (returnspec-sublis subst str-subst (car x))
      (returnspec-sublis subst str-subst (cdr x))
      x)))
returnspec-strsubstfunction
(defun returnspec-strsubst
  (fnname fnname-fn)
  `(("<FN>" . ,(SYMBOL-NAME STD::FNNAME)) ("<FN!>" . ,(SYMBOL-NAME STD::FNNAME-FN))))
returnspec-single-thmfunction
(defun returnspec-single-thm
  (name name-fn
    x
    body-subst
    ruleclass-subst
    badname-okp
    config
    world)
  "Returns EVENTS"
  (declare (xargs :guard (and (symbolp name)
        (symbolp name-fn)
        (returnspec-p x)
        (plist-worldp world))))
  (b* (((returnspec x) x) (formals (look-up-formals name-fn world))
      (binds `(,STD::X.NAME (,STD::NAME-FN . ,STD::FORMALS)))
      (formula (returnspec-sublis body-subst
          nil
          (returnspec-thm-body name-fn
            binds
            x
            world)))
      ((when (eq formula t)) nil)
      (strsubst (returnspec-strsubst name name-fn))
      (hints-sub-returnnames (getarg :hints-sub-returnnames (getarg :hints-sub-returnnames nil config)
          x.opts))
      (hints (if x.hintsp
          (returnspec-sublis (if hints-sub-returnnames
              ruleclass-subst
              body-subst)
            strsubst
            x.hints)
          (returnspec-default-hints name-fn world))))
    `((defthm ,(STD::RETURNSPEC-GENERATE-NAME STD::NAME STD::X T STD::BADNAME-OKP)
       ,STD::FORMULA
       :hints ,STD::HINTS
       :rule-classes ,(STD::RETURNSPEC-SUBLIS STD::RULECLASS-SUBST NIL STD::X.RULE-CLASSES)))))
returnspec-multi-thmfunction
(defun returnspec-multi-thm
  (name name-fn
    binds
    x
    body-subst
    ruleclass-subst
    badname-okp
    config
    world)
  "Returns EVENTS"
  (declare (xargs :guard (and (symbolp name)
        (symbolp name-fn)
        (returnspec-p x)
        (symbol-alistp config)
        (plist-worldp world))))
  (b* (((returnspec x) x) (formula (returnspec-sublis body-subst
          nil
          (returnspec-thm-body name-fn
            binds
            x
            world)))
      ((when (equal formula t)) nil)
      (strsubst (returnspec-strsubst name name-fn))
      (hints-sub-returnnames (getarg :hints-sub-returnnames (getarg :hints-sub-returnnames nil config)
          x.opts))
      (hints (if x.hintsp
          (returnspec-sublis (if hints-sub-returnnames
              ruleclass-subst
              body-subst)
            strsubst
            x.hints)
          (returnspec-default-hints name-fn world))))
    `((defthm ,(STD::RETURNSPEC-GENERATE-NAME STD::NAME STD::X NIL STD::BADNAME-OKP)
       ,STD::FORMULA
       :hints ,STD::HINTS
       :rule-classes ,(STD::RETURNSPEC-SUBLIS STD::RULECLASS-SUBST NIL STD::X.RULE-CLASSES)))))
returnspec-multi-thmsfunction
(defun returnspec-multi-thms
  (name name-fn
    binds
    x
    body-subst
    ruleclass-subst
    badname-okp
    config
    world)
  "Returns EVENTS"
  (declare (xargs :guard (and (symbolp name)
        (symbolp name-fn)
        (returnspeclist-p x)
        (symbol-alistp config)
        (plist-worldp world))))
  (if (atom x)
    nil
    (append (returnspec-multi-thm name
        name-fn
        binds
        (car x)
        body-subst
        ruleclass-subst
        badname-okp
        config
        world)
      (returnspec-multi-thms name
        name-fn
        binds
        (cdr x)
        body-subst
        ruleclass-subst
        badname-okp
        config
        world))))
make-symbol-ignorablefunction
(defun make-symbol-ignorable
  (x)
  (declare (xargs :guard (symbolp x)))
  (intern-in-package-of-symbol (concatenate 'string "?" (symbol-name x))
    x))
make-symbols-ignorablefunction
(defun make-symbols-ignorable
  (x)
  (declare (xargs :guard (symbol-listp x)))
  (if (atom x)
    nil
    (cons (make-symbol-ignorable (car x))
      (make-symbols-ignorable (cdr x)))))
returnspec-mv-nth-substfunction
(defun returnspec-mv-nth-subst
  (names idx call)
  (if (atom names)
    nil
    (cons (cons (car names) `(mv-nth ,STD::IDX ,STD::CALL))
      (returnspec-mv-nth-subst (cdr names)
        (1+ idx)
        call))))
returnspec-symbol-packagesfunction
(defun returnspec-symbol-packages
  (syms)
  (if (atom syms)
    nil
    (add-to-set-equal (symbol-package-name (car syms))
      (returnspec-symbol-packages (cdr syms)))))
returnspec-call-sym-pairsfunction
(defun returnspec-call-sym-pairs
  (packages call)
  (if (atom packages)
    nil
    (cons (cons (intern$ "<CALL>" (car packages)) call)
      (returnspec-call-sym-pairs (cdr packages)
        call))))
returnspec-return-value-substfunction
(defun returnspec-return-value-subst
  (name name-fn formals names)
  (declare (xargs :guard (and (symbolp name) (symbol-listp names))))
  (b* ((call (cons name-fn formals)) (both-subst `(("<CALL>" . ,STD::CALL) ("<FN>" . ,STD::NAME)
          ("<FN!>" . ,STD::NAME-FN)
          ("<VALUES>" . ,STD::NAMES)))
      ((when (eql (len names) 1)) (mv both-subst
          (cons (cons (car names) call) both-subst))))
    (mv both-subst
      (append both-subst
        (returnspec-mv-nth-subst names 0 call)))))
returnspec-thmsfunction
(defun returnspec-thms
  (name name-fn specs world)
  "Returns EVENTS"
  (declare (xargs :guard (and (symbolp name)
        (symbolp name-fn)
        (returnspeclist-p specs)
        (plist-worldp world))))
  (b* ((- (arity-check-returns name
         name-fn
         specs
         world)) ((unless specs) nil)
      (badname-okp t)
      (names (returnspeclist->names specs))
      (formals (look-up-formals name-fn world))
      (config (cdr (assoc 'returnspec-config
            (table-alist 'define world))))
      ((mv body-subst ruleclass-subst) (returnspec-return-value-subst name
          name-fn
          formals
          names))
      ((when (equal (len specs) 1)) (returnspec-single-thm name
          name-fn
          (car specs)
          body-subst
          ruleclass-subst
          badname-okp
          config
          world))
      (ignorable-names (make-symbols-ignorable names))
      (binds `((mv . ,STD::IGNORABLE-NAMES) (,STD::NAME-FN . ,STD::FORMALS))))
    (returnspec-multi-thms name
      name-fn
      binds
      specs
      body-subst
      ruleclass-subst
      badname-okp
      config
      world)))
keyval-list-to-kwd-alistfunction
(defun keyval-list-to-kwd-alist
  (args)
  (if (atom args)
    nil
    (cons (cons (first args) (second args))
      (keyval-list-to-kwd-alist (cddr args)))))
make-returnspec-configmacro
(defmacro make-returnspec-config
  (&rest args)
  (declare (xargs :guard (subsetp-eq (strip-cars (keyval-list-to-kwd-alist args))
        '(:hints-sub-returnnames))))
  `(local (table define
      'returnspec-config
      (keyval-list-to-kwd-alist ',STD::ARGS))))