Commit d5209d47b8a261d8fef2dc834c105ce95f2848b5 - cafeobj

Fixed sbcl acz match problem. Now it works, but this is not a complete fix. TODO. tswd 8 years ago

6 changed file(s) with 395 addition(s) and 467 deletion(s). Raw diff Collapse all Expand all

+55

-87

chaos/e-match/match-ac.lisp less more

389	389
390	390	;;; x = term
391	391	;;; y = ((term . eqn-num) ... )
392		#\|\|
393		(defun delete-one-term
394		(x y)
	392	;;; #\|\|
	393	(defun delete-one-term (x y)
395	394	(block exit
396	395	(if (null y)
397	396	'none
398		(if (term-is-applform? x)
399		;; application form
400		(let ((head (term-head x))
401		(pos nil))
402		(setq pos
403		(position-if
404		#'(lambda (tv)
405		(let ((term (car tv)))
406		(and (term-is-applform? term)
407		(method-is-of-same-operator head
408		(term-head term)))))
409		(the list y)))
	397	(if (term-is-applform? x)
	398	;; application form
	399	(let ((head (term-head x))
	400	(pos nil))
	401	(setq pos (position-if #'(lambda (tv)
	402	(let ((term (car tv)))
	403	(and (term-is-applform? term)
	404	(method-is-of-same-operator head
	405	(term-head term)))))
	406	(the list y)))
410	407	;; (break "0")
411		(unless pos
	408	(unless pos
412	409	(return-from exit :never-match))
413		(if (zerop pos)
414		(if (term-equational-equal x (caar y))
415		(return-from exit (cdr y))
416		(return-from exit 'none))
417		(let ((last y)
418		(rest (cdr y))
419		(cur-pos 1))
420		(declare (type fixnum cur-pos))
421		(loop
422		(when (= cur-pos pos)
423		(if (term-equational-equal x
424		(caar rest))
425		(progn
426		;; delete pattern
427		(rplacd last (cdr rest))
428		(return-from exit y))
429		(return-from exit 'none)))
430		(incf cur-pos)
431		(setq last rest rest (cdr rest))))
432		))
433		;;
434		(if (term-equational-equal x (caar y))
435		(cdr y)
436		(let ((last y) (rest (cdr y)))
437		(loop (when (null rest) (return 'none))
438		(when (term-equational-equal x (caar rest))
439		;; delete pattern
440		(rplacd last (cdr rest))
441		;; new
442		(return y))
443		(setq last rest rest (cdr rest))))
444		))
445		)))
446		\|\|#
447
448		;; #\|\|
	410	(if (zerop pos)
	411	(if (term-equational-equal x (caar y))
	412	(return-from exit (cdr y))
	413	(return-from exit 'none))
	414	(let ((last y)
	415	(rest (cdr y))
	416	(cur-pos 1))
	417	(declare (type fixnum cur-pos))
	418	(loop
	419	(when (= cur-pos pos)
	420	(if (term-equational-equal x (caar rest))
	421	(progn
	422	;; delete pattern
	423	(rplacd last (cdr rest))
	424	(return-from exit y))
	425	(return-from exit 'none)))
	426	(incf cur-pos)
	427	(setq last rest rest (cdr rest))))))
	428	;; term is not application form
	429	(if (term-equational-equal x (caar y))
	430	(cdr y)
	431	(let ((last y) (rest (cdr y)))
	432	(loop (when (null rest) (return 'none))
	433	(when (term-equational-equal x (caar rest))
	434	;; delete pattern
	435	(rplacd last (cdr rest))
	436	;; new
	437	(return y))
	438	(setq last rest rest (cdr rest)))))))
	439	))
	440
	441	#\|\|
449	442	(defun delete-one-term
450	443	(x y)
451	444	(if (null y)

462	455	(setq last rest rest (cdr rest))))
463	456	))
464	457	)
465		;; \|\|#
	458	\|\|#
466	459
467	460	(defvar ac-failure-eq nil)
468	461

558	551	.z. (theory-info-code minfo-2)))
559	552	(push (make-equation t1 t2) new-eqns)
560	553	(progn
561		(when match-debug
	554	(with-match-debug ()
562	555	(setq ac-failure-eq (cons t1 t2)))
563	556	(setq new-eqns nil)
564	557	(return nil)) )))))))

567	560	(progn
568	561	(dolist (eq (nreverse new-eqns))
569	562	(add-equation-to-m-system new-sys eq))
570		(when match-debug
	563	(with-match-debug ()
571	564	(format t "~%** ac-solution-from-state")
572	565	(print-m-system new-sys))
573	566	new-sys)
574	567	(progn
575		(when match-debug
	568	(with-match-debug ()
576	569	(format t "~%** no ac solution")
577	570	(print-next)
578	571	(princ " - t1 = ") (term-print (car ac-failure-eq))
579	572	(print-next)
580		(princ " - t2 = ") (term-print (cdr ac-failure-eq))
581		)
	573	(princ " - t2 = ") (term-print (cdr ac-failure-eq)))
582	574	nil))))
583	575
584	576	(#+GCL si:define-inline-function #-GCL defun test_same_term_list (x y)

643	635	(declare (type list list))
644	636	(let ((ms-list nil))
645	637	(declare (type list ms-list))
646		#\|\|
647		(when match-debug
648		(mapc #'(lambda (x) (format t "~&,,,~s" x)) list))
649		\|\|#
650	638	(dolist (x list) ;;(copy-tree list)
651	639	(declare (type list x))
652	640	(let ((ms-elt (assoc-if #'(lambda (y)
653	641	(declare (type list y))
654		#\|\|
655		(when match-debug
656		(format t "~%..x\|~d\| " (cdr x))
657		(term-print (car x))
658		(format t "~&..y\|~d\| " (cdr y))
659		(term-print (car y))
660		(trace term-equational-equal))
661		\|\|#
662	642	(and (= (the fixnum (cdr x))
663	643	(the fixnum (cdr y)))
664	644	(term-equational-equal (car y) (car x))))
665	645	ms-list)))
666	646	(if ms-elt
667	647	(progn
668		#\|\|
669		(when match-debug
670		(format t "~%..inc: ~s" ms-elt))
671		\|\|#
672	648	(incf (the fixnum (cdr ms-elt))))
673	649	(progn
674		#\|\|
675		(when match-debug
676		(format t "~%..add: ~s" x))
677		\|\|#
678	650	(push (cons x 1) ms-list)))))
679		#\|\|
680		(when match-debug
681		(untrace term-equational-equal))
682		\|\|#
683	651	ms-list))
684	652
685	653	;;; check for multi-set equality

900	868	(push (cons term eqn-number)
901	869	rhs-constants)
902	870	(progn
903		(when match-debug
	871	(with-match-debug ()
904	872	(format t "~%- :never-match : lhs-vars ")
905	873	(print-chaos-object lhs-vars))
906	874	;; (format t "~&failure case #3")

914	882	(push (cons term eqn-number)
915	883	rhs-funs)
916	884	(progn
917		(when match-debug
	885	(with-match-debug ()
918	886	(format t "~%- :never-match : lhs-vars ")
919	887	(print-chaos-object lhs-vars))
920	888	;; (format t "~&failure case #4")

994	962	(type fixnum rhs-c-max rhs-f-max rhs-full-bits
995	963	dummy-bit lhs-r-mask))
996	964	;;
997		(when match-debug
998		(format t "~%..lhs-f-ms=~s, lhs-f-r=~s lhs-v-ms=~s, lhs-v-r=~s, l-m=~d l-gcd=~d" lhs-f-ms lhs-f-r lhs-v-ms lhs-v-r l-m l-gcd)
999		(format t "~&..all-rhs-funs=~s, rhs-c-ms=~s, rhs-c-r=~s, rhs-f-ms=~s, rhs-f-r=~s, r-m=~d, r-gcd=~d" all-rhs-funs rhs-c-ms rhs-c-r rhs-f-ms rhs-f-r r-m r-gcd))
	965	;; (when match-debug
	966	;; (format t "~%..lhs-f-ms=~s, lhs-f-r=~s lhs-v-ms=~s, lhs-v-r=~s, l-m=~d l-gcd=~d" lhs-f-ms lhs-f-r lhs-v-ms lhs-v-r l-m l-gcd)
	967	;; (format t "~&..all-rhs-funs=~s, rhs-c-ms=~s, rhs-c-r=~s, rhs-f-ms=~s, rhs-f-r=~s, r-m=~d, r-gcd=~d" all-rhs-funs rhs-c-ms rhs-c-r rhs-f-ms rhs-f-r r-m r-gcd))
1000	968	;; one more easy failure check
1001	969	(when (or (> l-m r-m) ; a lhs item is repeated more than any rhs
1002	970	(not (integerp (/ r-gcd l-gcd))))

+123

-144

chaos/e-match/match-acz.lisp less more

258	258	(when (term-equational-equal ,term_!* $$_term2)
259	259	(return t))))
260	260
261		;;; acz-state-pool
262
263		#\|\|
264		(defvar .acz-state-pool. nil)
265
266		(defmacro allocate-acz-state ()
267		` (if .acz-state-pool.
268		(pop .acz-state-pool.)
269		(make-match-ACZ-state)))
270
271		(defmacro deallocate-acz-state (acz-state)
272		`(push ,acz-state .acz-state-pool.))
273
274		(eval-when (:execute :load-toplevel)
275		(dotimes (x 20) (push (make-match-ACZ-state) .acz-state-pool.)))
276		\|\|#
277
278	261	(defmacro allocate-acz-state ()
279	262	(make-match-ACZ-state))
280
281		#\|\|
282		(defmacro deallocate-acz-state (acz-state)
283		nil)
284		\|\|#
285	263
286	264	#+CMU (declaim (ext:start-block match-acz-state-initialize
287	265	match-acz-next-state

294	272	(unless (eq (car x) (car y))
295	273	(return nil))
296	274	(setq x (cdr x))
297		(setq y (cdr y))
298		))
	275	(setq y (cdr y))))
