(in-package "PACO")

; Next we develop clausify, the function that reduces an IF-expression
; to a set of clauses.

; The basic idea here is to normalize the term and then walk the
; branches that terminate in non-T, accumulating literals.

; For example,
; (if p
;     (if q T r)
;   (if s NIL T))
; generates ((P (NOT S)) ((NOT P) Q R)) which is equivalent to
; (implies (not P) (not S))
; and
; (implies (and P (not Q)) R).

; The ACL2 version of clausify is complicated by the fact that it
; avoids IF-normalization.  It compiles the term into a program for a
; certain abstract machine and then explores all paths through the
; program.  This makes its space-behavior linear in the size of the
; term, whereas the Paco function is exponential.

(defun strip-branches (term clause clauses)

; Term is in IF-normal form.  All terminal literals are T, NIL, or
; function applications.  No branch terminating in NIL is
; contradictory.

  (cond ((variablep term)
         (cons (revappend (cons term clause) nil) clauses))
        ((fquotep term)
         (cond ((equal term *t*) clauses)
               (t (cons (revappend clause nil) clauses))))
        ((eq (ffn-symb term) 'IF)
         (let* ((test (fargn term 1))
                (clauses (strip-branches (fargn term 2)
                                         (cons (dumb-negate-lit test) clause)
                                         clauses)))
           (strip-branches (fargn term 3)
                           (cons test clause)
                           clauses)))
        (t (cons (revappend (cons term clause) nil) clauses))))

(defun clausify (term ens wrld)
  (strip-branches (normalize term t nil ens wrld) nil nil))
    
(defun if-tautologyp (term ens wrld)

; The main application of this function is to determine whether a
; rewritten hypothesis is a tautology.  For that reason, we do not
; expand non-rec fns in term.  Thus, we do not recognize certain
; common tautologies, like (IF P 'T (NOT P)), while we would if we
; expanded the NOT.

  (equal (normalize term t nil ens wrld) *t*))

(mutual-recursion

(defun expand-some-non-rec-fns (fns term wrld)
  (cond ((variablep term) term)
        ((fquotep term) term)
        (t (let ((args (expand-some-non-rec-fns-lst fns (fargs term) wrld)))
             (cond ((member-equal (ffn-symb term) fns)
                    (subcor-var (formals (ffn-symb term) wrld)
                                args
                                (body (ffn-symb term) t wrld)))
                   (t (cons-term (ffn-symb term) args)))))))

(defun expand-some-non-rec-fns-lst (fns lst wrld)
  (cond ((endp lst) nil)
        (t (cons (expand-some-non-rec-fns fns (car lst) wrld)
                 (expand-some-non-rec-fns-lst fns (cdr lst) wrld)))))

)

; We now begin the development of the rewriter itself.

(defun smallest-term (term terms)

; Return the smallest term in (cons term terms), under term-order.

  (cond ((endp terms) term)
        ((term-order (car terms) term) (smallest-term (car terms) (cdr terms)))
        (t (smallest-term term (cdr terms)))))

(defun find-smallest-equal-term (term type-alist eterms)
  (cond
   ((endp type-alist)
    (smallest-term term eterms))
   ((and (ts= (cdr (car type-alist)) *ts-t*)
         (nvariablep (car (car type-alist)))
         (eq (ffn-symb (car (car type-alist))) 'EQUAL))
    (let ((arg1 (fargn (car (car type-alist)) 1))
          (arg2 (fargn (car (car type-alist)) 2)))
      (cond
       ((equal term arg1)
        (find-smallest-equal-term term (cdr type-alist) (cons arg2 eterms)))
       ((equal term arg2)
        (find-smallest-equal-term term (cdr type-alist) (cons arg1 eterms)))
       ((member-equal arg1 eterms)
        (find-smallest-equal-term term (cdr type-alist) (cons arg2 eterms)))
       ((member-equal arg2 eterms)
        (find-smallest-equal-term term (cdr type-alist) (cons arg1 eterms)))
       (t (find-smallest-equal-term term (cdr type-alist) eterms)))))
   (t (find-smallest-equal-term term (cdr type-alist) eterms))))

(defun rewrite-solidify (term type-alist iff-flg ens wrld)

; We simplify term wrt type-alist.  In particular, if term is known to
; be in a singleton type-set, we return the corresponding constant
; (reduced mod iff-flg).  In addition, if term is equated to a series
; of other terms, we return the smallest (in term-order).  The
; type-set for all the equivalent terms should be the same.

  (cond
   ((quotep term)
    (cond ((equal term *nil*) *nil*)
          (iff-flg *t*)
          (t term)))
   (t (let ((ts (type-set term type-alist nil ens wrld *type-set-nnn*)))
        (cond
         ((ts= ts *ts-t*) *t*)
         ((ts= ts *ts-nil*) *nil*)
         ((and iff-flg (not (ts-intersectp ts *ts-nil*))) *t*)
         ((ts= ts *ts-zero*) *0*)
         (t (find-smallest-equal-term term type-alist nil)))))))

(defun loop-stopperp-rec (loop-stopper unify-subst)

; Only call this at the top level when loop-stopper is non-nil.

  (cond
   ((endp loop-stopper) nil)
   (t
    (let ((pre (cdr (assoc-eq (car (car loop-stopper)) unify-subst)))
          (post (cdr (assoc-eq (cadr (car loop-stopper)) unify-subst))))
      (cond
       ((equal pre post)
        (loop-stopperp-rec (cdr loop-stopper) unify-subst))
       (t (term-order post pre)))))))

(defun loop-stopperp (loop-stopper unify-subst)
  (or (null loop-stopper)
      (loop-stopperp-rec loop-stopper unify-subst)))

(defrec rewrite-rule ((nume . hyps)
                      (equiv lhs . rhs)
                      subclass . heuristic-info))

; Hyps is a list of terms, equiv is EQUAL or IFF, lhs and rhs are
; terms.  The presence of such a rule means (implies hyps (equiv lhs
; rhs)) is a theorem.  Subclass is either:

; 'backchain - the traditional rewrite rule.  In this case, :heuristic-info is
;   the loop-stopper for the rule: a list of elements of the form (x . y),
;   indicating that in replacing lhs by rhs (the binding of) y moves forward to
;   the spot occupied by (the binding of) x, and that x and y only appear on
;   the left-hand side as arguments to functions in fns.  Thus, to prevent
;   loops we adopt the heuristic convention of replacing lhs by rhs only if
;   there exists a pair (x . y) such that the binding of y is smaller than
;   that of x and all earlier pairs have equal bindings.

; 'definition - a rule implementing a non-abbreviational definitional
;   equation.  In this case :heuristic-info is the pair (recursivep
;   . controller-alists) where recursivep is nil (if this is a nonrec
;   definition) or a truelist of symbols naming all the fns in the
;   ``clique'' (singly recursive functions have a singleton list as
;   their recursivep property); and controller-alists is a non-empty
;   list of alists, each pairing each fn named in recursivep to a mask
;   of t's and nil's in 1:1 correspondence with the formals of the fn
;   and indicating with t's which arguments control the recursion for
;   this definition.

; 'meta - a rule justified by a metatheorem.  In this case, the lhs is
;   the the metafunction symbol to be applied and hyps is the
;   metafunction symbol to generate the hyps.  If the rhs is the
;   symbol 'extended then both metafunctions are extended and take two
;   arguments, the target term and the mfc.  Otherwise, they just take
;   one argument.

; This layout is unoptimized.

(defrec rewrite-constant
  ((expand-lst . terms-to-be-ignored-by-rewrite)
   (top-clause . current-clause)
   (ens . current-literal)
   . fns-to-be-ignored))

; The expand-lst and the terms-to-be-ignored-by-rewrite have dual uses
; in ACL2.  They are used by induct to communicate to rewrite and they
; are used to implement parts of the user-supplied hint mechanism.  In
; Paco, they only see the use by induct.

; The current-literal is a record, not a literal.  Its not-flg and atm
; are always used together so we bundle them so we can extract them
; both at once.

(defrec current-literal (not-flg . atm))

; We here implement the check that the term we are about to rewrite is
; not a member of :terms-to-be-ignored-by-rewrite.  The trouble is,
; the ``term we are about to rewrite'' is represented by a term and a
; substitution alist.  We do not want to create the instantiation.  So
; we first need the concept of whether a term is equal to another term
; mod a substitution.

(mutual-recursion

(defun equal-mod-alist (term1 alist1 term2)

; We determine whether (sublis-var alist1 term1) is equal to term2.
; We just chase vars in term1 and use equal at the tips.  There is
; one subtlety.  Consider 

; (equal-mod-alist '(foo x z (cons x y))
;                  '((x . '1) (y . '2))
;                  '(foo '1 z '(1 . 2)))

; The idea is that if term2 is a quoted constant and term1 is some
; function application, then it is possible that the sublis-var will
; convert term1 to a quoted constant.  We know that only happens if
; the top-most function symbol in term1 is a primitive, so we check
; that and do the sublis-var if we have to.  But it only happens on
; the ``tips.''

  (cond ((variablep term1)
         (let ((temp (assoc-eq term1 alist1)))
           (cond (temp (equal (cdr temp) term2))
                 (t (equal term1 term2)))))
        ((fquotep term1)
         (equal term1 term2))
        ((variablep term2) nil)
        ((fquotep term2)
         (cond ((cons-term-primitivep (ffn-symb term1))
                (equal term2 (sublis-var alist1 term1)))
               (t nil)))
        ((equal (ffn-symb term1) (ffn-symb term2)) ; may be lambdas.
         (equal-mod-alist-lst (fargs term1) alist1 (fargs term2)))
        (t nil)))

(defun equal-mod-alist-lst (term1-lst alist1 term2-lst)
  (cond
   ((endp term1-lst) t)
   (t (and (equal-mod-alist (car term1-lst) alist1 (car term2-lst))
           (equal-mod-alist-lst (cdr term1-lst) alist1 (cdr term2-lst))))))
)

(defun member-equal-mod-alist (term1 alist1 term2-lst)

; Is (sublis-var alist1 term1) a member-equal of term2-lst?

  (cond ((endp term2-lst) nil)
        ((equal-mod-alist term1 alist1 (car term2-lst))
         t)
        (t (member-equal-mod-alist term1 alist1 (cdr term2-lst)))))

(defun not-to-be-rewrittenp1 (fn lst)

; This function determines whether fn is the ffn-symb of any term on
; lst.  We assume lst is a true list of non-variablep non-quotep
; terms.

  (cond ((endp lst)
         nil)
        ((equal fn (ffn-symb (car lst))) ; Both may be LAMBDAs.
         t)
        (t (not-to-be-rewrittenp1 fn (cdr lst)))))

(defun not-to-be-rewrittenp (term alist terms-to-be-ignored-by-rewrite)

; We assume term is a nonvariable non-quotep and that
; terms-to-be-ignored-by-rewrite contains no vars or quoteps.  Let
; term' be (sublis-var alist term).  If term' is a member of
; terms-to-be-ignored-by-rewrite we return term' else nil.  We have
; a faster preliminary check, namely, whether terms-to-be-ignored-
; by-rewrite contains any terms with the same top-level function
; symbol as term.

  (cond ((not-to-be-rewrittenp1 (ffn-symb term)
                                terms-to-be-ignored-by-rewrite)
         (member-equal-mod-alist term alist
                                 terms-to-be-ignored-by-rewrite))
        (t nil)))

(defrec metafunction-context
  (type-alist obj iff-flg wrld fnstack ancestors rcnst))

(defun ev-synp (synp-term unify-subst mfc wrld)

; Synp-term is the quotation of the term to be evaluated.  Unify-subst is the
; unifying substitution presently in force, and mfc is the meta-level context
; (formerly referred to as "metafunction-context").

  (let* ((unify-subst1 (if mfc
                           (cons (cons 'mfc mfc)
                                 unify-subst)
                         unify-subst)))
    (eval (cadr synp-term) unify-subst1 wrld)))

(defun tautologyp (term ens wrld)

; If this function returns t, then term is a theorem.  This function
; can be made as fancy as you want, as long as it recognizes theorems.

  (let ((fns '(if iff not implies eq atom eql = /= null zerop synp plusp
                  minusp listp prog2$ force case-split)))

; Note that fns contains IF as its first element.  If term mentions
; none of these functions, there is no point in doing expansion or
; if-distribution.  We just reduce to catch the trivial cases like
; (consp (cons x y)).  But if term does contain any of these
; functions, we expand all of them (cdring past the undefined IF on
; the front).

    (if (ffnnamesp fns term)
        (if-tautologyp
         (expand-some-non-rec-fns (cdr fns) term wrld)
         ens
         wrld)
      (equal (reduce term t nil ens wrld t)
             *t*))))

(defun refinementp (equiv iff-flg)

; We determine whether equiv is a refinment of the equivalence relation
; indicated by iff-flg, where nil means EQUAL and t means IFF.

  (if iff-flg
      (or (eq equiv 'equal) (eq equiv 'iff))
    (eq equiv 'equal)))

(defun being-openedp-rec (fn fnstack)

; The fnstack used by the rewriter is a list.  Each element is a
; function symbol, a list of function symbols, or of the form (:term
; . term) for some term, term.  The first case means we are expanding
; a definition of that symbol and the symbol is non-recursively
; defined.  The second means we are expanding a singly or mutually
; recursive function.  (In fact, the fnstack element is the recursivep
; flag of the function we're expanding.)  The third means that we are
; rewriting the indicated term (through the recursive dive in the
; rewriter that rewrites the just-rewritten term).  Lambda-expressions
; are not pushed onto the fnstack, though fn may be a
; lambda-expression.  We determine whether fn is on fnstack (including
; being a member of a mutually recursive clique).

  (cond ((endp fnstack) nil)
        ((consp (car fnstack))
         (or (eq fn (caar fnstack)) ; and hence (not (eq (caar fnstack) :term))
             (being-openedp-rec fn (cdr fnstack))))
        (t (or (eq fn (car fnstack))
               (being-openedp-rec fn (cdr fnstack))))))

(defmacro being-openedp (fn fnstack clique)

; We found a 1.8% slowdown when we modified the code, in a preliminary cut at
; v2-7, to improve the speed of being-openedp when large cliques are on the
; fnstack by looking up the representative of fn on the fnstack, rather than
; looking up fn itself.  Presumably that slowdown resulted from the new calls
; to getprop to get the 'recursivep property.  Here we avoid computing that
; getprop (in the case that clique is a getprop expression) in a case we
; suspect is pretty common:  fnstack is empty.  The fnstack argument will
; always be a symbolp expression, so we do not need to let-bind it below.

  (declare (xargs :guard (symbolp fnstack)))
  `(and ,fnstack
        (let ((clique ,clique))
          (being-openedp-rec (if clique
                                 (car clique)
                               ,fn)
                             ,fnstack))))

(defun recursive-fn-on-fnstackp (fnstack)

; We return t iff there is an element of fnstack that is recursively
; defined.  We assume that any mutually recursive clique on the stack
; is truly indicative of mutual recursion.  See the description of the
; fnstack in being-openedp.

  (cond ((endp fnstack) nil)
        ((and (consp (car fnstack))
              (not (eq (caar fnstack) :term)))
         t)
        (t (recursive-fn-on-fnstackp (cdr fnstack)))))

(defun some-fnstack-term-dumb-occur (fnstack term)
  (cond ((endp fnstack) nil)
        ((and (consp (car fnstack))
              (eq (caar fnstack) :term)
              (dumb-occur (cdar fnstack) term))
         t)
        (t (some-fnstack-term-dumb-occur (cdr fnstack) term))))

(mutual-recursion

(defun occur-cnt-rec (term1 term2 acc)

; Return a lower bound on the number of times term1 occurs in term2.
; We do not go inside of quotes.

  (cond ((equal term1 term2) (1+ acc))
        ((variablep term2) acc)
        ((fquotep term2) acc)
        (t (occur-cnt-lst term1 (fargs term2) acc))))

(defun occur-cnt-lst (term1 lst acc)
  (cond ((endp lst) acc)
        (t (occur-cnt-rec term1
                          (car lst)
                          (occur-cnt-lst term1 (cdr lst) acc)))))
)

(defun occur-cnt (term1 term2)
  (occur-cnt-rec term1 term2 0))

(mutual-recursion

(defun count-ifs (term)
  (cond ((variablep term) 0)
        ((fquotep term) 0)
        ((eq (ffn-symb term) 'if)
         (+ 1
            (count-ifs (fargn term 1))
            (count-ifs (fargn term 2))
            (count-ifs (fargn term 3))))
        (t (count-ifs-lst (fargs term)))))

(defun count-ifs-lst (lst)
  (cond ((endp lst) 0)
        (t (+ (count-ifs (car lst))
              (count-ifs-lst (cdr lst))))))

)

(defun too-many-ifs1 (args val lhs rhs)
  (cond
   ((endp args) nil)
   (t (let ((x (count-ifs (car args))))
        (cond ((int= x 0)
               (too-many-ifs1 (cdr args) val lhs rhs))
              (t (let ((lhs (+ lhs (* x (occur-cnt (car args) val)))))
                   (cond ((> lhs rhs) t)
                         (t (too-many-ifs1 (cdr args) val lhs rhs))))))))))

(defun too-many-ifs (args val)

; Let args be the list of actuals to a nonrec fn.  Let val be the
; rewritten body.  We wish to determine whether the expansion of the
; fn call introduces too many IFs all at once.  Our motivation comes
; from an example like (M2 (ZTAK & & &) (ZTAK & & &) (ZTAK & & &))
; where the careless opening up of everybody produces a formula with
; several hundred IFs in it because of M2's duplication of the IFs
; coming from the simplification of the ZTAKs.  My first thought was
; to never expand a nonrec fn -- at the top level of the clause -- if
; it had some IFs in its args and to wait till CLAUSIFY has cleaned
; things up.  That slowed a proveall down by a factor of 2 -- and by a
; factor of 13 in PRIME-LIST-TIMES-LIST -- because of the ridiculously
; slow expansion of such basic nonrec fns as AND, OR, NOT, and NLISTP.

; This function computes:

; (> (ITERATE FOR ARG IN ARGS SUM (* (COUNT-IFS ARG) (OCCUR-CNT ARG VAL)))
;    (ITERATE FOR ARG IN ARGS SUM (COUNT-IFS ARG)))

; but does it slightly more efficiently by observing that if no IFs
; occur in any arg then there is no point in doing the OCCUR-CNTs and
; that once the left hand side has been pushed beyond the right there
; is no point in continuing.

  (let ((rhs (count-ifs-lst args)))
    (cond ((int= rhs 0) nil)
          (t (too-many-ifs1 args val 0 rhs)))))

(defun all-args-occur-in-top-clausep (args top-clause)
  (cond ((endp args) t)
        (t (and (dumb-occur-lst (car args) top-clause)
                (all-args-occur-in-top-clausep (cdr args) top-clause)))))

(defun cons-count-ac (x i)
  (cond ((atom x) i)
        (t (cons-count-ac (cdr x) (cons-count-ac (car x) (1+ i))))))

(defun cons-count (x)
  (cons-count-ac x 0))

(mutual-recursion

(defun max-form-count (term)

; This function is used in the control of recursive fn expansion.
; Many years ago, we used the fn count part of var-fn-count in this
; role.  Then we decided that for controlling expansion we should not
; count (IF x y z) to have size 1+|x|+|y|+|z| because the IF will be
; distributed and the y or the z will rest in the argument position of
; the recursive call.  So we started to compute the maximum fn count
; in the branches.  Then we added explicit values (this really was
; years ago!) and decided not to consider 1000 to be better than 999,
; since otherwise (< x 1000) would open.  So we measure quoted
; constants by their Lisp size.

  (cond ((variablep term) 0)
        ((fquotep term) (cons-count (cadr term)))
        ((eq (ffn-symb term) 'if)
         (max (max-form-count (fargn term 2))
              (max-form-count (fargn term 3))))
        (t (1+ (max-form-count-lst (fargs term))))))

(defun max-form-count-lst (lst)
  (cond ((endp lst) 0)
        (t (+ (max-form-count (car lst))
              (max-form-count-lst (cdr lst))))))

)

(defun controller-complexity1 (flg args controller-pocket)

; Flg is either t (meaning we measure the controllers) or nil
; (meaning we measure the non-controllers).  Args is the arg list
; to a call of a fn with the given controller pocket.

; In this implementation a controller pocket is a list of
; Booleans in 1:1 correspondence with the formals.  A t in an
; argument position indicates that the formal is a controller.

; We sum the max-form-counts of the arguments in controller (or
; non-controller, according to flg) positions.

  (cond ((endp args) 0)
        ((eq (car controller-pocket) flg)
         (+ (max-form-count (car args))
            (controller-complexity1 flg
                                    (cdr args)
                                    (cdr controller-pocket))))
        (t (controller-complexity1 flg
                                   (cdr args)
                                   (cdr controller-pocket)))))

(defun controller-complexity (flg term controller-alist)

; Term is a call of some recursive fn in a mutually recursive clique.
; Controller-alist is an alist that assigns to each fn in the clique a
; controller-pocket.  We compute the controller complexity (or
; non-controller complexity, according to flg being t or nil) of term
; for the controller pocket assigned fn in the alist.

  (controller-complexity1 flg
                          (fargs term)
                          (cdr (assoc-eq (ffn-symb term)
                                         controller-alist))))

(defun some-controller-pocket-simplerp
  (call result controller-alists)

; Call has rewritten to something involving result.  Both call and
; result are applications of functions in the same mutually recursive
; clique.

; Controller-alists is a list of alists.  Each alist associates a fn
; in the clique to a controller pocket.  A controller pocket is a list
; in 1:1 correspondence with the formals of the fn with a t in those
; slots that are controllers and a nil in the others.  Thus, each
; alist assigns a complexity to both call and to result.

; We determine whether there exists an alist in controller-alists that
; assigns a lower complexity to result than to call.

  (cond ((endp controller-alists) nil)
        ((< (controller-complexity t result (car controller-alists))
            (controller-complexity t call (car controller-alists)))
         t)
        (t (some-controller-pocket-simplerp call
                                            result
                                            (cdr controller-alists)))))

(defun constant-controller-pocketp1 (args controller-pocket)
  (cond ((endp args) t)
        ((car controller-pocket)
         (and (quotep (car args))
              (constant-controller-pocketp1 (cdr args)
                                            (cdr controller-pocket))))
        (t (constant-controller-pocketp1 (cdr args)
                                         (cdr controller-pocket)))))

(defun constant-controller-pocketp (term controller-alist)

; Term is a call of some fn in the clique for which controller-alist is
; a controller alist.  That alist assigns a controller-pocket to fn.
; We determine whether the controller arguments to fn in term are all
; quoted.

  (constant-controller-pocketp1 (fargs term)
                                (cdr (assoc-eq (ffn-symb term)
                                               controller-alist))))

(defun some-controller-pocket-constant-and-non-controller-simplerp
  (call result controller-alists)

; Call and result are both applications of functions in the same
; mutually recursive clique.  Controller-alists is a list of alists.
; Each alist assigns to each fn in the clique a controller pocket.
; We determine whether some alist in controller-alists assigns
; controllers in such a way that the controllers of result are
; constant and the complexity of the non-controllers in result
; is less than that of the non-controllers in call.

  (cond ((endp controller-alists) nil)
        ((and (constant-controller-pocketp result (car controller-alists))
              (< (controller-complexity nil result (car controller-alists))
                 (controller-complexity nil call (car controller-alists))))
         t)
        (t (some-controller-pocket-constant-and-non-controller-simplerp
            call result (cdr controller-alists)))))

(mutual-recursion

(defun rewrite-fncallp (call result cliquep top-clause current-clause
                             controller-alists)

; Call has rewritten to (some term involving) result.  We want to know
; if we should replace call by result or leave the call unopened.  The
; ffn-symb of call is known to be a recursive function symbol, fn.  It
; is not a lambda-expression.  Cliquep is nil if fn is singly
; recursive and is the list of functions in fn's clique if it is
; mutually recursive.  Top-clause and current-clause are two clauses
; from simplify-clause0 (the input clause there and the result of
; removing trivial equations).  Controller-alists is the
; 'controller-alists property of fn.

; The controller-alists property of fn is a list of alists.  Each
; alist pairs every function in fn's mutually recursive clique with a
; controller pocket.  Thus, if fn is singly recursive,
; controller-alists looks like this:
; (((fn . controller-pocket1))...((fn . controller-pocketk))).
; But if fn is mutually recursive with clique fn1...fnm, then each
; alist assigns a controller pocket to each fni.

  (cond
   ((variablep result) t)
   ((fquotep result) t)
   ((flambda-applicationp result)

; This should not normally happen.  The only time we refuse to open a
; lambda-application is (a) we are at the top level of the clause and
; it has too many ifs, or (b) we were told not to open it by the user.
; But (a) can't have happened while we were constructing result
; because we were opening up a recursive fn.  Of course, the worry is
; that the body of this lambda-expression contains a recursive call
; that will somehow get loose and we will indefinitely recur.  But if
; the only way we get here is via case (b) above, we won't ever open
; this lambda and so we're safe.  We therefore act as though this
; lambda were just some ordinary function symbol.

    (rewrite-fncallp-listp call (fargs result)
                           cliquep
                           top-clause
                           current-clause
                           controller-alists))
   ((if cliquep
        (member-eq (ffn-symb result) cliquep)
      (eq (ffn-symb result) (ffn-symb call)))
    (and (or (all-args-occur-in-top-clausep (fargs result)
                                            top-clause)
             (dumb-occur-lst result current-clause)
             (some-controller-pocket-simplerp
              call
              result
              controller-alists)
             (some-controller-pocket-constant-and-non-controller-simplerp
              call
              result
              controller-alists))
         (rewrite-fncallp-listp call (fargs result)
                                cliquep
                                top-clause
                                current-clause
                                controller-alists)))
   (t (rewrite-fncallp-listp call (fargs result)
                             cliquep
                             top-clause
                             current-clause
                             controller-alists))))

(defun rewrite-fncallp-listp (call lst cliquep top-clause current-clause
                                   controller-alists)
  (cond ((endp lst) t)
        (t (and (rewrite-fncallp call (car lst)
                                 cliquep
                                 top-clause
                                 current-clause
                                 controller-alists)
                (rewrite-fncallp-listp call (cdr lst)
                                       cliquep
                                       top-clause
                                       current-clause
                                       controller-alists)))))

)

(mutual-recursion

(defun contains-rewriteable-callp
  (fn term cliquep terms-to-be-ignored-by-rewrite)

; This function scans the non-quote part of term and determines
; whether it contains a call, t, of any fn in the mutually recursive
; clique of fn, such that t is not on terms-to-be-ignored-by-rewrite.
; Fn is known to be a symbol, not a lambda-expression.  If cliquep is
; nil, fn is singly recursive.  Otherwise, cliquep is the list of
; functions in the clique (including fn).

  (cond ((variablep term) nil)
        ((fquotep term) nil)
        ((flambda-applicationp term)

; If term is a lambda-application then we know that it contains no recursive
; calls of fns in the clique, as described in the comment on the subject
; in rewrite-fncallp above.

         (contains-rewriteable-callp-lst fn (fargs term)
                                         cliquep
                                         terms-to-be-ignored-by-rewrite))
        ((and (if cliquep
                  (member-eq (ffn-symb term) cliquep)
                (eq (ffn-symb term) fn))
              (not (member-equal term terms-to-be-ignored-by-rewrite)))
         t)
        (t (contains-rewriteable-callp-lst fn (fargs term)
                                           cliquep
                                           terms-to-be-ignored-by-rewrite))))

(defun contains-rewriteable-callp-lst
  (fn lst cliquep terms-to-be-ignored-by-rewrite)
  (cond ((endp lst) nil)
        (t (or (contains-rewriteable-callp fn (car lst)
                                           cliquep
                                           terms-to-be-ignored-by-rewrite)
               (contains-rewriteable-callp-lst
                fn (cdr lst)
                cliquep
                terms-to-be-ignored-by-rewrite)))))

)

(defun free-p (x)
  (and (consp x) (eq (car x) :free)))

(defun expand-permission-p (term expand-lst)

; This is a generalized version of member-equal that asks whether
; expand-lst gives term permission to be expanded.  Here, term is a
; function application.

  (if (endp expand-lst)
      nil
      (or (let ((x (car expand-lst)))
            (or (and (eq x :LAMBDAS)
                     (flambda-applicationp term))
                (if (free-p x)
                    (mv-let (flg sbst)
                            (one-way-unify1 (caddr x) term (cadr x))
                            (declare (ignore sbst))
                            flg)
                  (equal x term))))
          (expand-permission-p term (cdr expand-lst)))))

; There are many discrepancies between Paco's rewriter and ACL2's.
; The most important is that Paco does not support linear arithmetic.
; Another major omission is that Paco does not support equivalence or
; congruence relations.  Paco does not support enabling or disabling
; of runes -- indeed, it has no concept of rune or of an enabled
; structure.  In addition, Paco does not support HIDE, FORCE,
; CASE-SPLIT, BIND-FREE or the search for multiple instantiations of
; free vars.  HIDE would not be difficult to add but seemed to be too
; minor to warrant the complexity.  FORCE and CASE-SPLIT require the
; presence of ttrees or other dependency tracking to implement.
; BIND-FREE seemed too complicated for the first pass.  However, Paco
; does support SYNTAXP and metafunctions, which require some of the
; same basic machinery as BIND-FREE.


; Essay on Rewrite Entry and the Extra Arguments

; The next major concern is the fact that rewrite and its peers in the
; rewrite clique take so many arguments.  Each function in the clique
; takes some arguments specific to itself and some other ``extra''
; arguments shared by every other function in the clique.  Most often,
; when functions in the clique call other functions, the extra
; arguments are passed as is, e.g., type-alist and wrld.  We make a
; convenient macro, (rewrite-entry term :key1 val1 ...) that extends
; term by passing all the extra args as is, except for the ones indicated
; by keywords.

; The extra arguments are
#|

 ; &extra formals
 type-alist obj iff-flg wrld fnstack ancestors rcnst nnn

|#

; Important Note:  The string "&extra formals" is included where ever
; this list has been copied.

; Convention: Not every function uses all 7 of the extra formals.
; Ignored formals are so declared and we pass nil into such a slot
; (to be consistent while avoiding the appearance of using the old value).

(defun plist-to-alist (lst)

; Convert '(key1 val1 key2 val2 ...) to '((key1 . val1) (key2 . val2) ...).
; In use here, the keys are all in the keyword package.

  (cond ((endp lst) nil)
        (t (cons (cons (car lst) (cadr lst))
                 (plist-to-alist (cddr lst))))))

(defun add-rewrite-args (extra-formals keyword-extra-formals alist)

; extra-formals is '(type-alist ...)
; keyword-extra-formals is '(:type-alist ...)
; alist pairs keyword extra formals and terms

; We return a list in 1:1 correspondence with extra-formals.  The
; element corresponding to an extra-formal is the value specified by
; the alist if one is so specified, otherwise it is the extra-formal
; itself.

  (cond ((endp extra-formals) nil)
        (t (cons (let ((pair (assoc-eq (car keyword-extra-formals)
                                       alist)))
                   (cond (pair (cdr pair))
                         (t (car extra-formals))))
                 (add-rewrite-args (cdr extra-formals)
                                   (cdr keyword-extra-formals)
                                   alist)))))

(defmacro rewrite-entry (&rest args)
  (declare (xargs :guard (and (true-listp args)
                              (keyword-value-listp (cdr args)))))
  (append (car args)
          (add-rewrite-args '( ; &extra formals
                              type-alist obj iff-flg wrld fnstack
                              ancestors rcnst nnn)
                            '( ; &extra formals -- keyword versions
                              :type-alist :obj :iff-flg :wrld :fnstack
                              :ancestors :rcnst :nnn)
                            (plist-to-alist (cdr args)))))


; Theorems used to speed up the admission of the rewrite clique.

(defthm rewrite-clique-speedup-26
  (implies
   (not (zp nnn))
   (e0-ord-<
    (cons (cons (cons (+ 1 (nfix (+ -1 nnn))) 6)
                (acl2-count (mv-nth 1
                                    (let nil
                                      (cond ((atom term) (list nil term))
                                            ((equal 'quote (car term))
                                             (list nil term))
                                            ((equal (car term) 'not)
                                             (list 'not (cadr term)))
                                            ((and (equal (car term) 'if)
                                                  (equal (caddr term) ''nil)
                                                  (equal (cadddr term) ''t))
                                             (list 'if (cadr term)))
                                            (t (list nil term)))))))
          0)
    (cons (cons (cons (+ 1 (nfix nnn)) 0) 0)
          0))))

(defthm rewrite-clique-speedup-5
  (implies
   (not (zp nnn))
   (e0-ord-<
    (cons
     (cons
      (cons (+ 1 (nfix nnn)) 1)
      any)
     0)
    (cons (cons (cons (+ 1 (nfix nnn)) 4) 0)
          0)))
  :rule-classes nil)

(defthm rewrite-clique-speedup-4
  (implies
   (not (zp nnn))
   (e0-ord-<
    (cons
     (cons
      (cons (+ 1 (nfix (+ -1 nnn))) 6)
      any)
     0)
    (cons (cons (cons (+ 1 (nfix nnn)) 4) 0)
          0)))
  :rule-classes nil)

; The rewrite clique:

(ACL2::SET-WELL-FOUNDED-RELATION e0-ord-<)

(mutual-recursion

(defun rewrite (term alist
                ; &extra formals
                type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

  (declare (xargs :measure (lex4 (nfix nnn) 6 (acl2-count term) 0)
                  :hints (("Goal"
                           :in-theory
                           (disable assume-true-false
                                    type-set))
                          ("Subgoal 26" :do-not '(preprocess)
                           :by rewrite-clique-speedup-26)
                          ("Subgoal 17" :do-not '(preprocess)
                           :by rewrite-clique-speedup-5)
                          ("Subgoal 16" :do-not '(preprocess)
                           :by rewrite-clique-speedup-4)
;                         ("Subgoal 5" :do-not '(preprocess)
;                          :by rewrite-clique-speedup-5)
;                         ("Subgoal 4" :do-not '(preprocess)
;                          :by rewrite-clique-speedup-4)
                          )))

  (cond ((zp nnn) (sublis-var alist term))
        ((variablep term)
         (rewrite-solidify (sublis-var alist term)
                           type-alist iff-flg
                           (access rewrite-constant rcnst :ens) wrld))
        ((fquotep term)
         (if iff-flg
             (if (equal term *nil*) *nil* *t*)
           term))
        ((eq (ffn-symb term) 'if)

; We handle (if x y y) as a special case since it allows us to avoid
; rewriting x.

         (cond
          ((equal (fargn term 2) (fargn term 3))
           (rewrite-entry
            (rewrite (fargn term 2) alist)))
          (t
           (let ((rewritten-test
                  (rewrite-entry
                   (rewrite (fargn term 1) alist)
                   :obj
                   (case obj
                     ((t)
                      (cond ((equal (fargn term 2) *nil*)
                             nil)
                            ((equal (fargn term 3) *nil*)
                             t)
                            (t '?)))
                     ((nil)
                      (cond ((equal (fargn term 2) *t*)
                             nil)
                            ((equal (fargn term 3) *t*)
                             t)
                            (t '?)))
                     (t '?))
                   :iff-flg t)))
             (rewrite-entry
              (rewrite-if rewritten-test
                          (fargn term 1)
                          (fargn term 2)
                          (fargn term 3)
                          alist))))))
        ((eq (ffn-symb term) 'IMPLIES)

; We handle IMPLIES specially.  We rewrite both the hyps and the concl
; under the original type-alist, and then immediately return the
; resulting expansion of the body of IMPLIES.  This prevents the concl
; from being rewritten under the (presumably) more powerful type-alist
; gotten from assuming the hyps true until after any normalization has
; occurred.

         (subcor-var (formals 'IMPLIES wrld)
                     (list (rewrite-entry (rewrite (fargn term 1) alist)
                                          :obj '?
                                          :iff-flg t)
                           (rewrite-entry (rewrite (fargn term 2) alist)
                                          :obj '?
                                          :iff-flg t))
                     (body 'IMPLIES t wrld)))
        ((not-to-be-rewrittenp term alist
                               (access rewrite-constant
                                       rcnst
                                       :terms-to-be-ignored-by-rewrite))
         (rewrite-solidify (sublis-var alist term)
                           type-alist iff-flg
                           (access rewrite-constant rcnst :ens)
                           wrld))
        (t
         (let ((fn (ffn-symb term))
               (rewritten-args (rewrite-entry (rewrite-args (fargs term) alist)
                                :obj '?
                                :iff-flg nil)))
           (cond
            ((and (all-quoteps rewritten-args)
                  (enabled-numep (fn-nume :EXECUTABLE-COUNTERPART fn wrld)
                                 (access rewrite-constant rcnst :ens)))
             (mv-let (erp val)
                     (apply fn
                            (strip-cadrs rewritten-args)
                            wrld)
                     (cond (erp (cons-term fn rewritten-args))
                           (t
                            (<rewrite-id>
                             (kwote val))))))
            (t
             (rewrite-entry
              (rewrite-with-lemmas
               (rewrite-entry
                (rewrite-primitive fn rewritten-args)
                :nnn (- nnn 1))))))))))

(defun rewrite-if (test unrewritten-test left right alist
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

  (declare (xargs :measure (lex4 (nfix nnn)
                                 6
                                 (+ 1
                                    (acl2-count unrewritten-test)
                                    (acl2-count left)
                                    (acl2-count right))
                                 (acl2-count test))))

; Test is the result of rewriting unrewritten-test under the same alist and
; extra formals.  Except, unrewritten-test can be nil, in which case we of
; course make no such claim.

  (cond
   ((zp nnn)
    (fcons-term* 'if
                 test
                 (sublis-var alist left)
                 (sublis-var alist right)))
   ((and (nvariablep test)
         (not (fquotep test))
         (eq (ffn-symb test) 'if)
         (equal (fargn test 2) *nil*)
         (equal (fargn test 3) *t*))
    (rewrite-entry (rewrite-if (fargn test 1) nil right left alist)))
   ((quotep test)

; It often happens that the test rewrites to *t* or *nil* and we can
; avoid the assume-true-false below.

    (if (cadr test)
        (if (and unrewritten-test ; optimization (see e.g. rewrite-if above)
                 iff-flg
                 (equal unrewritten-test left))

; We are in the process of rewriting a term of the form (if x x y), which
; presumably came from an untranslated term of the form (or x y).  We do not
; want to rewrite x more than once if we can get away with it.  We are using
; the fact that the following is a theorem:  (iff (if x x y) (if x t y)).
; We will use this observation later in the body of this function as well.

            *t*
          (rewrite-entry (rewrite left alist)))
      (rewrite-entry (rewrite right alist))))
   (t (mv-let
       (must-be-true must-be-false true-type-alist false-type-alist)
       (assume-true-false test type-alist nil
                          (access rewrite-constant rcnst :ens)
                          wrld *type-set-nnn*)
       (cond
        (must-be-true
         (if (and unrewritten-test
                  iff-flg
                  (equal unrewritten-test left))
             *t*
           (rewrite-entry (rewrite left alist)
                          :type-alist true-type-alist)))
        (must-be-false
         (rewrite-entry (rewrite right alist)
                        :type-alist false-type-alist))
        (t (let ((rewritten-left
                  (if (and unrewritten-test
                           iff-flg
                           (equal unrewritten-test left))
                      *t*
                    (rewrite-entry (rewrite left alist)
                                   :type-alist true-type-alist)))
                 (rewritten-right
                  (rewrite-entry (rewrite right alist)
                                 :type-alist false-type-alist)))
             (cons-term-if test rewritten-left rewritten-right
                           iff-flg type-alist
                           (access rewrite-constant rcnst :ens)
                           wrld))))))))

(defun rewrite-args (args alist
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

  (declare (xargs :measure (lex4 (nfix nnn) 6 (acl2-count args) 0))
           (ignore iff-flg))

  (cond ((zp nnn)
         (sublis-var-lst alist args))
        ((endp args)
         nil)
        (t (cons
            (rewrite-entry (rewrite (car args) alist)
                           :iff-flg nil)
            (rewrite-entry (rewrite-args (cdr args) alist)
                           :iff-flg nil)))))

(defun rewrite-primitive (fn args
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

  (declare (xargs :measure (lex4 (nfix nnn) 6 (acl2-count args) 0))
           (ignore obj))

  (cond
   ((zp nnn) (cons-term fn args))
   ((flambdap fn) (fcons-term fn args))
   ((eq fn 'equal)
    (rewrite-entry (rewrite-equal (car args) (cadr args))
                   :obj nil
                   :iff-flg nil))
   (t (rewrite-solidify (cons-term fn args) type-alist iff-flg
                        (access rewrite-constant rcnst :ens)
                        wrld))))

(defun rewrite-equal (lhs rhs
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

; We rewrite and return a term equivalent to (EQUAL lhs rhs).

  (declare (xargs :measure (lex4 (nfix nnn)
                                 5
                                 (+ 1
                                    (acl2-count lhs)
                                    (acl2-count rhs))
                                 0))
           (ignore obj iff-flg))

  (cond
   ((zp nnn) (cons-term 'equal (list lhs rhs)))
   ((equal lhs rhs) *t*)
   ((and (quotep lhs)
         (quotep rhs))
    *nil*)
   (t
    (let* ((ens (access rewrite-constant rcnst :ens))
           (ts-lhs (type-set lhs type-alist nil ens wrld *type-set-nnn*))
           (ts-rhs (type-set rhs type-alist nil ens wrld *type-set-nnn*)))
      (cond
       ((not (ts-intersectp ts-lhs ts-rhs)) *nil*)
       ((equal-x-cons-x-yp lhs rhs) *nil*)
       ((and (ts-subsetp ts-lhs *ts-boolean*)
             (equal rhs *t*))
        lhs)
       ((and (ts-subsetp ts-rhs *ts-boolean*)
             (equal lhs *t*))
        rhs)
       ((equal lhs *nil*)
        (fcons-term* 'if rhs *nil* *t*))
       ((equal rhs *nil*)
        (fcons-term* 'if lhs *nil* *t*))
       ((equalityp lhs)
        (fcons-term* 'if lhs
                     (fcons-term* 'equal rhs *t*)
                     (fcons-term* 'if rhs *nil* *t*)))
       ((equalityp rhs)
        (fcons-term* 'if rhs
                     (fcons-term* 'equal lhs *t*)
                     (fcons-term* 'if lhs *nil* *t*)))
       ((and (ts-subsetp ts-lhs *ts-cons*)
             (ts-subsetp ts-rhs *ts-cons*))

; If lhs and rhs are both of type cons, we recursively rewrite the
; equality of their cars and then of their cdrs.  If either of these
; two tests fails, this equality is nil.  If both succeed, this one is
; t.  Otherwise, we don't rewrite term.

        (let* ((alist (list (cons 'lhs lhs)
                            (cons 'rhs rhs)))
               (rewritten-car
                (rewrite-entry (rewrite '(equal (car lhs) (car rhs))
                                        alist)
                               :obj '?
                               :iff-flg t
                               :nnn (- nnn 1))))
                  (cond
                   ((equal rewritten-car *t*)
                    (let ((rewritten-cdr
                           (rewrite-entry (rewrite '(equal (cdr lhs)
                                                           (cdr rhs))
                                                   alist)
                                          :obj '?
                                          :iff-flg t
                                          :nnn (- nnn 1))))
                      (cond ((equal rewritten-cdr *t*)
                             *t*)
                            ((equal rewritten-cdr *nil*)
                             *nil*)
                            (t (fcons-term* 'equal lhs rhs)))))
                   ((equal rewritten-car *nil*)
                    *nil*)

                   (t
                    (let ((rewritten-cdr
                           (rewrite-entry (rewrite '(equal (cdr lhs)
                                                           (cdr rhs))
                                                   alist)
                                          :obj '?
                                          :iff-flg t
                                          :nnn (- nnn 1))))
                      (cond ((equal rewritten-cdr *nil*)
                             *nil*)
                            (t (fcons-term* 'equal lhs rhs))))))))
       (t (fcons-term* 'equal lhs rhs)))))))

(defun relieve-hyp (term unify-subst
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

; This function is a No-Change Loser.

  (declare (xargs :measure (lex4 (nfix nnn) 0 0 0))
           (ignore obj iff-flg))

  (cond ((zp nnn) (mv nil unify-subst))
        ((and (nvariablep term)
              (not (fquotep term))
              (eq (ffn-symb term) 'synp))
         (let ((mfc (if (member-eq 'mfc (all-vars (cadr (fargn term 3))))
                        (make metafunction-context 
                              :type-alist type-alist
                              :obj '?
                              :iff-flg nil
                              :wrld wrld
                              :fnstack fnstack
                              :ancestors ancestors
                              :rcnst rcnst)
                      nil))
               (synp-fn (car (cadr (fargn term 2)))))
           (mv-let (erp val)
                   (ev-synp (fargn term 3) unify-subst mfc wrld)
                   (cond
                    ((or erp (null val)) (mv nil unify-subst))
                    ((eq synp-fn 'SYNTAXP) (mv val unify-subst))

; Here we could handle BIND-FREE forms as in ACL2, but I don't want to be
; distracted by them.

                    (t (mv nil unify-subst))))))
        ((and (equalityp term)
              (variablep (fargn term 1))
              (not (assoc-eq (fargn term 1) unify-subst))
              (not (free-varsp (fargn term 2) unify-subst)))
         (let ((rewritten-rhs
                (rewrite-entry
                 (rewrite (fargn term 2)
                          unify-subst)
                 :obj '?
                 :iff-flg nil
                 :nnn (- nnn 1))))
           (mv t
               (cons (cons (fargn term 1) rewritten-rhs)
                     unify-subst))))
        (t
         (mv-let
          (flg unify-subst)
          (lookup-hyp term type-alist wrld unify-subst)
          (cond
           (flg (mv t unify-subst))
           ((free-varsp term unify-subst) (mv nil unify-subst))
           (t
            (let ((inst-hyp (sublis-var unify-subst term)))
              (mv-let
               (on-ancestorsp assumed-true)
               (ancestors-check inst-hyp ancestors)
               (cond
                (on-ancestorsp (mv assumed-true unify-subst))
                (t
                 (mv-let
                  (knownp nilp)
                  (known-whether-nil inst-hyp type-alist
                                     (access rewrite-constant rcnst :ens)
                                     wrld)
                  (cond
                   (knownp (mv (not nilp) unify-subst))
                   (t
                    (mv-let
                     (not-flg atm)
                     (strip-not term)
                     (let ((rewritten-atm
                            (rewrite-entry
                             (rewrite atm unify-subst)
                             :obj (if not-flg nil t)
                             :iff-flg t
                             :ancestors (push-ancestor
                                         (dumb-negate-lit inst-hyp)
                                         ancestors)
                             :nnn (- nnn 1))))
                      (cond
                       (not-flg
                        (mv (equal rewritten-atm *nil*) unify-subst))
                       ((if-tautologyp rewritten-atm
                                       (access rewrite-constant rcnst :ens)
                                       wrld)
                        (mv t unify-subst))
                       (t (mv nil unify-subst))))))))))))))))))

(defun relieve-hyps (hyps unify-subst
                   ; &extra formals
                     type-alist obj iff-flg wrld fnstack ancestors
                     rcnst nnn)

; We return t or nil indicating success and an extended unify-subst.
; This function is a No-Change Loser.

  (declare (xargs :measure (lex4 (nfix nnn) 1 (acl2-count hyps) 0))
           (ignore obj iff-flg))

  (cond ((endp hyps) (mv t unify-subst))
        (t (mv-let (flg unify-subst)
                   (rewrite-entry (relieve-hyp (car hyps) unify-subst)
                                  :obj nil
                                  :iff-flg nil)
                   (cond
                    (flg
                     (rewrite-entry (relieve-hyps (cdr hyps) unify-subst)
                                    :obj nil
                                    :iff-flg nil))
                    (t (mv nil unify-subst)))))))
           
(defun rewrite-with-lemma (term lemma
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

; The two values returned by this function are t or nil, indicating
; whether lemma was used to rewrite term, and the rewritten version of
; term.  This is a No-Change Loser.

  (declare (xargs :measure (lex4 (nfix nnn) 4 0 0)))

  (cond
   ((zp nnn) (mv nil term))
   ((eq (access rewrite-rule lemma :subclass) 'meta)
    (cond
     ((refinementp (access rewrite-rule lemma :equiv) iff-flg)

; Metafunctions come in two flavors.  Vanilla metafunctions take just
; one arg, the term to be rewritten.  Extended metafunctions take
; three args.  We cons up the args here and use this list of args
; twice below, once to eval the metafunction and once to eval the hyp
; fn.  The :rhs of the rewrite-rule is the special flag 'extended
; if we are in the extended case; otherwise, :rhs is nil.  We must
; manufacture a context in the former case.

      (let* ((args
              (cond
               ((eq (access rewrite-rule lemma :rhs)
                    'extended)
                (list term
                      (make metafunction-context 
                            :type-alist type-alist
                            :obj obj
                            :iff-flg iff-flg
                            :wrld wrld
                            :fnstack fnstack
                            :ancestors ancestors
                            :rcnst rcnst)))
               (t (list term)))))
        (mv-let
         (erp val)
         (apply (access rewrite-rule lemma :lhs) args wrld)
         (cond
          (erp
           (mv nil term))
          ((equal term val)
           (mv nil term))
          ((termp val wrld)
           (let ((hyp-fn (access rewrite-rule lemma :hyps)))
             (mv-let
              (erp evaled-hyp)
              (if (eq hyp-fn nil)
                  (mv nil *t*)
                (apply hyp-fn args wrld))
              (cond
               (erp (mv nil term))
               ((termp evaled-hyp wrld)
                (cond
                 ((ffnnamep 'synp evaled-hyp)
                  (mv nil term))
                 (t
                  (mv-let
                   (relieve-hyps-ans unify-subst)
                   (rewrite-entry (relieve-hyps
                                   (flatten-ands-in-lit

; Note: The sublis-var below normalizes the explicit constant
; constructors in evaled-hyp, e.g., (cons '1 '2) becomes '(1 . 2).

                                    (sublis-var nil evaled-hyp))

; The meta function has rewritten term to val and has generated a
; hypothesis called evaled-hyp.  Now ignore the metafunction and just
; imagine that we have a rewrite rule (implies evaled-hyp (equiv term
; val)).  The unifying substitution just maps the vars of term to
; themselves.  There may be additional vars in both evaled-hyp and in
; val.  But they are free at the time we do this relieve-hyps.

                                   (let ((vars (all-vars term)))
                                     (pairlis vars vars)))
                                  :obj nil
                                  :geneqv nil)
                   (cond
                    (relieve-hyps-ans
                     (let ((rewritten-rhs
                            (rewrite-entry
                             (rewrite

; Note: The sublis-var below normalizes the explicit constant
; constructors in val, e.g., (cons '1 '2) becomes '(1 . 2).

                              (sublis-var nil val)

; At one point we ignored the unify-subst constructed above and used a
; nil here.  That was unsound if val involved free vars bound by the
; relief of the evaled-hyp.  We must rewrite val under the extended
; substitution.  Often that is just the identity substitution.

                              unify-subst)
                             :nnn (- nnn 1))))
                       (mv t rewritten-rhs)))
                    (t (mv nil term)))))))
               (t (mv nil term))))))
          (t (mv nil term))))))
     (t (mv nil term))))
   ((not (refinementp (access rewrite-rule lemma :equiv) iff-flg))
    (mv nil term))
   ((eq (access rewrite-rule lemma :subclass) 'definition)
    (let ((rewritten-term
           (rewrite-entry (rewrite-fncall lemma term))))
      (mv (not (equal term rewritten-term)) rewritten-term)))
   ((and (or (null (access rewrite-rule lemma :hyps))
             (not (eq obj t))
             (not (equal (access rewrite-rule lemma :rhs) *nil*)))
         (or (flambdap (ffn-symb term)) ; hence not on fnstack
             (not (being-openedp (ffn-symb term) fnstack
                                 (getprop (ffn-symb term) 'recursivep nil
                                          wrld)))
             (not (ffnnamep (ffn-symb term)
                            (access rewrite-rule lemma :rhs)))))
    (let ((lhs (access rewrite-rule lemma :lhs)))
      (mv-let (unify-ans unify-subst)
              (one-way-unify lhs term)
              (cond
               (unify-ans
                (cond
                 ((null (loop-stopperp
                         (access rewrite-rule lemma :heuristic-info)
                         unify-subst))
                  (mv nil term))
                 (t
                  (mv-let
                   (relieve-hyps-ans unify-subst)
                   (rewrite-entry
                    (relieve-hyps (access rewrite-rule lemma :hyps)
                                  unify-subst)
                    :obj nil
                    :geneqv nil)
                   (cond
                    (relieve-hyps-ans
                     (let ((rewritten-rhs
                            (rewrite-entry
                             (rewrite
                              (access rewrite-rule lemma :rhs)
                              unify-subst)
                             :nnn (- nnn 1))))
                      (mv t rewritten-rhs)))
                    (t (mv nil term)))))))
               (t (mv nil term))))))
          (t (mv nil term))))

(defun rewrite-with-lemmas1 (term lemmas
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)


; Try to rewrite term with the lemmas in lemmas.  Return t or nil
; indicating success, and the rewritten term.  This function is a
; No-Change Loser.

  (declare (xargs :measure (lex4 (nfix nnn) 5 (acl2-count lemmas) 0)))

  (cond ((zp nnn) (mv nil term))
        ((endp lemmas) (mv nil term))
        ((not (enabled-numep (access rewrite-rule (car lemmas) :nume)
                             (access rewrite-constant rcnst :ens)))
         (rewrite-entry
          (rewrite-with-lemmas1 term (cdr lemmas))))
        (t 
         (mv-let
          (rewrittenp rewritten-term)
          (<rewrite-with-lemmas1-id>
           (rewrite-entry (rewrite-with-lemma term (car lemmas))))
          (cond (rewrittenp
                 (mv t rewritten-term))
                (t (rewrite-entry
                    (rewrite-with-lemmas1 term (cdr lemmas)))))))))

(defun rewrite-fncall (rule term

                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

; Rule is a :REWRITE rule of subclass DEFINITION or else it is nil.
; Rule is nil iff term is a lambda application.  The value returned by
; this function is the (possibly) rewritten term.

; Term is of the form (fn . args).

  (declare (xargs :measure (lex4 (nfix nnn) 3 0 0)))

  (let* ((fn (ffn-symb term))
         (args (fargs term))
         (body (if (null rule)
                   (lambda-body fn)
                 (access rewrite-rule rule :rhs)))
         (recursivep (and rule ; it's a don't-care if (flambdap fn)
                          (car (access rewrite-rule rule :heuristic-info))))
         (ens (access rewrite-constant rcnst :ens)))
    (cond ((zp nnn) term)
          ((and (not (flambdap fn))
                (being-openedp fn fnstack recursivep))
           (rewrite-solidify term type-alist iff-flg ens wrld))
          ((null rule)  ; i.e., (flambdap fn)
           (let ((rewritten-body
                  (rewrite-entry (rewrite body
                                          (pairlis (lambda-formals fn) args))
                                 :fnstack fnstack
                                 :nnn (- nnn 1))))

; Observe that we do not put the lambda-expression onto the fnstack.
; We act just as though we were rewriting a term under a substitution.
; But we do decide on heuristic grounds whether to keep the expansion.
; See the handling of non-recursive functions below for some comments
; relating to the too-many-ifs code.

            (cond
             ((and (not (recursive-fn-on-fnstackp fnstack))
                   (too-many-ifs args rewritten-body))
              (rewrite-solidify term type-alist iff-flg ens wrld))
             (t rewritten-body))))
          (t
           (let* ((new-fnstack (cons (or recursivep fn) fnstack)))
             (mv-let
              (unify-ans unify-subst)
              (one-way-unify (access rewrite-rule rule :lhs)
                             term)
              (cond
               (unify-ans
                (mv-let
                 (relieve-hyps-ans unify-subst)
                 (rewrite-entry
                  (relieve-hyps (access rewrite-rule rule :hyps)
                                unify-subst)
                  :obj nil
                  :iff-flg nil)
                 (cond
                  (relieve-hyps-ans
                   (let ((rewritten-body
                          (rewrite-entry (rewrite body unify-subst)
                                         :fnstack new-fnstack
                                         :nnn (- nnn 1))))
                    (cond
                     ((null recursivep)

; We are dealing with a nonrecursive fn.  If we are at the top-level of the
; clause but the expanded body has too many IFs in it compared to the number
; in the args, we do not use the expanded body.  We know the IFs in
; the args will be clausified out soon and then this will be permitted to
; open.

                      (cond
                       ((and (not (recursive-fn-on-fnstackp fnstack))
                             (too-many-ifs args rewritten-body))
                        (rewrite-solidify term type-alist iff-flg ens wrld))
                       (t rewritten-body)))
                     ((rewrite-fncallp
                       term rewritten-body
                       (if (cdr recursivep) recursivep nil)
                       (access rewrite-constant rcnst
                               :top-clause)
                       (access rewrite-constant rcnst
                               :current-clause)
                       (cdr (access rewrite-rule rule :heuristic-info)))
                      (cond 
                       ((contains-rewriteable-callp
                         fn rewritten-body
                         (if (cdr recursivep)
                             recursivep
                           nil)
                         (access rewrite-constant
                                 rcnst :terms-to-be-ignored-by-rewrite))

; Ok, we are prepared to rewrite the once rewritten body.  But beware!  There
; is an infinite loop lurking here.  It can be broken by using :fnstack
; new-fnstack below, but we do something weaker; more on this below.  The
; problem is the interaction between opening up function definitions and use of
; equalities on the type-alist.  Suppose that (foo x) is defined to be (bar
; (foo (cdr x))) in a certain case.  But imagine that on the type-alist we have
; (foo (cdr x)) = (foo x).  Then rewritten-body, here, is (bar (foo x)).
; Because it contains a rewriteable call we rewrite it again.  If we do so with
; the old fnstack, we will open (foo x) to (bar (foo x)) again and infinitely
; regress.

; This same loop occurs in Nqthm, though it has never been fired in anger, as
; far as we know.  While the loop can be broken by using new-fnstack, that
; approach has a bad side-effect: (member x '(a b c)) is not runout.  It opens
; to (if (equal x 'a) (member x '(b c))) and because new-fnstack mentions
; member, we don't expand the inner call.

; In Version  2.5 and before we handled this rare loop in a very non-rugged
; way, using fnstack unchanged in the recursive call below: If the term we're
; expanding reoccurs in the rewritten body, we won't rewrite the rewritten
; body.  In that approach, if we're expanding (foo x a) and it rewrites to (bar
; (foo (cdr x) a)) and thence to (bar (foo x a)), we'll break the loop.  BUT if
; it goes instead to (bar (foo x a')), we'll just naively go around the loop.

; Starting with Version  2.6, we extend fnstack with (:term . rewritten-body)
; in the recursive call to rewrite, below.  But first, we check the fnstack to
; see if an entry (:term . x) is already there for some subterm x of the
; rewritten body.  This is the only place that we pay attention to elements of
; fnstack of the form (:term . x).

                        (cond
                         ((or (dumb-occur term rewritten-body)
                              (some-fnstack-term-dumb-occur fnstack
                                                            rewritten-body))
                          rewritten-body)
                         (t
                          (let ((rewritten-body
                                 (rewrite-entry
                                  (rewrite rewritten-body nil)
; See the reference to fnstack in the comment above.
                                  :fnstack (cons (cons :term term)
                                                 fnstack)
                                  :nnn (- nnn 1))))
                            rewritten-body))))
                       (t 
                        rewritten-body)))
                     (t (rewrite-solidify term type-alist iff-flg ens wrld)))))
                  (t (rewrite-solidify term type-alist iff-flg ens wrld)))))
               (t (rewrite-solidify term type-alist iff-flg ens wrld)))))))))

(defun rewrite-with-lemmas (term
                   ; &extra formals
                   type-alist obj iff-flg wrld fnstack ancestors rcnst nnn)

  (declare (xargs :measure (lex4 (nfix nnn) 6 0 0)))
  (cond
   ((zp nnn) term)
   ((variablep term)
    (rewrite-solidify term type-alist iff-flg
                      (access rewrite-constant rcnst :ens)
                      wrld))
   ((fquotep term) term)
   ((member-equal (ffn-symb term)
                  (access rewrite-constant rcnst :fns-to-be-ignored))
    term)
   ((flambda-applicationp term)
    (cond ((expand-permission-p term
                                (access rewrite-constant rcnst :expand-lst))
           (rewrite-entry
            (rewrite (lambda-body (ffn-symb term))
                     (pairlis (lambda-formals (ffn-symb term))
                              (fargs term)))
            :nnn (- nnn 1)))
          (t (rewrite-entry (rewrite-fncall nil term)))))
   (t (mv-let
       (rewrittenp rewritten-term)
       (rewrite-entry
        (rewrite-with-lemmas1 term
                              (getprop (ffn-symb term) 'lemmas nil wrld)))
       (cond
        (rewrittenp rewritten-term)
        ((and (expand-permission-p term
                                   (access rewrite-constant rcnst :expand-lst))
              (not (being-openedp (ffn-symb term) fnstack
                                  (getprop (ffn-symb term) 'recursivep nil
                                           wrld))))
         (rewrite-entry (rewrite
                         (body (ffn-symb term) t wrld)
                         (pairlis (formals (ffn-symb term) wrld)
                                  (fargs term)))
                        :nnn (- nnn 1)))
        (t (rewrite-solidify term type-alist iff-flg
                             (access rewrite-constant rcnst :ens)
                             wrld)))))))

)

(defconst *rewrite-nnn* 100)