Filtering...

do-not

books/tools/do-not

Included Books

bstar top
other
(in-package "ACL2")
include-book
(include-book "std/util/bstar" :dir :system)
include-book
(include-book "xdoc/top" :dir :system)
strip-quotes-for-do-notfunction
(defun strip-quotes-for-do-not
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
    ((and (quotep (car x)) (consp (cdr (car x)))) (cons (unquote (car x)) (strip-quotes-for-do-not (cdr x))))
    (t (cons (car x) (strip-quotes-for-do-not (cdr x))))))
*allowed-for-do-not*constant
(defconst *allowed-for-do-not*
  '(induct preprocess
    simplify
    eliminate-destructors
    fertilize
    generalize
    eliminate-irrelevance))
check-allowed-for-do-notfunction
(defun check-allowed-for-do-not
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) t)
    ((member-equal (car x) *allowed-for-do-not*) (check-allowed-for-do-not (cdr x)))
    (t (er hard?
        'do-not
        "~x0 is not allowed.  The allowed symbols are ~x1."
        (car x)
        *allowed-for-do-not*))))
other
(table do-not-table 'things-not-to-be-done nil)
other
(table do-not-table 'do-not-inductp nil)
do-notmacro
(defmacro do-not
  (&rest things)
  (declare (xargs :guard t))
  (b* ((things (strip-quotes-for-do-not things)) (- (check-allowed-for-do-not things))
      (induct (if (member-eq 'induct things)
          t
          nil))
      (others (remove-eq 'induct things)))
    `(with-output :off (event summary)
      (progn (table do-not-table 'do-not-inductp ',INDUCT)
        (table do-not-table 'things-not-to-be-done ',OTHERS)))))
other
(defsection do-not-hint
  :parents (hints)
  :short "Give @(':do-not') hints automatically."
  :long "<p>@('Do-not-hint') is a computed hint (~l[computed-hints]) that gives
@(':do-not') and perhaps @(':do-not-induct') hints automatically.  For
instance:</p>

@({
  (local (do-not generalize fertilize))
  (defthm thm1 ...)
  (defthm thm2 ...)
  ...
})

<p>is roughly equivalent to:</p>

@({
  (defthm thm1 ... :hints (("Goal" :do-not '(generalize fertilize))))
  (defthm thm2 ... :hints (("Goal" :do-not '(generalize fertilize))))
})

<p>except that the @(':do-not') hints are actually given at
@('stable-under-simplificationp') checkpoints.  This is kind of useful: the
hints will apply to forced subgoals in addition to regular subgoals, and won't
clutter proofs that never hit a @('stable-under-simplificationp')
checkpoint.</p>

<p>The @('do-not') macro expands to some @(see table) events that update the
@('do-not-table').  It should typically be made local to a book or encapsulate
since globally disabling these proof engines is likely to be particularly
disruptive to other proofs.</p>

<p>The arguments to @('do-not') can be any of the keywords used for
@(':do-not') hints, and may also include @('induct') which results in
@(':do-not-induct t') hints.</p>"
  (defun do-not-hint
    (world stable-under-simplificationp state)
    (declare (xargs :mode :program :stobjs state))
    (b* (((unless stable-under-simplificationp) nil) (tbl (table-alist 'do-not-table world))
        (things (cdr (assoc 'things-not-to-be-done tbl)))
        (inductp (cdr (assoc 'do-not-inductp tbl)))
        ((when (and (atom things) (not inductp))) nil)
        (- (or (gag-mode)
            (cw "~%;; do-not-hint: prohibiting ~x0.~|"
              (if inductp
                (cons 'induct things)
                things))))
        (hint (if inductp
            '(:do-not-induct t)
            nil))
        (hint (if (consp things)
            (append `(:do-not ',THINGS) hint)
            hint)))
      hint))
  (add-default-hints! '((do-not-hint world stable-under-simplificationp state))))