299	276
300	277	;;; NOTE this is a version for ACZ-internal use only.
301	278	;;; it simply takes care of the "from which equation" info.

573	550	(when match-debug
574	551	(format t "~%*** acz solution: ")
575	552	(print-m-system new-sys)
576		(format t "~%***")
577		)
	553	(format t "~%***"))
578	554	(values new-sys made-zero))
579	555	(progn
580		(when match-debug
581		(format t "~%*** no possible solution in this case")
	556	(with-match-debug()
	557	(format t "~%***[acz] no possible solution in this case")
582	558	(print-next)
583	559	(princ "t1 = ") (term-print (car acz-failure-pat))
584	560	(print-next)
585		(princ "t2 = ") (term-print (cdr acz-failure-pat))
586		)
587		(values nil nil)))
588		)))
	561	(princ "t2 = ") (term-print (cdr acz-failure-pat)))
	562	(values nil nil))))))
589	563
590	564
591	565	;;; ACZ State Intialization

597	571
598	572	(defun match-ACZ-state-initialize (sys env)
599	573	(declare (type list sys env))
	574	(with-match-debug ()
	575	(format t "~%** match-acz-state-initialize -------------------------------------")
	576	(print-next)
	577	(print-match-system-sys sys)
	578	(print-next)
	579	(print-match-system-env env))
600	580	(block TOP
601	581	(let ((eqn-number -1)
602	582	(sys-methods (alloc-svec (length sys)))

611	591	(type list all-lhs-vars all-lhs-funs all-rhs-constants
612	592	all-rhs-funs))
613	593	(dolist (equation sys)
614		(setf eqn-number
615		(1+ eqn-number))
	594	(setf eqn-number (1+ eqn-number))
616	595	(let* ((lhs-1 (equation-t1 equation))
617	596	(rhs-1 (equation-t2 equation))
618	597	(lh-meth (term-method lhs-1))
619		(rhs-meth (if (and (term-is-applform? rhs-1)
620		(not (term-is-builtin-constant? rhs-1)))
	598	(rhs-meth (if (term-is-applform? rhs-1)
621	599	(term-method rhs-1)
622		nil))
	600	nil))
623	601	(lhs-2 (list-ACZ-subterms lhs-1 lh-meth))
624		(rhs-2
625		(if (and rhs-meth
626		(method-is-AC-restriction-of rhs-meth lh-meth))
627		(list-ACZ-subterms rhs-1 rhs-meth)
628		(list rhs-1)))
	602	(rhs-2 (if (and rhs-meth
	603	(method-is-AC-restriction-of rhs-meth lh-meth))
	604	(list-ACZ-subterms rhs-1 rhs-meth)
	605	(list rhs-1)))
629	606	(lhs-vars nil)
630	607	(lhs-constants nil)
631	608	(lhs-funs nil)
632	609	(rhs-constants nil)
633		(rhs-funs nil)
634		)
	610	(rhs-funs nil))
635	611	(declare (type term rhs-1 rhs-1)
636	612	(type method lh-meth)
637	613	(type (or null method) rhs-meth)
638		(type list lhs-2 rhs-2 lhs-vars lhs-constants lhs-funs
	614	(type list lhs-2 rhs-2 lhs-vars
	615	lhs-constants lhs-funs
639	616	rhs-constants rhs-funs))
640	617	;;
641	618	(setf (svref sys-methods eqn-number) lh-meth)

644	621	(dolist (term lhs-2)
645	622	;; for each subterm of lhs
646	623	;; note: unit elements are already eliminated from lhs-2.
647		;;
648	624	(cond ((term-is-variable? term)
649	625	(let ((image (if env (environment-image env term) term)))
650	626	(cond ((null image)

655	631	(push (cons image eqn-number) lhs-constants))
656	632	((method-is-AC-restriction-of lh-meth
657	633	(term-method image))
658		(dolist (term2 (list-ACZ-subterms
659		image (term-head image)))
	634	(dolist (term2 (list-ACZ-subterms image (term-head image)))
660	635	(cond ((term-is-variable? term2)
661	636	(push (cons term2 eqn-number)
662	637	lhs-vars))

674	649	(push (cons term eqn-number) lhs-constants)
675	650	)
676	651	(t (push (cons term eqn-number) lhs-funs))))
	652	(with-match-debug ()
	653	(format t "~%[acz] lhs-funs = ~d, lhs-constants = ~d, lhs-vars = ~d"
	654	(length lhs-funs) (length lhs-constants) (length lhs-vars))
	655	(format t "~%[acz] lhs-funs")
	656	(dolist (lf lhs-funs)
	657	(print lf))
	658	(format t "~%[acz] lhs-constants")
	659	(dolist (lc lhs-constants)
	660	(print lc))
	661	(format t "~%[acz] lhs-vars")
	662	(dolist (lv lhs-vars)
	663	(print lv)))
677	664	;;
678	665	;; now that the lhs is partitioned - lets play with the rhs
679	666	;;

688	675	(if (eq new :never-match)
689	676	(if lhs-vars
690	677	(push (cons term eqn-number) rhs-constants)
691		(return-from TOP (values nil t)))
692		(setq lhs-constants new))))))
	678	(progn
	679	(with-match-debug ()
	680	(format t "~%++ :never-match 1"))
	681	(return-from TOP (values nil t))))
	682	(setq lhs-constants new))))))
693	683	(t (let ((new (delete-one-term term lhs-funs)))
694	684	(if (eq 'none new)
695	685	(push (cons term eqn-number) rhs-funs)
696		(if (eq new :never-match)
697		(if lhs-vars
698		(push (cons term eqn-number) rhs-funs)
699		(return-from TOP (values nil t)))
700		(setq lhs-funs new)))))))
	686	(if (eq new :never-match)
	687	(if lhs-vars
	688	(push (cons term eqn-number) rhs-funs)
	689	(progn
	690	(with-match-debug ()
	691	(format t "~%++ :never-match 2"))
	692	(return-from TOP (values nil t))))
	693	(setq lhs-funs new)))))))
