Improved checking extra variables in RHS. Vars introduced by := are
no harm, but for other cases, system marks them as 'bad' and does not
use them in rewriting.
tswd
8 years ago
| 591 | 591 |
rule)
|
| 592 | 592 |
(loop
|
| 593 | 593 |
(setq rule (car rr-current))
|
| 594 | |
(when (apply-rule rule term)
|
| 595 | |
(setq rr-mark rr-current)
|
| 596 | |
(loop (unless (apply-rule rule term) (return nil))))
|
| 597 | |
(setq rr-current (cdr rr-current))
|
| 598 | |
(when (eq rr-current rr-mark) (return nil)))))))
|
|
594 |
(unless (eq (axiom-kind rule) :bad-rule)
|
|
595 |
(when (apply-rule rule term)
|
|
596 |
(setq rr-mark rr-current)
|
|
597 |
(loop (unless (apply-rule rule term) (return nil))))
|
|
598 |
(setq rr-current (cdr rr-current))
|
|
599 |
(when (eq rr-current rr-mark) (return nil))))))))
|
| 599 | 600 |
|
| 600 | 601 |
(defun apply-rules-with-different-top (term rules)
|
| 601 | 602 |
(declare (type term term)
|
|
| 603 | 604 |
(values (or null t)))
|
| 604 | 605 |
(block the-end
|
| 605 | 606 |
(dolist (rule rules nil)
|
| 606 | |
(when (apply-rule rule term) (return-from the-end t)))))
|
|
607 |
(unless (eq (axiom-kind rule) :bad-rule)
|
|
608 |
(when (apply-rule rule term) (return-from the-end t))))))
|
| 607 | 609 |
|
| 608 | 610 |
(defun apply-rules (term strategy)
|
| 609 | 611 |
(declare (type term term)
|
| 116 | 116 |
(cond ((and lhsv
|
| 117 | 117 |
(or (not (subsetp rhs-vars lhsv))
|
| 118 | 118 |
(not (subsetp cond-vars lhsv))))
|
| 119 | |
(if (or (term-contains-match-op (axiom-lhs rule))
|
| 120 | |
(term-contains-match-op (axiom-rhs rule)))
|
|
119 |
(if (or (term-contains-match-op (axiom-rhs rule))
|
|
120 |
(term-contains-match-op (axiom-condition rule)))
|
| 121 | 121 |
;; it's ok to have extra variables in RHS side.
|
| 122 | 122 |
(progn
|
| 123 | 123 |
(add-rule-to-module module rule)
|
|
| 126 | 126 |
(term-head (axiom-lhs rule))
|
| 127 | 127 |
rule)
|
| 128 | 128 |
(specialize-rule rule module)))
|
| 129 | |
;; else we don't allow it
|
|
129 |
;; else we don't allow it as rewrite rule
|
| 130 | 130 |
(progn
|
| 131 | 131 |
(setf (axiom-kind rule) ':bad-rule)
|
|
132 |
(add-rule-to-module module rule)
|
| 132 | 133 |
(with-output-chaos-warning ()
|
| 133 | 134 |
(format t "RHS of the axiom has extra variable(s) which does not occur in LHS.")
|
| 134 | |
(format t "~%... ignored.")
|
|
135 |
(format t "~%... ignored as rewrite rule.")
|
| 135 | 136 |
(return-from gen-rule-internal nil)))))
|
| 136 | 137 |
((and (axiom-is-behavioural rule)
|
| 137 | 138 |
(not (and (term-can-be-in-beh-axiom? (axiom-lhs rule))
|