		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-infer-domain

Infer the domain over which some applicability conditions must hold.

Signature
(tailrec-infer-domain combine q r variant$ verbose wrld) → domain
Arguments: combine — Guard (pseudo-termp combine).; q — Guard (symbolp q).; r — Guard (symbolp r).; variant$ — Guard (tailrec-variantp variant$).; verbose — Guard (booleanp verbose).; wrld — Guard (plist-worldp wrld).
Returns: domain — A pseudo-termfnp.

This is used when the :domain input is :auto. A domain is inferred as described in the documentation.

Definitions and Theorems

Function: tailrec-infer-domain

(defun tailrec-infer-domain (combine q r variant$ verbose wrld)
 (declare (xargs :guard (and (pseudo-termp combine)
                             (symbolp q)
                             (symbolp r)
                             (tailrec-variantp variant$)
                             (booleanp verbose)
                             (plist-worldp wrld))))
 (let ((__function__ 'tailrec-infer-domain))
   (declare (ignorable __function__))
   (b*
    ((default '(lambda (x) 't))
     (domain (if (member-eq variant$ '(:monoid :monoid-alt))
                 (case-match combine
                   ((op . args)
                    (b* (((unless (symbolp op)) default)
                         ((unless (or (equal args (list q r))
                                      (equal args (list r q))))
                          default)
                         ((list y1 y2) (formals op wrld))
                         (guard (uguard op wrld)))
                      (case-match guard
                        (('if (dom !y1) (dom !y2) *nil*)
                         (if (symbolp dom) dom default))
                        (('if (dom !y2) (dom !y1) *nil*)
                         (if (symbolp dom) dom default))
                        ((dom !y1)
                         (if (symbolp dom) dom default))
                        ((dom !y2)
                         (if (symbolp dom) dom default))
                        (& default))))
                   (& default))
               default))
     ((run-when verbose)
      (cw "~%")
      (cw "Inferred domain for the applicability conditions: ~x0.~%"
          domain)))
    domain)))