|
|
|---|
|
|
|
|---|
To access context sensitive information within break-rewrite
Example: (brr@ :target) ; the term being rewritten (brr@ :unify-subst) ; the unifying substitution General Form: (brr@ :symbol)
where
:symbol (brr@ :symbol) ------- --------------------- :target the term to be rewritten. This term is an instantiation of the left-hand side of the conclusion of the rewrite-rule being broken. This term is in translated form! Thus, if you are expecting (equal x nil) -- and your expectation is almost right -- you will see (equal x 'nil); similarly, instead of (cadr a) you will see (car (cdr a)). In translated forms, all constants are quoted (even nil, t, strings and numbers) and all macros are expanded. :unify-subst the substitution that, when applied to :target, produces the left-hand side of the rule being broken. This substitution is an alist pairing variable symbols to translated (!) terms. :wonp t or nil indicating whether the rune was successfully applied. (brr@ :wonp) returns nil if evaluated before :EVALing the rule. :rewritten-rhs the result of successfully applying the rewrite rule or else nil if (brr@ :wonp) is nil. The result of successfully applying the rule is always a translated (!) term and is never nil. :poly-list the result of successfully applying the linear rule or else nil if (brr@ :wonp) is nil. This result represents the list of polynomials produced by the rule application. The leading term of each polynomial is enclosed in an extra set of parentheses. :pot-list * the pot-list, which is the set of polynomials that are assumed in the current context, organized by maximal term. Each polynomial in the list is a linear-pot record. :failure-reason some non-nil lisp object indicating why the rule was not applied or else nil. Before the rule is :EVALed, (brr@ :failure-reason) is nil. After :EVALing the rule, (brr@ :failure-reason) is nil if (brr@ :wonp) is t. Rather than document the various non-nil objects returned as the failure reason, we encourage you simply to evaluate (brr@ :failure-reason) in the contexts of interest. Alternatively, study the ACL2 function tilde-@- failure-reason-phrase. :lemma * the rewrite rule being broken. For example, (access rewrite-rule (brr@ :lemma) :lhs) will return the left-hand side of the conclusion of the rule. :type-alist * a display of the type-alist governing :target. Elements on the displayed list are of the form (term type), where term is a term and type describes information about term assumed to hold in the current context. (See also the documentation for type-alist.) The type-alist may be used to determine the current assumptions, e.g., whether A is a CONSP. :ancestors * a stack of frames indicating the backchain history of the current context. The theorem prover is in the process of trying to establish each hypothesis in this stack. Thus, the negation of each hypothesis can be assumed false. Each frame also records the rules on behalf of which this backchaining is being done and the weight (function symbol count) of the hypothesis. All three items are involved in the heuristic for preventing infinite backchaining. Exception: Some frames are ``binding hypotheses'' (equal var term) or (equiv var (double-rewrite term)) that bind variable var to the result of rewriting term. The ACL2 source code has a definition (defrec ancestor ...) that may provide some relevant insight. :initial-ttree * the initial and (after :EVAL) final tag trees, :final-ttree respectively. (Tag trees are low-level data structures that store lemmas used and other information, as documented in topic TTREE.) :gstack * the current goal stack. The gstack is maintained by rewrite and is the data structure printed as the current ``path.'' Thus, any information derivable from the :path brr command is derivable from gstack. For example, from gstack one might determine that the current term is the second hypothesis of a certain rewrite rule.
In general