defrule

(in-package "STD")

(include-book "xdoc/top" :dir :system)

(include-book "support")

(include-book "tools/rulesets" :dir :system)

(program)

(defxdoc defrule
  :parents (std/util)
  :short "An enhanced version of @(see defthm)."
  :long "<p>@('defrule') is a drop-in replacement for @('defthm') that
adds:</p>

<ul>

<li>A more concise syntax for @(see acl2::hints) that target
@('"Goal"').</li>

<li>A very concise syntax for
@({
  (encapsulate ()
    (local (in-theory (e/d ...)))
    (defthm ...))
})
with @(see acl2::rulesets) integration.</li>

<li>Integration with @(see xdoc).  You can give @(':parents'), @(':short'), and
@(':long') documentation right at the top level of the @('defrule').</li>

<li>The ability to make the theorem local.</li>

<li>The ability to provide lemmas and include books in support of the theorem's
proof.</li>

</ul>

<h3>Top-level Hints</h3>

<p>You can give @('"Goal"') hints directly at the top level of the rule.
For example:</p>

@({
  (defrule repeated-insert           -->  (defthm repeated-insert
    (equal (insert a (insert a X))          (equal (insert a (insert a X))
           (insert a X))                           (insert a X))
    :induct t                               :hints(("Goal"
    :expand ((...)))                                :induct t
                                                    :expand ((...))))
})

<p>This works for any hint except for @(':instructions').  If you give
top-level hints and a "Goal" hint, the top-level hints will be appended onto
the front of the explicit "Goal" hint.</p>

<h3>Theory Support</h3>

<p>Theory hints are especially common.</p>

<p>One option is to just give a top-level @(':in-theory') hint, and it just
gets attached to goal.  But note that such hints are not inherited when you
give an in-theory hint in a subgoal.  This can be quite confusing and
annoying.</p>

<p>As an alternative, @('defrule') also adds top-level @(':enable'),
@(':disable'), and @(':e/d') options.  When you use these keywords, they turn
into a local theory event that is submitted before your defthm.  That way,
they're part of the theory that is inherited by all subgoals.</p>

<p>To make @(':enable'), @(':disable'), and @(':e/d') slightly more powerful,
they are actually integrated with the @(see acl2::rulesets) book.  In
particular, these keywords are always translated into an @(see acl2::e/d*).</p>

<h3>Support for @('Local')</h3>

<p>Another option is to provide a non-@('nil') value to the keyword argument
@(':local').  This results in surrounding the rule with a @(see
acl2::local).</p>

<h3>Supporting Lemmas and Books</h3>

<p>We often write lemmas in support of one larger theorem.  In this case, you
can provide these lemmas as a list of events with the @(':prep-lemmas')
argument.  Despite the name, it is also possible to include function
definitions with the @(':prep-lemmas') keyword; for instance, when a recursive
function is needed to serve as an induction scheme. Note that including a book
via @(':prep-lemmas') does not work.</p>

<p>To include a book or many books for use in the main theorem you are proving,
supply a list of include-book commands with the @(':prep-books')
argument.</p>

<p>Some examples:</p>

@({
  (defrule foo            -->  (encapsulate ()
     ...                         (local (in-theory (e/d* (append) (revappend))))
     :enable append              (defthm foo ...))
     :disable revappend)
})

@({
  (defrule bar            -->  (encapsulate ()
     ...                         (local (in-theory (e/d* (append rev)
     :enable (append rev)                                revappend
     :disable revappend                                  (logior)
     :e/d ((logior) (logand)))                           (logand)))
                                 (defthm bar ...))
})

@({
  (defrule baz            -->  (local
      ...                        (encapsulate ()
      :local t)                    (defthm baz ...)))
})

@({
  (defrule lets-loop                  --> (defsection lets-loop
    (equal (+ x y)                          (local
           (+ y x))                          (encapsulate ()
                                              (defrule pretend-we-need-this
    :prep-lemmas                                ...)
    ((defrule pretend-we-need-this            (defrule pretend-we-need-this-too
       ...)                                     ...)))
     (defrule pretend-we-need-this-too        (local (progn (include-book
       ...))                                                "arithmetic/top"
                                                            :dir :system)))
    :prep-books                             (defthm lets-loop (equal (+ x y) (+ y x))
      ((include-book "arithmetic/top"             ...))
      :dir :system)))
})
")

(defxdoc defruled
  :parents (defrule)
  :short "Variant of @(see defrule) that disables the theorem afterwards."
  :long "<p>This is identical to @('defrule') except that the theorem is
generated using @(see defthmd) instead of @(see defthm).</p>")

(defxdoc defrulel
  :parents (defrule)
  :short "Variant of @(see defrule) that makes the theorem local."
  :long "<p>This is identical to @('defrule') except that the @(':local')
argument is set to @('t').</p>")

(defxdoc defruledl
  :parents (defrule)
  :short "Variant of @(see defrule) that disables the theorem afterwards and
  makes it local."
  :long "<p>This is identical to @('defrule') except that the theorem is
 generated using @(see defthmd) instead of @(see defthm) and the @(':local')
 argument is set to @('t').</p>")

(defconst *defrule-keywords*
  (union-equal '(:hints :rule-classes :otf-flg :instructions :doc :parents :short :long :enable :disable :e/d :local :prep-lemmas :prep-books)
    *hint-keywords*))

(defun split-alist
  (keys al)
  "Returns (MV NAMED-PART UNNAMED-PART)"
  (b* (((when (atom al)) (mv nil nil)) ((mv named-rest unnamed-rest) (split-alist keys (cdr al)))
      ((when (member-equal (caar al) keys)) (mv (cons (car al) named-rest)
          unnamed-rest)))
    (mv named-rest
      (cons (car al) unnamed-rest))))

(defun find-goal-entry-in-user-hints
  (user-hints)
  (cond ((atom user-hints) nil)
    ((and (consp (car user-hints))
       (stringp (caar user-hints))
       (string-equal "goal" (caar user-hints))) (car user-hints))
    (t (find-goal-entry-in-user-hints (cdr user-hints)))))

(defun alist-to-plist
  (al)
  (if (atom al)
    nil
    (list* (caar al)
      (cdar al)
      (alist-to-plist (cdr al)))))

(defun merge-keyword-hints-alist-into-ordinary-hints
  (hints-al user-hints)
  (b* (((when (atom hints-al)) user-hints) (user-goal-entry (find-goal-entry-in-user-hints user-hints))
      (user-hints (remove-equal user-goal-entry user-hints))
      (user-goal (cdr user-goal-entry))
      (new-goal (append (alist-to-plist hints-al) user-goal))
      (new-entry (cons "Goal" new-goal)))
    (cons new-entry user-hints)))

(defun defrule-fn
  (name args disablep)
  (b* ((ctx `(defrule ,STD::NAME)) ((mv kwd-alist args) (extract-keywords ctx
          *defrule-keywords*
          args
          nil))
      ((mv hint-alist &) (split-alist (remove :instructions *hint-keywords*)
          kwd-alist))
      (enable (cdr (assoc :enable kwd-alist)))
      (disable (cdr (assoc :disable kwd-alist)))
      (e/d (cdr (assoc :e/d kwd-alist)))
      (enable (if (and enable (atom enable))
          (list enable)
          enable))
      (disable (if (and disable (atom disable))
          (list disable)
          disable))
      (theory-hint (if (or enable disable e/d)
          `(local (in-theory (e/d* ,STD::ENABLE ,STD::DISABLE . ,STD::E/D)))
          nil))
      (hints (cdr (assoc :hints kwd-alist)))
      (hints (merge-keyword-hints-alist-into-ordinary-hints hint-alist
          hints))
      (kwd-alist (if hints
          (put-assoc-eq :hints hints kwd-alist)
          kwd-alist))
      (local (cdr (assoc :local kwd-alist)))
      (prep-lemmas (cdr (assoc :prep-lemmas kwd-alist)))
      (prep-books (cdr (assoc :prep-books kwd-alist)))
      ((unless (tuplep 1 args)) (er hard?
          'defrule
          (if (atom args)
            "In ~x0: no formula found?"
            "In ~x0: multiple formulas found?  Forget parens around a list ~
               of runes?")
          ctx))
      (formula (car args))
      (parents (cdr (assoc :parents kwd-alist)))
      (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (want-xdoc (or parents short long))
      (prep-lemmas-form (if prep-lemmas
          `(local (encapsulate nil ,@STD::PREP-LEMMAS))
          nil))
      (prep-books-form (if prep-books
          `(local (progn ,@STD::PREP-BOOKS))
          nil))
      ((mv thm-kwd-alist &) (split-alist '(:hints :rule-classes :otf-flg :instructions)
          kwd-alist))
      (thm `(,(IF STD::DISABLEP
     'STD::DEFTHMD
     'STD::DEFTHM) ,STD::NAME
          ,STD::FORMULA
          ,@(STD::ALIST-TO-PLIST STD::THM-KWD-ALIST)))
      (event (if (and (not want-xdoc)
            (not theory-hint)
            (not prep-lemmas)
            (not prep-books))
          thm
          `(with-output :stack :push :off :all (defsection ,STD::NAME
              ,@(AND STD::PARENTS `(:PARENTS ,STD::PARENTS))
              ,@(AND STD::SHORT `(:SHORT ,STD::SHORT))
              ,@(AND STD::LONG `(:LONG ,STD::LONG))
              ,@(AND STD::PREP-LEMMAS-FORM
       `((STD::WITH-OUTPUT :STACK :POP ,STD::PREP-LEMMAS-FORM)))
              ,@(AND STD::PREP-BOOKS-FORM
       `((STD::WITH-OUTPUT :STACK :POP ,STD::PREP-BOOKS-FORM)))
              ,@(AND STD::THEORY-HINT `((STD::WITH-OUTPUT :ON (ERROR) ,STD::THEORY-HINT)))
              (with-output :stack :pop ,STD::THM))))))
    (if local
      `(local ,STD::EVENT)
      event)))

(defmacro defrule
  (name &rest args)
  (defrule-fn name args nil))

(defmacro defruled
  (name &rest args)
  (defrule-fn name args t))

(defmacro defrulel
  (name &rest rst)
  `(defrule ,STD::NAME :local t ,@STD::RST))

(defmacro defruledl
  (name &rest rst)
  `(defruled ,STD::NAME :local t ,@STD::RST))

(table ppr-special-syms 'defrule 1)

(table ppr-special-syms 'defruled 1)

(table ppr-special-syms 'defrulel 1)

(table ppr-special-syms 'defruledl 1)

(defxdoc rule
  :parents (defrule thm)
  :short "A @(see thm)-like version of @(see defrule)."
  :long "<p>The @('rule') macro is a thin wrapper around @(see defrule).  It
supports all of the same syntax extensions like top-level @(':enable') and
@(':expand') @(see acl2::hints).  However, like @(see thm), @('rule') does not
take a rule name and does not result in the introduction of a rule
afterward.</p>

<p>Examples:</p>

@({
    (rule (implies x x))                    ;; will work

    (rule (equal (append x y)               ;; will fail
                 (append y x))
          :enable append
          :expand (append y x))

    (rule (equal (consp x)                  ;; will work
                 (if (atom x) nil t))
          :do-not '(generalize fertilize))
})

<p>The @('rule') command is implemented with a simple @(see make-event), and
its calls are valid embedded events.  However, on
success a @('rule') merely expands into @('(value-triple :success)').  No
record of the rule's existence is found in the world, so there is no way to use
the rule once it has been proven, etc.</p>")

(defmacro rule
  (&rest args)
  `(with-output :off :all :stack :push (make-event (er-progn (with-output :stack :pop (defrule temporary-rule
            ,@STD::ARGS
            :rule-classes nil))
        (value '(value-triple :invisible))))))