701	694	;; now there are no duplicates (things appearing on both sides)
702	695	(let ((lhs-c-count (length lhs-constants))
703	696	(lhs-f-count (length lhs-funs))
704	697	(lhs-v-count (length lhs-vars))
705	698	(rhs-c-count (length rhs-constants))
706		(rhs-f-count (length rhs-funs))
707		)
	699	(rhs-f-count (length rhs-funs)))
708	700	(declare (type fixnum lhs-c-count lhs-f-count lhs-v-count
709	701	rhs-c-count rhs-f-count))
710	702	;; check trivial failure conditions

714	706	(> lhs-f-count rhs-f-count)) ; too many funs to match
715	707	;; this assumption may be dubius in ACZ --- can arbitrary
716	708	;; funs eventually reduce to identity?
	709	(with-match-debug ()
	710	(format t "~%++ fail exit 1"))
717	711	(return-from TOP (values nil t))) ; FAIL most miserably
718	712	(setq all-lhs-funs (nconc lhs-funs all-lhs-funs))
719	713	(setq all-lhs-vars (nconc lhs-vars all-lhs-vars))

725	719	(null all-lhs-vars))
726	720	(if (and (null all-rhs-constants) ; this is rare
727	721	(null all-rhs-funs))
728		(return-from TOP (values (make-trivial-match-ACZ-state
729		:sys (new-m-system)) nil))
730		(return-from TOP (values nil t))))
	722	(progn
	723	(with-match-debug ()
	724	(format t "~%++ done 1"))
	725	(return-from TOP (values (make-trivial-match-ACZ-state :sys (new-m-system))
	726	nil)))
	727	(progn
	728	(with-match-debug ()
	729	(format t "~%++ nomatch done 1"))
	730	(return-from TOP (values nil t)))))
731	731	;; maybe check for more simple cases, like one-var vs the world.
732	732	((and use-one-var-opt
733	733	(null all-lhs-funs) ; only one var left on lhs

741	741	(cdar all-lhs-vars))
742	742	(nconc all-rhs-constants
743	743	all-rhs-funs))))
744		(return-from TOP (values (make-trivial-match-ACZ-state :sys fresh-sys)
745		nil))))
	744	(with-match-debug ()
	745	(format t "~%++ done 2"))
	746	(return-from TOP (values (make-trivial-match-ACZ-state :sys fresh-sys) nil))))
746	747	(t
747	748	(let* ((lhs-f-count (length all-lhs-funs))
748	749	(lhs-v-count (1+ (length all-lhs-vars))) ; note this is "wrong"

801	802	;; TCW 14 Mar 91 need to restrict this for ACZ
802	803	(when (or (> l-f-m r-m) ; a lhs item is repeated more than any rhs
803	804	(not (integerp (/ r-gcd l-gcd))))
804		;; (deallocate-acz-state state)
	805	(with-match-debug ()
	806	(format t "~%++ nomatch done 4"))
805	807	(return-from TOP (values nil t))) ; FAIL most miserably
806	808	;; NOW, get down to the real work....
807	809	;; setup the repeat mask (first of v's)

881	883	(declare (type fixnum my-compat))
882	884	(do ()
883	885	((> dummy-bit rhs-c-max)
884		(progn ;; (deallocate-acz-state state)
885		(return-from TOP (values nil t))))
	886	(progn
	887	(with-match-debug ()
	888	(format t "~%++ nomatch done 5"))
	889	(return-from TOP (values nil t))))
886	890	(unless (zerop (make-and dummy-bit my-compat))
887	891	(setf (svref rhs-c-sol i) dummy-bit)
888	892	(return))

897	901	(do ()
898	902	((> dummy-bit rhs-f-max)
899	903	(progn
900		;; (deallocate-acz-state state)
	904	(with-match-debug ()
	905	(format t "~%++ nomatch-done 6"))
901	906	(return-from TOP (values nil t))))
902	907	(unless (zerop (make-and dummy-bit my-compat))
903	908	(setf (svref rhs-f-sol i) dummy-bit)

944	949	(setf (match-ACZ-state-no-more state) nil)
945	950	(setf (match-ACZ-state-acz-state-p state) 'acz-state)
946	951	;;
947		(when match-debug
	952	(with-match-debug ()
948	953	(format t "~%acz-init: state=~&")
949	954	(match-ACZ-unparse-match-ACZ-state state))
950	955	;;
951	956	(values state nil)))))))
952	957
953		#\|\|
954
955		(defun match-ACZ-state-initialize (sys env)
956		(match-AC-state-initialize sys env :have-unit))
957		\|\|#
958
959	958	(defun match-ACZ-next-state-sub (state)
960	959	(do* ((m 0) ; only initialize these vars
961	960	(rhs-c-sol (match-ACZ-state-rhs-c-sol state))

1007	1006	(values (trivial-match-ACZ-state-sys state) nil nil)))
1008	1007	(if (not (match-ACZ-state-p state))
1009	1008	(progn (format t "~% match-ACZ-Next-State given non match-ACZ-state:~A~%" state)
1010		(values nil t nil))
	1009	(values nil nil t))
1011	1010	(let ((sys nil)
1012	1011	(no-more (match-acz-state-no-more state))
1013	1012	(zero nil))

1026	1025	)
1027	1026	(if no-more
1028	1027	(match-acz-next-state state)
1029		(values sys state nil)
1030		)
1031		)
1032		)
1033		))))
	1028	(values sys state nil))))))))
