(in-package "PACO")

; Section:  More on Generating Variable Names

; Our top-level function for generating variables attempts to feed
; genvar with inputs that generate names suggestive of the term being
; replaced by the variable.  We now develop the code for generating
; these roots.  It involves a recursive descent through a term.  At
; the bottom, we see variable symbols, e.g., ABC123, and we wish to
; generate the root '("ABC" . 124).

(defun strip-final-digits1 (lst)
; See strip-final-digits.
  (cond ((endp lst) (mv "" 0))
        ((member (car lst) '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
         (mv-let (str n)
                 (strip-final-digits1 (cdr lst))
                 (mv str (+ (let ((c (car lst)))
                              (case c
                                    (#\0 0)
                                    (#\1 1)
                                    (#\2 2)
                                    (#\3 3)
                                    (#\4 4)
                                    (#\5 5)
                                    (#\6 6)
                                    (#\7 7)
                                    (#\8 8)
                                    (otherwise 9)))
                            (* 10 n)))))
        (t (mv (coerce (reverse lst) 'string) 0))))

(defun strip-final-digits (str)

; Given a string, such as "ABC123", we strip off the final digits in it,
; and compute the number they represent.  We return two things,
; the string and the number, e.g., "ABC" and 123.

  (strip-final-digits1 (reverse (coerce str 'list))))

; For non-variable, non-quote terms we try first the idea of
; generating a name based on the type of the term.  The following
; constant associates with selected type sets the names of some
; variables that we find pleasing and suggestive of the type.  When we
; generalize a term we look at its type and if it is a subtype of one
; of those listed we prefer to use the variables given.  The first
; variable in each family is additionally used as the root for a
; gensym, should it come to that.  This list can be extended
; arbitarily without affecting soundness, as long as (a) the car of
; each pair below is a type set and (b) the cdr is a true-list of
; symbols.  Arbitrary overlaps between the types and between the
; symbols are permitted.

;; RAG - I changed rational to real and complex-rational to complex in
;; the list below, since the new types are supersets of the old types,
;; so it should be harmless.

(defconst *var-families-by-type*
  (list (cons *ts-integer* '(I J K L M N))
        (cons *ts-rational*
              '(R S I J K L M N))
        (cons *ts-complex-rational*
              '(Z R S I J K L M N))
        (cons *ts-cons* '(L LST))
        (cons *ts-boolean* '(P Q R))
        (cons *ts-symbol* '(A B C D E))
        (cons *ts-string* '(S STR))
        (cons *ts-character* '(C CH))))

; The following function is used to find the family of vars, given the
; type set of a term:

(defun assoc-ts-subsetp (ts alist)

; Like assoc except we compare with ts-subsetp.

  (cond ((endp alist) nil)
        ((ts-subsetp ts (caar alist)) (car alist))
        (t (assoc-ts-subsetp ts (cdr alist)))))

; And here is how we look for an acceptable variable.

(defun first-non-member-eq (lst1 lst2)

; Return the first member of lst1 that is not a member-eq of lst2.

  (cond ((endp lst1) nil)
        ((member-eq (car lst1) lst2)
         (first-non-member-eq (cdr lst1) lst2))
        (t (car lst1))))

; If the above techniques don't lead to a choice we generate a string
; from the term by abbreviating the first symbol in the term.  Here is
; how we abbreviate:

(defun abbreviate-hyphenated-string1 (str i maximum prev-c)

; We return a list of characters that, when coerced to a string,
; abbreviates string str from position i to (but not including) maximum.
; Currently, it returns the first character after each block of "hyphens"
; and the last character.  Thus, "PITON-TEMP-STK" is abbreviated
; "PTSK".

; If prev-char is T it means we output the character we last saw.
; If prev-char is NIL it means the character we last saw was a "hyphen".
; Otherwise, prev-char is the previous character.  "Hyphen" here means
; any one of several commonly used "word separators" in symbols.
; This function can be changed arbitrarily as long as it returns a
; list of characters.

  (declare (xargs :measure (nfix (- (acl2::ifix maximum) (acl2::ifix i)))))
  (cond
   ((or (not (integerp i))
        (not (integerp maximum)))
    nil)
   ((< i maximum)
    (let ((c (char str i)))
      (cond
       ((member c '(#\- #\_ #\. #\/ #\+))
        (abbreviate-hyphenated-string1 str (1+ i) maximum nil))
       ((null prev-c)
        (cons c (abbreviate-hyphenated-string1 str (1+ i) maximum t)))
       (t (abbreviate-hyphenated-string1 str (1+ i) maximum c)))))
   ((characterp prev-c) (list prev-c))
   (t nil)))

(defconst *suspiciously-first-numeric-chars*
  '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\+ #\- #\. #\^ #\_))

(defun abbreviate-hyphenated-string (str)

; The function scans a string and collects the first and last character
; and every character immediately after a block of "hyphens" as defined
; above.

  (let ((lst (abbreviate-hyphenated-string1 str 0 (length str) nil)))
    (coerce
     (cond ((or (null lst)
                (member (car lst) *suspiciously-first-numeric-chars*))
            (cons #\V lst))
           (t lst))
     'string)))

; Just as strip-final-digits produces the genvar root for a variable,
; the following function produces the genvar root for a nonvariable term.

(defun generate-variable-root1 (term avoid-lst type-alist ens wrld)

; Term is a nonvariable, non-quote term.  This function returns two
; results, str and n, such that (str . n) is a "root" for genvar.

; In fact, it tries to return a root that when fed to genvar will
; create a variable symbol that is suggestive of term and which does
; not occur in avoid-lst.  But the function is correct as long as it
; returns any root, which could be any string.

  (let* ((ts (type-set term type-alist nil ens wrld *type-set-nnn*))
         (family (cdr (assoc-ts-subsetp ts *var-families-by-type*)))
         (var (first-non-member-eq family avoid-lst)))
    (cond (var

; If the type set of term is one of those for which we have a var family
; and some member of that family does not occur in avoid-lst, then we will
; use the symbol-name of var as the root from which to generate a
; variable symbol for term.  This will almost certainly result in the
; generation of the symbol var by genvar.  The only condition under which
; this won't happen is if var is an illegal variable symbol, in which case
; genvar will suffix it with some sufficiently large natural.

           (mv (symbol-name var) nil))
          (family

; If we have a family for this type of term but all the members are
; to be avoided, we'll genvar from the first member of the family and
; we might as well start suffixing immediately (from 0) because we
; know the unsuffixed var is in avoid-lst.

           (mv (symbol-name (car family)) 0))

          (t

; Otherwise, we will genvar from an abbreviated version of the "first
; symbol" in term.

           (mv (abbreviate-hyphenated-string
                (symbol-name
                 (cond ((variablep term)            'z) ; never happens
                       ((fquotep term)              'z) ; never happens
                       ((flambda-applicationp term) 'z)
                       (t (ffn-symb term)))))
               nil)))))

; And here we put them together with one last convention.  The
; root for (CAR ...) is just the root for ..., except we force
; there to be a suffix.  Thus, the root for (CAR X4) is going to be
; ("X" . 5).

(defun generate-variable-root (term avoid-lst type-alist ens wrld)
  (cond
   ((variablep term)
    (mv-let (str n)
            (strip-final-digits (symbol-name term))
            (mv str (1+ n))))
   ((fquotep term) (mv "CONST" 0))
   ((eq (ffn-symb term) 'CAR)
    (mv-let (str n)
            (generate-variable-root (fargn term 1) avoid-lst type-alist
                                    ens wrld)
            (mv str (or n 0))))
   ((eq (ffn-symb term) 'CDR)
    (mv-let (str n)
            (generate-variable-root (fargn term 1) avoid-lst type-alist
                                    ens wrld)
            (mv str (or n 0))))
   (t (generate-variable-root1 term avoid-lst type-alist ens wrld))))

; We must be able to find a package witness for the variable we generate.
; We search the term for a likely symbol.

(mutual-recursion

(defun find-first-var (term)
  (cond ((variablep term) term)
        ((fquotep term) nil)
        ((find-first-var-lst (fargs term)))
        ((flambdap (ffn-symb term))
         (car (lambda-formals (ffn-symb term))))
        (t nil)))

(defun find-first-var-lst (lst)
  (cond ((endp lst) nil)
        (t (or (find-first-var (car lst))
               (find-first-var-lst (cdr lst))))))
)

(mutual-recursion

(defun find-first-fnsymb (term)
  (cond ((variablep term) nil)
        ((fquotep term) nil)
        ((flambdap (ffn-symb term))
         (or (find-first-fnsymb-lst (fargs term))
             (find-first-fnsymb (lambda-body (ffn-symb term)))))
        (t (ffn-symb term))))

(defun find-first-fnsymb-lst (lst)
  (cond ((endp lst) nil)
        (t (or (find-first-fnsymb (car lst))
               (find-first-fnsymb-lst (cdr lst))))))
)

(defun find-pkg-witness (term)

; This function must return a symbol.  Imagine that term is to be replaced by
; some variable symbol.  In which package do we intern that symbol?  This
; function finds a symbol which is used with intern-in-package-of-symbol.
; Thus, the package of the returned symbol is important to human readability.
; We return the first variable we see in term, if there is one.  Otherwise, we
; return the first function symbol we see, if there is one.  Otherwise, we
; return the symbol 'find-pkg-witness.

  (or (find-first-var term)
      (find-first-fnsymb term)
      'find-pkg-witness))



(defun generate-variable (term avoid-lst type-alist ens wrld)

; We generate a legal variable symbol that does not occur in
; avoid-lst.  We use term, type-alist and wrld in a heuristic way to
; suggest a preferred name for the symbol.  Generally speaking, the
; symbol we generate will be used to replace term in some conjecture,
; so we try to generate a symbol that we think "suggests" term.

  (mv-let (str n)
          (generate-variable-root term avoid-lst type-alist ens wrld)
          (genvar (find-pkg-witness term) str n avoid-lst)))

(defun generate-variable-lst (term-lst avoid-lst type-alist ens wrld)

; And here we generate a list of variable names sequentially, one for
; each term in term-lst.

  (cond ((endp term-lst) nil)
        (t
         (let ((var (generate-variable (car term-lst) avoid-lst
                                       type-alist ens wrld)))
           (cons var (generate-variable-lst (cdr term-lst)
                                            (cons var avoid-lst)
                                            type-alist ens wrld))))))


; ---------------------------------------------------------------------------
; Section:  Destructor Elim Rules

; An elim-rule, as declared below, denotes a theorem of the form
; (implies hyps (equal lhs rhs)), where rhs is a variable symbol and
; lhs involves the terms destructor-terms, each of which is of the
; form (dfn v1 ... vn), where the vi are distinct variables and {v1
; ... vn} are all the variables in the formula.  We call rhs the
; "crucial variable".  It is the one we will "puff up" to eliminate
; the destructor terms.  For example, in (CONSP X) -> (CONS (CAR X)
; (CDR X)) = X, X is the crucial variable and by puffing it up to (CONS A
; B) we can eliminate (CAR X) and (CDR X).  We store an elim-rule
; under the function symbol, dfn, of each destructor term.  The rule
; we store for (dfn v1 ... vn) has that term as the car of destructor-
; terms and has crucial-position j where (nth j '(v1 ... vn)) = rhs.
; (Thus, the crucial-position is the position in the args at which the
; crucial variable occurs and for these purposes we enumerate the args
; from 0 (as by nth) rather than from 1 (as by fargn).)

(defrec elim-rule
  (((nume . crucial-position) . (destructor-term . destructor-terms))
   (hyps . equiv)
   .
   (lhs . rhs)))

; In Paco, equiv is always EQUAL.

(defun occurs-nowhere-else (var args c i)

; Index the elements of args starting at i.  Scan all args except the
; one with index c and return nil if var occurs in one of them and t
; otherwise.

  (cond ((endp args) t)
        ((int= c i)
         (occurs-nowhere-else var (cdr args) c (1+ i)))
        ((dumb-occur var (car args)) nil)
        (t (occurs-nowhere-else var (cdr args) c (1+ i)))))

(defun first-nomination (term votes nominations)

; See nominate-destructor-candidate for an explanation.

  (cons (cons term (cons term votes))
        nominations))

(defun second-nomination (term votes nominations)

; See nominate-destructor-candidate for an explanation.

  (cond ((endp nominations) nil)
        ((equal term (car (car nominations)))
         (cons (cons term
                     (union-equal votes (cdr (car nominations))))
               (cdr nominations)))
        (t (cons (car nominations)
                 (second-nomination term votes (cdr nominations))))))


(defun some-hyp-probably-nilp (hyps type-alist ens wrld)

; The name of this function is meant to limit its use to heuristics.
; In fact, if this function says some hyp is probably nil then in fact
; some hyp is known to be nil under the given type-alist and wrld.

  (cond
   ((endp hyps) nil)
   (t (mv-let
       (knownp nilp)
       (known-whether-nil
        (car hyps) type-alist ens wrld)
       (cond ((and knownp nilp) t)
             (t (some-hyp-probably-nilp (cdr hyps) type-alist ens wrld)))))))

(mutual-recursion

(defun sublis-expr (alist term)

; Alist is of the form ((a1 . b1) ... (ak . bk)) where the ai and bi are
; all terms.  We substitute bi for each occurrence of ai in term.
; Thus, if the ai are distinct variables, this function is equivalent to
; sublis-var.  We do not look for ai's properly inside of quoted objects.
; Thus,
;    (sublis-expr '(('3 . x)) '(f '3))       = '(f x)
; but
;    (sublis-expr '(('3 . x)) '(f '(3 . 4))) = '(f '(3 . 4)).

  (let ((temp (assoc-equal term alist)))
    (cond (temp (cdr temp))
          ((variablep term) term)
          ((fquotep term) term)
          (t (cons-term (ffn-symb term)
                        (sublis-expr-lst alist (fargs term)))))))

(defun sublis-expr-lst (alist lst)
  (cond ((endp lst) nil)
        (t (cons (sublis-expr alist (car lst))
                 (sublis-expr-lst alist (cdr lst))))))

)

(defthm acl2-count-nth
  (<= (acl2-count (nth i x)) (acl2-count x))
  :rule-classes :linear)

(defun nominate-destructor-candidate
  (term eliminables type-alist ens wrld votes nominations)

  (declare (xargs :measure (acl2-count term)))

; This function recognizes candidates for destructor elimination.  It
; is assumed that term is a non-variable, non-quotep term.  To be a
; candidate the term must not be a lambda application and the function
; symbol of the term must have an enabled destructor elimination rule.
; Furthermore, the crucial argument position of the term must be
; occupied by a variable symbol that is a member of the eliminables
; and that occurs nowhere else in the arguments of the term, or else
; the crucial argument position must be occupied by a term that itself
; is recursively a candidate.  (The :equiv slot of the rule will be
; EQUAL; should we expand Paco's elim technique to deal with other
; equivalence relations, we have to check that the crucial var occurs
; only in equiv-hittable positions within the target clause.)  (Note
; that if the crucial argument is an eliminable term then when we
; eliminate it we will introduce a suitable distinct var into the
; crucial argument of this term and hence it will be eliminable.)
; Finally, the instantiated hypotheses of the destructor elimination
; rule must not be known nil under the type-alist.

; Votes and nominations are accumulators.  Votes is a list of terms
; that contain term and will be candidates if term is eliminated.
; Nominations are explained below.

; If term is a candidate we either "nominate" it, by adding a
; "nomination" for term to the running accumulator nominations, or
; else we "second" a prior nomination for it.  A nomination of a term
; is a list of the form (dterm . votes) where dterm is the innermost
; eliminable candidate in term and votes is a list of all the terms
; that will be eliminable if dterm is eliminated.  To "second" a
; nomination is simply to add yourself as a vote.

; For example, if X is eliminable then (CAR (CAR (CAR X))) is a
; candidate.  If nominations is initially nil then at the conclusion
; of this function it will be

; (((CAR X) (CAR X) (CAR (CAR X)) (CAR (CAR (CAR X))))).

; We always return a nominations list.

  (cond
   ((flambda-applicationp term) nominations)
   (t (let ((rule (getprop (ffn-symb term) 'eliminate-destructors-rule
                           nil wrld)))
        (cond
         ((or (null rule)
              (not (enabled-numep (access elim-rule rule :nume) ens)))
          nominations)
         (t (let ((crucial-arg (nth (access elim-rule rule :crucial-position)
                                    (fargs term))))
              (cond
               ((variablep crucial-arg)

; Next we wish to determine that every occurrence of the crucial
; argument -- outside of the destructor nests themselves -- is equiv
; hittable.  For example, for car-cdr-elim, where we have A as the
; crucial arg (meaning term, above, is (CAR A) or (CDR A)), we wish to
; determine that every A in the clause is equal-hittable, except those
; A's occurring inside the (CAR A) and (CDR A) destructors.  Suppose
; the clause is p(A,(CAR A),(CDR A)).  The logical explanation of what
; elim does is to replace the A's not in the destructor nests by (CONS
; (CAR A) (CDR A)) and then generalize (CAR A) to HD and (CDR A) to
; TL.  This will produce p((CONS HD TL), HD, TL).  Observe that we do
; not actually hit the A's inside the CAR and CDR.  So we do not
; require that they be equiv-hittable.  (This situation actually
; arises in the elim rule for sets, where equiv tests equality on the
; canonicalizations.  In this setting, equiv is not a congruence for
; the destructors.)  So the question then is how do we detect that all
; the ``naked'' A's are equiv-hittable?  We ``ought'' to generalize
; away the instantiated destructor terms and then ask whether all the
; A's are equiv-hittable.  But we do not want to pay the price of
; generating n distinct new variable symbols.  So we just replace
; every destructor term by NIL.  This creates a ``pseudo-clause;'' the
; ``terms'' in it are not really legal -- NIL is not a variable
; symbol.  We only use this pseudo-clause to answer the question of
; whether the crucial variable, which certainly isn't NIL, is
; equiv-hittable in every occurrence.

                (let* ((alist (pairlis
                               (fargs
                                (access elim-rule rule :destructor-term))
                               (fargs term))))
                  (cond
                   ((assoc-equal term nominations)
                    (second-nomination term votes nominations))
                   ((member crucial-arg eliminables)
                    (cond
                     ((occurs-nowhere-else crucial-arg
                                           (fargs term)
                                           (access elim-rule rule
                                                   :crucial-position)
                                           0)
                      (let* ((inst-hyps
                              (sublis-var-lst alist
                                              (access elim-rule rule :hyps))))
                        (cond
                         ((some-hyp-probably-nilp inst-hyps
                                                  type-alist ens wrld)
                          nominations)
                         (t (first-nomination term votes nominations)))))
                     (t nominations)))
                   (t nominations))))
               (t (nominate-destructor-candidate crucial-arg
                                                 eliminables
                                                 type-alist
                                                 ens
                                                 wrld
                                                 (cons term votes)
                                                 nominations))))))))))

(mutual-recursion

(defun nominate-destructor-candidates
  (term eliminables type-alist ens wrld nominations)

; We explore term and accumulate onto nominations all the nominations.

  (cond ((variablep term) nominations)
        ((fquotep term) nominations)
        (t (nominate-destructor-candidates-lst
            (fargs term)
            eliminables
            type-alist
            ens
            wrld
            (nominate-destructor-candidate term
                                           eliminables
                                           type-alist
                                           ens
                                           wrld
                                           nil
                                           nominations)))))

(defun nominate-destructor-candidates-lst
  (terms eliminables type-alist ens wrld nominations)
  (cond ((endp terms) nominations)
        (t (nominate-destructor-candidates-lst
            (cdr terms)
            eliminables
            type-alist
            ens
            wrld
            (nominate-destructor-candidates (car terms)
                                             eliminables
                                             type-alist
                                             ens
                                             wrld
                                             nominations)))))

)

; We next turn to the problem of choosing which candidate we will
; eliminate.  We want to eliminate the most complicated one.  We
; measure them with max-level-no.  The level-no of each function
; symbol is computed at definition time and stored as a property of
; that name.  Functions with no stored level-no (primitives) have
; level-no 0.  Lambda expressions are assigned the max level-no
; of their bodies.

(mutual-recursion

(defun max-level-no (term wrld)
  (cond ((variablep term) 0)
        ((fquotep term) 0)
        (t (max (get-level-no (ffn-symb term) wrld)
                (max-level-no-lst (fargs term)
                                  wrld)))))

(defun max-level-no-lst (args wrld)
  (cond ((endp args) 0)
        (t (max (max-level-no (car args) wrld)
                (max-level-no-lst (cdr args) wrld)))))

(defun get-level-no (fn wrld)
  (cond ((flambdap fn) (max-level-no (lambda-body fn) wrld))
        ((getprop fn 'level-no nil wrld))
        (t 0)))

)

(defun sum-level-nos (lst wrld)

; Lst is a list of non-variable, non-quotep terms.  We sum the
; level-no of the function symbols of the terms.

  (cond ((endp lst) 0)
        (t (+ (if (flambda-applicationp (car lst))
                  (max-level-no (lambda-body (ffn-symb (car lst))) wrld)
                  (or (getprop (ffn-symb (car lst)) 'level-no nil wrld)
                      0))
              (sum-level-nos (cdr lst) wrld)))))

(defun pick-highest-sum-level-nos (nominations wrld dterm max-score)

; Nominations is a list of pairs of the form (dterm . votes), where
; votes is a list of terms.  The "score" of a dterm is the
; sum-level-nos of its votes.  We scan nominations and return a dterm
; with maximal score, assuming that dterm and max-score are the
; winning dterm and its score seen so far.

  (cond
   ((endp nominations) dterm)
   (t (let ((score (sum-level-nos (cdr (car nominations)) wrld)))
        (cond
         ((> score max-score)
          (pick-highest-sum-level-nos (cdr nominations) wrld
                                      (caar nominations) score))
         (t
          (pick-highest-sum-level-nos (cdr nominations) wrld
                                      dterm max-score)))))))

(defun select-instantiated-elim-rule (clause type-alist eliminables ens wrld)

; Clause is a clause to which we wish to apply destructor elimination.
; Type-alist is the type-alist obtained by assuming all literals of cl nil.
; Eliminables is the list of legal "crucial variables" which can be
; "puffed up" to do an elim.  For example, to eliminate (CAR X), X
; must be puffed up to (CONS A B).  X is the crucial variable in (CAR
; X).  Upon entry to the destructor elimination process we consider
; all the variables eliminable (except the ones historically
; introduced by elim).  But once we get going within the elim process,
; the only eliminable variables are the ones we introduce ourselves
; (because they won't be eliminable by subsequent processes since they
; will have been introduced by elim).

; If there is at least one nomination for an elim, we choose the one
; with maximal score and return an instantiated version of the
; elim-rule corresponding to it.  Otherwise we return nil.

  (let ((nominations
         (nominate-destructor-candidates-lst clause
                                             eliminables
                                             type-alist
                                             ens
                                             wrld
                                             nil)))
    (cond
     ((endp nominations) nil)
     (t
      (let* ((dterm (pick-highest-sum-level-nos nominations wrld nil -1))
             (rule (getprop (ffn-symb dterm) 'eliminate-destructors-rule
                            nil wrld))
             (alist (pairlis (fargs (access elim-rule rule :destructor-term))
                             (fargs dterm))))
        (change elim-rule rule
                :hyps (sublis-var-lst alist (access elim-rule rule :hyps))
                :lhs  (sublis-var alist (access elim-rule rule :lhs))
                :rhs  (sublis-var alist (access elim-rule rule :rhs))
                :destructor-term
                (sublis-var alist (access elim-rule rule :destructor-term))
                :destructor-terms
                (sublis-var-lst
                 alist
                 (access elim-rule rule :destructor-terms))))))))

; We now take a break from elim and develop the code for the
; generalization that elim uses.  After replacing a term by a variable
; (sublis-expr, above), must to restrict the new variable by noting
; the type-set of the term replaced.  We must also use generalization
; rules provided in the data base.

; We now develop the function that converts a type-set into a term.

(defrec type-set-inverter-rule ((nume . ts) . terms))

; A type-set-inverter-rule states that x has type-set ts iff the conjunction of
; terms{X/x} is true.  Thus, for example, if :ts is *ts-integer* then :terms is
; '((INTEGERP X)).

; A type-set, s, is a disjunction of the individual bits in it.  Thus, to
; create a term whose truth is equivalent to the claim that X has type-set s it
; is sufficient to find any type-set-inverter-rule whose :ts is a subset of s
; and then disjoin the :term of that rule to the result of recursively creating
; the term recognizing s minus :ts.  This assumes one has a rule for each
; single type bit.

; The database contains a global-val, type-set-inverter-rules, of all
; known type-set-inverter-rules.  The list is ordered in a
; heuristically important way: the larger type-sets are at the front.
; This ordering is exploited by convert-type-set-to-term-lst which
; operates by finding the largest recognized type set group and knocks
; it out of the type set.

(defun convert-type-set-to-term-lst (ts rules ens lst)

; We map over the list of type-set-inverter rules and each time we
; find an enabled rule whose :ts is a subset of ts, we accumulate its
; conjoined :terms and its :rune, and knock off those bits of ts.  We
; return lst, where lst is a list of terms in the variable X whose
; disjunction is equivalent to ts.

  (cond
   ((endp rules) (reverse lst))
   ((and (enabled-numep (access type-set-inverter-rule (car rules) :nume) ens)
         (ts= (access type-set-inverter-rule (car rules) :ts)
              (ts-intersection
               (access type-set-inverter-rule (car rules) :ts)
               ts)))
    (<convert-type-set-to-term-lst-id>
     (convert-type-set-to-term-lst
      (ts-intersection
       ts
       (ts-complement (access type-set-inverter-rule (car rules) :ts)))
      (cdr rules)
      ens
      (add-to-set-equal
       (conjoin (access type-set-inverter-rule (car rules) :terms))
       lst))))
   (t (convert-type-set-to-term-lst ts (cdr rules) ens lst))))

(defun convert-type-set-to-term (x ts ens w)

; Given a term x and a type set ts we generate a term that expresses
; the assertion that "x has type set ts".  E.g., if x is the term (FN
; X Y) and ts is *ts-rational* then our output will be (RATIONALP (FN
; X Y)).  We return term.  We do not use disabled type-set-inverters.

  (cond ((ts= ts *ts-unknown*) *t*)
        ((and (ts= ts *ts-t*)
              (ts-booleanp x nil ens w))
         x)
        ((ts-complementp ts)
         (subst-var x 'x
                    (conjoin
                     (dumb-negate-lit-lst
                      (convert-type-set-to-term-lst
                       (ts-complement ts)
                       (global-val 'type-set-inverter-rules w)
                       ens nil)))))
        (t (subst-var x 'x
                      (disjoin
                       (convert-type-set-to-term-lst
                        ts
                        (global-val 'type-set-inverter-rules w)
                        ens nil))))))

(defun type-restriction-segment (terms vars type-alist ens wrld)

; Terms is a list of terms.  Vars is a list in 1:1 correspondence with
; terms.  We are in the process of generalizing some clause by
; replacing each term with the corresponding var.  We wish to restrict
; the new vars to have the types of their terms.  Type-alist is the
; result of assuming false every literal of the clause.

; This function returns a list of literals that can be disjoined to
; the GENERALIZED clause.  That is, the new literals contain the new
; vars, not the old terms.

; It is sound, of course, to restrict the new variable to have
; whatever properties the corresponding term has.  This function is
; responsible for selecting the restrictions we want to place on each
; variable, based on type-set reasoning alone.  Thus, if t is known to
; have properties h1 & ... & hk, then we can include (not h1), ...,
; (not hk) in our first answer to restrict the variable introduced for
; t.

; We do not want our type restrictions to cause the new clause to
; explode into cases.  Therefore, we adopt the following heuristic.
; We convert the type set of each term t into a term (hyp t) known to
; be true of t.  Then we generalize t to the var v.  We negate (hyp v)
; and clausify the result.  If that produces a single clause (segment)
; then that segment is added to our answer.  Otherwise, we add no
; restriction.  There are probably better ways to do this than to call
; the full-blown convert-type-set-to-term and clausify.  But this is
; simple, elegant, and lets us take advantage of improvements to those
; two utilities.

; Subtle Design Issue: Once upon a time, Paco clausified (not (hyp t))
; rather than (not (hyp v)) and then generalized the assembled clause.
; But because Paco's clausify uses type-set, this strategy (which is
; used by ACL2) doesn't work!  The clausify below erased much of the
; the type information.  E.g., if we're restricting (* i j) to with
; (acl2-numberp (* i j)), the clausification will just eliminate the
; restriction.  We must create (acl2-numberp (* i j)), generalize it
; to (acl2-numberp v), and then clausify.

  (cond
   ((endp terms) nil)
   (t
    (let* ((ts
            (type-set (car terms) type-alist nil ens wrld *type-set-nnn*))
           (generalized-term
            (convert-type-set-to-term (car vars) ts ens wrld))
           (clauses
            (clausify (dumb-negate-lit generalized-term) ens wrld))
           (lits
            (type-restriction-segment (cdr terms)
                                      (cdr vars)
                                      type-alist ens wrld)))
      (cond ((null clauses)

; If the negation of the type restriction term clausifies to the empty
; set of clauses, then the term is nil.  Since we get to assume it,
; we're done.  But this can only happen if the type-set of the term is
; empty.  We don't think this will happen, but we test for it
; nonetheless, and toss a nil hypothesis into our answer literals if
; it happens.

             (add-to-set-equal *nil* lits))
            ((and (endp (cdr clauses))
                  (not (endp (car clauses))))

; If there is only one clause and it is not the empty clause, we'll
; assume everything in it.  (If the clausify above produced '(NIL)
; then the type restriction was just *t* and we ignore it.)

             (disjoin-clauses (car clauses) lits))
            (t

; There may be useful type information we could extract, but we don't.
; It is always sound to exit here, giving ourselves no additional
; assumptions.

             lits))))))

(mutual-recursion

(defun subterm-one-way-unify (pat term)

; This function searches pat for a non-variable non-quote subterm s
; such that (one-way-unify s term) returns t and a unify-subst.  If it
; finds one, it returns t and the unify-subst.  Otherwise, it returns
; two nils.

  (cond ((variablep pat) (mv nil nil))
        ((fquotep pat) (mv nil nil))
        (t (mv-let (ans alist)
                   (one-way-unify pat term)
                   (cond (ans (mv ans alist))
                         (t (subterm-one-way-unify-lst (fargs pat) term)))))))

(defun subterm-one-way-unify-lst (pat-lst term)
  (cond
   ((endp pat-lst) (mv nil nil))
   (t (mv-let (ans alist)
              (subterm-one-way-unify (car pat-lst) term)
              (cond (ans (mv ans alist))
                    (t (subterm-one-way-unify-lst (cdr pat-lst) term)))))))

)

(defrec generalize-rule (nume . formula))

(defun apply-generalize-rule (gen-rule term ens)

; Gen-rule is a generalization rule.  Term is a term which we are
; intending to generalize by replacing it with a new variable.  We
; return two results.  The first is either t or nil indicating whether
; gen-rule provides a useful restriction on the generalization of
; term.  If the first result is nil, so is the second.  Otherwise, the
; second result is an instantiation of the formula of gen-rule in
; which term appears.

; Our heuristic for deciding whether to use gen-rule is: (a) the rule
; must be enabled, (b) term must unify with a non-variable non-quote
; subterm of the formula of the rule, (c) the unifying substitution
; must leave no free vars in that formula, and (d) the function symbol
; of term must not occur in the instantiation of the formula except in
; the occurrences of term itself.

  (cond
   ((not (enabled-numep (access generalize-rule gen-rule :nume) ens))
    (mv nil nil))
   (t (mv-let
       (ans unify-subst)
       (subterm-one-way-unify (access generalize-rule gen-rule :formula)
                              term)
       (cond
        ((null ans)
         (mv nil nil))
        ((free-varsp (access generalize-rule gen-rule :formula)
                     unify-subst)
         (mv nil nil))
        (t (let ((inst-formula (sublis-var unify-subst
                                           (access generalize-rule
                                                   gen-rule
                                                   :formula))))
             (cond ((ffnnamep (ffn-symb term)
                              (subst-expr 'x term inst-formula))
                    (mv nil nil))
                   (t
                    (<apply-generalize-rule-id>
                     (mv t inst-formula)))))))))))

(defun generalize-rule-segment1 (generalize-rules term ens)

; Given a list of :GENERALIZE rules and a term we return the list of
; instantiated negated formulas of those applicable rules.  The list
; is suitable for splicing into a clause to add the formulas as
; hypotheses.

  (cond
   ((endp generalize-rules) nil)
   (t (mv-let (ans formula)
              (apply-generalize-rule (car generalize-rules) term ens)
              (let ((formulas
                     (generalize-rule-segment1 (cdr generalize-rules)
                                               term ens)))
                (cond (ans (add-literal (dumb-negate-lit formula)
                                        formulas nil))
                      (t formulas)))))))

(defun generalize-rule-segment (terms ens wrld)

; Given a list of terms, we return a clause segment containing the
; instantiated negated formulas derived from every applicable
; :GENERALIZE rule for each term in terms.  This segment can be
; spliced into a clause to restrict the range of a generalization of
; terms.

  (cond
   ((endp terms) nil)
   (t (disjoin-clauses
       (generalize-rule-segment1 (global-val 'generalize-rules wrld)
                                 (car terms) ens)
       (generalize-rule-segment (cdr terms) ens wrld)))))

(defun generalize1 (cl type-alist terms vars ens wrld)

; Cl is a clause.  Type-alist is a type-alist obtained by assuming all
; literals of cl false.  Terms and vars are lists of terms and
; distinct variables, respectively, in 1:1 correspondence.  We assume
; no var in vars occurs in cl.  We generalize cl by substituting vars
; for the corresponding terms.  We restrict the variables by using
; type-set information about the terms and by using :GENERALIZE rules
; in wrld.

; We return the new clause.

  (disjoin-clauses
   (type-restriction-segment terms vars type-alist ens wrld)
   (sublis-expr-lst
    (pairlis terms vars)
    (disjoin-clauses (generalize-rule-segment terms ens wrld) cl))))

; This completes our brief flirtation with generalization.  We now
; have enough machinery to finish coding destructor elimination.
; However, it might be noted that generalize1 is the main subroutine
; of the generalize-clause waterfall processor.

(defun apply-instantiated-elim-rule (rule cl type-alist avoid-vars ens wrld)

; This function takes an instantiated elim-rule, rule, and applies it
; to a clause cl.  Avoid-vars is a list of variable names to avoid
; when we generate new ones.  See eliminate-destructors-clause for
; an explanation of that.

; An instantiated :ELIM rule has hyps, lhs, rhs, and destructor-terms,
; all instantiated so that the car of the destructor terms occurs
; somewhere in the clause.  To apply such an instantiated :ELIM rule to
; a clause we assume the hyps (adding their negations to cl), we
; generalize away the destructor terms occurring in the clause and in
; the lhs of the rule, and then we substitute that generalized lhs for
; the rhs into the generalized cl to obtain the final clause.  The
; generalization step above may involve adding additional hypotheses
; to the clause and using generalization rules in wrld.

; We return two things: the clause described above, which implies cl
; if the hyps of the rule are known to be true and the set of elim
; variables we have just introduced into it.

  (<apply-instantiated-elim-rule-id>
   (let* ((hyps (access elim-rule rule :hyps))
          (lhs (access elim-rule rule :lhs))
          (rhs (access elim-rule rule :rhs))
          (dests (access elim-rule rule :destructor-terms))
          (negated-hyps (dumb-negate-lit-lst hyps))
          (cl-with-hyps (disjoin-clauses negated-hyps cl)))
     (mv-let
      (contradictionp type-alist)
      (type-alist-clause negated-hyps type-alist ens wrld)
      (cond
       (contradictionp

; We compute the type-alist of the clause to allow us to generate nice
; variable names and to restrict the coming generalization.  We know
; that a contradiction cannot arise, because we would not have chosen
; an :ELIM rule with nil hypotheses.  However, we will return an
; accurate answer, namely cl.  We'll report that we introduced the
; variable rhs (which was actually already there) thus preventing any
; future attempt to elim it.

        (mv cl (list rhs)))
       (t
        (let* ((elim-vars (generate-variable-lst dests
                                                 (all-vars1-lst cl-with-hyps
                                                                avoid-vars)
                                                 type-alist ens wrld))
               (generalized-cl-with-hyps
                (generalize1 cl-with-hyps type-alist dests elim-vars
                             ens wrld))
               (alist (pairlis dests elim-vars))
               (generalized-lhs (sublis-expr alist lhs))
               (final-cl
                (subst-var-lst generalized-lhs
                               rhs
                               generalized-cl-with-hyps))
               (actual-elim-vars
                (intersection-eq elim-vars
                                 (all-vars1-lst final-cl nil))))
          (mv final-cl
              actual-elim-vars))))))))

(defun eliminate-destructors-clause1
  (cl eliminables avoid-vars ens wrld top-flg nnn)

; Cl is a clause we are trying to prove.  Eliminables is the set of
; variables on which we will permit a destructor elimination.
; Avoid-vars is a list of variable names we are to avoid when
; generating new names.  In addition, we avoid the variables in cl.
; (See below and then the discussion in owned-vars, further below, for
; more on variable name avoidance.)  We look for an eliminable
; destructor, select the highest scoring one and get its instantiated
; rule, split on the hyps of that rule to produce a "pathological"
; case of cl for each hyp and apply the rule to cl to produce the
; "normal" elim case.  Then we iterate until there is nothing more to
; eliminate.

; The handling of the eliminables needs explanation however.  At the
; top-level (when top-flg is t) eliminables is the set of all
; variables occurring in cl except those historically introduced by
; destructor elimination.  It is with respect to that set that we
; select our first elimination rule.  Thereafter (when top-flg is nil)
; the set of eliminables is always just the set of variables we have
; introduced into the clauses.  We permit these variables to be
; eliminated by this elim and this elim only.  For example, the
; top-level entry might permit elimination of (CAR X) and of (CAR Y).
; Suppose we choose X, introducing A and B.  Then on the second
; iteration, we'll allow eliminations of A and B, but not of Y.

; We return two things.  The first is a set of clauses to prove
; instead of cl.  The second is the set of variable names introduced
; by this destructor elimination step.

  (declare (xargs :measure (acl2-count nnn)))
  (cond
   ((zp nnn)

; We have an artificial termination condition to make admission
; simple.  This function probably terminates without this, because the
; number of eligible destructor terms in it decreases every round.
; But rather than try to formalize that measure, we just count down.
; The answer below is always correct: to prove cl it is sufficient to
; prove the set of clauses containing cl, and no new variables were
; introduced.

    (mv (list cl) nil))
   (t

; Our first step is to get the type-alist of cl.  It is used in two
; different ways: to identify contradictory hypotheses of candidate
; :ELIM lemmas and to generate names for new variables.

    (mv-let
     (contradictionp type-alist)
     (type-alist-clause cl nil ens wrld)
     (cond
      (contradictionp

; This is unusual.  We don't really expect to find a contradiction.

       (mv (list cl) nil))
      (t
       (let ((rule (select-instantiated-elim-rule cl type-alist eliminables
                                                  ens wrld)))
         (cond
          ((null rule)
           (mv (list cl) nil))
          (t
           (let ((clauses1 (split-on-assumptions
                            (access elim-rule rule :hyps)
                            cl nil)))

; Clauses1 is a set of clauses obtained by splitting on the
; instantiated hyps of the rule.  It contains n clauses, each obtained
; by adding one member of inst-hyps to cl.  (If any of these new
; clauses is a tautology, it will be deleted, thus there may not be as
; many clauses as there are inst-hyps.)  Because these n clauses are
; all "pathological" wrt the destructor term, e.g., we're assuming
; (not (consp x)) in a clause involving (car x), we do no further
; elimination down those paths.

             (mv-let
              (new-clause elim-vars1)
              (apply-instantiated-elim-rule rule cl type-alist
                                            avoid-vars ens wrld)
              (cond
               ((equal new-clause *true-clause*)
                (mv clauses1 elim-vars1))
               (t
                (mv-let
                 (clauses2 elim-vars2)
                 (eliminate-destructors-clause1
                  new-clause
                  (if top-flg
                      elim-vars1
                    (union-eq elim-vars1
                              (remove1-eq
                               (access elim-rule rule :rhs)
                               eliminables)))
                  avoid-vars
                  ens
                  wrld
                  nil
                  (- nnn 1))
                 (mv (conjoin-clause-sets clauses1 clauses2)
                     (union-eq elim-vars1 elim-vars2))))))))))))))))

(defconst *eliminate-destructors-nnn* 10)

(defun owned-vars (process mine-flg history)

; This function takes a process name, e.g., 'eliminate-destructors-
; clause, a flag which must be either nil or t, and a clause history.
; If the flag is t, it returns all of the variables introduced into
; the history by the given process.  If the flag is nil, it returns
; all of the variables introduced into the history by any other
; process.  Note: the variables returned may not even occur in the
; clause whose history we scan.

; For example, if the only two processes that introduce variables are
; destructor elimination and generalization, then when given
; 'eliminate-destructors-clause and mine-flg nil this function will
; return all the variables introduced by 'generalize-clause.

; Every history entry has an :alist field and if the process for the
; entry introduced new variables, those variables are listed in the
; :VARIABLES pair of that alist.

; Why are we interested in this concept?  Destructor elimination is
; controlled by a heuristic meant to prevent indefinite elim loops
; involving simplification.  For example, suppose you eliminate (CDR
; X0) by introducing (CONS A X1) for X0, and then open a recursive
; function so as to produce (CDR X1).  It is easy to cause a loop if
; you then eliminate (CDR X1) by replacing X1 it with (CONS B X2),
; etc.  To prevent this, we do not allow destructor elimination to
; work on a variable that was introduced by destructor elimination
; (except within the activation of the elim process that introduces
; that variable).

; That raises the question of telling how a variable was introduced
; into a clause.  In ACL2 we adopt the convention described above and
; follow the rule that no process shall introduce a variable into a
; clause that has been introduced by a different process in the
; history of that clause.  Thus, if X1 is introduced by elim into the
; history, then X1 cannot also be introduced by generalization, even
; if X1 is new for the clause when generalization occurs.  By
; following this rule we know that if a variable is in a clause and
; that variable was introduced into the history of the clause by elim
; then that variable was introduced into the clause by elim.  If
; generalize could "re-use" a variable that was already "owned" by
; elim in the history, then we could not accurately determine by
; syntactic means the elim variables in the clause.

  (cond ((endp history) nil)
        ((eq mine-flg
             (eq (access history-entry (car history) :processor)
                 process))
         (union-eq (cdr (assoc-eq :VARIABLES
                                  (access history-entry (car history) :alist)))
                   (owned-vars process mine-flg (cdr history))))
        (t (owned-vars process mine-flg (cdr history)))))

(defun eliminate-destructors-clause (id cl hist pspv wrld)

; This is the waterfall processor that eliminates destructors.  Like
; all waterfall processors it returns four values: 'hit or 'miss, and,
; if 'hit, a set of clauses, a history alist, and a possibly modified
; pspv.

  (declare (ignore id))
  (mv-let
   (clauses elim-vars)
   (eliminate-destructors-clause1 cl
                                  (set-difference-eq
                                   (all-vars1-lst cl nil)
                                   (owned-vars 'eliminate-destructors-clause t
                                               hist))
                                  (owned-vars 'eliminate-destructors-clause nil
                                              hist)
                                  (access rewrite-constant
                                          (access prove-spec-var
                                                  pspv
                                                  :rewrite-constant)
                                          :ens)
                                  wrld
                                  t
                                  *eliminate-destructors-nnn*)
   (cond (elim-vars (mv 'hit clauses
                        (list (cons :VARIABLES elim-vars))
                       pspv))
         (t (mv 'miss nil nil nil)))))