computed-hints

(defun rewriting-goal-lit
  (mfc state)
  (declare (xargs :stobjs state)
    (ignore state))
  (null (mfc-ancestors mfc)))

(defun rewriting-conc-lit
  (term mfc
    state)
  (declare (xargs :stobjs state)
    (ignore state))
  (let ((clause (mfc-clause mfc)))
    (member-equal term
      (last clause))))

(defun harvest-trigger
  (clause trigger-fn)
  (if (endp clause)
    nil
    (if (and (consp (car clause))
        (eq (caar clause)
          trigger-fn))
      (cons (car clause)
        (harvest-trigger (cdr clause)
          trigger-fn))
      (harvest-trigger (cdr clause)
        trigger-fn))))

(defun others-to-negated-list
  (others)
  (if (endp others)
    nil
    (if (and (consp (car others))
        (equal (caar others) 'not))
      (cons (second (car others))
        (others-to-negated-list (cdr others)))
      (cons (list 'not (car others))
        (others-to-negated-list (cdr others))))))

(defun others-to-hyps
  (others)
  (if (endp others)
    t
    (let ((negated (others-to-negated-list others)))
      (if (endp (cdr negated))
        (car negated)
        (cons 'and
          (others-to-negated-list others))))))

(defun build-hint
  (trigger generic-theorem
    generic-hyps
    generic-collection
    generic-predicate
    generic-collection-p
    collection-p-sub
    hyps-sub
    predicate-rewrite)
  (let* ((base-pred (cons generic-predicate
         (cons '?x (cddr trigger)))) (pred-sub (instance-rewrite base-pred
          predicate-rewrite)))
    `(:functional-instance ,COMPUTED-HINTS::GENERIC-THEOREM
      (,COMPUTED-HINTS::GENERIC-HYPS (lambda nil ,COMPUTED-HINTS::HYPS-SUB))
      (,COMPUTED-HINTS::GENERIC-COLLECTION (lambda nil ,(SECOND COMPUTED-HINTS::TRIGGER)))
      (,COMPUTED-HINTS::GENERIC-COLLECTION-P (lambda (?x)
          ,(CONS COMPUTED-HINTS::COLLECTION-P-SUB
       (CONS 'COMPUTED-HINTS::?X (CDDR COMPUTED-HINTS::TRIGGER)))))
      (,COMPUTED-HINTS::GENERIC-PREDICATE (lambda (?x) ,COMPUTED-HINTS::PRED-SUB)))))

(defun build-hints
  (triggers generic-theorem
    generic-hyps
    generic-collection
    generic-predicate
    generic-collection-p
    collection-p-sub
    hyps-sub
    predicate-rewrite)
  (if (endp triggers)
    nil
    (cons (build-hint (car triggers)
        generic-theorem
        generic-hyps
        generic-collection
        generic-predicate
        generic-collection-p
        collection-p-sub
        hyps-sub
        predicate-rewrite)
      (build-hints (cdr triggers)
        generic-theorem
        generic-hyps
        generic-collection
        generic-predicate
        generic-collection-p
        collection-p-sub
        hyps-sub
        predicate-rewrite))))

(defun automate-instantiation-fn
  (new-hint-name generic-theorem
    generic-hyps
    generic-collection
    generic-predicate
    generic-collection-p
    collection-p-sub
    predicate-rewrite
    trigger-symbol
    tagging-theorem)
  `(encapsulate nil
    (defun ,COMPUTED-HINTS::NEW-HINT-NAME
      (id clause
        world
        stable)
      (declare (xargs :mode :program)
        (ignore id world))
      (if (not stable)
        nil
        (let ((triggers (harvest-trigger clause
               ,COMPUTED-HINTS::TRIGGER-SYMBOL)))
          (if (not triggers)
            nil
            (let* ((others (set-difference-equal clause
                   triggers)) (hyps (others-to-hyps others))
                (fi-hints (build-hints triggers
                    ,COMPUTED-HINTS::GENERIC-THEOREM
                    ,COMPUTED-HINTS::GENERIC-HYPS
                    ,COMPUTED-HINTS::GENERIC-COLLECTION
                    ,COMPUTED-HINTS::GENERIC-PREDICATE
                    ,COMPUTED-HINTS::GENERIC-COLLECTION-P
                    ,COMPUTED-HINTS::COLLECTION-P-SUB
                    hyps
                    ,COMPUTED-HINTS::PREDICATE-REWRITE))
                (hints (list :use fi-hints
                    :expand triggers)))
              (prog2$ (cw "~|~%Attempting to discharge subgoal by a ~
                            pick-a-point strategy; disable ~x0 to ~
                            prevent this.~%~%"
                  ,COMPUTED-HINTS::TAGGING-THEOREM)
                hints))))))
    (add-default-hints! '((,COMPUTED-HINTS::NEW-HINT-NAME id
         clause
         world
         stable-under-simplificationp)))))