1034	1029
1035	1030	(defun match-acz-next-state-aux (state)
1036		(when match-debug
	1031	(with-match-debug ()
1037	1032	(format t "~%** ACZ next state"))
1038	1033	(if (match-ACZ-state-no-more state)
1039	1034	(progn

1047	1042	(rhs-f-count (match-ACZ-state-rhs-f-count state))
1048	1043	;; (rhs-full-bits (match-ACZ-state-rhs-full-bits state)) ;@@
1049	1044	(lhs-r-mask (match-ACZ-state-lhs-r-mask state))
1050		(made-zero nil)
1051		)
	1045	(made-zero nil))
1052	1046	(nil) ; do forever
1053	1047	(declare (type fixnum n rhs-f-count rhs-f-max lhs-r-mask)
1054	1048	(type #+GCL vector #-GCL simple-vector

1087	1081	(dotimes (i (length lhs-v) t)
1088	1082	(declare (type fixnum i))
1089	1083	(if (< i 1) nil
1090		(unless (sort<=
1091		(term-sort
1092		(car (theory-zero
1093		(method-theory (svref
1094		ops
1095		(cdr
1096		(svref
1097		lhs-v
1098		i)))))))
1099		(term-sort (car (svref lhs-v i))))
	1084	(unless (sort<= (term-sort (car (theory-zero (method-theory (svref ops (cdr (svref lhs-v i)))))))
	1085	(term-sort (car (svref lhs-v i))))
1100	1086	(return nil))))))
1101	1087	(let ((sol nil))
1102	1088	(multiple-value-setq (sol made-zero)

1108	1094	;; failed at f-level
1109	1095	;; (deallocate-acz-state state)
1110	1096	(return (values nil t nil))))
1111		(setq n (1- n)))
1112		)
	1097	(setq n (1- n))))
