Codebase list cafeobj / 0be30fd
Fixed the parsing problem introduced by the change in ordering algorithm of operators. tswd 8 years ago
6 changed file(s) with 81 addition(s) and 54 deletion(s). Raw diff Collapse all Expand all
+10
-0
chaos/cafein/reducer.lisp less more
248248 (rewrite $$target-term *current-module* rewrite-mode))))
249249 $$term)
250250
251 (defun simplify-on-top (term context-module)
252 (declare (type term term)
253 (values t))
254 (with-in-module ((prepare-reduction-env term context-module :red nil))
255 (catch 'rewrite-abort
256 (if (term-is-application-form? term)
257 (apply-rules-with-different-top term
258 (method-rules-with-different-top
259 (term-method term)))
260 term))))
251261 )
252262
253263
+2
-0
chaos/cafein/rengine.lisp less more
779779 ;; return t iff the rule is applied.
780780 is-applied))
781781
782 #| -- moved to reducer.lisp
782783 (defun simplify-on-top (term)
783784 (declare (type term term)
784785 (values t))
787788 (method-rules-with-different-top
788789 (term-method term)))
789790 term))
791 |#
790792
791793 ;;;
792794 ;;; REWRITE ENGINE
+39
-38
chaos/construct/gen-rule.lisp less more
3535 (declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
3636 #+:chaos-debug
3737 (declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
38
39 ;;; (defvar *gen-rule-debug* nil)
4038
4139 ;;; GENERATE REWRITE RULES module : -> module'
4240 ;;;-----------------------------------------------------------------------------
581579 (values t))
582580 (when *gen-rule-debug*
583581 (format t "~%[id-compl] given rule ~a, of kind ~a " r (axiom-kind r))
584 (print-next)
585 (print-chaos-object r))
582 (print-next))
586583 (unless (axiom-kind r)
587584 (let (varval
588585 (res nil)
617614 (setq sub1 (cons varval nil))
618615 (setq newsubst (substitution-can (cons varval subst)))
619616 (setq donesubst (cons (car sub1) donesubst))
620 (setq new-axiom (insert-val sub1 a-axiom))
617 (setq new-axiom (insert-val sub1 a-axiom module))
621618 (unless (or (null new-axiom)
622619 (rule-inf-subst-member newsubst res))
623620 (setq newres (cons (list new-axiom newsubst) newres)))))))
672669 (when e
673670 (setf (axiom-id-condition e) newidcond)))
674671 (unless (eq r rul)
672 (when *gen-rule-debug*
673 (format t "~%[id-compl]=> ")
674 (print-chaos-object newrule))
675675 (adjoin-axiom-to-module module newrule)))))))))
676676
677677 (defun test-bad-axiom (ax)
791791 (eq val (cdr ye)))
792792 (return t))))
793793
794 (defun insert-val (subs rul)
794 (defun insert-val (subs rul &optional (module *current-module*))
795795 (declare (type list subs)
796796 (type axiom rul)
797797 (values (or null axiom)))
800800 (*m-pattern-subst* nil))
801801 (let ((newcond (if (is-true? (axiom-condition rul))
802802 *BOOL-true*
803 (term-simplify
804 (normalize-for-identity-total
805 (substitution-partial-image subs (axiom-condition rul)))))))
803 (term-simplify
804 (normalize-for-identity-total
805 (substitution-partial-image subs (axiom-condition rul)))
806 module))))
806807 (if (is-false? newcond)
807808 nil
808809 (let ((rule nil)
811812 (rhs (term-simplify
812813 (normalize-for-identity-total
813814 (substitution-partial-image subs
814 (axiom-rhs rul)))))
815 (axiom-rhs rul)))
816 module))
815817 (condition (if (is-true? newcond)
816818 *BOOL-TRUE*
817819 newcond)))
834836 :labels (cons (car (create-rule-name 'dummy "idcomp")) (axiom-labels rul))))
835837 ;;
836838 (when *gen-rule-debug*
837 (format t "~%invert-val: ")
839 (format t "~%[insert-val]:----------")
838840 (format t "~% given rule : ")
839841 (print-chaos-object rul)
840842 (format t "~% gen rule : ")
10391041 (theory-standard-form (normalize-for-identity tm)))
10401042
10411043 ;;; rules for and or not == =/= identical nonidentical must not have conditions
1042 (defun term-simplify (tm)
1044 (defun term-simplify (tm &optional (module *current-module*))
10431045 (declare (type term tm)
10441046 (values (or null term)))
10451047 (if (term-is-variable? tm)
10461048 nil
1047 (if (term-is-constant? tm)
1048 nil
1049 (let ((meth (term-head tm)))
1050 (dolist (subtm (term-subterms tm))
1051 (term-simplify subtm))
1052 (if (or (eq *BOOL-and* meth)
1053 (eq *BOOL-or* meth)
1054 (eq *BOOL-not* meth)
1055 (eq *BOOL-if* meth))
1056 (simplify-on-top tm)
1057 (if (and (or (eq *BOOL-equal* meth)
1058 (eq *BOOL-nonequal* meth)
1059 (eq *identical* meth)
1060 (eq *nonidentical* meth))
1061 (term-is-ground? (term-arg-1 tm))
1062 (term-is-ground? (term-arg-2 tm)))
1063 (if (or (eq *BOOL-equal* meth)
1064 (eq *identical* meth))
1065 (if (term-is-similar? (term-arg-1 tm) (term-arg-2 tm))
1066 (term-replace tm (simple-copy-term *BOOL-true*))
1067 nil)
1068 (if (term-is-similar? (term-arg-1 tm) (term-arg-2 tm))
1069 (term-replace tm (simple-copy-term *BOOL-false*))
1070 nil))
1071 nil))
1072 )))
1049 (if (term-is-constant? tm)
1050 nil
1051 (let ((meth (term-head tm)))
1052 (dolist (subtm (term-subterms tm))
1053 (term-simplify subtm module))
1054 (if (or (eq *BOOL-and* meth)
1055 (eq *BOOL-or* meth)
1056 (eq *BOOL-not* meth)
1057 (eq *BOOL-if* meth))
1058 (simplify-on-top tm module)
1059 (if (and (or (eq *BOOL-equal* meth)
1060 (eq *BOOL-nonequal* meth)
1061 (eq *identical* meth)
1062 (eq *nonidentical* meth))
1063 (term-is-ground? (term-arg-1 tm))
1064 (term-is-ground? (term-arg-2 tm)))
1065 (if (or (eq *BOOL-equal* meth)
1066 (eq *identical* meth))
1067 (if (term-is-similar? (term-arg-1 tm) (term-arg-2 tm))
1068 (term-replace tm (simple-copy-term *BOOL-true*))
1069 nil)
1070 (if (term-is-similar? (term-arg-1 tm) (term-arg-2 tm))
1071 (term-replace tm (simple-copy-term *BOOL-false*))
1072 nil))
1073 nil)))))
10731074 tm)
10741075
10751076 (defun normalize-for-identity (term)
+13
-12
chaos/primitives/boperator.lisp less more
14721472 (return-from choose-lowest-op nil))))
14731473 (when *on-operator-debug*
14741474 (format t "~%--> ")
1475 (print-chaos-object res))))
1475 (print-chaos-object res))
1476 res))
14761477
14771478 (defun lowest-method (method lower-bound
14781479 &optional (module *current-module*))
15951596 (if (null (cdr overloaded-methods))
15961597 (if overloaded-methods
15971598 (car overloaded-methods)
1598 method)
1599 (let* ((*current-sort-order* (module-sort-order module))
1600 (*current-opinfo-table* (module-opinfo-table module))
1601 (eligible-flag (if upper-bound
1602 (sort<= (method-coarity method) upper-bound)
1603 t))
1604 (method-res (if eligible-flag method nil))
1605 (cur-arity (if eligible-flag (method-arity method) nil))
1606 (cur-coarity (if eligible-flag (method-coarity method) nil)))
1607 (declare (type hash-table *current-sort-order*
1608 *current-opinfo-table*)
1599 method)
1600 (let* ((*current-sort-order* (module-sort-order module))
1601 (*current-opinfo-table* (module-opinfo-table module))
1602 (eligible-flag (if upper-bound
1603 (sort<= (method-coarity method) upper-bound)
1604 t))
1605 (method-res (if eligible-flag method nil))
1606 (cur-arity (if eligible-flag (method-arity method) nil))
1607 (cur-coarity (if eligible-flag (method-coarity method) nil)))
1608 (declare (type hash-table *current-sort-order*
1609 *current-opinfo-table*)
16091610 (type (or null t) eligible-flag)
16101611 (type list cur-arity)
16111612 (type (or null method) method-res)
+12
-1
chaos/primitives/term-utils.lisp less more
226226 (term-sort arg3)
227227 so)
228228 (with-output-chaos-error ('incompatible-sorts)
229 (princ "value of if_then_else_fi must be of the same sort.")))
229 (princ "2nd. and 3rd. arguments of if_then_else_fi must be of the same sort.")))
230230 (update-lowest-parse arg2)
231231 (update-lowest-parse arg3)
232232 (if (sort<= (term-sort arg2) (term-sort arg3))
234234 (setf (term-sort term) (term-sort arg2)))))
235235 )
236236
237 (defun select-if-then-least (ifs &optional (so *current-sort-order*))
238 (unless (cdr ifs) (return-from select-if-then-least ifs))
239 (dolist (x ifs)
240 (set-if-then-else-sort x so))
241 (let ((result (car ifs)))
242 (dolist (ift (cdr ifs))
243 (if (sort< (term-sort ift) (term-sort result) so)
244 (setq result ift)
245 (unless (is-in-same-connected-component (term-sort ift) (term-sort result) so)
246 (return-from select-if-then-least ifs))))
247 (list result)))
237248
238249 (declaim (special *update-lowest-parse-in-progress*))
239250 (defvar *update-lowest-parse-in-progress* nil)
+5
-3
chaos/term-parser/parse-top.lisp less more
254254 ;; first find the lowest one
255255 (setq least-op (choose-lowest-op mslist))
256256 (cond (least-op
257 (push (find-if #'(lambda (x) (method= least-op (term-head x)))
258 result)
259 res)
257 (if (method= *bool-if* least-op)
258 (setq res (select-if-then-least result (module-sort-order module)))
259 (push (find-if #'(lambda (x) (method= least-op (term-head x)))
260 result)
261 res))
260262 (setq result res))
261263 (t (setq gen-op (choose-most-general-op mslist))
262264 ;; then select most general one