; expander.lisp  --  symbolic expansion utilities for ACL2
; Copyright (C) 1997  Computational Logic, Inc.

; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; Originally written by Matt Kaufmann at Computational Logic, Inc.
; Although some attempt has been made to bring it up to date with ACL2
; Release 2.0, this file should be viewed as a set of routines that
; may prove useful in using ACL2 but _not_ as code that can be trusted
; to the extent that the ACL2 system prover may be trusted.  For example,
; SYMSIM currently (8/97) does at best a minimimally adequate job
; of reporting when it has left unproved some forced assumptions.

; The top-level routines have documentation strings.  They are: SYMSIM
; and DEFTHM?.  Macro SYMSIM-FOR-VALUE may have value for some users
; as well.

; To certify this book:
; (certify-book "expander").

(in-package "ACL2")

; The following deflabel is placed here primarily to provide a section in which
; to hang documentation.
(deflabel expander :doc
 ":Doc-Section Expander

  routines for simplifying terms~/

  The routines provided by the expander can be useful in generating
  theorems and simplifying expressions, under given assumptions.~/

  They were developed rather in a hurry and should be used without
  expecting the usual standards of care present in development of ACL2
  code.  Once these routines are used to generate theorems for you,
  you should check the theorems directly with ACL2.~/")

; We know what we are doing when using state:
(set-state-ok t)

(encapsulate
 ((hidden-expander-function (x) t))
 (logic)
 (local (defun hidden-expander-function (x) x)))

(defun silly-rec-fn-for-rewrite* (x)
  (if (consp x)
      (silly-rec-fn-for-rewrite* (cdr x))
    x))

(verify-guards silly-rec-fn-for-rewrite*)

(program)

#|
At one time, I wrote an email message explaining tool1 and tool2 as
follows.  I don't know if these descriptions are still applicable.

Tool 1: Takes a list of hypotheses and some hints and returns a
simplified version, as a list of clauses.  Also returns a list of all
runes used.

Tool 2: Takes a term and a list of hypotheses, together with some
hints, and returns a term that is the result of rewriting the term
under those hypotheses, using those hints.  Note that the hypotheses
are used to build a context, using forward chaining and probably
linear arithmetic as well, but are not simplified.  This tool also
sends back list of runes.

By the way, I imagine that the hints for Tool 1 look like ordinary
prover hints, but for Tool 2 they look like what we usually associate
with "Goal", since there are no subgoals generated by Tool 2.
|#

(defmacro tool1 (hyps &key hints (prove-assumptions 't) inhibit-output)
  `(er-progn (tool1-fn ',hyps state ',hints ',prove-assumptions
                       ',inhibit-output
                       t t)
             (value :invisible)))

(defun pop-clauses (pool)
  (mv-let (signal pool-lst cl-set hint-settings pop-history new-pool)
          (pop-clause1 pool nil)
          (declare (ignore pool-lst hint-settings pop-history))
          (cond
           ((or (eq signal 'win) (eq signal 'lose))
            (mv signal cl-set))
           (t
            (mv-let (signal rest-clauses)
                    (pop-clauses new-pool)
                    (cond
                     ((eq signal 'win) (mv 'win (append cl-set rest-clauses)))
                     (t (mv signal nil))))))))

(defun prove-loop1-clauses (pool-lst clauses pspv hints wrld ctx state)

; Based on prove-loop1, except returns (mv erp ttree clauses pairs
; new-pspv state), where pairs is a list of pairs (assumnotes
; . clause), suitable for the third argument of prove-loop1 starting
; with forcing round 1.

  (mv-let (erp pspv jppl-flg state)
          (waterfall 0 pool-lst clauses pspv hints wrld ctx state)
          (declare (ignore jppl-flg))
          (cond
           (erp (mv t nil nil nil nil state))
           (t
            (mv-let
             (signal new-clauses)
             (pop-clauses (access prove-spec-var pspv :pool))
             (cond
              ((eq signal 'lose)
               (mv t nil nil nil nil state))
              (t
               (mv-let
                (pairs new-pspv state)

; Forcing round...

                (process-assumptions 0 pspv wrld state)
                (mv-let
                 (erp ttree state)
                 (accumulate-ttree-into-state
                  (access prove-spec-var new-pspv :tag-tree)
                  state)
                 (cond
                  (erp (mv nil nil nil nil nil state))
                  (t (mv nil ttree new-clauses pairs new-pspv
			 state))))))))))))

(defun prove-loop-clauses (clauses pspv hints wrld ctx state)

; We either cause an error or return a ttree.  If the ttree contains
; :byes, the proof attempt has technically failed, although it has
; succeeded modulo the :byes.

  (pprogn
   (increment-timer 'other-time state)
   (mv-let (erp ttree new-clauses pairs new-pspv state)
           (prove-loop1-clauses nil
                                clauses
                                pspv
                                hints wrld ctx state)
           (pprogn
            (increment-timer 'prove-time state)
            (cond
             (erp (mv erp nil nil nil nil state))
             (t (mv nil ttree new-clauses pairs new-pspv state)))))))

(defun prove-clauses (term pspv hints wrld ctx state)

; Adapted from prove.

  (prog2$
   (initialize-brr-stack state)
   (mv-let (erp ttree1 clauses pairs new-pspv state)
           (prove-loop-clauses (list (list term))
                               (change prove-spec-var pspv
                                       :user-supplied-term term
                                       :orig-hints hints)
                               hints wrld ctx state)
           (cond
            (erp (mv t nil nil nil nil state))
            (t
             (mv-let
              (erp val state)
              (chk-assumption-free-ttree ttree1 ctx state)
              (declare (ignore val))
              (cond
               (erp (mv t nil nil nil nil state))
               (t (pprogn
                   (cond
                    ((tagged-object :bye ttree1)
                     (let ((byes (reverse (tagged-objects :bye ttree1
							  nil))))
                       (pprogn

; The use of ~*1 below instead of just ~&1 forces each of the defthm
; forms to come out on a new line indented 5 spaces.  As is already
; known with ~&1, it can tend to scatter the items randomly -- some on
; the left margin and others indented -- depending on where each item
; fits flat on the line first offered.

                        (io? prove nil state
                             (wrld byes)
                             (fms "To complete this proof you should try to ~
                                   admit the following ~
                                   event~#0~[~/s~]~|~%~*1~%See the discussion ~
                                   of :by hints in :DOC hints regarding the ~
                                   name~#0~[~/s~] displayed above."
                                  (list (cons #\0 byes)
                                        (cons #\1
                                              (list ""
                                                    "~|~     ~q*."
                                                    "~|~     ~q*,~|and~|"
                                                    "~|~     ~q*,~|~%" 
                                                   
						    (make-defthm-forms-for-byes
                                                     byes wrld))))
                                  (proofs-co state)
                                  state
                                  nil))
                        state)))
                    (t state))
                   (mv erp ttree1 clauses pairs
                       (change prove-spec-var new-pspv
                               :pool nil)
                       state))))))))))

(defun chk-for-hidden-expander-function1 (cl)
  (let ((term (car (last cl))))
    (case-match term
                (('hide ('hidden-expander-function &))
                 term)
                (t
                 (er hard 'remove-hidden-expander-function
                     "Expected clause to end with hidden call of ~
                      HIDDEN-EXPANDER-FUNCTION, but instead clause is ~p0."
                     cl)))))

(defun chk-for-hidden-expander-function (clauses)
  (cond ((null clauses) nil)
        (t (and (chk-for-hidden-expander-function1 (car clauses))
                (chk-for-hidden-expander-function (cdr clauses))))))

(defun untranslate-clause-lst (cl-lst wrld)
  (cond
   ((null cl-lst)
    nil)
   (t
    (cons (prettyify-clause1 (car cl-lst) wrld)
          (untranslate-clause-lst (cdr cl-lst) wrld)))))

(defun tool1-print (print-flg runes clauses state)
  (cond
   (print-flg
    (fms "~%***OUTPUT OF TOOL1***~%~%Tag tree:~%  ~p0~%~%List of simplified ~
          hypotheses:~%  ~p1~|~%"
         (list (cons #\0 runes)
               (cons #\1
                     (untranslate-clause-lst clauses (w state))))
         *standard-co* state nil))
   (t state)))

(defun hide-special-hyps (lst)
  "We do this stuff so that equalities and SYNP hyps won't be thrown out.
   Perhaps what we really need is a hyp simplifier with less aggressive
   heuristics." 
  (cond
   ((null lst) nil)
   (t (let ((hyp (car lst)))
        (let ((new-hyp
               (case-match hyp
		 (('equal x y)
		  (let ((x1 (if (variablep x)
				(list 'hide x)
			      x))
			(y1 (if (variablep y)
				(list 'hide y)
			      y)))
		    (list 'equal x1 y1)))
		 (('synp . x) (list 'hide (cons 'synp x)))
		 (& hyp))))
          (cons new-hyp (hide-special-hyps (cdr lst))))))))

(defun fix-special-hyps (lst)
  (cond
   ((null lst) nil)
   (t (let ((hyp (car lst)))
        (let ((new-hyp
               (case-match hyp
                           (('not ('equal ('hide x) ('hide y)))
                            (list 'not (list 'equal x y)))
                           (('not ('equal ('hide x) y))
                            (list 'not (list 'equal x y)))
                           (('not ('equal y ('hide x)))
                            (list 'not (list 'equal y x)))
			   (('not ('hide ('synp . x)))
			    (list 'not (cons 'synp x)))
                           (& hyp))))
          (cons new-hyp (fix-special-hyps (cdr lst))))))))

(defun remove-hidden-terms (cl-set)
  (cond
   ((null cl-set)
    nil)
   (t (cons (fix-special-hyps (butlast (car cl-set) 1))
            (remove-hidden-terms (cdr cl-set))))))

(defun add-key-val-pair-to-key-val-alist (key key1 val alist)
  ;; adapted from ACL2 function add-to-set-equal-in-alist
  (cond ((null alist) (list (list key key1 val)))
        ((equal key (caar alist))
         (cons (list* key key1 val (cdar alist))
               (cdr alist)))
        (t (cons (car alist)
                 (add-key-val-pair-to-key-val-alist key key1 val (cdr
								  alist))))))

(defun tool1-fn (hyps state hints prove-assumptions inhibit-output
                      translate-flg print-flg)

; returns error triple with value (cons runes clauses)

  (with-ctx-summarized
   "( TOOL1 ...)"
   (let ((wrld (w state)))
     (er-let* ((hints (if (alistp hints)
                          (value (add-key-val-pair-to-key-val-alist
                                  "Goal"
                                  ;; only preprocess and simplify are allowed 
                                  :do-not
                                  (list 'quote '(generalize
                                                 eliminate-destructors
                                                 fertilize
                                                 eliminate-irrelevance))
                                  hints))
                        (er soft ctx
                            "The hints must be an alist, but ~p0 is not."
                            hints)))
               (thints (translate-hints 'tool1 hints ctx wrld state))
               (thyps0
                (if translate-flg
                    (translate-term-lst hyps t t t ctx wrld state)
                  (value hyps)))
               (thyps
                (value (hide-special-hyps thyps0)))
               (vars
                (value (all-vars1-lst thyps nil)))
               (tconc
                (translate (list 'hide
                                 (list 'hidden-expander-function

; overkill?

                                       (cons 'list vars)))
                           t t t  ctx wrld state))
               (tterm (value (implicate (conjoin thyps) tconc))))
              (state-global-let*
               ((ld-skip-proofsp nil)
                (inhibit-output-lst
                 (if inhibit-output
                     (union-eq '(proof-tree prove) (@ inhibit-output-lst))
                   (@ inhibit-output-lst))))
               (mv-let
                (erp ttree clauses pairs new-pspv state)
                (prove-clauses tterm
                               (make-pspv wrld
                                          :displayed-goal
                                          (untranslate tterm t wrld)
                                          :otf-flg t)
                               thints wrld ctx state)
                (prog2$
                 (chk-for-hidden-expander-function clauses)
                 (cond
                  (erp
                   (mv erp nil state))
                  (prove-assumptions
                   (er-let* ((thints
                              (if (eq prove-assumptions t)
                                  (value thints)
                                (translate-hints 'tool1
						 *bash-skip-forcing-round-hints*
                                                 ctx wrld state))))
                            (state-global-let*
                             ((inhibit-output-lst
                               (if (eq prove-assumptions t)
                                   (@ inhibit-output-lst)
                                 (remove1-eq 'prove (@
						     inhibit-output-lst)))))
                             (er-let*
                              ((new-ttree
                                (prove-loop1 1 nil pairs new-pspv
                                             thints wrld ctx state)))
                              (let ((runes (all-runes-in-ttree
                                            new-ttree
                                            (all-runes-in-ttree ttree nil))))
                                (pprogn
                                 (tool1-print print-flg runes clauses state)
                                 (value (cons runes
                                              (dumb-negate-lit-lst-lst
                                               (remove-hidden-terms clauses))))))))))
                  (t (let ((runes (all-runes-in-ttree ttree nil)))
                       (pprogn
                        (tool1-print print-flg runes clauses state)
                        (value (cons runes
                                     (dumb-negate-lit-lst-lst
                                      (remove-hidden-terms clauses)))))))))))))))

;;;;;;; Tool 2

(defmacro tool2 (term hyps &key hints equiv (prove-assumptions 't)
inhibit-output)
  `(er-progn (tool2-fn ',term ',hyps ',equiv state ',hints ',prove-assumptions
                       ',inhibit-output t t)
             (value :invisible)))

(defun tool2-print (print-flg runes rewritten-term state)
  (cond
   (print-flg
    (fms "~%***OUTPUT OF TOOL2***~%~%Tag tree:~%  ~p0~%~%Rewritten term:~% ~
          ~p1~|~%"
         (list (cons #\0 runes)
               (cons #\1 (untranslate rewritten-term nil (w state))))
         *standard-co* state nil))
   (t state)))

(defun expander-repeat-limit (state)
  (if (f-boundp-global 'expander-repeat-limit state)
      (f-get-global 'expander-repeat-limit state)
    3))

(defun rewrite* (term hyps ctx
                      repeat-limit
                      completed-iterations
                      ;; alist bkptr
                      ;; &extra formals
                      type-alist
                      ;; obj
                      geneqv wrld state
                      ;; fnstack ancestors
                      simplify-clause-pot-lst
                      rcnst gstack ttree)

; hyps is T after the first time through

  (mv-let (val new-ttree)
          (rewrite-entry (rewrite term nil 1)
                         :obj '?
                         :fnstack 
; We want to fool rewrite-fncall on lambdas.
                         '(silly-rec-fn-for-rewrite*)
                         :pre-dwp nil  ;; RBK:
                         :ancestors nil
                         :backchain-limit 500
                         :rdepth (rewrite-stack-limit wrld))
          (cond
           ((equal val term)
            (cond
             ((eq hyps t)
              (mv term ttree state))
             (t (er soft ctx
                    "The term~%  ~p0~%failed to rewrite to a new term under ~
                     hypotheses~%  ~p1."
                    (untranslate val nil wrld)
                    (untranslate-lst hyps t wrld)))))
           ((= repeat-limit completed-iterations)
            (pprogn
             (fms "OUT OF PATIENCE!  Completed ~n0 iterations."
                  (list (cons #\0 (list completed-iterations)))
                  *standard-co* state nil)
             (mv val new-ttree state)))
           (t (pprogn (fms "NOTE:  Starting ~n0 repetition of rewrite.~%"
                           (list (cons #\0 (list (1+ completed-iterations))))
                           *standard-co* state nil)
                      (rewrite* val t ctx
                                repeat-limit
                                (1+ completed-iterations)
                                type-alist geneqv wrld state
                                simplify-clause-pot-lst rcnst gstack
                                new-ttree))))))

(defun tool2-fn
  (term hyps equiv state hints prove-assumptions inhibit-output translate-flg
        print-flg)

; returns error triple with value (cons runes rewritten-term)

  (let ((ctx 'TOOL2))
    (prog2$
     (initialize-brr-stack state)
     (er-let*
      ((wrld (value (w state)))
       (thints (translate-hints 'tool2 hints ctx wrld state)))
      (let ((ens (ens state))
	    (saved-pspv (make-pspv wrld
				   :displayed-goal term ; from, e.g., thm-fn
				   :user-supplied-term term ;from, e.g., prove
				   :orig-hints thints))) ;from, e.g., prove
	(er-let*
	 ((thyps (if translate-flg
		     (translate-term-lst hyps t t t ctx wrld state)
		   (value hyps)))
	  (tterm (if translate-flg
		     (translate term t t t ctx wrld state)
		   (value term))))
	 (mv-let			;from waterfall1
	   (erp pair state)
	   (find-applicable-hint-settings
	    *initial-clause-id*
	    (add-literal tterm (dumb-negate-lit-lst thyps) t)
            nil saved-pspv ctx
	    thints thints wrld nil state)
	   (cond
	    (erp (silent-error state))
	    (t (let ((hint-settings (car pair))
		     (thints (cdr pair)))
	    (pprogn
	    (cond ((null hint-settings)
		   state)
		  (t (thanks-for-the-hint nil state))) ;BB
	    (let ((pspv (load-hint-settings-into-pspv
			 t hint-settings saved-pspv wrld)))
	      (cond
	       ((intersectp-eq
		 '(:do-not-induct :do-not :induct :use :cases :by)
		 (strip-cars hint-settings))
		(er soft ctx
		    "It makes no sense for TOOL2 to be given hints for ~
                     \"Goal\" that include any of :do-not-induct, :do-not,~
                     :induct, :use, :cases, or :by.  The hint ~p0 is therefore ~
                     illegal."
		    (cons "Goal" hint-settings)))
	       (t
		(state-global-let*
		 ((inhibit-output-lst
		   (if inhibit-output
		       (union-eq '(proof-tree prove) (@ inhibit-output-lst))
		     (@ inhibit-output-lst)))
		  (old-style-forcing nil))
		 (pprogn
		  (initialize-proof-tree ;from waterfall
		   *initial-clause-id*
		   (list (list (implicate (conjoin thyps) tterm)))
		   ctx
		   state)
		  (let*			;from simplify-clause1
		    ((current-clause (dumb-negate-lit-lst thyps))
		     (rcnst
		      (change rewrite-constant
			      (access prove-spec-var pspv :rewrite-constant)
			      :force-info
			      (if (ffnnamep-lst 'if current-clause)
				  'weak
				t)))
		     (pts 
		      ;; (current-clause-pts (enumerate-elements current-clause 0))
		      nil))
		    (mv-let		;from simplify-clause1
		      (contradictionp type-alist fc-pair-lst)
		      (forward-chain current-clause
				     pts
				     (access rewrite-constant
					     rcnst :force-info)
				     nil wrld ens
                                     (access rewrite-constant rcnst
                                             :oncep-override)
                                     state)
		      (declare (ignore fc-pair-lst))
		      (cond
		       (contradictionp
			(er soft ctx
			    "Contradiction found in hypotheses~%  ~p0~%using ~
                              type-set reasoning!"
			    hyps))
		       (t
			(mv-let		;from simplify-clause1
			  (contradictionp simplify-clause-pot-lst)
			  (setup-simplify-clause-pot-lst current-clause
							 (pts-to-ttree-lst 
                                                          pts)
                                                         nil ; fc-pair-lst  ;; RBK:
							 type-alist
							 rcnst
							 wrld state)
			  (cond
			   (contradictionp
			    (er soft ctx
				"Contradiction found in hypotheses~%  ~
                                 ~p0~%using linear reasoning!"
				hyps))
			   (t

; We skip the call of process-equational-polys in simplify-clause1; I think
; that we can assume that by the time tool2 is called, that call wouldn't have
; any effect anyhow.  By the way, we skipped remove-trivial-equivalence
; earlier.

; Now we continue as in rewrite-clause.

			    (mv-let
			      (not-flg atm)
			      (strip-not tterm)
			      (let ((local-rcnst
				     (change rewrite-constant rcnst
					     :current-literal
					     (make current-literal
						   :not-flg not-flg
						   :atm atm)))
				    (gstack (initial-gstack 'simplify-clause
							    nil current-clause)))
				(mv-let
				  (val ttree state)
				  (rewrite* atm hyps ctx
					    (expander-repeat-limit state)
					    0
					    type-alist
					    (cadr (car (last (getprop
							      equiv
							      'congruences
							      nil
							      'current-acl2-world
							      wrld))))
					    wrld state
					    simplify-clause-pot-lst rcnst gstack
					    nil)
				  (cond
				   ((equal val t)
				    (mv t nil state))
				   (t
				    (mv-let
				      (bad-ass ttree)
				      (resume-suspended-assumption-rewriting
				       ttree
				       nil
				       gstack
				       simplify-clause-pot-lst
				       local-rcnst
				       wrld
				       state)
				      (cond
				       (bad-ass
					(er soft ctx
					    "Generated false assumption, ~p0!  So, ~
                                      rewriting is aborted, just as it would ~
                                      be in the course of a regular Acl2 proof."
					    bad-ass))
				       (t
					(let ((rewritten-term
					       (if not-flg
						   (dumb-negate-lit val)
						 val)))
					  (cond
					   (prove-assumptions
					    (mv-let
					      (pairs pspv state)
					      (process-assumptions
					       0
					       (change prove-spec-var saved-pspv
						       :tag-tree
						       (set-cl-ids-of-assumptions
							ttree *initial-clause-id*))
					       wrld state)
					      (er-let*
					       ((ttree
						 (accumulate-ttree-into-state
						  (access prove-spec-var pspv :tag-tree)
						  state))
						(thints
						 (if (eq prove-assumptions t)
						     (value thints)
						   (translate-hints 'tool2
								    *bash-skip-forcing-round-hints*
								    ctx wrld state))))
					       (er-progn
						(state-global-let*
						 ((inhibit-output-lst
						   (if (eq prove-assumptions t)
						       (@ inhibit-output-lst)
						     (remove1-eq 'prove (@ inhibit-output-lst)))))
						 (er-let*
						  ((new-ttree
						    (prove-loop1 1 nil pairs pspv
								 thints wrld ctx state)))
						  (let ((runes
							 (all-runes-in-ttree
							  new-ttree
							  (all-runes-in-ttree ttree nil))))
						    (pprogn (tool2-print print-flg runes
									 rewritten-term state)
							    (f-put-global 'tool2-error
									  nil state)
							    (f-put-global
							     'tool2-result
							     (cons runes rewritten-term)
							     state)
							    (value (cons runes rewritten-term))))))))))
					   (t (let ((runes (all-runes-in-ttree ttree
									       nil)))
						(pprogn
						 (tool2-print print-flg runes
							      rewritten-term
							      state)
						 (f-put-global 'tool2-error
							       nil state)
						 (f-put-global
						  'tool2-result
						  (cons runes rewritten-term)
						  state)
						 (value (cons runes rewritten-term))))))))))))))))))))))))))))))))))))))

;;;;;;; Hooking them together

(defun tool2-fn-lst
  (term runes hyps-lst equiv state hints prove-assumptions inhibit-output
	print-flg)

; Returns the result of mapping tool2-fn over the list hyps-lst, pairing each
; result with the corresponding member of hyps-lst.  Assumes hyps-lst is
; already translated.  The value returned is actually a list of triples
; (list* runes hyps rewritten-term).

  (cond
   ((null hyps-lst)
    (value nil))
   (t
    (mv-let
     (erp x state)
     (tool2-fn term (car hyps-lst) equiv state hints prove-assumptions
               inhibit-output nil print-flg)
     (cond
      (erp
       (tool2-fn-lst term runes (cdr hyps-lst) equiv state
                     hints prove-assumptions inhibit-output print-flg))
      (t
       (er-let*
        ((rst (tool2-fn-lst term runes (cdr hyps-lst) equiv state
                            hints prove-assumptions inhibit-output print-flg)))
        (value (cons (list* (union-equal runes (car x)) (car hyps-lst) (cdr x))
                     rst)))))))))

(defun tool-fn
  (term hyps equiv state hints prove-assumptions inhibit-output print-flg ctx)
  ;; term and hyps are already translated
  (er-let* ((runes-hyps-lst (tool1-fn hyps state hints prove-assumptions
                                      inhibit-output nil print-flg)))
           (cond
            ((null (cdr runes-hyps-lst))
             (er soft ctx
                 "It does not make sense to simplify the term ~p0, because the ~
                  hypothesis list ~p1 is contradictory."
                 (untranslate term nil (w state))
                 (untranslate-lst hyps t (w state))))
            (t
             (pprogn
              (cond (print-flg
                     (fms "***NOTE***:  Starting TOOL2.~%" nil *standard-co* state nil))
                    (t state))
              (er-let*
               ((x (tool2-fn-lst term (car runes-hyps-lst) (cdr runes-hyps-lst)
                                 equiv state hints prove-assumptions
                                 inhibit-output print-flg)))
               (cond
                ((not (= (length x) (length (cdr runes-hyps-lst))))
                 (er soft ctx
                     "Unable to successfully simplify term~%  ~p0~%and ~
                      hypotheses~%  ~p1 in every case generated."
                     (untranslate term nil (w state))
                     (untranslate-lst hyps t (w state))))
                (x (value x))
                (t (er soft ctx
                       "No theorems were suggested for term~%  ~p0~%and ~
                        hypotheses~%  ~p1.")))))))))

(defmacro defthm?
  (name term &key hints (prove-assumptions 't) print-flg)

  ":Doc-Section Expander

  generate a theorem~/
  ~bv[]
  Example:
  (defthm? app-simplify
    (implies (true-listp x)
	     (equal (append x y)
		    ?))
    :hints ((\"Goal\" :expand ((true-listp x)
			     (true-listp (cdr x))
			     (append x y))))
    ; show some output
    :print-flg t)
  ~ev[]~/

  General Forms:
  (DEFTHM? name
    (IMPLIES hyps (equiv term ?))
    :hints             hints
    :prove-assumptions prove-flg ; t or nil, default t
    :print-flg         print-flg ; t or nil, default nil
  )

  (DEFTHM? name
    (equiv term ?)
    :hints             hints
    :prove-assumptions prove-flg ; t or nil, default t
    :print-flg         print-flg ; t or nil, default nil
  )
  ~ev[]
  where ~c[name] is a new symbolic name (~pl[name]), ~c[term] is a
  term to be simplified assuming ~c[hyps] is true, and ~ilc[hints] is
  as described in its ~il[documentation].  The three keyword arguments
  above are all optional.

  If the given ~c[term] cannot be simplified, then the event fails.
  Otherwise, the result is an ~ilc[encapsulate] event with one or more
  ~ilc[defthm] events of the form of the theorem, except with ~c[hyps]
  simplified (and even omitted if simplified to ~c[t]) and ~c[term]
  simplified under the assumption that ~c[hyps] is true.  The reason
  that there can be more than one ~ilc[defthm] event is that ~c[hyps] may
  simplify to an expression that generates a case split, for example
  if it simplifies to an ~ilc[if] expression that does not represent a
  conjunction.

  In general, simplification may generate assumptions because of
  ~ilc[force].  By default, an attempt is made to prove these
  assumptions, which must succeed or else this event fails.  However,
  if ~c[:prove-assumptions] is ~c[nil], then roughly speaking, no
  proof of forced hypotheses is attempted until after simplification
  is complete.  The documentation of :prove-assumptions is admittedly
  weak here; feel free to experiment.

  Also ~pl[symsim].

  Here are some examples, including the one above.  Try them out and
  see what happens.
  ~bv[]

  ; Doesn't simplify, so fails:
  (defthm? app-simplify
    (implies (true-listp x)
             (equal (append x y)
                    ?))
    :hints ((\"Goal\" :expand (true-listp x))))

  :pbt 0

  ; The following creates one event, but maybe we'd prefer cases to be
  ; broken out into separate events.  That comes next.
  (defthm? app-simplify
    (implies (true-listp x)
             (equal (append x y)
                    ?))
    :hints ((\"Goal\" :expand (append x y))))

  :pbt 0
  :pe :here
  :pe APP-SIMPLIFY
  :u

  (defthm? app-simplify
    (implies (true-listp x)
             (equal (append x y)
                    ?))
    :hints ((\"Goal\" :expand ((true-listp x)
                             (true-listp (cdr x))
                             (append x y))))
    ; show some extra output; this is optional
    :print-flg t)

  :pe :here
  :u
  ~ev[]~/"

  `(defthm?-fn ',name ',term ',hints ',prove-assumptions
     ',print-flg (w state) state))

; This is new in 8/97.  If we don't include executable counterparts of some
; functions, one of the examples in the documentation fails to simplify.
; Try the following.  If you define *adjust-hints-exec-theory* to be nil
; instead, the defthm? will still fail, but it will get more stuck in the
; final proof attempt than it should.
#|
(defthm true-listp-expand-append
  (implies (and (force (true-listp x))
                x)
           (equal (append x y)
                  (cons (car x) (append (cdr x) y)))))
(defthm? foo (implies (consp x) (equal (append X Y) ?))
  :prove-assumptions nil)
|#
(defconst *adjust-hints-exec-theory*
  '(definition-runes
     (union-eq '(iff) *expandable-boot-strap-non-rec-fns*)
     t
     world))

(defun adjust-hints-with-runes1 (hint runes)

; hint is an alternating list of keywords and hints, e.g.,
; (:expand (foo x) :in-theory *s-prop-theory*)

  (cond
   ((null hint)
    (list :in-theory
          (list 'union-theories
                *adjust-hints-exec-theory*
                (list 'quote runes))))
   ((eq (car hint) :in-theory)
    (list* :in-theory
           (list 'union-theories
                 *adjust-hints-exec-theory*
                 `(intersection-theories ',runes ,(cadr hint)))
           (cddr hint)))
   (t
    (list* (car hint)
           (cadr hint)
           (adjust-hints-with-runes1 (cddr hint) runes)))))

(defun adjust-hints-with-runes (hints runes top-goal-seen-p)

; We know that only runes were used in the proof, and we want to adjust hints
; correspondingly.

  (cond
   ((null hints)
    (if top-goal-seen-p
        nil
      `(("Goal" :in-theory (union-theories
                            ,*adjust-hints-exec-theory*
                            ',runes)))))
   (t (cons (cons (caar hints) (adjust-hints-with-runes1 (cdar hints) runes))
            (adjust-hints-with-runes (cdr hints) runes
                                     (or top-goal-seen-p
                                         (equal (caar hints) "Goal")))))))

(defconst *fake-runes*
  (list *fake-rune-for-anonymous-enabled-rule*
        *fake-rune-for-type-set*
        *fake-rune-for-linear*))

(defun defthm-?-fn-forms1-lst (name index x equiv lhs hints wrld)

; x is from the output of tool-fn:  a list of elements of the form
; (list* runes hyps rewritten-term)
; If there is only one lemma, it has the name <name>, else we create
; <name>$0, ... <name>$n etc.

  (cond
   ((null x)
    nil)
   (t (let ((runes (set-difference-equal (car (car x))
                                         *fake-runes*))
            (hyps (cadr (car x)))
            (rhs (cddr (car x))))
        (cons `(defthm
		 ,(if (and (zerop index) (null (cdr x)))
		      name
		    (packn (list name '$ index)))
                 ,(untranslate (implicate (conjoin hyps) (fcons-term* equiv lhs rhs))
                               t wrld)
                 :hints ,(adjust-hints-with-runes hints runes nil))
              (defthm-?-fn-forms1-lst name (1+ index) (cdr x) equiv lhs hints wrld))))))

(defun defthm?-fn-forms
  (name form hints prove-assumptions inhibit-output print-flg wrld state)
  (with-ctx-summarized
   (cons 'defthm? name)
   (er-let*
    ((tform (translate form t t t ctx wrld state)))
    (let* ((x (unprettyify tform))
           (hyps (car (car x)))
           (concl (cdr (car x))))
      (cond
       ((and (null (cdr x))
             (not (variablep concl))
             (not (fquotep concl))
             (variablep (fargn concl 2)))
        (cond
         ((equivalence-relationp (ffn-symb concl) wrld)
          (er-let*
           ((x (tool-fn (fargn concl 1) hyps (ffn-symb concl) state
                        hints prove-assumptions inhibit-output print-flg ctx)))
           (value (defthm-?-fn-forms1-lst name 0 x (ffn-symb concl)
                    (fargn concl 1) hints wrld))))
         (t (er soft ctx
                "The form supplied to DEFTHM? must be of the form ~p0 or ~p1, ~
                 where equiv is an equivalence relation.  However, ~p2 is not ~
                 an equivalence relation in the current world."
                '(implies hyps (equiv lhs var))
                '(equiv lhs var)
                (ffn-symb concl)))))
       (t (er soft ctx
              "The form supplied to DEFTHM? must be of the form ~p0 or ~p1,~
               where var is a variable.  But ~p2 is not of this form."
              '(implies hyps (equiv lhs var))
              '(equiv lhs var)
              form)))))))

(defun defthm?-fn
  (name term hints prove-assumptions print-flg wrld state)
  (state-global-let*
   ((inhibit-output-lst
     (if (boundp-global 'defthm?-inhibit-output-lst state)
; Suggestion:  '(warning observation prove event summary proof-tree)
         (f-get-global 'defthm?-inhibit-output-lst state)
       (@ inhibit-output-lst)))
    (ld-pre-eval-print nil)
    (ld-prompt nil))
   (er-let* ((forms (defthm?-fn-forms name term hints prove-assumptions
                      nil print-flg wrld state)))
            (er-progn (encapsulate-fn nil (cons '(logic) forms) state nil)
                      (value (list* 'encapsulate () forms))))))

(defmacro symsim
  (term hyps &key hints prove-assumptions (inhibit-output 't) print-flg)

  ":Doc-Section Expander

  simplify given term and hypotheses~/
  ~bv[]
  Example:

  (symsim (append x y)
          ((not (atom x)) (not (cdr x)))
          :hints ((\"Goal\" :expand
                   ((true-listp x)
                    (true-listp (cdr x))
                    (append x y)))))
  ~ev[]
  yields
  ~bv[]
  Simplified term:
    (CONS (CAR X) Y)
  Simplified hyps:
   ((CONSP X) (NOT (CDR X)))~/

  General Form:
  (symsim term hyps
          :hints             hints
          :inhibit-output    inhibit-flg ; t or nil, default t
          :prove-assumptions prove-flg   ; t or nil, default nil
          :print-flg         print-flg   ; t or nil, default nil
  )
  ~ev[]
  where ~c[term] is a term to be simplified assuming that each ~c[hyp]
  in the list ~c[hyps] is true, and ~ilc[hints] is as described in its
  ~il[documentation].  The keyword arguments above are all optional.

  Also ~pl[defthm?], which has a related functionality and is a

  bit more thoroughly documented.  Here are some examples that should
  help give an idea of how ~c[symsim] works.  (The name, by the way,
  is short for \"symbolically simulate\".)  Try these, as well as the
  examples shown above.
  ~bv[]

  (symsim (append x y)
          nil
          :hints ((\"Goal\" :expand
                   ((true-listp x)
                    (append x y)
                    (append (cdr x) y)))))

  ; Fails because several cases are generated.
  (symsim (APPEND X Y)
          ((true-listp x))
          :hints ((\"Goal\" :expand
                   ((true-listp x)
                    (true-listp (cdr x))
                    (append x y)
                    (append (cdr x) y)))))

  ; Let's illustrate the role of FORCE.  The following rule
  ; forces append to open up, and comes into play below.
  (defthm true-listp-expand-append
    (implies (and (force (true-listp x))
                  x)
             (equal (append x y)
                    (cons (car x) (append (cdr x) y)))))

  ; No problem
  (symsim (APPEND X Y)
          ((NOT (ATOM X))))

  ; But now we fail; but why?  See next form.
  (symsim (APPEND X Y)
          ((CONSP X))
          :prove-assumptions t)

  ; Let's not inhibit output.  Then we can see the failed forcing round.
  (symsim (APPEND X Y)
          ((CONSP X))
          :prove-assumptions t
          :inhibit-output nil)

  ; Succeds, and warns of the forced goals (whose proof is not attempted).
  (symsim (APPEND X Y)
          ((CONSP X))
          :prove-assumptions warn)
  ~ev[]"

  `(symsim-fn ',term ',hyps ',hints ',prove-assumptions ',inhibit-output
              ',print-flg (w state) state))

(defun symsim-fn
  (term hyps hints prove-assumptions inhibit-output print-flg wrld state)
  (er-let*
   ((tterm (translate term t t t 'top-level wrld state))
    (thyps (translate-term-lst hyps t t t 'top-level wrld state))
    (triples-lst
     ;; list of triples of the form (list* runes hyps rewritten-term)
     (tool-fn tterm thyps 'equal state
              hints prove-assumptions
              inhibit-output
              print-flg (cons 'symsim-fn term))))
   (pprogn (cond
            ((= (length triples-lst) 1)
             (fms "Simplified term:~%  ~p0~%Simplified hyps:~% ~p1~%Runes:~%  ~p2~%"
                  (list (cons #\0 (untranslate (cddr (car triples-lst)) nil wrld))
                        (cons #\1 (untranslate-lst (cadr (car triples-lst)) t wrld))
                        (cons #\2 (car (car triples-lst))))
                  *standard-co* state nil))
            (t
             (fms "Sorry; we got ~n0 clauses, but we need one here.~%"
                  (list (cons #\0 (length triples-lst)))
                  *standard-co* state nil)))
           (value :invisible))))


; Presumably Bishop Brock found symsim-for-value to be useful at one time.
; I believe that it's intended to set some global variables rather than to
; print the simplification results to the screen.
(defmacro symsim-for-value
  (term hyps &key hints prove-assumptions (inhibit-output 't) print-flg)
  `(symsim-for-value-fn ',term ',hyps ',hints ',prove-assumptions
			',inhibit-output
			',print-flg (w state) state))

(defun symsim-for-value-fn
  (term hyps hints prove-assumptions inhibit-output print-flg wrld state)
  ;;  Set the error flag up front, and clear later if no error.
  (er-let*
   ((tterm (translate term t t t 'top-level wrld state))
    (thyps (translate-term-lst hyps t t t 'top-level wrld state))
    (triples-lst
     ;; list of triples of the form (list* runes hyps rewritten-term)
     (tool-fn tterm thyps 'equal state
	      hints prove-assumptions
	      inhibit-output
	      print-flg (cons 'symsim-fn term))))
   (pprogn
    (cond
     ((= (length triples-lst) 1)
      (pprogn
       (f-put-global 'symsim-for-value-error nil state)
       (f-put-global 'symsim-for-value-triple (car triples-lst) state)))
     (t (pprogn
	 (f-put-global 'symsim-for-value-error "Too many clauses" state)
	 (fms "Sorry; we got ~n0 clauses, but we need one here.~%"
	      (list (cons #\0 (length triples-lst)))
	      *standard-co* state nil))))
    (value :invisible))))