(in-package "ACL2")

; This is a fix for :pl and the proof-checker's show-rewrites (sr) command,
; ACL2 Version 3.0.1.

#|
; Example suggested by Eric Smith:

(defaxiom not-equal-hack
  (implies (and (member-eq y lst)
                (equal width 16))
           (not (equal x y))))

:pl (equal x y)
|# ; |

; Only if modifying source code: Move untranslate-subst-abb to
; other-events.lisp in front of show-rewrite, and change show-unify-subst to
; pl-p in all show-rewrite* fns.  But if source code is modified, then banner
; needs to be modified.

(defun meta-fn-args (term extendedp ens state)
  (cond
   (extendedp
    (list term
          (make metafunction-context 
                :type-alist nil
                :obj '?
                :geneqv nil
                :wrld (w state)
                :fnstack nil
                :ancestors nil
                :simplify-clause-pot-lst nil
                :rcnst
                (make-rcnst ens
                            (w state)
                            :force-info t
                            :top-clause (list term)
                            :current-clause (list term))
                :gstack nil
                :ttree nil)
          (coerce-state-to-object state)))
   (t (list term))))

(defun chk-meta-function (metafn name trigger-fns extendedp
                                 term-list ctx ens state)

; If extendedp is nil we call metafn on only one term arg.  Otherwise, we call
; it on args of the type: (term context state).  We manufacture a trivial
; context.  We don't care what non-nil value extendedp is.

  (cond
   ((null term-list)
    (value nil))
   ((or (variablep (car term-list))
        (fquotep (car term-list))
        (flambda-applicationp (car term-list))
        (not (member-eq (ffn-symb (car term-list)) trigger-fns)))
    (chk-meta-function metafn name trigger-fns extendedp
                       (cdr term-list) ctx ens state))
   (t
    (let ((args (meta-fn-args (car term-list) extendedp ens state)))
      (pprogn
       (cond
        ((warning-disabled-p "Meta")
         state)
        (t
         (mv-let (erp val latches)
                 (ev-fncall-meta metafn args state)
                 (declare (ignore latches))
                 (cond
                  (erp

; We use warnings rather than errors when the checks fail, partly so
; that we can feel free to change the checks without changing what the
; prover will accept.  Put differently, we don't want user-managed
; tables to affect what the prover is able to prove.

                   (warning$ ctx ("Meta")
                             "An error occurred upon running the metafunction ~
                              ~x0 on the term ~x1.  This does not bode well ~
                              for the utility of this metafunction for the ~
                              meta rule ~x2.  See :DOC term-table."
                             metafn (car term-list) name))
                  ((termp val (w state))
                   state)
                  (t
                   (warning$ ctx ("Meta")
                             "The value obtained upon running the ~
                              metafunction ~x0 on the term ~x1 is ~x2, which ~
                              is NOT a termp in the current ACL2 world.  This ~
                              does not bode well for the utility of this ~
                              metafunction for the meta rule ~x3.  See :DOC ~
                              term-table."
                             metafn (car term-list) val name))))))
       (chk-meta-function
        metafn name trigger-fns extendedp (cdr term-list) ctx ens state))))))

