Filtering...

easy-simplify

books/tools/easy-simplify

Included Books

bstar
other
(in-package "ACL2")
include-book
(include-book "std/util/bstar" :dir :system)
other
(defxdoc easy-simplify-term
  :parents (programming)
  :short "A simple interface for simplifying a term, perhaps under a hypothesis
and equivalence context, and with optional guidance from a hint."
  :long "<p>This provides a straightforward interface for simplifying a term.
It uses the proof checker's pc-rewrite* function.  It can handle rewriting
under some hypotheses, under a user-provided equivalence relation.</p>

<p>Usage:</p>

@({
    (easy-simplify-term (my-fn (foo) (bar baz))
                        ;; optional keyword args:
                        :hyp (and (integerp baz) (<= 0 baz))
                        :hint (:in-theory (enable my-fn) :expand ((foo)))
                        :equiv equal
                        :normalize t
                        :rewrite t
                        :repeat 555
                        :backchain-limit 5)
})

<p>Important NOTE: The HINT keyword should be given a hint keyword/val list, as
in the example above, NOT a list of subgoal or computed hints,
e.g. (("Goal" :foo)).</p>")
easy-simplify-term1-fnfunction
(defun easy-simplify-term1-fn
  (term hyps
    hints
    equiv
    normalize
    rewrite
    repeat
    backchain-limit
    state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((world (w state)) ((er hint-settings) (translate-hint-settings 'simp-term
          "Goal"
          hints
          'easy-simplify-term
          world
          state))
      (ens (ens state))
      (base-rcnst (change rewrite-constant
          *empty-rewrite-constant*
          :current-enabled-structure ens
          :force-info t))
      ((er rcnst) (load-hint-settings-into-rcnst hint-settings
          base-rcnst
          :easy-simplify world
          'easy-simplify-term
          state))
      (ens (access rewrite-constant rcnst :current-enabled-structure))
      ((mv flg hyps-type-alist ?ttree) (hyps-type-alist hyps ens world state))
      ((when flg) (mv "Contradiction in the hypotheses" nil state))
      ((mv ?step-limit new-term ?new-ttree state) (pc-rewrite* term
          hyps-type-alist
          (if (eq equiv 'equal)
            nil
            (list (make congruence-rule
                :rune *fake-rune-for-anonymous-enabled-rule*
                :nume nil
                :equiv equiv)))
          (eq equiv 'iff)
          world
          rcnst
          nil
          nil
          normalize
          rewrite
          ens
          state
          repeat
          backchain-limit
          (initial-step-limit world state))))
    (value new-term)))
easy-simplify-term-fnfunction
(defun easy-simplify-term-fn
  (term hyp-term
    hints
    equiv
    normalize
    rewrite
    repeat
    backchain-limit
    untrans-result
    state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((world (w state)) ((er trans-term) (translate term t nil t 'easy-simplify-term world state))
      ((er trans-hyp-term) (translate hyp-term t nil t 'easy-simplify-term world state))
      (hyps (expand-assumptions-1 trans-hyp-term))
      ((er new-term) (easy-simplify-term1-fn trans-term
          hyps
          hints
          equiv
          normalize
          rewrite
          repeat
          backchain-limit
          state)))
    (if untrans-result
      (value (untranslate new-term nil (w state)))
      (value new-term))))
easy-simplify-termmacro
(defmacro easy-simplify-term
  (term &key
    (hyp 't)
    hint
    (equiv 'equal)
    (normalize 't)
    (rewrite 't)
    (repeat '1000)
    (backchain-limit '1000)
    (untrans-result 't))
  `(easy-simplify-term-fn ',TERM
    ',HYP
    ',HINT
    ',EQUIV
    ',NORMALIZE
    ',REWRITE
    ',REPEAT
    ',BACKCHAIN-LIMIT
    ',UNTRANS-RESULT
    state))
other
(defxdoc defopen
  :parents (programming)
  :short "A simple event generator that creates a theorem by finding out what a
term simplifies to under some hyp and with some hint."
  :long "<p>In contrast to @('misc/defopener') (see @(see defopener)), the
reductions carried out by @('defopen') may be less powerful because we only do
simplification (no clausify).  However, this seems to produce more compact
expressions than @('defopener'), where the result is formed by combining
several clauses produced from the original term.</p>

<p>General form:</p>

@(ccall defopen)

<p>See also @(see easy-simplify-term).</p>")
defopenmacro
(defmacro defopen
  (name term &key (hyp 't) hint (rule-classes ':rewrite))
  `(make-event (b* (((er new-hyp-term) (easy-simplify-term ,HYP :hint ,HINT)) ((er new-term) (easy-simplify-term-fn ',TERM
            new-hyp-term
            ',HINT
            'equal
            t
            t
            1000
            1000
            t
            state)))
      (value `(defthm ,',NAME
          ,(IF (NOT (EQ ',HYP T))
     `(IMPLIES ,',HYP (EQUAL ,',TERM ,NEW-TERM))
     `(EQUAL ,',TERM ,NEW-TERM))
          :hints (("goal" . ,',HINT))
          :rule-classes ,',RULE-CLASSES)))))