other
(in-package "ACL2")
include-book
(include-book "std/util/bstar" :dir :system)
include-book
(include-book "xdoc/top" :dir :system)
other
(program)
other
(set-state-ok t)
other
(defxdoc rewrite$ :parents (proof-automation) :short "Rewrite a term" :long "<p>@('Rewrite$') is a macro that provides a convenient and flexible interface to the ACL2 @(see rewrite)r, which can be called programmatically. The documentation below is divided into the following sections.</p> <ul> <li>An introductory example</li> <li>Return values</li> <li>General Form</li> <li>Basic options</li> <li>Hint options, each with default @('nil')</li> <li>Advanced options</li> <li>Summary of algorithm</li> <li>Related tools</li> </ul> <h3>An introductory example</h3> <p>We begin with the following example of a call of @('rewrite$'). The keyword option @(':translate t') is used because the first argument is not a translated @(see term), due to the call of the macro, @(tsee append). We see that the call of @('rewrite$') produces a 2-element list consisting of the result, @('X'), of rewriting the input term, together with a list of @(see rune)s justifying that rewrite.</p> @({ ACL2 !>(rewrite$ '(car (append (cons x y) z)) :translate t) (X ((:DEFINITION BINARY-APPEND) (:REWRITE CDR-CONS) (:REWRITE CAR-CONS) (:FAKE-RUNE-FOR-TYPE-SET NIL))) ACL2 !> }) <p>Notice the ``fake rune'' that is returned. Fake runes are easy to remove; see for example the constant @('*fake-rune-alist*') in the ACL2 sources or function @('drop-fake-runes') defined in community book @('kestrel/utilities/runes.lisp').</p> <p>Other simple examples may be found in community book @('books/demos/rewrite-dollar-input.lsp').</p> <h3>Return values</h3> <p>A call @('(rewrite$ term ...)') returns an @(see error-triple), @('(mv erp val state)'). @('Erp') is non-@('nil') when an error has occurred. Otherwise @('val') is of the form @('(rewritten-term runes . pairs)') where @('pairs') is typically @('nil') (as discussed further below) and:</p> <ul> <li>@('rewritten-term') is the result of rewriting @('term') as directed by the other inputs; and</li> <li>@('runes') is a list containing the @(see rune)s that participated in the rewriting of @('term') to @('rewritten-term').</li> </ul> <p>Because of forcing (see @(see force)), rewriting of the input term may generate goals to be proved later, based on the forced hypotheses encountered during rewriting that were not relieved at that time. We call these ``forced assumptions''. If there are forced assumptions, then they are conjoined into a single goal, which by default is the target of a separate call to the prover, much like a call of @(tsee thm). The return value @('pairs'), mentioned above, is @('nil') exactly when there are no forced assumptions. We say no more here about @('pairs'), as it will suffice for most users to view them solely as an indicator of forced assumptions. (Technical note for advanced users: these are the pairs returned by ACL2 source function @('extract-and-clausify-assumptions').)</p> <p>There are many keyword arguments that control the rewriting process. One of particular importance semantically is @(':alist'). When this argument is @('nil') then the resulting rewritten term is provably equivalent (with respect to the current ACL2 @(see world)) to the input term. Otherwise the rewritten term is provably equivalent to the result of substituting the specified alist into the input term. Another important keyword argument is @(':hyps'), which provides hypotheses under which the given term is to be rewritten. The hypotheses themselves may be rewritten, using keyword argument @(':rewrite-hyps'). All keywords are documented below.</p> <h3>General Form</h3> <p>All arguments of @('rewrite$') except the first are keyword arguments, hence are optional, with appropriate defaults. All are evaluated.</p> @({ (rewrite$ term ; Basic options (in alphabetical order): :alist ; default nil :ctx ; default 'rewrite$ :default-hints-p ; default t :equiv ; default nil :geneqv ; default nil :hyps ; default nil :must-rewrite ; default nil :prove-forced-assumptions ; default t :repeat ; default 1 :translate ; default nil :untranslate ; default nil ; Hint options (in alphabetical order), each with default nil: :backchain-limit-rw :expand :hands-off :in-theory :no-thanks :nonlinearp :restrict :rw-cache-state ; Advanced options (in alphabetical order): :obj ; default '? :rrec ; default nil :wrld ; default (w state) ) }) <p>@('Term') should evaluate to a translated or untranslated term (see @(see term)) according to whether the value of @(':translate') is @('nil') or non-@('nil'), respectively. If @(':translate') is @('nil') (the default), @('term') should already be in translated form; otherwise @('term') will be translated.</p> <p>IMPORTANT: The keyword options, discussed below according to the groups above, are all evaluated. So for example:</p> @({ ; Correct (rewrite$ '(cons a (cdr x)) :alist '((a . (car x))) :hyps '((consp x))) ; WRONG! (rewrite$ '(cons a (cdr x)) :alist ((a . (car x))) :hyps ((consp x))) }) <h3>Basic options</h3> <ul> <li>@(':alist') (default @('nil'))<br/> is an association list mapping variables to terms, where each term is already translated or else is untranslated according to whether the value of @(':translate') is @('nil') or non-@('nil'), respectively.</li> <li>@(':ctx') (default @(''rewrite$'))<br/> is a ``context'', such as the @('ctx') argument of @(tsee er).</li> <li>@(':default-hints-p') (default @('t'))<br/> is non-@('nil') when the construction of hints for the rewriter call is to take into account the @(see default-hints) in the current @(see world).</li> <li>@(':equiv') and @(':geneqv') (both with default @('nil'))<br/> specify the equivalence relation(s) to be preserved by (@(see congruence)-based) rewriting. It is illegal to specify a non-@('nil') value for more than one of these. Most users will prefer to use @(':equiv'), which should be a function symbol that is a known (to ACL2) equivalence relation. The keyword option @(':geneqv') is really only for those who know how generated equivalence relations are represented in the ACL2 system.</li> <li>@(':hyps') (default @('nil'))<br/> is a non-empty list of hypotheses under which rewriting takes place. Each hypothesis is already translated or is untranslated according to whether the value of @(':translate') is @('nil') or non-@('nil'), respectively.</li> <li>@(':must-rewrite') (default @('nil'))<br/> indicates, when its value is non-@('nil'), that the rewritten term must not be equal to the input term. It is illegal to supply non-@('nil') values for both @(':alist') and @(':must-rewrite'), since it's usually not a sensible combination since at the least, the alist will be substituted into the term.</li> <li>@(':prove-forced-assumptions') (default @('t'))<br/> affects the proof of the forced assumptions. It has the following legal values. <ul> <li>@('t'): prove the forced assumptions as mentioned above: a single prover call to prove their conjunction.</li> <li>@(':same-hints'): same as @('t'), except generate the same @(':hints') for the prover call as are generated for the rewriting (from the eight hint options discussed below).</li> <li>@('nil'): do not attempt a proof of the forced assumptions, instead returning a non-@('nil') `@('pairs')' value as discussed above.</li> <li>@(':none-forced'): cause an error if there are any forced assumptions.</li> <li>Otherwise, the value of @(':prove-forced-assumptions') should be of the form expected for the value of @(':hints') supplied to @(tsee defthm). For example, the following might follow @(':prove-forced-assumptions') in a call of @('rewrite$'): @(''(("Goal" :in-theory (enable reverse)))').</li> </ul></li> <li>@(':repeat') (default @('1'))<br/> indicates how many times to call the rewriter. The value should be a positive integer. If the value of @(':repeat') is greater than 1, then the term resulting from the first call is the input term for the second call, whose result (if the value of @(':repeat') is greater than 2) is the input term for the third call, and so on. Note that the value of @(':alist') is @('nil') for all calls after the first.</li> <li>@(':translate') (default @('nil'))<br/> indicates whether or not terms in the input are to be translated or not (see @(see term) for a discussed of ``translate''). If the value is @('nil') then translation will not take place, so the given terms — not only the input term, but also terms in the @('cdr') positions of the @(':alist') and terms in the @(':hyps') — should already be in translated form. But if the value is not @('nil'), then all of these will be translated.</li> <li>@(':untranslate') (default @('nil'))<br/> indicates whether the rewritten term will be given in translated or untranslated form. It also specifies, when not @('nil'), that certain error messages display terms in untranslated form.</li> </ul> <h3>Hint options, each with default @('nil')</h3> <p>The eight hint options displayed above are the same as discussed in the documentation topic, @(see hints). These are the only legal hint keywords for @('rewrite$').</p> <h3>Advanced options</h3> <p>The ``advanced options'' @(':obj'), @(':wrld'), and @(':rrec') can generally be ignored, so we say little about them here. @(':Obj') is the ``obj'' argument of the rewriter, typically the symbol `@('?')' but @('t') when backchaining. See @(see rewrite$-hyps) and its use in community book @('books/kestrel/apt/simplify-defun-impl.lisp') for how @(':rrec') can avoid repeating some computations. @(':Wrld') should probably be left as its default, which is the current ACL2 logical @(see world).</p> <h3>Summary of algorithm</h3> <p>Here we provide a brief summary of the algorithm used by @('rewrite$'). Most users can probably skip this section.</p> <p>Not surprisingly, the primary simplification technique used by @('rewrite$') is rewriting. However, @(see forward-chaining) and @(see linear-arithmetic) are also used, as follows.</p> <p>Initially, a function called @('rewrite$-setup') is invoked on the given @(':hyps') to produce data structures that record facts from forward-chaining — a so-called @('fc-pair-lst') data structure — and linear arithmetic — a so-called @('pot-lst') data structure. (Exception: this step is skipped if @(':rrec') is supplied, since the value of that option already contains such information.) Then we loop through @(':repeat') iterations, where each iteration proceeds according the the following pseudocode. Note that the initial alist is given by @(':alist'), but subsequent alists are all @('nil').</p> @({ Replace term with its rewrite with respect to the alist, hyps, fc-pair-lst, and pot-lst. If the alist is empty and the term didn't change, exit the loop. }) <h3>Related tools</h3> <p>See @(see rewrite$-hyps) for a tool that rewrites a list of hypotheses. That tool does more than just apply rewriting directly to each hypothesis: it also uses @(see forward-chaining) and @(see linear-arithmetic) derived from the hypotheses. A related tool @(see rewrite$-context), is similar but takes an ``@('rrec')'' input that already contains any @(see forward-chaining) and @(see linear-arithmetic) information.</p> <p>For related tools see @(see expander) and @(see easy-simplify-term). In particular, code from the expander function @('tool2-fn') served as a guide to the coding of @('rewrite$'); see @(see community-book) @('books/misc/expander.lisp').</p>")
other
(defxdoc rewrite$-hyps :parents (proof-automation) :short "Rewrite a list of hypotheses" :long "<p>See @(see rewrite$) for relevant background.</p> <p>Roughly speaking, @('rewrite$-hyps') applies rewriting to each term in a given list. However, it treats that input as a list of hypotheses: each term in the list is rewritten under the assumption that the other terms in the list are true. Both @(see forward-chaining) and @(see linear-arithmetic) are used.</p> <h3>General Form</h3> <p>All arguments of @('rewrite$-hyps') except the first are keyword arguments, hence are optional, with appropriate defaults. All are evaluated.</p> @({ (rewrite$-hyps hyps &key ; Hint options: thints ; must be nil if any other hint options are supplied backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p ; default t ; Other options: ctx ; default 'rewrite$-hyps prove-forced-assumptions ; default t repeat ; default 1 translate ; default nil untranslate ; default nil update-rrec ; default t wrld ; default (w state) ) }) <p>This macro returns an @(see error-triple) whose non-erroneous value is a list of the form @('(rewritten-hyps rrec ttree . pairs)'). Here, @('rewritten-hyps') is (of course) the result of rewriting the input, @('hyps'); @('rrec') is a so-called ``@('rewrite$-record')'' that can be passed as the @(':rrec') input of @(tsee rewrite$); @('ttree') is the @(see tag-tree) that records information from the rewriting, including the @(see rune)s used; and @('pairs') is @('nil') unless there are @(see force)d assumptions, which should never happen if input @(':prove-forced-assumptions') has its default value of @('t').</p> <p>Additional documentation may be provided here if desired. It may suffice to see community book @('books/kestrel/apt/simplify-defun-impl.lisp') for an illustration of how @(see rewrite$-hyps) may be used. The key idea there is for @('rewrite$-hyps') to produce the @(':rrec') input of @(tsee rewrite$) when there are repeated calls of @('rewrite$') under the same @(':hyps'), and especially when you want first to simplify those hypotheses (perhaps together with subterm governors).</p>")
other
(defxdoc rewrite$-context :parents (proof-automation) :short "Rewrite a list of contextual assumptions" :long "<p>See @(see rewrite$) for relevant background. The macro @('rewrite$-context') is similar to @(see rewrite$-hyps), but it takes a @('rewrite$-record') (``@('rrec')'') as an input to provide any @(see forward-chaining) and @(see linear-arithmetic) assumptions.</p> <p>Additional documentation may be provided here if requested by someone who is considering use of this utility. As of its initial introduction, it is not used in any of the @(see community-books)</p>")
*simplify$-hyps-contradiction-string*constant
(defconst *simplify$-hyps-contradiction-string* "An attempt has been made to simplify the following ~ hypotheses:~|~%~x0.~|~%However, that list is contradictory! (Technical ~ note: the contradiction was found ~@1.)")
other
(defrec rewrite$-record ((saved-pspv rcnst . type-alist) gstack fc-pair-lst . pot-lst) nil)
rewrite$-clause-type-alistfunction
(defun rewrite$-clause-type-alist (clause fc-pair-lst rcnst wrld pot-lst) (mv-let (lits ttree-lst) (select-forward-chained-concls-and-ttrees fc-pair-lst nil nil nil) (mv-let (current-clause current-ttree-lst) (mv (append clause lits) (make-list-ac (len clause) nil ttree-lst)) (mv-let (contradictionp type-alist ttree) (type-alist-clause current-clause current-ttree-lst nil nil (access rewrite-constant rcnst :current-enabled-structure) wrld pot-lst nil) (mv contradictionp type-alist ttree)))))
rewrite$-setupfunction
(defun rewrite$-setup (hyps-clause rcnst untranslate ctx wrld state) (b* (((when (null hyps-clause)) (value (list* nil nil))) (pts (enumerate-elements hyps-clause 0)) ((mv contradictionp type-alist fc-pair-lst) (forward-chain-top 'rewrite$ hyps-clause pts (access rewrite-constant rcnst :force-info) nil wrld (access rewrite-constant rcnst :current-enabled-structure) (access rewrite-constant rcnst :oncep-override) state)) ((when contradictionp) (er soft ctx *simplify$-hyps-contradiction-string* (let ((x (dumb-negate-lit-lst hyps-clause))) (if untranslate (untranslate-lst x t wrld) x)) "using type-set reasoning, based perhaps on forward chaining")) ((mv ?step-limit contradictionp pot-lst) (setup-simplify-clause-pot-lst hyps-clause (pts-to-ttree-lst pts) fc-pair-lst type-alist rcnst wrld state *default-step-limit*)) ((when contradictionp) (er soft ctx *simplify$-hyps-contradiction-string* (dumb-negate-lit-lst hyps-clause) "using linear arithmetic reasoning")) ((mv contradictionp type-alist ?ttree) (rewrite$-clause-type-alist hyps-clause fc-pair-lst rcnst wrld pot-lst)) ((when contradictionp) (er soft ctx *simplify$-hyps-contradiction-string* (dumb-negate-lit-lst hyps-clause) "using type-set reasoning (after forward chaining and linear ~ arithmetic)"))) (value (list* type-alist pot-lst fc-pair-lst))))
*rewrite$-last-literal*constant
(defconst *rewrite$-last-literal* (fcons-term* 'rewrite$-last-literal-fn))
*rewrite$-note-msg*constant
(defconst *rewrite$-note-msg* "<<Rewrite$ NOTE:>>~|")
rewrite$*function
(defun rewrite$* (term alist bkptr repeat-limit completed-iters type-alist obj geneqv pot-lst rcnst gstack ttree rewrite-stack-limit ctx wrld state) (b* (((mv ?step-limit val new-ttree) (rewrite-entry (rewrite term alist bkptr) :rdepth rewrite-stack-limit :step-limit *default-step-limit* :pequiv-info nil :fnstack nil :ancestors nil :backchain-limit (access rewrite-constant rcnst :backchain-limit-rw) :simplify-clause-pot-lst pot-lst)) (completed-iters (1+ completed-iters)) ((when (and (null alist) (equal val term))) (value (list* t term ttree))) ((when (int= repeat-limit completed-iters)) (value (list* nil val new-ttree))) (state (io? prove nil state (completed-iters) (fms "~@0Starting ~n1 call of the rewriter.~%" (list (cons #\0 *rewrite$-note-msg*) (cons #\1 (list (1+ completed-iters)))) (proofs-co state) state nil))) ((mv ?step-limit bad-ass new-ttree) (resume-suspended-assumption-rewriting new-ttree nil gstack pot-lst rcnst wrld state *default-step-limit*)) ((when bad-ass) (er soft ctx "Generated false assumption (from force or case-split):~|~x0" bad-ass))) (rewrite$* val nil bkptr repeat-limit completed-iters type-alist obj geneqv pot-lst rcnst gstack new-ttree rewrite-stack-limit ctx wrld state)))
rewrite$-returnfunction
(defun rewrite$-return (rewritten-term ttree pairs untranslate wrld state) (b* ((new-term (if untranslate (untranslate rewritten-term nil wrld) rewritten-term))) (value (list* new-term (all-runes-in-ttree ttree nil) pairs))))
rewrite$-process-assumptions-msgfunction
(defun rewrite$-process-assumptions-msg (n0 pairs untranslate clause-set forced-goal wrld state) (io? prove nil state (n0 pairs untranslate clause-set forced-goal wrld) (fms "~@0Rewriting is complete for the input term, but ~ it remains to prove the goal generated by cleaning up ~n1 forced ~ ~#2~[hypothesis~/hypotheses (and conjoining into a single ~ term)~], as follows:~|~%~x3~|~%" (list (cons #\0 *rewrite$-note-msg*) (cons #\1 n0) (cons #\2 (if (cdr pairs) 1 0)) (cons #\3 (if untranslate (prettyify-clause-set clause-set (let*-abstractionp state) wrld) forced-goal))) (proofs-co state) state nil)))
*rewrite$-hint-keywords*constant
(defconst *rewrite$-hint-keywords* '(:backchain-limit-rw :expand :hands-off :in-theory :no-thanks :nonlinearp :restrict :rw-cache-state))
rewrite$-mainfunction
(defun rewrite$-main (term alist geneqv obj prove-forced-assumptions forced-assumptions-hints untranslate must-rewrite repeat rrec ctx wrld state) (b* ((rcnst (access rewrite$-record rrec :rcnst)) (type-alist (access rewrite$-record rrec :type-alist)) (gstack (access rewrite$-record rrec :gstack)) (pot-lst (access rewrite$-record rrec :pot-lst)) (bkptr 0) ((er (list* flg rewritten-term ttree)) (rewrite$* term alist bkptr repeat 0 type-alist obj geneqv pot-lst rcnst gstack nil (rewrite-stack-limit wrld) ctx wrld state)) ((when (and must-rewrite (if (and (int= repeat 1) (null alist)) flg (equal term rewritten-term)))) (er soft ctx "The term~| ~x0~|failed to rewrite to a new term." (if untranslate (untranslate term nil wrld) term))) (ttree (set-cl-ids-of-assumptions ttree *initial-clause-id*)) ((mv n0 assns pairs ttree) (extract-and-clausify-assumptions nil ttree nil (access rewrite-constant rcnst :current-enabled-structure) wrld (splitter-output))) ((when (or (null pairs) (not prove-forced-assumptions))) (rewrite$-return rewritten-term ttree pairs untranslate wrld state)) (clause-set (strip-cdrs pairs)) (forced-goal (termify-clause-set clause-set)) (state (rewrite$-process-assumptions-msg n0 pairs untranslate clause-set forced-goal wrld state)) ((when (eq prove-forced-assumptions :none-forced)) (er soft ctx "The call of rewrite$ has failed because there were forced ~ assumptions and keyword option :PROVE-FORCED-ASSUMPTIONS ~ :NONE-FORCED was supplied.")) (state (io? prove nil state nil (fms "~@0Beginning forcing round.~|" (list (cons #\0 *rewrite$-note-msg*)) (proofs-co state) state nil))) ((mv erp val state) (prove forced-goal (change prove-spec-var (access rewrite$-record rrec :saved-pspv) :user-supplied-term forced-goal) forced-assumptions-hints (ens state) wrld ctx state)) ((when erp) (er soft ctx "Rewriting has failed because of failure to prove all of the ~ assumptions forced during rewriting. Either disable forcing ~ (see :DOC disable-forcing) or, if you are willing to ignore the ~ forced assumptions, specify option :PROVE-FORCED-ASSUMPTIONS NIL ~ for rewrite$.")) (ttree (process-assumptions-ttree assns ttree))) (rewrite$-return rewritten-term (cons-tag-trees val ttree) nil untranslate wrld state)))
rewrite$-pspvfunction
(defun rewrite$-pspv (thints wrld state) (make-pspv (ens state) wrld state :orig-hints thints))
weak-type-alistpfunction
(defun weak-type-alistp (x wrld) (and (alistp x) (let ((a (strip-cars x)) (d (strip-cdrs x))) (and (term-listp a wrld) (alistp d) (integer-listp (strip-cars d))))))
chk-rrec-pfunction
(defun chk-rrec-p (rrec ctx wrld state) (b* (((unless (weak-rewrite$-record-p rrec)) (er soft ctx "The value of :RREC in a call of rewrite$ must have the shape of ~ a rewrite$-record record, but that value has been supplied as ~ ~x0, which fails to satisfy the predicate ~x1." rrec 'weak-rewrite$-record-p)) ((unless (weak-rewrite-constant-p (access rewrite$-record rrec :rcnst))) (er soft ctx "The value of :RREC in a call of rewrite$ must have an :RCNST ~ field that is the shape of a rewrite-constant record. But that ~ field has been supplied as ~x0, which fails to satisfy the ~ predicate ~x1." (access rewrite$-record rrec :rcnst) 'weak-rewrite-constant-p)) ((unless (weak-prove-spec-var-p (access rewrite$-record rrec :saved-pspv))) (er soft ctx "The value of :RREC in a call of rewrite$ must have a :SAVED-PSPV ~ field that is the shape of a prove-spec-var record. But that ~ field has been supplied as ~x0, which fails to satisfy the ~ predicate ~x1." (access rewrite$-record rrec :saved-pspv) 'weak-prove-spec-var-p)) ((unless (weak-type-alistp (access rewrite$-record rrec :type-alist) wrld)) (er soft ctx "The value of :RREC in a call of rewrite$ must have a :TYPE-ALIST ~ field that is a type-alist. But that field has been supplied as ~ ~x0, which fails to satisfy the predicate ~x1." (access rewrite$-record rrec :type-alist) 'weak-type-alistp))) (value nil)))
chk-repeatfunction
(defun chk-repeat (repeat ctx state) (cond ((posp repeat) (value nil)) (t (er soft ctx "The :REPEAT argument must be a positive integer; ~x0 is thus ~ illegal." repeat))))
rewrite$-check-argsfunction
(defun rewrite$-check-args (alist must-rewrite repeat hyps backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state rrec ctx wrld state) (er-progn (cond ((and must-rewrite alist) (er soft ctx "It is illegal for rewrite$ to specify non-nil values for both ~ :ALIST and :MUST-REWRITE.")) (t (value nil))) (chk-repeat repeat ctx state) (cond ((null rrec) (value nil)) ((or hyps backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state) (er soft ctx "It is illegal for a call of rewrite$ to supply values both to ~ :RREC and to ~v0." `(,@(AND BACKCHAIN-LIMIT-RW '(:BACKCHAIN-LIMIT-RW)) ,@(AND EXPAND '(:EXPAND)) ,@(AND HANDS-OFF '(:HANDS-OFF)) ,@(AND IN-THEORY '(:IN-THEORY)) ,@(AND NO-THANKS '(:NO-THANKS)) ,@(AND NONLINEARP '(:NONLINEARP)) ,@(AND RESTRICT '(:RESTRICT)) ,@(AND RW-CACHE-STATE '(:RW-CACHE-STATE))))) (t (chk-rrec-p rrec ctx wrld state)))))
rewrite$-rcnstfunction
(defun rewrite$-rcnst (clause saved-pspv hints ctx wrld state) (b* (((er pair) (find-applicable-hint-settings *initial-clause-id* clause nil saved-pspv ctx hints wrld nil state)) (hint-settings (car pair)) (bad-keywords (set-difference-eq (strip-cars hint-settings) *rewrite$-hint-keywords*)) ((when bad-keywords) (er soft ctx "The hints keyword~#0~[ ~&0 is~/s ~&0 are~] illegal for rewrite$." bad-keywords)) ((mv hint-settings state) (cond ((null hint-settings) (mv nil state)) (t (thanks-for-the-hint nil hint-settings nil state)))) ((er rcnst) (load-hint-settings-into-rcnst hint-settings (access prove-spec-var saved-pspv :rewrite-constant) *initial-clause-id* wrld ctx state))) (value (change rewrite-constant rcnst :current-clause clause :current-literal (make current-literal :not-flg nil :atm *rewrite$-last-literal*) :force-info t))))
make-rrecfunction
(defun make-rrec (thyps thints untranslate ctx wrld state) (b* ((saved-pspv (rewrite$-pspv thints wrld state)) (hyps-clause (dumb-negate-lit-lst thyps)) (clause (add-literal *rewrite$-last-literal* hyps-clause t)) ((er rcnst) (rewrite$-rcnst clause saved-pspv thints ctx wrld state)) (gstack (initial-gstack 'simplify-clause nil clause)) ((er (list* type-alist pot-lst fc-pair-lst)) (rewrite$-setup hyps-clause rcnst untranslate ctx wrld state))) (value (make rewrite$-record :saved-pspv saved-pspv :rcnst rcnst :type-alist type-alist :gstack gstack :fc-pair-lst fc-pair-lst :pot-lst pot-lst))))
rewrite$-forced-assumptions-hintsfunction
(defun rewrite$-forced-assumptions-hints (prove-forced-assumptions thints ctx wrld state) (cond ((consp prove-forced-assumptions) (translate-hints 'rewrite$ prove-forced-assumptions ctx wrld state)) ((eq prove-forced-assumptions :same-hints) (value thints)) ((member-eq prove-forced-assumptions '(t nil :none-forced)) (value nil)) (t (er soft ctx "The :prove-forced-assumptions argument, ~x0, is illegal." prove-forced-assumptions))))
collect-non-termp-cdrsfunction
(defun collect-non-termp-cdrs (alist wrld) (declare (xargs :guard (alistp alist))) (cond ((endp alist) nil) ((termp (cdar alist) wrld) (collect-non-termp-cdrs (cdr alist) wrld)) (t (cons (cdar alist) (collect-non-termp-cdrs (cdr alist) wrld)))))
collect-non-termsfunction
(defun collect-non-terms (lst wrld) (cond ((endp lst) nil) ((termp (car lst) wrld) (collect-non-terms (cdr lst) wrld)) (t (cons (car lst) (collect-non-terms (cdr lst) wrld)))))
rewrite$-translate-hints-fnfunction
(defun rewrite$-translate-hints-fn (backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p ctx wrld state) (b* ((kwd-alist (append (and backchain-limit-rw (list :backchain-limit-rw backchain-limit-rw)) (and expand (list :expand expand)) (and hands-off (list :hands-off hands-off)) (and in-theory (list :in-theory in-theory)) (and no-thanks (list :no-thanks no-thanks)) (and nonlinearp (list :nonlinearp nonlinearp)) (and restrict (list :restrict restrict)) (and rw-cache-state (list :rw-cache-state rw-cache-state)))) (hints0 `(("Goal" ,@KWD-ALIST))) (default-hints (default-hints wrld))) (cond ((or kwd-alist default-hints) (if default-hints-p (translate-hints+ ctx hints0 default-hints ctx wrld state) (translate-hints ctx hints0 ctx wrld state))) (t (value nil)))))
rewrite$-translate-lstfunction
(defun rewrite$-translate-lst (lst translate ctx wrld state) (cond ((null lst) (value nil)) ((not (true-listp lst)) (er soft ctx "Not a true-list:~|~x0." lst)) (translate (translate-term-lst lst t t t ctx wrld state)) (t (let ((bad (collect-non-terms lst wrld))) (cond ((null bad) (value lst)) (t (er soft ctx "A supplied list of terms included the following, ~ which ~#0~[is not a term~/are not terms~]: ~&0. ~ Specify :translate t to avoid this error." bad)))))))
rewrite$-fnfunction
(defun rewrite$-fn (term alist hyps equiv geneqv obj backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p prove-forced-assumptions translate untranslate must-rewrite repeat ctx wrld rrec state) (with-guard-checking-error-triple nil (b* (((er ?) (rewrite$-check-args alist must-rewrite repeat hyps backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state rrec ctx wrld state)) ((er tterm) (cond (translate (translate term t t t ctx wrld state)) ((termp term wrld) (value term)) (t (er soft ctx "The first argument of rewrite$ must be a term unless ~ :translate is specifed, but ~x0 is not a term." term)))) ((er translated-alist) (cond ((not (symbol-alistp alist)) (er soft ctx "The :ALIST argument that was supplied rewrite$ is not a ~ symbol-alistp:~|~x0." alist)) (translate (b* (((er cdrs) (translate-term-lst (strip-cdrs alist) t t t ctx wrld state))) (value (pairlis$ (strip-cars alist) cdrs)))) (t (b* ((bad (collect-non-termp-cdrs alist wrld)) ((when bad) (er soft ctx "Non-term value~#0~[~/s~] in :ALIST argument of ~ rewrite$:~|~&0" bad))) (value alist))))) ((er thyps) (cond (rrec (value :ignored)) (t (rewrite$-translate-lst hyps translate ctx wrld state)))) ((er geneqv) (cond ((null equiv) (value geneqv)) (geneqv (er soft ctx "It is illegal for a call of rewrite$ to include values ~ for both the :EQUIV and :GENEQV options.")) ((eq equiv 'equal) (value nil)) ((not (symbolp equiv)) (er soft ctx "The :EQUIV argument of rewrite$ must be a symbol, unlike ~ ~x0." equiv)) ((equivalence-relationp equiv wrld) (value (cadr (car (last (getpropc equiv 'congruences nil wrld)))))) (t (er soft ctx "The :EQUIV argument of rewrite$ must denote a known ~ equivalence relation, unlike ~x0." equiv)))) ((er thints) (cond (rrec (value (access prove-spec-var (access rewrite$-record rrec :saved-pspv) :orig-hints))) (t (rewrite$-translate-hints-fn backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p ctx wrld state)))) ((er rrec) (cond (rrec (value rrec)) (t (make-rrec thyps thints untranslate ctx wrld state)))) ((er forced-assumptions-hints) (rewrite$-forced-assumptions-hints prove-forced-assumptions thints ctx wrld state)) (- (semi-initialize-brr-wormhole state)) (- (initialize-fc-wormhole-sites))) (rewrite$-main tterm translated-alist geneqv obj prove-forced-assumptions forced-assumptions-hints untranslate must-rewrite repeat rrec ctx wrld state))))
rewrite$macro
(defmacro rewrite$ (term &key alist (ctx ''rewrite$) hyps equiv geneqv backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state (default-hints-p 't) (prove-forced-assumptions 't) translate untranslate must-rewrite (repeat '1) (obj ''?) rrec (wrld '(w state))) `(rewrite$-fn ,TERM ,ALIST ,HYPS ,EQUIV ,GENEQV ,OBJ ,BACKCHAIN-LIMIT-RW ,EXPAND ,HANDS-OFF ,IN-THEORY ,NO-THANKS ,NONLINEARP ,RESTRICT ,RW-CACHE-STATE ,DEFAULT-HINTS-P ,PROVE-FORCED-ASSUMPTIONS ,TRANSLATE ,UNTRANSLATE ,MUST-REWRITE ,REPEAT ,CTX ,WRLD ,RREC state))
flatten-ors-in-litfunction
(defun flatten-ors-in-lit (term) (case-match term (('not ('if & & &)) (dumb-negate-lit-lst (flatten-ands-in-lit (fargn term 1)))) (('if t1 t2 t3) (cond ((or (equal t2 *t*) (equal t2 t1)) (append (flatten-ors-in-lit t1) (flatten-ors-in-lit t3))) ((equal t3 *t*) (append (flatten-ors-in-lit (dumb-negate-lit t1)) (flatten-ors-in-lit t2))) (t (list term)))) (& (cond ((equal term *nil*) nil) (t (list term))))))
flatten-ors-in-lit-lstfunction
(defun flatten-ors-in-lit-lst (x) (if (endp x) nil (append (flatten-ors-in-lit (car x)) (flatten-ors-in-lit-lst (cdr x)))))
rewrite$-clause-tailfunction
(defun rewrite$-clause-tail (tail pts bkptr gstack new-clause fc-pair-lst wrld pot-lst rcnst ttree state) (cond ((null tail) (mv nil (flatten-ors-in-lit-lst new-clause) ttree)) (t (b* (((mv not-flg atm) (strip-not (car tail))) (new-pts (cons (car pts) (access rewrite-constant rcnst :pt))) (local-rcnst (change rewrite-constant rcnst :current-literal (make current-literal :not-flg not-flg :atm atm) :pt new-pts)) ((mv contradictionp type-alist ttree0 current-clause) (rewrite-clause-type-alist tail new-clause fc-pair-lst local-rcnst wrld pot-lst)) ((when contradictionp) (mv nil (list *t*) (cons-tag-trees ttree0 ttree))) (rw-cache-state (access rewrite-constant rcnst :rw-cache-state)) ((mv ?step-limit val ttree1 ?fttree1) (pstk (rewrite-atm atm not-flg bkptr gstack type-alist wrld pot-lst local-rcnst current-clause state *default-step-limit* (cond ((eq rw-cache-state :atom) (erase-rw-cache ttree)) (t ttree))))) (ttree1 (cond ((eq rw-cache-state :atom) (erase-rw-cache ttree1)) (t ttree1))) ((mv ?step-limit bad-ass ttree1) (resume-suspended-assumption-rewriting ttree1 nil gstack pot-lst local-rcnst wrld state *default-step-limit*)) (val (cond (bad-ass (car tail)) (not-flg (dumb-negate-lit val)) (t val))) ((when (equal val *t*)) (mv "by rewriting a negated hypothesis, ~x0, to T" (car tail) nil))) (rewrite$-clause-tail (cdr tail) (cdr pts) (1+ bkptr) gstack (add-literal val new-clause t) fc-pair-lst wrld pot-lst (if (equal val *nil*) local-rcnst rcnst) (cond (bad-ass ttree) ((eq rw-cache-state :atom) ttree1) (t (accumulate-rw-cache t ttree1 ttree))) state)))))
rewrite$-clause*function
(defun rewrite$-clause* (clause repeat-limit completed-iters rcnst gstack ttree fc-pair-lst pot-lst untranslate ctx wrld state) (b* (((mv str new-clause new-ttree) (rewrite$-clause-tail clause (enumerate-elements clause 0) 1 gstack nil fc-pair-lst wrld pot-lst rcnst ttree state)) ((when str) (let ((term new-clause) (cl (dumb-negate-lit-lst clause))) (er soft ctx *simplify$-hyps-contradiction-string* (if untranslate (untranslate-lst cl t wrld) cl) (msg str (if untranslate (untranslate term t wrld) term))))) ((when (equal clause new-clause)) (value (list* clause ttree))) (completed-iters (1+ completed-iters)) ((er (list* ?type-alist new-pot-lst new-fc-pair-lst)) (rewrite$-setup new-clause rcnst untranslate ctx wrld state)) ((when (int= repeat-limit completed-iters)) (value (list* new-clause new-ttree))) (state (io? prove nil state (completed-iters) (fms "NOTE: Starting ~n0 iteration for rewrite$-hyps.~%" (list (cons #\0 (list (1+ completed-iters)))) (proofs-co state) state nil))) (rcnst (change rewrite-constant rcnst :current-clause new-clause)) ((mv ?step-limit bad-ass new-ttree) (resume-suspended-assumption-rewriting new-ttree nil gstack pot-lst rcnst wrld state *default-step-limit*)) ((mv fc-pair-lst pot-lst) (cond (bad-ass (mv fc-pair-lst pot-lst)) (t (mv new-fc-pair-lst new-pot-lst))))) (rewrite$-clause* new-clause repeat-limit completed-iters rcnst gstack new-ttree fc-pair-lst pot-lst untranslate ctx wrld state)))
update-rrecfunction
(defun update-rrec (rrec hyps-clause untranslate ctx wrld state) (b* ((clause (add-literal *rewrite$-last-literal* hyps-clause t)) (rcnst (change rewrite-constant (access rewrite$-record rrec :rcnst) :current-clause clause)) ((er (list* type-alist pot-lst fc-pair-lst)) (rewrite$-setup hyps-clause rcnst untranslate ctx wrld state))) (value (change rewrite$-record rrec :rcnst rcnst :type-alist type-alist :fc-pair-lst fc-pair-lst :pot-lst pot-lst))))
rewrite$-hyps-returnfunction
(defun rewrite$-hyps-return (clause update-rrec rrec ttree pairs untranslate ctx wrld state) (b* (((er rrec) (cond ((not update-rrec) (value rrec)) (t (update-rrec rrec clause untranslate ctx wrld state))))) (value (list* (dumb-negate-lit-lst clause) rrec ttree pairs))))
rewrite$-translate-hintsmacro
(defmacro rewrite$-translate-hints (ctx &key backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p (wrld '(w state))) `(rewrite$-translate-hints-fn ctx ,BACKCHAIN-LIMIT-RW ,EXPAND ,HANDS-OFF ,IN-THEORY ,NO-THANKS ,NONLINEARP ,RESTRICT ,RW-CACHE-STATE ,DEFAULT-HINTS-P ,CTX ,WRLD state))
rewrite$-hyps-mainfunction
(defun rewrite$-hyps-main (hyps thints backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p default-hints-p-p update-rrec prove-forced-assumptions translate untranslate repeat-limit ctx wrld state) (with-guard-checking-error-triple nil (b* (((er ?) (chk-repeat repeat-limit ctx state)) ((er thyps) (rewrite$-translate-lst hyps translate ctx wrld state)) ((er thints) (cond ((and thints (or backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p-p)) (er soft ctx "It is illegal to supply keyword :THINTS to rewrite$-hyps if ~ any individual hints keywords are supplied, in this case: ~&0." `(,@(AND BACKCHAIN-LIMIT-RW '(:BACKCHAIN-LIMIT-RW)) ,@(AND EXPAND '(:EXPAND)) ,@(AND HANDS-OFF '(:HANDS-OFF)) ,@(AND IN-THEORY '(:IN-THEORY)) ,@(AND NO-THANKS '(:NO-THANKS)) ,@(AND NONLINEARP '(:NONLINEARP)) ,@(AND RESTRICT '(:RESTRICT)) ,@(AND RW-CACHE-STATE '(:RW-CACHE-STATE)) ,@(AND DEFAULT-HINTS-P-P '(:DEFAULT-HINTS-P-P))))) (thints (value thints)) (t (rewrite$-translate-hints-fn backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state default-hints-p ctx wrld state)))) ((er rrec) (make-rrec thyps thints untranslate ctx wrld state)) (rcnst (access rewrite$-record rrec :rcnst)) (gstack (access rewrite$-record rrec :gstack)) (fc-pair-lst (access rewrite$-record rrec :fc-pair-lst)) (pot-lst (access rewrite$-record rrec :pot-lst)) (saved-pspv (access rewrite$-record rrec :saved-pspv)) ((er (list* clause ttree)) (rewrite$-clause* (dumb-negate-lit-lst thyps) repeat-limit 0 rcnst gstack nil fc-pair-lst pot-lst untranslate ctx wrld state)) (ttree (set-cl-ids-of-assumptions ttree *initial-clause-id*)) ((mv n0 assns pairs ttree) (extract-and-clausify-assumptions nil ttree nil (access rewrite-constant rcnst :current-enabled-structure) wrld (splitter-output))) ((when (or (null pairs) (not prove-forced-assumptions))) (rewrite$-hyps-return clause update-rrec rrec ttree pairs untranslate ctx wrld state)) ((when (eq prove-forced-assumptions :none-forced)) (er soft ctx "There were forced assumptions from simplifying hypotheses, ~ which is not allowed in this context.")) (clause-set (strip-cdrs pairs)) (forced-goal (termify-clause-set clause-set)) (state (rewrite$-process-assumptions-msg n0 pairs untranslate clause-set forced-goal wrld state)) ((er forced-assumptions-hints) (rewrite$-forced-assumptions-hints prove-forced-assumptions thints ctx wrld state)) ((mv erp val state) (prove forced-goal (change prove-spec-var saved-pspv :user-supplied-term forced-goal) forced-assumptions-hints (ens state) wrld ctx state)) ((when erp) (er soft ctx "Rewriting of hypotheses has failed because of failure to prove ~ all of the assumptions forced during the rewriting. Either ~ disable forcing (see :DOC disable-forcing) or, if you are ~ willing to ignore the forced assumptions, specify option ~ :PROVE-FORCED-ASSUMPTIONS NIL for rewrite$-hyps.")) (ttree (process-assumptions-ttree assns ttree))) (rewrite$-hyps-return clause update-rrec rrec (cons-tag-trees val ttree) pairs untranslate ctx wrld state))))
rewrite$-hypsmacro
(defmacro rewrite$-hyps (hyps &key thints backchain-limit-rw expand hands-off in-theory no-thanks nonlinearp restrict rw-cache-state (default-hints-p 't default-hints-p-p) (update-rrec 't) (prove-forced-assumptions 't) translate untranslate (repeat '1) (ctx ''rewrite$-hyps) (wrld '(w state))) `(rewrite$-hyps-main ,HYPS ,THINTS ,BACKCHAIN-LIMIT-RW ,EXPAND ,HANDS-OFF ,IN-THEORY ,NO-THANKS ,NONLINEARP ,RESTRICT ,RW-CACHE-STATE ,DEFAULT-HINTS-P ,DEFAULT-HINTS-P-P ,UPDATE-RREC ,PROVE-FORCED-ASSUMPTIONS ,TRANSLATE ,UNTRANSLATE ,REPEAT ,CTX ,WRLD state))
*rewrite$-false-context*constant
(defconst *rewrite$-false-context* (list *nil*))
*rewrite$-true-context*constant
(defconst *rewrite$-true-context* nil)
rewrite$-context-tailfunction
(defun rewrite$-context-tail (tail bkptr rdepth gstack type-alist wrld pot-lst rcnst ttree state step-limit ts-backchain-limit acc) (cond ((null tail) (mv nil (reverse acc) type-alist ttree)) (t (b* (((mv not-flg atm) (strip-not (car tail))) ((mv step-limit val ttree1) (rewrite-entry (rewrite atm nil bkptr) :rdepth rdepth :step-limit step-limit :type-alist type-alist :obj '? :geneqv *geneqv-iff* :pequiv-info nil :wrld wrld :state state :fnstack nil :ancestors nil :backchain-limit (access rewrite-constant rcnst :backchain-limit-rw) :simplify-clause-pot-lst nil :rcnst rcnst :gstack gstack :ttree ttree)) ((mv step-limit bad-ass ttree1) (resume-suspended-assumption-rewriting ttree1 nil gstack pot-lst rcnst wrld state step-limit)) ((mv term ttree) (cond (bad-ass (mv (car tail) ttree)) (not-flg (mv (dumb-negate-lit val) ttree1)) (t (mv val ttree1)))) (ens (access rewrite-constant rcnst :current-enabled-structure)) ((mv must-be-true must-be-false true-type-alist ?false-type-alist ts-ttree) (assume-true-false-bc term nil (ok-to-force rcnst) nil type-alist ens wrld pot-lst nil :fta ts-backchain-limit)) ((when must-be-true) (rewrite$-context-tail (cdr tail) (1+ bkptr) rdepth gstack type-alist wrld pot-lst rcnst (cons-tag-trees ts-ttree ttree) state step-limit ts-backchain-limit acc)) ((when must-be-false) (mv "by rewriting a contextual test term, ~x0, to NIL" (car tail) nil (cons-tag-trees ts-ttree ttree)))) (rewrite$-context-tail (cdr tail) (1+ bkptr) rdepth gstack true-type-alist wrld pot-lst rcnst ttree state step-limit ts-backchain-limit (cons term acc))))))
rewrite$-context*function
(defun rewrite$-context* (lst repeat-limit completed-iters rdepth gstack type-alist wrld pot-lst rcnst contradiction-ok untranslate ttree step-limit ts-backchain-limit ctx state) (b* (((mv str new-lst new-type-alist new-ttree) (rewrite$-context-tail lst 1 rdepth gstack type-alist wrld pot-lst rcnst ttree state step-limit ts-backchain-limit nil)) ((when str) (cond (contradiction-ok (value (list* *rewrite$-false-context* new-type-alist new-ttree))) (t (let ((term new-lst)) (er soft ctx *simplify$-hyps-contradiction-string* (if untranslate (untranslate-lst lst t wrld) lst) (msg str (if untranslate (untranslate term t wrld) term))))))) ((when (equal lst new-lst)) (value (list* lst new-type-alist ttree))) (completed-iters (1+ completed-iters)) ((when (int= repeat-limit completed-iters)) (value (list* (flatten-ands-in-lit-lst new-lst) new-type-alist new-ttree))) (state (io? prove nil state (completed-iters) (fms "NOTE: Starting ~n0 iteration for rewrite$-context.~%" (list (cons #\0 (list (1+ completed-iters)))) (proofs-co state) state nil)))) (rewrite$-context* new-lst repeat-limit completed-iters rdepth gstack type-alist wrld pot-lst rcnst contradiction-ok untranslate new-ttree step-limit ts-backchain-limit ctx state)))
rewrite$-context-returnfunction
(defun rewrite$-context-return (lst type-alist rrec ttree pairs) (list* lst (change rewrite$-record rrec :type-alist type-alist) ttree pairs))
rewrite$-context-mainfunction
(defun rewrite$-context-main (lst rrec contradiction-ok prove-forced-assumptions translate untranslate repeat-limit ctx wrld state) (with-guard-checking-error-triple nil (b* (((er ?) (chk-repeat repeat-limit ctx state)) (rcnst (access rewrite$-record rrec :rcnst)) (gstack (access rewrite$-record rrec :gstack)) (type-alist (access rewrite$-record rrec :type-alist)) (pot-lst (access rewrite$-record rrec :pot-lst)) (saved-pspv (access rewrite$-record rrec :saved-pspv)) ((er tlst) (rewrite$-translate-lst lst translate ctx wrld state)) ((er (list* lst2 type-alist ttree)) (rewrite$-context* tlst repeat-limit 0 (rewrite-stack-limit wrld) gstack type-alist wrld pot-lst rcnst contradiction-ok untranslate nil *default-step-limit* (backchain-limit wrld :ts) ctx state)) (ttree (set-cl-ids-of-assumptions ttree *initial-clause-id*)) ((mv n0 assns pairs ttree) (extract-and-clausify-assumptions nil ttree nil (access rewrite-constant rcnst :current-enabled-structure) wrld (splitter-output))) ((when (or (null pairs) (not prove-forced-assumptions))) (value (rewrite$-context-return lst2 type-alist rrec ttree pairs))) ((when (eq prove-forced-assumptions :none-forced)) (er soft ctx "There were forced assumptions from simplifying the context, but ~ proving of forced assumptions has been disabled for this call ~ of rewrite$-context.")) (clause-set (strip-cdrs pairs)) (forced-goal (termify-clause-set clause-set)) (state (rewrite$-process-assumptions-msg n0 pairs untranslate clause-set forced-goal wrld state)) (thints (access prove-spec-var saved-pspv :orig-hints)) ((er forced-assumptions-hints) (rewrite$-forced-assumptions-hints prove-forced-assumptions thints ctx wrld state)) ((mv erp val state) (prove forced-goal (change prove-spec-var saved-pspv :user-supplied-term forced-goal) forced-assumptions-hints (ens state) wrld ctx state)) ((when erp) (er soft ctx "Rewriting of hypotheses has failed because of failure to prove ~ all of the assumptions forced during the rewriting. Either ~ disable forcing (see :DOC disable-forcing) or, if you are ~ willing to ignore the forced assumptions, specify option ~ :PROVE-FORCED-ASSUMPTIONS NIL for rewrite$-context.")) (ttree (process-assumptions-ttree assns ttree))) (value (rewrite$-context-return lst2 type-alist rrec (cons-tag-trees val ttree) pairs)))))
rewrite$-contextmacro
(defmacro rewrite$-context (lst rrec &key contradiction-ok (prove-forced-assumptions 't) translate untranslate (repeat '1) (ctx ''rewrite$-context) (wrld '(w state))) `(rewrite$-context-main ,LST ,RREC ,CONTRADICTION-OK ,PROVE-FORCED-ASSUMPTIONS ,TRANSLATE ,UNTRANSLATE ,REPEAT ,CTX ,WRLD state))