(defun show-rewrite (index col rune nume show-more subst-hyps subst-hyps-2
                           unify-subst unify-subst-2 free free-2 rhs
                           abbreviations term-id-iff ens enabled-only-flg
                           equiv pl-p state)

; Pl-p is true when we are calling this function on behalf of :pl, and is false
; when we are calling it on behalf of the proof-checker.

  (let ((enabledp (enabled-numep nume ens))
        (subst-rhs (sublis-var unify-subst rhs)))
    (if (and enabled-only-flg
             (not enabledp))
        state
      (pprogn
       (fms "~|~#a~[~c0. ~/  ~]~x1~#2~[~/ (disabled)~]"
            (list (cons #\a (if index 0 1))
                  (cons #\0 (cons index col))
                  (cons #\1
                        ;; Let's just print the name of the rune if it appears
                        ;; to be unique.
                        (if (cddr rune) rune (base-symbol rune)))
                  (cons #\2 (if enabledp 0 1)))
            (standard-co state) state nil)
       (let ((fmt-string
              "~ ~ New term: ~y3~|~
               ~ ~ Hypotheses: ~#b~[<none>~/~y4~]~|~
               ~ ~ Equiv: ~ye~|~
               ~#s~[~/~ ~ Substitution: ~ya~|~]~
               ~#5~[~/~
                    ~ ~ Remaining free variable: ~&6~/~
                    ~ ~ Remaining free variables: ~&6~sn~]~
               ~#7~[~/  WARNING:  One of the hypotheses is (equivalent to) NIL, ~
               and hence will apparently be impossible to relieve.~]~|"))
         (pprogn
          (cond
           ((and show-more pl-p) ; then just show more
            state)
           (t
            (fms fmt-string
                 (list (cons #\3 (untrans0 subst-rhs term-id-iff
                                           abbreviations))
                       (cons #\s (if pl-p 1 0))
                       (cons #\a (untranslate-subst-abb unify-subst
                                                        abbreviations
                                                        state))
                       (cons #\b (if subst-hyps 1 0))
                       (cons #\e equiv)
                       (cons #\4 (untrans0-lst subst-hyps t abbreviations))
                       (cons #\5 (zero-one-or-more (length free)))
                       (cons #\6 free)
                       (cons #\n "")
                       (cons #\7 (if (member-eq nil subst-hyps) 1 0)))
                 (standard-co state) state nil)))
          (cond (show-more
                 (pprogn
                  (cond (pl-p state)
                        (t (fms0 "  -- IF REWRITE is called with ~
                                  instantiate-free=t: --")))
                  (fms fmt-string
                       (list (cons #\3 (untrans0
                                        (sublis-var unify-subst-2 rhs)
                                        term-id-iff abbreviations))
                             (cons #\s (if pl-p 1 0))
                             (cons #\a (untranslate-subst-abb unify-subst-2
                                                              abbreviations
                                                              state))
                             (cons #\b (if subst-hyps-2 1 0))
                             (cons #\e equiv)
                             (cons #\4 (untrans0-lst subst-hyps-2 t
                                                     abbreviations))
                             (cons #\5 (if (eql (length free-2) 1)
                                           1
                                         2))
                             (cons #\6 free-2)
                             (cons #\n (if (null free-2)
                                           "[none]"
                                         ""))
                             (cons #\7 (if (member-eq nil subst-hyps-2)
                                           1
                                         0)))
                       (standard-co state) state nil)))
                (t state))))))))

(defun show-meta-lemmas1 (lemmas index term wrld ens state)
  (cond ((endp lemmas) state)
        (t
         (mv-let
          (new-index state)
          (let ((lemma (car lemmas)))
            (cond ((eq (access rewrite-rule lemma :subclass)
                       'meta)
                   (let* ((fn (access rewrite-rule lemma :lhs))
                          (extendedp (access rewrite-rule lemma :rhs))
                          (args (meta-fn-args term extendedp ens state)))
                     (mv-let
                      (erp new-term latches)
                      (ev-fncall-meta fn args state)
                      (declare (ignore latches))
                      (cond ((or erp
                                 (equal new-term term)
                                 (not (termp new-term wrld)))
                             (mv index state))
                            (t
                             (let ((hyp-fn (access rewrite-rule lemma :hyps)))
                               (mv-let
                                (erp hyp latches)
                                (if hyp-fn
                                    (ev-fncall-meta
                                     hyp-fn
                                     (meta-fn-args term extendedp ens state)
                                     state)
                                  (mv nil *t* nil))
                                (declare (ignore latches))
                                (cond
                                 ((or erp (not (termp hyp wrld)))
                                  (mv index state))
                                 (t
                                  (pprogn
                                   (fms
                                    "META ~x0. ~y1~|~
                                     ~ ~ New term: ~y2~|~
                                     ~ ~ Hypothesis: ~y3~|~
                                     ~ ~ Equiv: ~y4~|"
                                    (list (cons #\0 index)
                                          (cons #\1
                                                (let ((rune
                                                       (access rewrite-rule
                                                               lemma
                                                               :rune)))
                                                  (if (cddr rune)
                                                      rune
                                                    (base-symbol rune))))
                                          (cons #\2 new-term)
                                          (cons #\3 (untranslate hyp
                                                                 nil
                                                                 wrld))
                                          (cons #\4 (access rewrite-rule lemma
                                                            :equiv)))
                                    (standard-co state) state nil)
                                   (mv (1+ index) state)))))))))))
                  (t (mv index state))))
          (show-meta-lemmas1 (cdr lemmas) new-index term wrld ens state)))))

(defun show-meta-lemmas (term state)
  (cond ((and (nvariablep term)
              (not (fquotep term))
              (not (flambdap (ffn-symb term))))
         (let ((wrld (w state)))
           (show-meta-lemmas1 (getprop (ffn-symb term) 'lemmas nil
                                       'current-acl2-world wrld)
                              1 term wrld (ens state) state)))
        (t state)))

(defun pl-fn (name state)
  (if (symbolp name)
      (let* ((wrld (w state))
             (name (deref-macro-name name (macro-aliases wrld))))
        (if (function-symbolp name wrld)
            (pprogn (print-lemmas
                     (getprop name 'lemmas nil 'current-acl2-world wrld)
                     t
                     (ens state)
                     wrld
                     state)
                    (value :invisible))
          (if (getprop name 'macro-body nil 'current-acl2-world wrld)
              (er soft 'pl
                  "The argument to PL must be a function symbol in ~
                   the current world, but ~x0 is a macro."
                  name)
            (er soft 'pl
                "The argument to PL must be a function symbol in the current ~
                 world, or else a macro that is associated with a function ~
                 symbol (see :DOC add-macro-alias)."))))
    (er-let* ((term (translate name t t nil 'pl (w state) state)))
      (pprogn (show-rewrites-fn nil nil (ens state) term
                                nil nil nil :none t state)
              (show-meta-lemmas term state)
              (value :invisible)))))

;;; Documentation change only (for sources, but commented out in patch file).
#+acl2-sources-only ; undefined feature
(defmacro pl (name)

  ":Doc-Section History

  print the rules for the given name or term~/
  ~bv[]
  Examples:
  :pl foo     ; prints rules that rewrite some call of foo
  :pl (+ x y) ; prints rules that rewrite (+ x y)
  ~ev[]~/

  ~c[Pl] takes one argument, which should be a symbol or a term.  If the
  argument is a function symbol (or a macro corresponding to a function;
  ~pl[macro-aliases-table]), ~c[:pl] displays the ~c[:]~ilc[rewrite],
  ~c[:]~ilc[definition], and ~c[:]~ilc[meta] rules that rewrite some term whose
  top function symbol is the one specified.  Otherwise, ~c[:pl] displays the
  ~c[:]~ilc[rewrite] and ~c[:]~ilc[definition] rules that rewrite the specified
  term, followed by the applicable ~c[:]~ilc[meta] rules.  For
  ~c[:]~ilc[rewrite] and ~c[:]~ilc[definition] rules, ~c[:pl] also shows the
  substitution that, when applied to the left-hand side of the rule, yields the
  specified term.  For ~c[:]~ilc[meta] rules, only those are displayed that
  meet two conditions: the application of the metafunction returns a term
  different from the input term, and if there is a hypothesis metafunction then
  it also returns a term.  (A subtlety: In the case of extended metafunctions
  (~pl[extended-metafunctions]), a trivial metafunction context is used for the
  application of the metafunction.)

  The kinds of rules printed by ~c[:pl] are ~c[:]~ilc[rewrite] rules,
  ~c[:]~ilc[definition] rules, and ~il[meta] rules (not, for example,
  ~c[:]~ilc[forward-chaining] rules).~/"

  (list 'pl-fn name 'state))