Commit ff0f8a53b4c9d3575f18a055501da5017f38a52a - cafeobj

Having extra variables in RHS is only reported when verbose is on. tswd 8 years ago

1 changed file(s) with 13 addition(s) and 18 deletion(s). Raw diff Collapse all Expand all

+13

-18

chaos/construct/gen-rule.lisp less more

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-rhs rule))
120		(term-contains-match-op (axiom-condition rule)))
121		;; it's ok to have extra variables in RHS side.
122		(progn
123		(add-rule-to-module module rule)
124		(unless (term-is-variable? (axiom-lhs rule))
125		(add-associative-extensions module
126		(term-head (axiom-lhs rule))
127		rule)
128		(specialize-rule rule module)))
129		;; else we don't allow it as rewrite rule
130		(progn
131		(setf (axiom-kind rule) ':bad-rule)
132		(add-rule-to-module module rule)
133		(with-output-chaos-warning ()
134		(format t "RHS of the axiom has extra variable(s) which does not occur in LHS.")
135		(format t "~%... ignored as rewrite rule.")
136		(return-from gen-rule-internal nil)))))
	119	(unless (or (term-contains-match-op (axiom-rhs rule))
	120	(term-contains-match-op (axiom-condition rule)))
	121	(when chaos-verbose
	122	(with-output-chaos-warning ()
	123	(format t "RHS of the axiom has extra variable(s) which does not occur in LHS.")
	124	(print-next)
	125	(print-axiom-brief rule))))
	126	(add-rule-to-module module rule)
	127	(unless (term-is-variable? (axiom-lhs rule))
	128	(add-associative-extensions module
	129	(term-head (axiom-lhs rule))
	130	rule)
	131	(specialize-rule rule module)))
137	132	((and (axiom-is-behavioural rule)
138	133	(not (and (term-can-be-in-beh-axiom? (axiom-lhs rule))
139	134	(term-can-be-in-beh-axiom? (axiom-rhs rule)))))