Codebase list cafeobj / 21b4573
Treatment of =*= proof in which match method is not computed yet. This is symptomatic treatment, no fundamental fix. Had no problem prior 1.5.3. tswd 8 years ago
3 changed file(s) with 37 addition(s) and 62 deletion(s). Raw diff Collapse all Expand all
+11
-42
chaos/cafein/rengine.lisp less more
263263 ;;; BASIC PROCS for REWRITE RULE APPLICATION
264264 (defvar *memo-debug* nil)
265265
266 #| NOT USED
267 (defmacro term-replace-with-memo (old new)
268 (once-only (old new)
269 ` (if (and (not (term-is-builtin-constant? ,old))
270 (or *always-memo*
271 (method-has-memo (term-head ,old))))
272 (let ((term-memo (simple-copy-term ,old)))
273 (when *memo-debug*
274 (when (term-equational-equal term-memo ,new)
275 (with-output-chaos-warning ()
276 (format t "E-E term is about to hashed!")
277 (terpri)
278 (term-print-with-sort ,new)))
279 (format t "~%[memo]: ")
280 (term-print-with-sort term-memo)
281 (format t "~% ==> ")
282 (term-print-with-sort ,new))
283 (set-hashed-term term-memo *term-memo-table* ,new)
284 (term-replace ,old ,new))
285 (term-replace ,old ,new))))
286 |#
287
288266 (declaim (inline term-replace-dd-simple))
289267 #-gcl
290268 (defun term-replace-dd-simple (old new)
339317 (rhs-instance nil))
340318 (multiple-value-bind (global-state subst no-match E-equal)
341319 ;; first we find matching rewrite rule
342 (funcall (rule-first-match-method rule) (rule-lhs rule) term)
320 (funcall (or (rule-first-match-method rule)
321 (progn
322 (with-output-chaos-warning ()
323 (format t "Internal, no 'matching-mehod' is assigned for:")
324 (print-next)
325 (print-axiom-brief rule))
326 (compute-rule-method rule)
327 (rule-first-match-method rule)))
328 (rule-lhs rule)
329 term)
343330 ;; stat, count up number of matching trials
344331 (incf $$matches)
345332 (setq *cafein-current-subst* subst) ; I don't remember for what this is used
816803 ;; return t iff the rule is applied.
817804 is-applied))
818805
819 #|| -- moved to reducer.lisp
820 (defun simplify-on-top (term)
821 (declare (type term term)
822 (values t))
823 (if (term-is-application-form? term)
824 (apply-rules-with-different-top term
825 (method-rules-with-different-top
826 (term-method term)))
827 term))
828 ||#
829
830806 ;;;
831807 ;;; REWRITE ENGINE
832808 ;;;
843819 (declare (type term term)
844820 (type list strategy)
845821 (values (or null t)))
846 ;;
847822 (when *rewrite-debug*
848823 (with-output-simple-msg ()
849824 (format t "[reduce-term](NF=~a,LP=~a): " (term-is-reduced? term) (term-is-lowest-parsed? term))
857832 (unless (term-is-lowest-parsed? term)
858833 (multiple-value-bind (xterm assoc?)
859834 (update-lowest-parse term)
835 (declare (ignore xterm))
860836 (when (or assoc?
861837 (not (method= (term-method term) top)))
862838 (when *rewrite-debug*
16431619 (setq $$term saved-$$term)
16441620 term))))
16451621
1646 ;;; ****
1647 ;;; INIT
1648 ;;; ****
1649 ;;;(eval-when (:execute :load-toplevel)
1650 ;;; (setf (symbol-function 'apply-one-rule)
1651 ;;; #'apply-one-rule-simple))
1652
16531622 ;;; EOF
16541623
+25
-19
chaos/construct/axiom.lisp less more
471471 ;;;
472472 (defun compute-rule-method (rule)
473473 (declare (type axiom rule)
474 (values t))
474 (values t))
475 (when *on-axiom-debug*
476 (format t "~%[CRM] compute rule method")
477 (format t "~% (~x) " (addr-of rule))
478 (print-axiom-brief rule))
475479 (let ((m (choose-match-method (axiom-lhs rule)
476 (axiom-condition rule)
477 (axiom-kind rule))))
480 (axiom-condition rule)
481 (axiom-kind rule))))
478482 (setf (axiom-first-match-method rule) (car m))
479483 (setf (axiom-next-match-method rule) (cdr m))
480484 rule))
481
485
482486 ;;; RULE-COPY : rule -> rule
483487 ;;;-----------------------------------------------------------------------------
484488 ;;; Returns a copy of "rule". The variable occuring in the rule are also
614618 (values list))
615619 (do* ((lst rs (cdr lst))
616620 (r (car lst) (car lst)))
617 ((null lst) (cons rule rs))
621 ((null lst) (cons rule rs))
618622 (when (rule-is-similar? rule r)
619 (when (and *chaos-verbose*
623 (when (and (or *chaos-verbose* *on-axiom-debug*)
620624 (not (eq rule r))
621625 (not (member (axiom-kind rule) .ext-rule-kinds.)))
622626 (with-output-msg ()
630634 (let ((newlhs (axiom-lhs rule))
631635 (oldlhs (axiom-lhs r)))
632636 (when (and (not (term-is-variable? newlhs))
633 (not (term-is-variable? oldlhs))
634 (not (method= (term-method newlhs) (term-method oldlhs)))
635 (sort<= (term-sort oldlhs) (term-sort newlhs)))
636 (rplaca lst rule))
637 (not (term-is-variable? oldlhs))
638 (not (method= (term-method newlhs) (term-method oldlhs)))
639 (sort<= (term-sort oldlhs) (term-sort newlhs)))
640 (rplaca lst rule))
637641 (return-from adjoin-rule rs)))))
638642
639643 ;;; RULE-OCCURS : rule ruleset -> Bool
714718 (declare (type module module)
715719 (type axiom ax)
716720 (values t))
717 (if (memq (axiom-type ax) '(:equation :pignose-axiom :pignose-goal))
718 (setf (module-equations module)
719 (adjoin-rule ax (module-equations module)))
721 (with-in-module (module)
722 (if (memq (axiom-type ax) '(:equation :pignose-axiom :pignose-goal))
723 (setf (module-equations module)
724 (adjoin-rule ax (module-equations module)))
720725 (setf (module-rules module)
721 (adjoin-rule ax (module-rules module)))))
726 (adjoin-rule ax (module-rules module))))))
722727
723728 (defun add-rule-to-module (module rule)
724729 (declare (type module module)
725730 (type axiom rule)
726731 (values t))
727 (add-rule-to-method rule
728 (term-head (axiom-lhs rule))
729 (module-opinfo-table module))
730 (pushnew rule (module-rewrite-rules module)
731 :test #'rule-is-similar?))
732 (with-in-module (module)
733 (add-rule-to-method rule
734 (term-head (axiom-lhs rule))
735 (module-opinfo-table module))
736 (pushnew rule (module-rewrite-rules module)
737 :test #'rule-is-similar?)))
732738
733739 (defun add-rule-to-method (rule method
734740 &optional (opinfo-table *current-opinfo-table*))
+1
-1
chaos/construct/beh.lisp less more
401401 (set-needs-rule module))))))
402402
403403 (defun beh-rewrite (term mod)
404 (reducer term mod :red))
404 (reducer-no-stat term mod :red))
405405
406406 ;;; EOF