1113	1098	((< (the fixnum (svref rhs-f-sol n)) rhs-f-max)
1114	1099	(match-ACZ-Rotate-Left rhs-f-sol n)
1115	1100	(when (and ; this is a compatible position for this bit

1130	1115	(setf (svref rhs-f-sol n) 1) ; reset this row to one
1131	1116	(setq n (1+ n)))))))
1132	1117
1133		#\|\|
1134		(defun match-ACZ-next-state (state)
1135		(match-AC-next-state state))
1136		\|\|#
1137
1138	1118	#+CMU (declaim (ext:end-block))
1139	1119
1140	1120	;; printout of important parts of ACZ state.
1141	1121	(defun match-ACZ-unparse-match-ACZ-state (ACZ-st)
1142		(format t "~%no more=~A~%" (match-ACZ-state-no-more ACZ-st))
1143		(format t "operators: ~%")
1144		(map nil #'print-chaos-object(match-ACZ-state-methods ACZ-st))
1145		(format t "RHS-f: ~%")
1146		(map nil #'print-chaos-object (match-ACZ-state-RHS-f ACZ-st))
1147		(format t "RHS-c: ~%")
1148		(map nil #'print-chaos-object (match-ACZ-state-RHS-c ACZ-st))
1149		(format t "LHS-v: ~%")
1150		(map nil #'print-chaos-object (match-ACZ-state-LHS-v ACZ-st))
1151		(format t "LHS-f: ~%")
1152		(map nil #'print-chaos-object (match-ACZ-state-LHS-f ACZ-st))
1153		(format t " rhs-c-count=~A, rhs-f-count=~A~%"
1154		(match-ACZ-state-RHS-c-count ACZ-st)
1155		(match-ACZ-state-RHS-f-count ACZ-st))
1156		(format t " lhs-c-count=~A, lhs-f-count=~A, lhs-v-count=~A~%"
1157		(match-ACZ-state-LHS-c-count ACZ-st)
1158		(match-ACZ-state-LHS-f-count ACZ-st)
1159		(match-ACZ-state-LHS-v-count ACZ-st))
1160		(let ((print-base 2)) ; these be bitvectors, print them as such
1161		(format t "-------------------~%rhs-c-sol= ~A~&rhs-f-sol=~A~%"
1162		(match-ACZ-state-RHS-c-sol ACZ-st) (match-ACZ-state-RHS-f-sol ACZ-st))
1163		(format t " rhs-c-max=~A, rhs-f-max=~A, rhs-full-bits=~A~%"
1164		(match-ACZ-state-RHS-c-max ACZ-st)
1165		(match-ACZ-state-RHS-f-max ACZ-st)
1166		(match-ACZ-state-RHS-full-bits ACZ-st))
1167		(format t " rhs-c-compat=~A, rhs-f-compat=~A~%"
1168		(match-ACZ-state-RHS-c-compat ACZ-st)
1169		(match-ACZ-state-RHS-f-compat ACZ-st))
1170		(format t " rhs-c-r=~A, rhs-f-r=~A~%"
1171		(match-ACZ-state-RHS-c-r ACZ-st)
1172		(match-ACZ-state-RHS-f-r ACZ-st))
1173		(format t " lhs-f-r=~A, lhs-v-r=~A~%"
1174		(match-ACZ-state-LHS-f-r ACZ-st)
1175		(match-ACZ-state-LHS-v-r ACZ-st))
1176		(format t " lhs-mask=~A~%"
1177		(match-ACZ-state-LHS-mask ACZ-st))
1178		(terpri)
1179		(format t " lhs-f-mask=~A~%"
1180		(match-ACZ-state-LHS-f-mask ACZ-st))
1181		(format t " lhs-r-mask=~A~%"
1182		(match-ACZ-state-LHS-r-mask ACZ-st))
1183		))
	1122	(format t "[ACZ State]")
	1123	(let ((print-indent (+ 2 print-indent)))
	1124	(format t "~%no more=~A" (match-ACZ-state-no-more ACZ-st))
	1125	(format t "~%operators:")
	1126	(map nil #'(lambda (x) (print-next) (print-chaos-object x))(match-ACZ-state-methods ACZ-st))
	1127	(format t "~%RHS-f:")
	1128	(map nil #'(lambda (x) (print-next) (print-chaos-object x)) (match-ACZ-state-RHS-f ACZ-st))
	1129	(format t "~%RHS-c:")
	1130	(map nil #'(lambda (x) (print-next) (print-chaos-object x)) (match-ACZ-state-RHS-c ACZ-st))
	1131	(format t "~%LHS-v:")
	1132	(map nil #'(lambda (x) (print-next) (print-chaos-object x)) (match-ACZ-state-LHS-v ACZ-st))
	1133	(format t "~%LHS-f:")
	1134	(map nil #'(lambda (x) (print-next) (print-chaos-object x)) (match-ACZ-state-LHS-f ACZ-st))
	1135	(format t "~%rhs-c-count=~A, rhs-f-count=~A"
	1136	(match-ACZ-state-RHS-c-count ACZ-st)
	1137	(match-ACZ-state-RHS-f-count ACZ-st))
	1138	(format t "~%lhs-c-count=~A, lhs-f-count=~A, lhs-v-count=~A"
	1139	(match-ACZ-state-LHS-c-count ACZ-st)
	1140	(match-ACZ-state-LHS-f-count ACZ-st)
	1141	(match-ACZ-state-LHS-v-count ACZ-st))
	1142	(let ((print-base 2)) ; these be bitvectors, print them as such
	1143	(format t "-------------------~%rhs-c-sol= ~A~&rhs-f-sol=~A~%"
	1144	(match-ACZ-state-RHS-c-sol ACZ-st) (match-ACZ-state-RHS-f-sol ACZ-st))
	1145	(format t " rhs-c-max=~A, rhs-f-max=~A, rhs-full-bits=~A~%"
	1146	(match-ACZ-state-RHS-c-max ACZ-st)
	1147	(match-ACZ-state-RHS-f-max ACZ-st)
	1148	(match-ACZ-state-RHS-full-bits ACZ-st))
	1149	(format t " rhs-c-compat=~s, rhs-f-compat=~s~%"
	1150	(match-ACZ-state-RHS-c-compat ACZ-st)
	1151	(match-ACZ-state-RHS-f-compat ACZ-st))
	1152	(format t " rhs-c-r=~s, rhs-f-r=~s~%"
	1153	(match-ACZ-state-RHS-c-r ACZ-st)
	1154	(match-ACZ-state-RHS-f-r ACZ-st))
	1155	(format t " lhs-f-r=~s, lhs-v-r=~s~%"
	1156	(match-ACZ-state-LHS-f-r ACZ-st)
	1157	(match-ACZ-state-LHS-v-r ACZ-st))
	1158	(format t " lhs-mask=~s~%"
	1159	(match-ACZ-state-LHS-mask ACZ-st))
	1160	(format t " lhs-f-mask=~s~%"
	1161	(match-ACZ-state-LHS-f-mask ACZ-st))
	1162	(format t " lhs-r-mask=~s~%"
	1163	(match-ACZ-state-LHS-r-mask ACZ-st))
	1164	)))
1184	1165
1185	1166	(defun match-ACZ-trivial-unparse (state)
1186	1167	(let ((sys (trivial-match-ACZ-state-sys state))
1187	1168	(no-more-p (trivial-match-ACZ-state-no-more-p state)))
1188	1169	sys
1189		(format t "~% acz-unparse-trivial no-more-p = ~A~%" no-more-p)
1190		)
1191		)
	1170	(format t "~% acz-unparse-trivial no-more-p = ~A~%" no-more-p)))
1192	1171
1193	1172	(defun match-ACZ-args-nss (x) (match-ACZ-unparse-match-ACZ-state (car x)) (terpri))
1194	1173	(setf (get 'match-ACZ-next-state-sub 'print-args) 'match-ACZ-args-nss)

+17

-44

chaos/e-match/match-e.lisp less more

49	49	;;; 1 means that the decomposition has been already done and that there is
50	50	;;; no more next state
51	51
52		#\|
53		(defstruct (match-empty-state (:constructor create-match-empty-state (flag sys)))
54		(flag 0 :type bit)
55		sys )
56
57		(defmacro match-empty-state-flag (_s) `(car ,_s))
58		(defmacro match-empty-state-sys (s_) `(cdr ,s_))
59		(defmacro create-match-empty-state (_*flag _sys) `(cons ,_flag ,_*sys))
60
61		(defvar .match-empty-state. nil)
62		(eval-when (:execute :load-toplevel)
63		(setq .match-empty-state. (create-match-empty-state 0 nil)))
64
65		(defun the-match-empty-state () .match-empty-state.)
66
67		\|#
68
69	52	;;; INITIALIZATION
70	53
71	54	;;; Initialize an empty state. It check if the top symbols of each equation of

79	62	(dolist (equation (m-system-to-list sys))
80	63	(let ((lhs (equation-t1 equation))
81	64	(rhs (equation-t2 equation)))
82		#\|\|
83		(when (or (term-is-builtin-constant? rhs)
84		(term-is-variable? rhs))
85		(return-from no-match (values nil t)))
86		\|\|#
87	65	(unless (term-type-eq lhs rhs)
88	66	(return-from no-match (values nil t)))
89	67	(unless (or (match-empty-equal lhs rhs)
90	68	(and (term-is-application-form? lhs)
91	69	(method-is-of-same-operator+ (term-head lhs)
92	70	(term-head rhs))))
93		(return-from no-match (values nil t))))
94		)
	71	(return-from no-match (values nil t)))))
95	72	(values (create-match-empty-state 0 sys) nil)))
96
97	73
98	74	;;; NEXT STATE
99	75
100	76	(defun match-empty-next-state (empty-st)
101		(declare (type list empty-st)
102		(values list list (or null t)))
103		#\|\|
104		(unless empty-st
105		(with-output-chaos-warning ()
106		(format t "match empty next PANIC: illegal situation, the null state!"))
107		(break)
108		(return-from match-empty-next-state (values nil nil t)))
109		\|\|#
	77	(declare (type list empty-st))
110	78	(let ((flag (match-empty-state-flag empty-st))
111	79	(sys (match-empty-state-sys empty-st)))
112	80	(declare (type fixnum flag)
113	81	(type list sys))
	82
	83	(with-match-debug ()
	84	(format t "~%[empty-next-state] : given m-system~%")
	85	(print-match-system-sys sys))
	86
114	87	(if (= flag 1)
115	88	;; no more state
116	89	(values nil nil t)
117		(multiple-value-bind (new-m-sys no-match)
118		(match-decompose&merge (create-match-system (new-environment)
119		sys))
120		(if no-match
121		(values nil nil t)
122		(progn
123		(setf (match-empty-state-flag empty-st) 1)
124		(values (match-system-to-m-system new-m-sys)
125		empty-st
126		nil)))))))
	90	(multiple-value-bind (new-m-sys no-match)
	91	(match-decompose&merge (create-match-system (new-environment)
	92	sys))
	93	(if no-match
	94	(values nil nil t)
	95	(progn
	96	(setf (match-empty-state-flag empty-st) 1)
	97	(values (match-system-to-m-system new-m-sys)
	98	empty-st
	99	nil)))))))
127	100
128	101	;;; EQUALITY
129	102

+48

-56

chaos/e-match/match-state.lisp less more

124	124	;;; Initialize a match-state in which a match system "m-sys" has been inserted.
125	125	;;; "m-s" is supposed to be merged and ready for mutation i.e. decomposed
126	126	;;;
127		;;; NOT-USED
128		;;;(defun match-state-initialize (t1 t2)
129		;;; (multiple-value-bind (m-sys no-match)
130		;;; (match-system.dec-merg (match-system.new t1 t2))
131		;;; (if no-match
132		;;; (values nil t)
133		;;; (multiple-value-bind (sys th-info)
134		;;; (match-system.extract-one-system m-sys)
135		;;; (values (match-state-create
136		;;; m-sys sys th-info (theory-state-match-initialize th-info sys))
137		;;; nil)
138		;;; ))))
139	127
140	128	;;; EMPTY-STATE, see "match-e.lisp"
141	129

165	153	;; computes the next solution of th-match-state we quit this loop either if
166	154	;; there is no more new th-match-state or a new match system has been computed.
167	155	(loop
168		(multiple-value-bind (sys new-th-match-state no-more)
169		(theory-state-match-next-state theory-info th-match-state)
170		(declare (type list sys)
171		(type t new-th-match-state)
172		(type (or null t) no-more))
173		(if no-more
174		(return (values nil t))
175		;; "match-add-m-system" performs the decomposition and merging
176		;; and must not destroy the current match system.
177		(multiple-value-bind (new-m-sys no-match)
178		;; create a new merged match-system containing the old one
179		;; and add sys.
180		(match-add-m-system (match-state-match-system st) sys)
181		;; if there is no-match, continue (the loop)
182		;; else try to returns the new match-state.
183		(unless no-match
184		(multiple-value-bind (sys-to-solve theory-info)
185		(m-system-extract-one-system (match-system-sys new-m-sys))
186		(declare (type list sys-to-solve)
187		(type theory-info theory-info))
188		(if (null sys-to-solve)
189		(return (values (match-state-create new-m-sys
190		nil
191		(theory-info the-empty-theory)
192		(the-match-empty-state))
193		nil))
194		(multiple-value-bind (th-st no-match)
195		(theory-state-match-initialize theory-info
196		sys-to-solve
197		(match-system-env new-m-sys))
198		;; if no match, try another theory-state
199		(unless no-match
200		;; else modify the th-match-state of st
201		(setf (match-state-theory-state st) new-th-match-state)
202		;; and returns
203		(return (values (match-state-create
204		(match-system-modif-m-sys
205		new-m-sys
206		sys-to-solve)
207		sys-to-solve
208		theory-info
209		th-st)
210		nil))))))))
211		)))))
	156	(multiple-value-bind (sys new-th-match-state no-more)
	157	(theory-state-match-next-state theory-info th-match-state)
	158	(declare (type list sys)
	159	(type t new-th-match-state)
	160	(type (or null t) no-more))
	161	(if no-more
	162	(return (values nil t))
	163	;; "match-add-m-system" performs the decomposition and merging
	164	;; and must not destroy the current match system.
	165	(multiple-value-bind (new-m-sys no-match)
	166	;; create a new merged match-system containing the old one
	167	;; and add sys.
	168	(match-add-m-system (match-state-match-system st) sys)
	169	;;
	170	(with-match-debug ()
	171	(let ((fun (theory-info-match-next-fun theory-info)))
	172	(format t "~%<--[Match-next-state] funcalled ~s" fun)))
	173	;; if there is no-match, continue (the loop)
	174	;; else try to returns the new match-state.
	175	(with-match-debug ()
	176	(if no-match
	177	(format t "[NEXT-MATCH-STATE] retun with no-match.")))
	178	(unless no-match
	179	(multiple-value-bind (sys-to-solve theory-info)
	180	(m-system-extract-one-system (match-system-sys new-m-sys))
	181	(declare (type list sys-to-solve)
	182	(type theory-info theory-info))
	183	(if (null sys-to-solve)
	184	(return (values (match-state-create new-m-sys
	185	nil
	186	(theory-info the-empty-theory)
	187	(the-match-empty-state))
	188	nil))
	189	(multiple-value-bind (th-st no-match)
	190	(theory-state-match-initialize theory-info
	191	sys-to-solve
	192	(match-system-env new-m-sys))
	193	;; if no match, try another theory-state
	194	(unless no-match
	195	;; else modify the th-match-state of st
	196	(setf (match-state-theory-state st) new-th-match-state)
	197	;; and returns
	198	(return (values (match-state-create (match-system-modif-m-sys new-m-sys sys-to-solve)
	199	sys-to-solve
	200	theory-info
	201	th-st)
	202	nil))))))))
	203	)))))
212	204	;;; EOF

+132

-117

chaos/e-match/match-system.lisp less more

267	267	(type list res)
268	268	(values (or null t)))
269	269	(with-match-debug ()
270		(princ "** !match-decompose-match:")
	270	(format t "~%** !match-decompose-match:")
271	271	(print-next)
272		(princ "-t1") (term-print-with-sort t1)
	272	(princ "-t1: ") (term-print-with-sort t1)
273	273	(print-next)
274		(princ "-t2") (term-print-with-sort t2)
275		(print-next)
276		(princ "-result:")
277		(dolist (x res)
278		(print-next)
279		(print-chaos-object x)))
	274	(princ "-t2: ") (term-print-with-sort t2))
280	275	(cond
281	276	;; [1] t1 is variable
282	277	((term-is-variable? t1)

293	288	(if one-way-match
294	289	(progn
295	290	(with-match-debug ()
	291	(print-next)
296	292	(princ ">> FAIL for t2 is variable."))
297	293	t) ; fail
298	294	(!match-decompose-match t2 t1 res)))

301	297	((term-is-builtin-constant? t1)
302	298	(let ((ans (not (term-builtin-equal t1 t2))))
303	299	(with-match-debug ()
	300	(print-next)
304	301	(if ans
305	302	(princ ">> SUCCESS, builtin-equal.")
306	303	(princ ">> FAIL, builtin not equal.")))

315	312	nil)
316	313	(progn
317	314	(with-match-debug ()
	315	(print-next)
318	316	(princ ">> FAIL, t2 is builtin."))
319	317	t))
320	318	;; t2 also is an application form.

331	329	(t2-subterms (term-subterms t2)))
332	330	(declare (type list t1-subterms t2-subterms))
333	331	(with-match-debug ()
334		(print ">> empty theory: do the full decompose..."))
	332	(format t "~%>> empty theory: do the full decompose..."))
335	333	(loop ; for each subterm try decomposition.
336	334	(unless t1-subterms (return nil))
337	335	(let ((ng (!match-decompose-match (car t1-subterms)

349	347	;;
350	348	(progn
351	349	(with-match-debug ()
352		(print ">> has theory: add their pair."))
	350	(format t "~%>> has theory: add their pair."))
353	351	(push (make-equation t1 t2) (cdr res))
354	352	nil))
355	353

360	358	(if (term-is-on-demand? t2)
361	359	(progn
362	360	(with-match-debug ()
363		(print ">> term t2 is on demand."))
	361	(format t "~%>> term t2 is on demand."))
364	362	(mark-term-as-not-on-demand t2)
365	363	(if (normalize-term t2)
366	364	;; no reduction has been performed.

381	379	(term-head t2)))))
382	380	(progn
383	381	(with-match-debug ()
384		(print ">> theory Z."))
	382	(format t "~%>> theory Z."))
385	383	(push (make-equation t1 t2) (cdr res))
386	384	nil)
387	385	;; will never match
388	386	t)) )))))))
389	387
390		;; (declaim (inline match-decompose-equation))
391	388
392	389	(defun match-decompose-equation (t1 t2 &optional (sigma nil))
393	390	(declare (type term t1 t2))

532	529	(dolist (e m)
533	530	(let ((t1 (equation-t1 e))
534	531	(t2 (equation-t2 e)))
535		(format t "~%===========")
	532	(format t "~%[m-system]===========")
536	533	(format t "~&t1 = ") (term-print-with-sort t1)
537	534	(format t "~&t2 = ") (term-print-with-sort t2))))
538	535

693	690	;;; must not be modified.
694	691	;;; U: used by "match-system.dec-merg" and "match-add-m-system"
695	692
696		; (defun match-insert-if-coherent-with (new-env test-env new-sys eq-list &optional (check-match nil))
697		; ;; note that new-env and new-sys are both initialy of the form (nil.nil)
698		; (block the-end
699		; (with-match-debug ()
700		; (format T "~%insert:--------------------------------------")
701		; (print-next)
702		; (format t "new-env = ")
703		; (if (car new-env)
704		; (dolist (eq new-env)
705		; (print-next)
706		; (format t " LHS = ") (term-print-with-sort (equation-t1 eq))(terpri)
707		; (print-next)
708		; (format t " RHS = ") (term-print-with-sort (equation-t2 eq))(terpri))
709		; (princ "empty"))
710		; (print-next)
711		; (format t "test-env = ")
712		; (if (car test-env)
713		; (dolist (eq test-env)
714		; (print-next)
715		; (format t " LHS = ") (term-print-with-sort (equation-t1 eq)) (terpri)
716		; (print-next)
717		; (format t " RHS = ") (term-print-with-sort (equation-t2 eq)) (terpri))
718		; (princ "empty")))
719		; (dolist (eq eq-list)
720		; (let ((t1 (equation-t1 eq))
721		; (t2 (equation-t2 eq)))
722		; (with-match-debug ()
723		; (print-next)
724		; (format t " t1 = ") (term-print-with-sort t1) (terpri)
725		; (print-next)
726		; (format t " t2 = ") (term-print-with-sort t2) (terpri))
727		; (cond ((term-is-variable? t1)
728		; ;; checking of the sort information; redundant with
729		; ;; `decompose-equation'.
730		; (unless (sort<= (term-sort t2) (variable-sort t1)
731		; current-sort-order)
732		; (with-match-debug ()
733		; (print-next)
734		; (format t "-- non coherent, sort match fail."))
735		; (return-from the-end t))
736		; ;; new-env may be modified.
737		; (let ((image-of-t1 (variable-image test-env t1)))
738		; (if image-of-t1
739		; (unless (term-equational-equal image-of-t1 t2)
740		; (with-match-debug ()
741		; (format t "~%-- non coherent, var binding conflicts in env."))
742		; (return-from the-end t)) ; i.e no-coherent
743		; (let ((image-of-t1-in-new (variable-image new-env t1)))
744		; (if image-of-t1-in-new
745		; (unless (term-equational-equal image-of-t1-in-new
746		; t2)
747		; (with-match-debug ()
748		; (format t "~%-- non coherent, var binding in new-env."))
749		; (return-from the-end t))
750		; (add-equation-to-environment new-env eq))))))
751		; (check-match
752		; (when (term-is-variable? t2)
753		; (return-from the-end t))
754		; (if (and (term-is-applform? t2)
755		; (term-is-applform? t1))
756		; (let ((t1-head (term-head t1))
757		; (t2-head (term-head t2)))
758		; (if (method-is-of-same-operator+ t1-head t2-head)
759		; (add-equation-to-m-system new-sys eq)
760		; (let ((match-info (method-theory-info-for-matching! t1-head)))
761		; (if (test-theory .Z. (theory-info-code match-info))
762		; (add-equation-to-m-system new-sys eq)
763		; (progn
764		; (with-match-debug ()
765		; (format t "~%-- non coherent, func conflict."))
766		; (return-from the-end t))))))
767		; (add-equation-to-m-system new-sys eq)))
768		; ;;
769		; (t (add-equation-to-m-system new-sys eq)))))
770
771		; ;; add now all the equation of test-env into new-env (copy test-env)
772		; (cond ((null (car test-env)) ())
773		; ((null (car new-env))
774		; (let ((l (environment-copy1 test-env)))
775		; (rplaca new-env (car l))
776		; (rplacd new-env (cdr l))) )
777		; (t (nconc new-env test-env)))
778		; (with-match-debug ()
779		; (format t "~% insert: return -- coherent -------------------"))
780		; nil ; i.e. the new-env is coherent
781		; ))
	693	(defun match-insert-if-coherent-with (new-env test-env new-sys eq-list &optional (check-match nil))
	694	;; note that new-env and new-sys are both initialy of the form (nil.nil)
	695	(block the-end
	696	(with-match-debug ()
	697	(format T "~%insert:--------------------------------------")
	698	(print-next)
	699	(format t "new-env = ")
	700	(if (car new-env)
	701	(dolist (eq new-env)
	702	(print-next)
	703	(format t "~% LHS = ") (term-print-with-sort (equation-t1 eq))
	704	(print-next)
	705	(format t " RHS = ") (term-print-with-sort (equation-t2 eq))
	706	(princ "empty")))
	707	(print-next)
	708	(format t "test-env = ")
	709	(if (car test-env)
	710	(dolist (eq test-env)
	711	(format t "~% LHS = ") (term-print-with-sort (equation-t1 eq))
	712	(print-next)
	713	(format t " RHS = ") (term-print-with-sort (equation-t2 eq)))
	714	(princ "empty"))
	715	(terpri))
	716	(dolist (eq eq-list)
	717	(let ((t1 (equation-t1 eq))
	718	(t2 (equation-t2 eq)))
	719	(cond ((term-is-variable? t1)
	720	;; checking of the sort information; redundant with
	721	;; `decompose-equation'.
	722	(unless (sort<= (term-sort t2) (variable-sort t1)
	723	current-sort-order)
	724	(with-match-debug ()
	725	(print-next)
	726	(format t "-- non coherent, sort match fail."))
	727	(return-from the-end t))
	728	;; new-env may be modified.
	729	(let ((image-of-t1 (variable-image test-env t1)))
	730	(if image-of-t1
	731	(unless (term-equational-equal image-of-t1 t2)
	732	(with-match-debug ()
	733	(format t "~%-- non coherent, var binding conflicts in env."))
	734	(return-from the-end t)) ; i.e no-coherent
	735	(let ((image-of-t1-in-new (variable-image new-env t1)))
	736	(if image-of-t1-in-new
	737	(unless (term-equational-equal image-of-t1-in-new
	738	t2)
	739	(with-match-debug ()
	740	(format t "~%-- non coherent, var binding in new-env."))
	741	(return-from the-end t))
	742	(add-equation-to-environment new-env eq))))))
	743	(check-match
	744	(when (term-is-variable? t2)
	745	(with-match-debug ()
	746	(format t "~%-- non coherent, t2 is variable."))
	747	(return-from the-end t))
	748	(if (and (term-is-applform? t2)
	749	(term-is-applform? t1))
	750	(let ((t1-head (term-head t1))
	751	(t2-head (term-head t2)))
	752	(if (method-is-of-same-operator+ t1-head t2-head)
	753	(add-equation-to-m-system new-sys eq)
	754	(let ((match-info (method-theory-info-for-matching! t1-head)))
	755	(if (test-theory .Z. (theory-info-code match-info))
	756	(add-equation-to-m-system new-sys eq)
	757	(progn
	758	(with-match-debug ()
	759	(format t "~%-- non coherent, func conflict."))
	760	(return-from the-end t))))))
	761	(add-equation-to-m-system new-sys eq)))
	762	;;
	763	(t (add-equation-to-m-system new-sys eq)))))
	764
	765	;; add now all the equation of test-env into new-env (copy test-env)
	766	(cond ((null (car test-env)) ())
	767	((null (car new-env))
	768	(let ((l (environment-copy1 test-env)))
	769	(rplaca new-env (car l))
	770	(rplacd new-env (cdr l))) )
	771	(t (nconc new-env test-env)))
	772	(with-match-debug ()
	773	(format t "~%insert: return -- coherent -------------------")
	774
	775	)
	776	nil ; i.e. the new-env is coherent
	777	))
	778
	779	#\|\|
782	780	(defun match-insert-if-coherent-with (new-env test-env new-sys eq-list &optional (check-match nil))
783	781	;; note that new-env and new-sys are both initialy of the form (nil.nil)
784	782	(block the-end

828	826	(t (nconc new-env test-env)))
829	827	nil ; i.e. the new-env is coherent
830	828	))
	829	\|\|#
831	830
832	831	;;; MATCH-SYSTEM ===========================================================
833	832	;;;

895	894	(if (term-is-variable? term1)
896	895	(create-match-system (create-environment term1 term2)
897	896	(new-m-system))
898		(create-match-system (new-environment)
899		(create-m-system term1 term2))))
	897	(create-match-system (new-environment)
	898	(create-m-system term1 term2))))
900	899
901	900	;;; returns from a match-system a system (equivalent)
902	901	;;;

943	942	)
944	943	(return-from no-match (values nil t)))
945	944
	945	(with-match-debug ()
	946	(format t "~%[Match-add-m-system]: given ---------------~%")
	947	(print-match-system match-system)
	948	(format t "~% m-sys")
	949	(dolist (eq (m-system-to-list m-sys))
	950	(let ((t1 (equation-t1 eq))
	951	(t2 (equation-t2 eq)))
	952	(print-next)
	953	(princ "t1: ")(term-print-with-sort t1)
	954	(print-next)
	955	(princ "t2: ")(term-print-with-sort t2))))
	956
946	957	;; new-system is modified but not match-system
947	958	(setq new-system (add-m-system new-system (match-system-sys match-system)))
948		(return-from no-match
949		(values (create-match-system new-environment
950		new-system)
951		nil)))))
	959	(let ((nsys (create-match-system new-environment new-system)))
	960	(with-match-debug ()
	961	(format t "~%[MATCH-ADD-M-SYSTEM]: generated new sys ----~%")
	962	(print-match-system nsys))
	963	(return-from no-match (values nsys nil))))))
952	964
953	965	;;; Decompose&Merge
954	966	;;; Returns the decompose and merging of the given match-system

956	968	(defun match-decompose&merge (m-sys &optional sigma)
957	969	(block no-match
958	970	(let ((sys (match-system-sys m-sys))
959		(env (match-system-env m-sys))
960		(new-env (new-environment) )
961		(new-sys (new-m-system)))
	971	(env (match-system-env m-sys))
	972	(new-env (new-environment) )
	973	(new-sys (new-m-system)))
962	974	(declare (type list new-env new-sys))
963	975	(dolist (eq (m-system-to-list sys))
964	976	(multiple-value-bind (eq-list clash-of-symbol)
965	977	(match-decompose-equation (equation-t1 eq) (equation-t2 eq) sigma)
966	978	(if clash-of-symbol
967	979	(return-from no-match (values nil t))
968		(when (match-insert-if-coherent-with new-env
969		env
970		new-sys
971		eq-list)
972		(return-from no-match (values nil t))))))
973		(values (create-match-system new-env
974		new-sys)
975		nil))))
	980	(when (match-insert-if-coherent-with new-env
	981	env
	982	new-sys
	983	eq-list)
	984	(return-from no-match (values nil t))))))
	985	(let ((msys (create-match-system new-env new-sys)))
	986	(with-match-debug ()
	987	(format t "~%[Match-Decompose&Merge]: match system created: ----~%")
	988	(print-match-system msys))
	989	(values msys nil)))))
	990
976	991
977	992	;;; Extracts from the non fully decomposed part of "m-s" the biggest system to
978	993	;;; be solved into the theory "th". "th" and "sys" are returned.

+20

-19

chaos/e-match/match.lisp less more

73	73	(defun first-match (t1 t2 &optional (sigma nil))
74	74	(declare (type term t1 t2)
75	75	(values list list (or null t) (or null t)))
76		(when match-debug
77		(format t "~%* First Match --------------------------------~%")
78		(princ " t1 = ") (term-print-with-sort t1)
79		(terpri)
80		(princ " t2 = ") (term-print-with-sort t2)
81		(terpri)
82		(format t " unify? = ~s" do-unify)
83		(terpri)
84		(format t " one way match? = ~s" one-way-match)
	76	(with-match-debug ()
	77	(format t "~%* First Match --------------------------------")
	78	(print-next)
	79	(princ "t1 = ") (term-print-with-sort t1)
	80	(print-next)
	81	(princ "t2 = ") (term-print-with-sort t2)
	82	(print-next)
	83	(format t "unify? = ~s" do-unify)
	84	(print-next)
	85	(format t "one way match? = ~s" one-way-match)
85	86	(force-output))
86	87	;;
87	88	(multiple-value-bind (m-sys no-match)

89	90	(match-decompose&merge (create-match-system (new-environment)
90	91	(create-m-system t1 t2))
91	92	sigma)
92		(when match-debug
	93	(with-match-debug()
93	94	(format t "~%result of match-deocmpose&merge, no-match=~a" no-match)
94	95	(force-output))
95	96	;; Note: if the two terms are similar then "m-sys" is empty.

98	99	(let ((gst (new-global-state)))
99	100	(declare (type list gst))
100	101	(cond ((m-system-is-empty? (match-system-sys m-sys))
101		(when match-debug
	102	(with-match-debug ()
102	103	(format t "~% return with success"))
103	104	(let ((subst (match-system-to-substitution m-sys)))
104		(when match-debug
	105	(with-match-debug ()
105	106	(print-substitution subst))
106	107	(values gst
107	108	subst

112	113	(t (multiple-value-bind (sys theory-info)
113	114	(match-system-extract-one m-sys)
114	115	(declare (type list sys) (type theory-info theory-info))
115		(when match-debug
	116	(with-match-debug()
116	117	(format t "~% extracted a system ")
117	118	(print-m-system sys)
118	119	(format t "~% theory = ")

127	128	(if no-match
128	129	(values nil nil t nil)
129	130	(let ((next-gst nil))
130		(when match-debug
	131	(with-match-debug ()
131	132	(format t "~%First match calls next-match")
132	133	(format t "~% old gst: ")
133	134	(print-global-state gst)

140	141	sys
141	142	theory-info
142	143	th-st)))
143		(when match-debug
	144	(with-match-debug ()
144	145	(format t "~% next gst :")
145	146	(print-global-state next-gst))
146	147	(multiple-value-bind (new-gst subst no-match)

158	159	(block the-end
159	160	(let (st)
160	161	(while (global-state-is-not-empty gst)
161		(when match-debug
	162	(with-match-debug()
162	163	(format t "~%* Next-match : global-state = ")
163	164	(print-global-state gst))
164	165	(setq st (global-state-top gst))

166	167	(next-match-state st)
167	168	(declare (type (or null match-state) new-st)
168	169	(type (or null t) no-more))
169		(when match-debug
	170	(with-match-debug ()
170	171	(format t "~%** Next-match : next-match-state returns no-more = ~a" no-more)
171	172	(unless no-more
172	173	(format t "~%-- new state =")

183	184	;; popping: the reasoning is that a successful state
184	185	;; also terminates .
185	186	(setq gst (global-state-pop gst))
186		(when match-debug
	187	(with-match-debug ()
187	188	(format t "~%* Next-match : return-with subst"))
188	189	(return-from the-end
189	190	(values gst
190	191	(match-system-to-substitution m-sys)
191	192	nil)))))))))
192		(when match-debug
	193	(with-match-debug ()
193	194	(format t "~%* Next-match : return with no-match"))
194	195	;; no match
195	196	(values nil nil t)))