Commit 03f86a143c4200a2964e774e3b76b337fb0e9d6d - cafeobj

+12

-0

.gitignore less more

43	43	manual/md/reference-manual.run.xml
44	44	manual/md/reference-manual.tex
45	45	auto
	46	build-stamp
	47	doc/refman/reference-manual.bcf
	48	doc/refman/reference-manual.epub
	49	doc/refman/reference-manual.odt
	50	doc/refman/reference-manual.run.xml
	51	doc/refman/reference-manual.tex
	52	install-stamp
	53	make-cafeobj.lisp
	54	tswd
	55	version.lisp
	56	xbin/cafeobj.in
	57	dumps⏎

+3

-4

BigPink/codes/butils.lisp less more

215	215
216	216	;;; IS-SKOLEM : method module -> Bool
217	217	;;;
218		(defun is-skolem (meth &optional (module (or current-module last-module)))
	218	(defun is-skolem (meth &optional (module (get-context-module)))
219	219	(declare (type method meth)
220		(type module module)
	220	(type (or null module) module)
221	221	(values boolean))
222	222	(memq meth (module-skolem-functions module)))
223	223

1787	1787	(princ "---"))
1788	1788	full-lit-table)))
1789	1789
1790		(defun show-demodulators (&optional (mod (or current-module
1791		last-module)))
	1790	(defun show-demodulators (&optional (mod (get-context-module)))
1792	1791	(unless mod (return-from show-demodulators nil))
1793	1792	(with-in-module (mod)
1794	1793	(let* ((psys (module-proof-system mod))

+53

-122

BigPink/codes/commands.lisp less more

384	384	(with-in-module (current-module)
385	385	(auto-db-reset current-module)
386	386	(setq psys (module-proof-system current-module))
387		#\|\|
388		(unless psys
389		(with-output-chaos-error ('no-psys)
390		(princ "no proof system prepared, do `db reset' first!"))
391		)
392		\|\|#
393		;;
394	387	(setq args (flatten-list args))
395	388	(dolist (arg args)
396	389	(cond ((is-nat arg)

436	429	(princ "specified term is not valid as formula.")
437	430	(term-print val)))
438	431	(dolist (cl (formula->clause-1 val psys))
439		(push cl real-set)))))))))
440		)
	432	(push cl real-set))))))))))
441	433	;;
442	434	(dolist (cl (if (eq type :sos)
443	435	(psystem-sos psys)

467	459	(nreverse real-set)
468	460	:test #'clause-equal)))
469	461	(when put-sysgoal-in-sos
470		(setq put-sysgoal-in-sos nil)))
471		)
	462	(setq put-sysgoal-in-sos nil))))
472	463	;;
473	464	(if (eq type :sos)
474	465	(dolist (cl (psystem-sos psys))

504	495	(when put-sysgoal-in-sos
505	496	(push :system-goal (psystem-sos psys)))
506	497	;;
507		psys
508		))))
	498	psys))))
509	499
510	500	;;; EVAL-CLAUSE-SHOW
511	501	;;;

515	505	(with-output-chaos-error ('no-context)
516	506	(princ "no context module is given.")))
517	507	(prepare-for-parsing current-module)
518		#\|\|
519		(unless (module-proof-system current-module)
520		(with-output-chaos-error ('no-psys)
521		(princ "no proof system prepared, do `db reset' first!")))
522		\|\|#
523	508	(auto-db-reset current-module)
524	509	(with-in-module (current-module)
525	510	(let* ((parse-variables nil)

538	523	(dolist (cl (formula->clause-1 term
539	524	(module-proof-system current-module)))
540	525	(print-next)
541		(print-clause cl standard-output)))
542		)))
	526	(print-clause cl standard-output))))))
543	527
544	528	;;; EVAL-PN-LIST
545	529	;;;

564	548	(princ " ")
565	549	(dolist (cl (psystem-axioms psys))
566	550	(print-next)
567		(print-clause cl standard-output)))
568		))
	551	(print-clause cl standard-output)))))
569	552	(:sos
570	553	(with-proof-context (current-module)
571		(print-sos-list)
572		#\|\|
573		(dolist (cl (psystem-sos psys))
574		(print-next)
575		(print-clause cl standard-output))
576		\|\|#
577		))
	554	(print-sos-list) ))
578	555	(:usable
579	556	(with-proof-context (current-module)
580		(print-usable-list)
581		#\|\|
582		(dolist (cl (psystem-usable psys))
583		(print-next)
584		(print-clause cl standard-output))
585		\|\|#
586		))
	557	(print-usable-list) ))
587	558	(:passive
588	559	(with-proof-context (current-module)
589	560	(print-passive-list)))
590
591	561	(:flag
592	562	(pr-list-of-flag))
593	563	(:param

596	566	(pr-list-of-option))
597	567	(:demod
598	568	(with-proof-context (current-module)
599		(print-demodulators-list)
600		#\|\|
601		(dolist (cl (psystem-demods psys))
602		(print-next)
603		(print-clause cl standard-output))
604		\|\|#
605		))
	569	(print-demodulators-list)))
606	570	(otherwise
607	571	(with-output-chaos-error ('invalid)
608		(format t "internal error, unknown list option ~a" arg)))
609		)))
	572	(format t "internal error, unknown list option ~a" arg))))))
610	573
611	574	;;; EVAL-RESOLVE
612	575	;;;
613	576	(defun eval-resolve (ast)
614		(unless current-module
615		(with-output-chaos-error ('no-context)
616		(princ "no context (current module) is set!"))
617		)
618		(let ((out-file (%resolve-arg ast)))
619		(if (and out-file (not (equal out-file ".")))
620		(with-open-file (stream out-file :direction :output
621		:if-exists :append :if-does-not-exist :create)
622		(let ((standard-output stream))
623		(do-resolve (if open-module
624		last-module
625		current-module))))
626		(do-resolve (if open-module
627		last-module
628		current-module)))))
	577	(let ((eval-context (get-context-module)))
	578	(unless eval-context
	579	(with-output-chaos-error ('no-context)
	580	(princ "no context (current module) is set!")))
	581	(let ((out-file (%resolve-arg ast)))
	582	(if (and out-file (not (equal out-file ".")))
	583	(with-open-file (stream out-file :direction :output
	584	:if-exists :append :if-does-not-exist :create)
	585	(let ((standard-output stream))
	586	(do-resolve eval-context)))
	587	(do-resolve eval-context)))))
629	588
630	589	(defun do-resolve (mod)
631	590	(let ((time1 nil)

690	649	(setf (pn-flag index) value)
691	650	(dependent-flags index)
692	651	;; run hook
693		(funcall (pn-flag-hook index) value)
694		)))
	652	(funcall (pn-flag-hook index) value))))
695	653
696	654	;;; SHOW-OPTION
697	655	;;;

730	688	(with-output-msg ()
731	689	(format t "setting parameter ~s to ~d."
732	690	name value)))
733		(setf (pn-parameter index) value)
734		)))
	691	(setf (pn-parameter index) value))))
735	692
736	693	;;; option reset
737	694	;;;

741	698	(case command
742	699	(:reset (init-pn-options))
743	700	(:save (save-option-set name))
744		(:restore (restore-option-set name))
745		)))
	701	(:restore (restore-option-set name)))))
746	702
747	703	;;; DEMOD
748	704	(defun perform-demodulation (ast)

753	709	(perform-demodulation* preterm modexp mode result-as-text)))
754	710
755	711	(defun perform-demodulation* (preterm &optional modexp mode (result-as-text nil))
756		;; (setq $$trials 1)
757	712	(let ((consider-object t)
758	713	(rewrite-exec-mode (eq mode :exec))
759	714	(rewrite-semantic-reduce nil)

765	720	(number-matches nil))
766	721	(let ((mod (if modexp
767	722	(eval-modexp modexp)
768		last-module)))
769		(unless (eq mod last-module)
	723	(get-context-module))))
	724	(unless (eq mod (get-context-module))
770	725	(clear-term-memo-table term-memo-table))
771	726	(if (or (null mod) (modexp-is-error mod))
772	727	(if (null mod)
773	728	(with-output-chaos-error ('no-context)
774		(princ "no module expression provided and no selected(current) module.")
775		)
	729	(princ "no module expression provided and no selected(current) module."))
776	730	(with-output-chaos-error ('no-such-module)
777	731	(princ "incorrect module expression, no such module ")
778		(print-chaos-object modexp)
779		))
780		(progn
781		(context-push-and-move last-module mod)
782		(with-in-module (mod)
783		(auto-db-reset mod))
784		(with-proof-context (mod)
785		(when auto-context-change
786		(change-context last-module mod))
787		(!setup-reduction mod)
788		(setq $$mod current-module)
789		(setq sort cosmos)
790		(when show-stats (setq time1 (get-internal-run-time)))
	732	(print-chaos-object modexp)))
	733	(progn
	734	(context-push-and-move (get-context-module) mod)
	735	(with-in-module (mod)
	736	(auto-db-reset mod))
	737	(with-proof-context (mod)
	738	(when auto-context-change
	739	(change-context (get-context-module) mod))
	740	(!setup-reduction mod)
	741	(setq $$mod (get-context-module))
	742	(setq sort cosmos)
	743	(when show-stats (setq time1 (get-internal-run-time)))
791	744	(setq rewrite-semantic-reduce
792	745	(and (eq mode :red)
793	746	(module-has-behavioural-axioms mod)))
794	747	;;
795	748	(let* ((parse-variables nil)
796		(term (simple-parse current-module preterm sort)))
	749	(term (simple-parse (get-context-module) preterm sort)))
797	750	(when (or (null (term-sort term))
798	751	(sort<= (term-sort term) syntax-err-sort chaos-sort-order))
799	752	(return-from perform-demodulation* nil))

802	755	(setq time2 (get-internal-run-time))
803	756	(setf time-for-parse
804	757	(format nil "~,3f sec"
805		;; (/ (float (- time2 time1)) internal-time-units-per-second)
806		(elapsed-time-in-seconds time1 time2)
807		)))
	758	(elapsed-time-in-seconds time1 time2))))
808	759	(unless chaos-quiet
809	760	(fresh-all)
810	761	(flush-all)

814	765	(princ "-- demodulate in ")
815	766	(princ "-- behavioural demodulate in "))
816	767	)
817		(print-simple-mod-name current-module)
	768	(print-simple-mod-name (get-context-module))
818	769	(princ " : ")
819	770	(let ((print-indent (+ 4 print-indent)))
820	771	(term-print term))
821	772	(flush-all))
822	773	;; ********
823		(reset-target-term term last-module mod)
	774	(reset-target-term term (get-context-module) mod)
824	775	;; ********
825	776	(setq $$matches 0)
826	777	(setq time1 (get-internal-run-time))
827	778	(let ((rule-count 0))
828	779	(let ((res nil))
829	780	(catch 'rewrite-abort
830		#\|\|
831		(if (sort<= (term-sort term) fopl-sentence-sort
832		current-sort-order)
833		(dolist (sub (term-subterms term))
834		(unless (term-is-variable? sub)
835		(demod-atom sub)))
836		(setq res (demod-atom term)))
837		\|\|#
838		(setq res (demod-atom term))
839		)
	781	(setq res (demod-atom term)))
840	782	(unless res (setq res $$term))
841	783	;;
842	784	(when mel-sort

848	790	(setq time2 (get-internal-run-time))
849	791	(setf time-for-reduction
850	792	(format nil "~,3f sec"
851		;; (/ (float (- time2 time1))
852		;; internal-time-units-per-second)
853	793	(elapsed-time-in-seconds time1 time2)))
854	794	(setf number-matches $$matches)
855	795	(setq $$matches 0)

864	804	(print-check)
865	805	(princ " : ")
866	806	(print-sort-name (term-sort res)
867		current-module))
868		s
869		))
	807	(get-context-module))
	808	s)))
870	809	(stat
871	810	(if show-stats
872	811	(concatenate

890	829	(print-check 0 3)
891	830	(princ " : ")
892	831	(print-sort-name (term-sort res)
893		current-module))
	832	(get-context-module)))
894	833	(when show-stats
895	834	(format t "~%(~a for parse, ~s rewrites(~a), ~d matches"
896	835	time-for-parse

901	840	(format t ")~%")
902	841	(format t ", ~d memo hits)~%"
903	842	term-memo-hash-hit)))
904		(flush-all)))
905		))
906		))
	843	(flush-all)))))))
907	844	(context-pop-and-recover))))))
908	845
909	846	;;; SIGMATCH

920	857	(princ "no such module: ")
921	858	(print-modexp (%sigmatch-mod2 ast))))
922	859	(setq views (sigmatch mod1 mod2))
923		;;
924	860	(if views
925	861	(princ views)
926		(princ "( )"))
927		))
	862	(princ "( )"))))
928	863
929	864	;;; LEX
930	865	(defun eval-pn-lex (ast)
931		(unless current-module
	866	(unless (get-context-module)
932	867	(with-output-chaos-error ('no-context)
933	868	(princ "no context(current) module is specified.")))
934		(compile-module current-module)
935		(with-in-module (current-module)
	869	(compile-module (get-context-module))
	870	(with-in-module ((get-context-module))
936	871	(let ((optokens (%pn-lex-ops ast))
937	872	(prec-list nil))
938	873	(dolist (e optokens)

946	881	(with-in-module (mod)
947	882	(dolist (opinfo ops)
948	883	(dolist (meth (reverse (opinfo-methods opinfo)))
949		(push meth prec-list))))))
950		)
951		))
	884	(push meth prec-list)))))))))
952	885	;;
953	886	(unless (memq :* prec-list)
954	887	(push :* prec-list))

956	889	(push :skolem prec-list))
957	890	(setq prec-list (nreverse prec-list))
958	891	;;
959		(setf (module-op-lex current-module) prec-list)
960		)))
961
	892	(setf (module-op-lex current-module) prec-list))))
962	893
963	894	;;; EOF

+2

-3

BigPink/codes/formula.lisp less more

667	667	;; must skolemize subformula first to avoid
668	668	;; problem in \Ax...\Ey...\Ex F(x,y)
669	669	(skolem (term-arg-2 sentence))
670		(let* ((mod (or current-module last-module))
	670	(let* ((mod (get-context-module))
671	671	(skfun-name
672	672	(make-skolem-function-name (term-sort
673	673	(term-arg-1 sentence))
674		variables))
675		)
	674	variables)))
676	675	(multiple-value-bind (op meth)
677	676	(declare-operator-in-module
678	677	(list skfun-name)

+1

-2

BigPink/codes/inv.lisp less more

770	770
771	771	(defun pn-check-invariance (args)
772	772	(declare (type list args))
773		(let ((target-module (or current-module
774		last-module)))
	773	(let ((target-module (get-context-module)))
775	774	(declare (type (or null module) target-module))
776	775	(unless target-module
777	776	(with-output-chaos-error ('no-context)

+1

-2

BigPink/codes/proof-sys.lisp less more

89	89
90	90	;;; PN-DB-RESET
91	91	;;;
92		(defun pn-db-reset (&optional (mod (or current-module
93		last-module)))
	92	(defun pn-db-reset (&optional (mod (get-context-module)))
94	93	(clear-all-index-tables)
95	94	(reset-module-proof-system mod))
96	95

+3

-4

BigPink/codes/types.lisp less more

188	188	(unless (literal-sign lit)
189	189	(princ "~(" stream)
190	190	(setq .file-col. (1+ .file-col.)))
191		(with-in-module ((or current-module last-module))
	191	(with-in-module ((get-context-module))
192	192	(cond ((eq-literal? lit)
193	193	(let* ((lhs (term-arg-1 (literal-atom lit)))
194	194	(rhs (term-arg-2 (literal-atom lit)))

231	231	(unless (literal-sign lit)
232	232	(princ "~(" stream)
233	233	(setq .file-col. (1+ .file-col.)))
234		(with-in-module ((or current-module last-module))
	234	(with-in-module ((get-context-module))
235	235	(setq .printed-vars-so-far.
236	236	(append .printed-vars-so-far.
237	237	(term-print (literal-atom lit) stream))))
238	238	(unless (literal-sign lit)
239	239	(princ ")" stream))
240		.printed-vars-so-far.)
241		)
	240	.printed-vars-so-far.))
242	241
243	242	;;;
244	243	;;; some gobal flags

+14

-0

TODO less more

	0	20150324 tswd
	1
	2	refactor, over 20 years old codes
	3	even 20 years a go, the style was already old fashioned.
	4	(1) many globals to be eliminated
	5	memoized-module ?
	6	(2) clean up and reorganize modules
	7	profiler -- new
	8	context
	9	(3) many dumplicated/similar code fragments
	10	much codes have been added in ad hoc manner
	11
0	12	20150225 np
1	13
2	14	we should add a check that a key is not define'd more than once

22	34	--end-toplevel-options <args-to-cafeobj>*
23	35	(Please refer to 3.2.3 Saving Core Image and 3.3 Command Line Options
24	36	of the manual. )
	37
	38	⏎

+21

-21

cafeobj/command-top.lisp less more

392	392	(defun print-cafeobj-prompt ()
393	393	(fresh-all)
394	394	(flush-all)
395		(cond ((eq prompt 'system)
396		(if last-module
397		(if (module-is-inconsistent last-module)
	395	(let ((cur-module (get-context-module)))
	396	(cond ((eq prompt 'system)
	397	(if cur-module
	398	(if (module-is-inconsistent cur-module)
398	399	(progn
399	400	(with-output-chaos-warning ()
400	401	(format t "~a is inconsistent due to changes in some of its submodules."
401		(module-name last-module))
	402	(module-name cur-module))
402	403	(print-next)
403	404	(princ "resetting the `current module' of the system.."))
404		(setq last-module nil)
405		(format error-output "~&CafeOBJ> ")
406		)
	405	(reset-context-module)
	406	(format error-output "~&CafeOBJ> "))
407	407	(let ((standard-output error-output))
408		(print-simple-mod-name last-module)
	408	(print-simple-mod-name cur-module)
409	409	(princ "> ")))
410		(format error-output "CafeOBJ> "))
411		(setf sub-prompt nil))
412		((eq prompt 'none))
413		(prompt
414		(let ((standard-output error-output))
415		(if (atom prompt)
416		(princ prompt)
417		(print-simple-princ-open prompt))
418		(princ " "))))
419		(flush-all))
	410	;; no context module
	411	(format error-output "CafeOBJ> "))
	412	(setf sub-prompt nil))
	413	;; prompt specified to NONE
	414	((eq prompt 'none))
	415	;; specified prompt
	416	(prompt
	417	(let ((standard-output error-output))
	418	(if (atom prompt)
	419	(princ prompt)
	420	(print-simple-princ-open prompt))
	421	(princ " "))))
	422	(flush-all)))
420	423
421	424	;;; SAVE INTERPRETER IMAGE
422	425	;;;_____________________________________________________________________________

602	605	(setq chaos-print-errors t)
603	606	(setq .in-in. nil)))))))
604	607
605		(defun try-reduce-term (inp)
606		(perform-reduction* inp current-module nil nil))
607
608	608	(defun handle-cafeobj-top-error (val)
609	609	(if chaos-input-source
610	610	(chaos-to-top val)

+3

-1

cafeobj/trans-com.lisp less more

582	582	;;; ******************
583	583	;;; MODULE Constructs.
584	584	;;; ******************
	585
	586	;;; it is an error unless a module is open.
585	587	(defun cafeobj-eval-module-element-proc (inp)
586	588	(if open-module
587		(with-in-module (last-module)
	589	(with-in-module ((get-context-module))
588	590	(multiple-value-bind (type ast)
589	591	(parse-module-element inp)
590	592	(declare (ignore type))

+3

-5

chaos/boot/builtins.lisp less more

186	186	(defun install-chaos-hard-wired-modules ()
187	187	(setq dribble-ast nil)
188	188	(setq ast-log nil)
189		(setq last-module nil current-module nil)
	189	(reset-context-module)
190	190	(setq include-bool nil)
191	191	(setq include-rwl nil)
192	192	(setq regularize-signature nil)

280	280	(%bsort-decl "String" nil nil prin1 stringp nil))))
281	281	(install-string)
282	282	;;
283		;;
284		(setq last-module nil current-module nil)
	283	(reset-context-module)
285	284	(setq include-bool t)
286	285	(setq include-rwl t)
287	286	)

302	301	(setq ast-log nil)
303	302	(setq include-bool t)
304	303	(setq include-rwl t)
305		(setq last-module nil
306		current-module nil)
	304	(reset-context-module)
307	305	(setq regularize-signature nil)
308	306	;; set recover proc.
309	307	(setq system-soft-wired

+1

-2

chaos/boot/preproc.lisp less more

54	54	(defun token-is-sort-id (token)
55	55	(and (stringp token)
56	56	(<= 1 (length token))
57		(find-all-sorts-in (or current-module last-module)
58		token)))
	57	(find-all-sorts-in (get-context-module) token)))
59	58	(defun create-sort-id (token) token)
60	59	(defun print-sort-id (x) (princ x))
61	60	(defun is-sort-Id (x)

+1

-2

chaos/cafein/rengine.lisp less more

1783	1783	(apply-sort-memb-internal term module)))
1784	1784	term)
1785	1785
1786		(defun sort-to-sort-id-term (sort &optional (module (or current-module
1787		last-module)))
	1786	(defun sort-to-sort-id-term (sort &optional (module (get-context-module)))
1788	1787	(let* ((name (string (sort-id sort)))
1789	1788	(op (find-method-in module (list name) nil sort-id-sort)))
1790	1789	(unless op

+68

-132

chaos/construct/axiom.lisp less more

144	144	(variable-name x))
145	145	variables))
146	146	subst
147		',s-simbol))
148		)
149		)))
	147	',s-simbol))))))
150	148	((term-is-general-lisp-form? term)
151	149	(setf fun-body
152	150	(make-fun* `(lambda (subst)

184	182	',(reverse (mapcar #'(lambda (x)
185	183	(variable-name x))
186	184	variables))
187		subst))
188		)
189		)
	185	subst))))
190	186	(setf (term-builtin-value term)
191	187	(list '\|%Chaos\| fun-body (term-builtin-value term)))
192	188	term))

249	245	(push (term-builtin-value value) bindings)
250	246	(return-from invoke (values nil nil))))
251	247	(return-from invoke (values value t))))
252		(return-from invoke (values nil nil)))
253		)
254		(return-from invoke (values nil nil))
255		)))
	248	(return-from invoke (values nil nil))))
	249	(return-from invoke (values nil nil)))))
256	250	(if (sort-is-builtin sort)
257	251	(values (make-bconst-term sort
258	252	(apply fun bindings))

290	284	(push (term-builtin-value value) bindings)
291	285	(return-from invoke (values nil nil))))
292	286	(return-from invoke (values value t))))
293		(return-from invoke (values nil nil)))
294		)
295		(return-from invoke (values nil nil))
296		)))
	287	(return-from invoke (values nil nil))))
	288	(return-from invoke (values nil nil)))))
297	289	(values (make-bconst-term sort
298	290	(apply fun bindings))
299		t)
300		))))
	291	t)))))
301	292
302	293	;;;
303	294	;;;

341	332	:rhs (make-applform (method-coarity top)
342	333	top
343	334	(list new-var
344		;;(substitution-check-builtin
345		;; (axiom-rhs rule))
346		(axiom-rhs rule)
347		))
	335	(axiom-rhs rule)))
348	336	:condition (axiom-condition rule)
349	337	:id-condition (axiom-id-condition rule)
350	338	:type (axiom-type rule)

380	368	:id-ext-theory
381	369	:A-right-theory)
382	370	:meta-and-or (axiom-meta-and-or rule)))
383		;; (compute-rule-method ext-rule)
384	371	(push ext-rule listext)
385
386	372	;; the middle associative extension:
387	373	(setf ext-rule
388	374	(make-rule

405	391	:meta-and-or (axiom-meta-and-or rule)))
406	392	;;
407	393	(push ext-rule listext)
408		(setf (axiom-A-extensions rule) listext))
409		)))
	394	(setf (axiom-A-extensions rule) listext)))))
410	395
411	396
412	397	;;; COMPUTE-AC-EXTENSION : rule method -> List[Rule]

438	423	:rhs (make-applform (method-coarity top)
439	424	top
440	425	(list new-var
441		(axiom-rhs rule)
442		))
	426	(axiom-rhs rule)))
443	427	:condition (axiom-condition rule)
444	428	:type (axiom-type rule)
445	429	:behavioural (axiom-is-behavioural rule)

450	434	':ac-theory)
451	435	:meta-and-or (axiom-meta-and-or rule)))
452	436	;;
453		(setf (axiom-AC-extension rule) (list ext-rule))
454		))))
	437	(setf (axiom-AC-extension rule) (list ext-rule))))))
455	438
456	439
457	440	;;; GIVE-AC-EXTENSION : rule -> List[Rule]

572	555	(cond ((term$is-variable? t1-body)
573	556	(or (eq t1 t2)
574	557	(and (term$is-variable? t2-body)
575		#\|\|
576		;; (eq (variable$name t1-body) (variable$name t2-body))
577		(sort= (variable$sort t1-body) (variable$sort t2-body))
578		\|\|#
579		(variable= t1 t2)
580		)))
	558	(variable= t1 t2))))
581	559	((term$is-variable? t2-body) nil)
582	560	((term$is-application-form? t1-body)
583	561	(and (term$is-application-form? t2-body)
584		(if ;;(method-is-same-qual-method (term$method t1-body)
585		;; (term$method t2-body))
586		(method-is-of-same-operator+ (term$method t1-body)
	562	(if (method-is-of-same-operator+ (term$method t1-body)
587	563	(term$method t2-body))
588	564	(let ((sl1 (term$subterms t1-body))
589	565	(sl2 (term$subterms t2-body)))

642	618	(when (rule-is-similar? rule r)
643	619	(when (and chaos-verbose
644	620	(not (eq rule r))
645		(not (member (axiom-kind rule) .ext-rule-kinds.))
646		)
	621	(not (member (axiom-kind rule) .ext-rule-kinds.)))
647	622	(with-output-msg ()
648	623	(format t "a similar pair of axioms is found:")
649	624	(print-next)

731	706	;;; ***********************
732	707	;;; ADDING AXIOMS TO MODULE
733	708	;;; ***********************
734		#\|\|
	709
735	710	(defun add-axiom-to-module (module ax)
736		(declare (type module module)
737		(type axiom ax)
738		(values t))
739		(if (memq (axiom-type ax) '(:equation :pignose-axiom :pignose-goal))
740		(push ax (module-equations module))
741		(push ax (module-rules module))))
742		\|\|#
743
744		(defun add-axiom-to-module (module ax)
745		(adjoin-axiom-to-module module ax)
746		)
	711	(adjoin-axiom-to-module module ax))
747	712
748	713	(defun adjoin-axiom-to-module (module ax)
749	714	(declare (type module module)
750	715	(type axiom ax)
751	716	(values t))
752		;; (when (eq (object-context-mod ax) module)
753		;; (let ((labels (axiom-labels ax)))
754		;; (dolist (lab labels)
755		;; (symbol-table-add (module-symbol-table module)
756		;; lab
757		;; ax)))
758		;; )
759	717	(if (memq (axiom-type ax) '(:equation :pignose-axiom :pignose-goal))
760	718	(setf (module-equations module)
761	719	(adjoin-rule ax (module-equations module)))

819	777	(substitution-partial-image
820	778	subst
821	779	(rule-condition r1))))))
822		(matches? newcond (rule-condition r2))
823		))))))))))
	780	(matches? newcond (rule-condition r2))))))))))))
824	781
825	782	(defun rule-strictly-subsumes (r1 r2)
826	783	(declare (type axiom r1 r2)

891	848	:condition (axiom-condition rule)
892	849	:labels (axiom-labels rule)
893	850	:kind (axiom-kind rule)
894		:type (axiom-type rule)
895		;; :meta-and-or (axiom-meta-and-or rule)
896		;; :no-method-computation t
897		)))
	851	:type (axiom-type rule))))
898	852
899	853	(defun make-rule-instance (rule subst)
900	854	(declare (type axiom rule)

932	886	;; we always need rule specifier
933	887	(when (equal "" rule-id)
934	888	(with-output-chaos-error ('invalid-rule-spec)
935		(format t "No rule number or name is specified.")
936		))
	889	(format t "No rule number or name is specified.")))
937	890	;; get module in which the specified rule is looked up
938		(if (equal "" mod)
939		(setq mod last-module)
940		(if (and last-module
941		(equal "%" (module-name last-module))
942		(module-submodules last-module)
943		(equal mod
944		(module-name
945		(caar (module-submodules last-module)))))
946		(setq mod last-module)
947		;; we also find in local modules
948		(setq mod (eval-modexp mod t))))
949		;;
950		(unless mod
951		(with-output-chaos-error ('no-context)
952		(princ "no context module.")))
953		;;
954		(when (modexp-is-error mod)
955		(let ((nxt (eval-mod (list (car rule-spec)))))
956		(if (modexp-is-error nxt)
957		(with-output-chaos-error ('invalid-module)
958		(format t "module is undefined or unreachable: ~a" (car rule-spec))
959		)
	891	(let ((cur-context (get-context-module)))
	892	(if (equal "" mod)
	893	(setq mod cur-context)
	894	(if (and cur-context
	895	(equal "%" (module-name cur-context))
	896	(module-submodules cur-context)
	897	(equal mod
	898	(module-name
	899	(caar (module-submodules cur-context)))))
	900	(setq mod cur-context)
	901	;; we also find in local modules
	902	(setq mod (eval-modexp mod t))))
	903	(unless mod
	904	(with-output-chaos-error ('no-context)
	905	(princ "no context module.")))
	906	(when (modexp-is-error mod)
	907	(let ((nxt (eval-mod (list (car rule-spec)))))
	908	(if (modexp-is-error nxt)
	909	(with-output-chaos-error ('invalid-module)
	910	(format t "module is undefined or unreachable: ~a" (car rule-spec)))
960	911	(setq mod nxt))))
961		;; check context
962		(unless (eq last-module mod)
963		(let ((e-mod (assoc mod (module-all-submodules last-module))))
964		(unless e-mod
965		(with-output-chaos-error ('invalid-context)
966		(format t "specified module is out of current context: ")
967		(print-simple-mod-name mod)))
968		(unless (member (cdr e-mod)
969		'(:protecting :extending :using))
970		(with-output-chaos-error ('invalid-rule-ref)
971		(format t "you cannot refer the rule ~a of module " rule-spec)
972		(print-simple-mod-name mod)
973		(princ " directly.")))))
974		;;
975		(with-in-module (mod)
976		;; find specified rule
977		(if (and (< 0 (length rule-id))
978		(every #'digit-char-p rule-id))
979		(setq rule (get-rule-numbered mod (str-to-int rule-id)))
	912	;; check context
	913	(unless (eq cur-context mod)
	914	(let ((e-mod (assoc mod (module-all-submodules cur-context))))
	915	(unless e-mod
	916	(with-output-chaos-error ('invalid-context)
	917	(format t "specified module is out of current context: ")
	918	(print-simple-mod-name mod)))
	919	(unless (member (cdr e-mod)
	920	'(:protecting :extending :using))
	921	(with-output-chaos-error ('invalid-rule-ref)
	922	(format t "you cannot refer the rule ~a of module " rule-spec)
	923	(print-simple-mod-name mod)
	924	(princ " directly.")))))
	925	;; do search in 'mod'
	926	(with-in-module (mod)
	927	;; find specified rule
	928	(if (and (< 0 (length rule-id))
	929	(every #'digit-char-p rule-id))
	930	(setq rule (get-rule-numbered mod (str-to-int rule-id)))
980	931	(setq rule (get-rule-labelled mod rule-id)))
981		;; make rule reverse order if need
	932	;; make rule reverse order if need
982	933	(when (nth 2 rule-spec) (setq rule (make-rule-reverse rule)))
983	934	;; apply variable substitution
984	935	(when subst-list
985	936	(setq rule
986		(make-rule-instance rule (compute-variable-substitution
987		rule subst-list))))
988		)
	937	(make-rule-instance rule (compute-variable-substitution
	938	rule subst-list)))))
989	939	;; the result
990		(when on-axiom-debug
991		(with-output-simple-msg ()
992		(princ "[compute-action-rule]: rule= ")
993		(print-chaos-object rule)))
994		;;
995		(values rule mod)
996		))
	940	(when on-axiom-debug
	941	(with-output-simple-msg ()
	942	(princ "[compute-action-rule]: rule= ")
	943	(print-chaos-object rule)))
	944	(values rule mod))))
997	945
998	946
999	947	;;; CHECK-AXIOM-ERROR-METHOD : Module Axiom -> Axiom

1010	958	(error-operators (module-error-methods module)))
1011	959	(macrolet ((check-check (_eops)
1012	960	` (when (every #'(lambda (x)
1013		#\|\|
1014		(and (memq x error-operators)
1015		(not (method-is-user-defined-error-method
1016		x)))
1017		\|\|#
1018		(memq x error-operators)
1019		)
	961	(memq x error-operators))
1020	962	,_eops)
1021	963	(setq ,_eops nil))))
1022	964	;;

1092	1034	(type list error-operators))
1093	1035	(macrolet ((check-check (_eops)
1094	1036	` (when (every #'(lambda (x)
1095		#\|\|
1096		(and (memq x error-operators)
1097		(not (method-is-user-defined-error-method
1098		x)))
1099		\|\|#
1100		(memq x error-operators)
1101		)
	1037	(memq x error-operators))
1102	1038	,_eops)
1103	1039	(setq ,_eops nil))))
1104	1040	;;

+4

-36

chaos/construct/gen-rule.lisp less more

46	46	(values t))
47	47	(compute-protected-modules module)
48	48
49		;; reset rewrite rule set.
50		;; (setf (module-all-rules module) nil)
51
52		;; adds axioms for record/class
53		(dolist (s (module-sorts module))
54		(cond ((class-sort-p s)
55		(declare-class-axioms module s))
56		((record-sort-p s)
57		(declare-record-axioms module s))))
58
59	49	;; install own rules.
60	50	(let ((axiom-set (module-axiom-set module)))
61	51	(dolist (eq (axiom-set$equations axiom-set))
62	52	(gen-rule-internal eq module))
63	53	(dolist (rule (axiom-set$rules axiom-set))
64	54	(gen-rule-internal rule module)))
65
66		;; install rules of submodules
67		;; (dolist (submodule (module-all-submodules module))
68		;; (unless (eq 'using (cdr submodule))
69		;; (transfer-axioms module (car submodule))))
70	55
71	56	;; specialize rules of sumodules.
72	57	(dolist (rule (gather-submodule-rules module))

82	67	(and (term-is-application-form? t2)
83	68	(dolist (sub (term-subterms t2) nil)
84	69	(when (variable-occurs-in t1 sub)
85		(return-from variable-occurs-in t))))
86		))
	70	(return-from variable-occurs-in t))))))
87	71
88	72	(defparameter non-exec-labels '(\|:nonexec\| \|:non-exec\| \|:no-ex\| \|:noex\| \|:noexec\|))
89	73

116	100	(when (term-is-variable? (axiom-lhs rule))
117	101	(when (variable-occurs-in (axiom-lhs rule)
118	102	(axiom-rhs rule))
119		;; (format t "..setting rule mark `need-copy'")
120	103	(setf (axiom-need-copy rule) t))
121		;;
122	104	(unless (eq (axiom-type rule) :rule)
123	105	(unless (axiom-non-exec rule)
124	106	(with-output-chaos-warning ()

130	112	(setf (axiom-kind rule) ':bad-rule)
131	113	(setf (axiom-kind ax) ':bad-rule))
132	114	(return-from gen-rule-internal nil))
133		;;
134	115	(let ((rhs-vars (term-variables (axiom-rhs rule)))
135	116	(cond-vars (term-variables (axiom-condition rule))))
136	117	(declare (type list rhs-vars cond-vars))

144	125	(print-chaos-object rule)
145	126	(print-next)
146	127	(princ "is not a subset of variables in LHS, system does not guarantee the result of the rewriting.")))
147		;; (setf (axiom-kind rule) ':bad-rule)
148		;; (setf (axiom-kind ax) ':bad-rule))
149	128	(add-rule-to-module module rule)
150	129	(unless (term-is-variable? (axiom-lhs rule))
151	130	(add-associative-extensions module

173	152	(progn
174	153	(setf (axiom-kind rule) ':bad-rule)
175	154	(setf (axiom-kind ax) ':bad-rule))))
176		;;
177	155	;; all is ok, we can use this axiom as a rewrite rule
178	156	(t (add-rule-to-module module rule)
179	157	(unless (term-is-variable? (axiom-lhs rule))

385	363	:kind (if (eq ':id-theorem (axiom-kind r))
386	364	':id-ext-theory
387	365	':a-right-theory)))
388		;; (compute-rule-method a-rule)
389	366	(add-rule-to-method a-rule method-above (module-opinfo-table mod))
390	367
391	368	(setf a-rule

413	390	:kind (if (eq ':id-theorem (axiom-kind r))
414	391	':id-ext-theory
415	392	':a-middle-theory)))
416		;; (compute-rule-method a-rule)
417		(add-rule-to-method a-rule method-above (module-opinfo-table mod))))
418		))))
	393	(add-rule-to-method a-rule method-above (module-opinfo-table mod))))))))
419	394
420	395	(defun rule-check-down (mod method terms)
421	396	(declare (ignore mod)

488	463	(cdr term-s))
489	464	cvi)))
490	465	(unless (eq ':fail res)
491		(return res)))))))))
492		))
	466	(return res)))))))))))
493	467
494	468	;;;-----------------------------------------------------------------------------
495	469	(defun normalize-rules-in (mod)

508	482	(values list))
509	483	(prog1
510	484	(list (intern (format nil "~a~a" label $rule-counter)))
511		(incf $rule-counter)))
512		)
	485	(incf $rule-counter))))
513	486
514	487	(defun add-operator-theory-axioms (module opinfo)
515	488	(declare (type module module)

690	663	(not (eq r newrule)))
691	664	(setf (axiom-labels newrule)
692	665	(create-rule-name module "compl")))
693		;; #\|\|
694	666	(when (axiom-extensions newrule)
695	667	(dolist (e (axiom-a-extensions newrule))
696	668	(setf (axiom-id-condition e) newidcond))
697	669	(dolist (e (axiom-AC-extension newrule))
698	670	(setf (axiom-id-condition e) newidcond)))
699		;; \|\|#
700	671	(dolist (e (axiom-extensions newrule))
701	672	(when e
702	673	(setf (axiom-id-condition e) newidcond)))
703		;;
704		;; (break)
705	674	(unless (eq r rul)
706	675	(adjoin-axiom-to-module module newrule)))))))))
707	676

863	832	:meta-and-or (rule-meta-and-or rul)
864	833	:labels (cons (car (create-rule-name 'dummy "idcomp")) (axiom-labels rul))))
865	834	;;
866		;;
867	835	(when gen-rule-debug
868	836	(format t "~%invert-val: ")
869	837	(format t "~% given rule : ")

+60

-337

chaos/construct/operator.lisp less more

36	36	#+:chaos-debug
37	37	(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
38	38
39		;;; (defvar on-operator-debug nil)
40	39	(defun on-debug-operator ()
41	40	(setq on-operator-debug t))
42	41	(defun off-debug-operator ()
43	42	(setq on-operator-debug nil))
44	43
45		;;; TODO, immediately
	44	;;; TODO
46	45	;;; syntax of an operator can be regular-expression.
47	46
48	47	;;; === DESCRIPTION ============================================================

323	322	(setq theory (merge-operator-theory-in current-module
324	323	method
325	324	old-th
326		theory
327		))
	325	theory))
328	326	(setq new-code (theory-code theory))))
329	327	;;
330	328	;; associativity

454	452	(princ "invalid strategy ")
455	453	(princ strat)
456	454	(princ " for operator ")
457		(princ (method-symbol meth))
458		))
	455	(princ (method-symbol meth))))
459	456	;; complete
460	457	(setf (method-supplied-strategy meth) (complete-strategy num-args strat))))
461	458

475	472	(t (with-output-chaos-warning ()
476	473	(format t "unknown associativity declaration ~a assoc for operator ~a, ignored"
477	474	assoc
478		(method-symbol meth)
479		))
	475	(method-symbol meth)))
480	476	nil)))
481	477
482	478	;;; PRECEDENCE ___________________________________________________________________

515	511	(setf (method-constructor method) constr)
516	512	(when constr
517	513	(pushnew method (sort-constructor (method-coarity method))
518		:test #'eq))
519		)
	514	:test #'eq)))
520	515
521	516	;;; COHERENCY ---------------------------------------------------------------------
522	517

525	520	(type (or null t) coherent)
526	521	(values (or null t)))
527	522	(setf (method-coherent method) coherent))
528
529		;;; COPIER ________________________________________________________________________
530		;;; COPY-METHOD-INFO : from-method to-method
531		;;;
532		#\|\| NOT USED
533		(defun copy-method-info (from to)
534		(let (sup-strat
535		theory
536		prec
537		memo
538		assoc
539		constr)
540		(when on-operator-debug
541		(format t "~&[copy-method-info]:")
542		(format t "~&-- copy from ") (print-chaos-object from)
543		(format t "~& to ") (print-chaos-object to))
544		(let ((from-module (method-module from)))
545		(with-in-module (from-module)
546		(setf sup-strat (method-supplied-strategy from)
547		theory (method-theory from)
548		prec (get-method-precedence from)
549		memo (method-memo from)
550		assoc (method-associativity from)
551		constr (method-constructor from))))
552		(let ((to-module (method-module to)))
553		(with-in-module (to-module)
554		(setf (method-supplied-strategy to) sup-strat
555		(method-theory to) theory
556		(method-precedence to) prec
557		(method-memo to) memo
558		(method-associativity to) assoc
559		(method-constructor to) constr)))
560		))
561
562		\|\|#
563	523
564	524	;;; ********************
565	525	;;; OPERATOR DECLARATION _______________________________________________________

587	547	(unless mod
588	548	(with-output-chaos-error ('no-such-module)
589	549	(princ "declaring operator, no such module ")
590		(princ module)
591		))
	550	(princ module)))
592	551
593	552	;; check arity, coarity
594	553	(with-in-module (mod)

628	587	(t
629	588	(with-output-chaos-error ('no-such-sort)
630	589	(princ "declaring operator, no such sort ")
631		(print-sort-ref coarity)
632		))))
633		;; name conflict check with existing variables
634		#\|\|
635		(when (and (null r-arity)
636		(find-variable-in module (car op-name)))
637		(with-output-chaos-warning ()
638		(format t "declaring op ~s" op-name)
639		(print-next)
640		(princ " there already a variable with the same name.")
641		(princ " ... ignoring"))
642		(return-from declare-operator-in-module (values nil nil nil))
643		)
644		\|\|#
645		;;
	590	(print-sort-ref coarity)))))
646	591	(multiple-value-bind (x y)
647	592	(add-operator-declaration-to-module op-name
648	593	(nreverse r-arity)

651	596	constructor
652	597	behavioural
653	598	coherent
654		error-operator
655		)
656		(values x y nil))))
657		))
	599	error-operator)
	600	(values x y nil))))))
658	601
659	602	(defun make-operator-in-module (op-name num-args module &optional qual-name)
660	603	(declare (ignore qual-name)

670	613	(unless arity
671	614	(let ((opstr (car op-name))
672	615	(sorts (module-all-sorts module)))
673		(dolist (bi sorts)
	616	(dolist (bi sorts nil)
674	617	(when (sort-is-builtin bi)
675	618	(let ((token-pred (bsort-token-predicate bi)))
676	619	(when (and token-pred

684	627	(print-sort-name bi module)
685	628	(print-next)
686	629	(princ "... ignored.")
687		(return-from check-overloading-with-builtin t)
688		))))))
689		)
690		nil)
	630	(return-from check-overloading-with-builtin t)))))))))
691	631
692	632	(defun add-operator-declaration-to-module (op-name arity coarity module
693	633	&optional

698	638	(declare (type t op-name)
699	639	(type list arity)
700	640	(type (or symbol sort-struct) coarity)
701		(type t module)
702		(type (or null t)
703		constructor behavioural coherent error-operator))
	641	(type (or null module) module))
704	642	(let* ((mod (if (module-p module)
705	643	module
706		(find-module-in-env module)))
	644	(find-module-in-env module)))
707	645	(op-infos (find-operators-in-module op-name (length arity) mod))
708	646	(opinfo nil)
709	647	(op nil))

716	654	arity coarity)
717	655	(format t "~% -- module = ~a, constructor = ~a, behavioural = ~a"
718	656	module constructor behavioural)
719		(format t "~% -- coherent = ~a, error-operator = ~a" coherent error-operator)
720		)
	657	(format t "~% -- coherent = ~a, error-operator = ~a" coherent error-operator))
721	658	;; checks hidden sort condition
722	659	(let ((hidden? nil))
723	660	(dolist (as arity)

727	664	(format t "more than one hidden sort in the declaration of operator \"~{~a~}\""
728	665	op-name)
729	666	))
730		(setf hidden? t)
731		#\|\| -----------------------------------------------
732		(when (and (not (sort= as huniversal-sort))
733		(not (eq module (sort-module as)))
734		behavioural)
735		(with-output-chaos-warning ()
736		(format t "behavioural operator \"~{~a~}\" has imported hidden sort " op-name)
737		(print-sort-name as)
738		(princ " in its arity.")
739		))
740		--------------------------------------------------- \|\|#
741		))
742		#\|\| NULL argument is acceptable...2012/6/28
743		(when (and behavioural (not hidden?))
744		(with-output-chaos-error ('invalid-op-decl)
745		(format t "behavioural operator must have exactly one hidden sort in its arity")
746		))
747		\|\|#
	667	(setf hidden? t)))
748	668	(when (and behavioural coherent)
749	669	(with-output-chaos-error ('invalid-op-decl)
750	670	(format t "coherency is meaningless for behavioural operator.")
751	671	))
752	672	(when (and coherent (not (some #'(lambda (x) (sort-is-hidden x)) arity)))
753	673	(with-output-chaos-error ('invalid-op-decl)
754		(format t "coherency is only meaningfull for operator with hidden sort in its arity.")
755		))
756		)
757
	674	(format t "coherency is only meaningfull for operator with hidden sort in its arity."))))
758	675	;;
759	676	(when builtin-overloading-check
760	677	(when (check-overloading-with-builtin op-name arity coarity module)
761	678	(return-from add-operator-declaration-to-module nil)))
762		;;
763
	679
764	680	;; uses pre-existing operator if it is the apropreate one,
765	681	;; i.e.,
766	682	;; (1) has method with coarity which is in the same connected component.

778	694	xcoarity
779	695	(module-sort-order mod)))
780	696
781		(when chaos-verbose ;; on-operator-debug
	697	(when chaos-verbose
782	698	(with-output-simple-msg ()
783	699	(format t "~&declaring overloading operator ~a : "
784	700	(operator-name (opinfo-operator x)))

800	716	(push opinfo (module-all-operators mod))
801	717	(symbol-table-add (module-symbol-table mod) op-name op)
802	718	(when on-operator-debug
803		(format t "~&opdecl: created new operator ~a" (operator-name op)))
804
805		)
	719	(format t "~&opdecl: created new operator ~a" (operator-name op))))
806	720	;;
807	721	(multiple-value-bind (ent? meth)
808	722	(add-operator-declaration-to-table opinfo

857	771	(unless opinfo (return-from declare-operator-precedence-in-module nil))
858	772	(declare-operator-precedence (opinfo-operator opinfo) prec)))
859	773
860		#\|\|
861		(defun declare-operator-theory-in-module (op-name number-of-args
862		theory
863		&optional
864		(module
865		current-module))
866		(declare (type t op-name)
867		(type fixnum number-of-args)
868		(type op-theory theory)
869		(type module module)
870		(values t))
871		(let ((opinfo (find-operator-or-warn op-name number-of-args module)))
872		(unless opinfo (return-from declare-operator-theory-in-module nil))
873		(declare-operator-theory (opinfo-operator opinfo) theory)))
874		\|\|#
875
876	774	(defun declare-operator-associativity-in-module (op-name number-of-args
877	775	assoc
878	776	&optional

954	852	(declare (type list list-of-method)
955	853	(type fixnum arg-pos num-args)
956	854	(type hash-table so))
957		;;
958		;;(debug-msg ("~%===================================================="))
959		;;(debug-msg ("~%arg-pos = ~d") arg-pos)
960		;;(debug-msg ("~%mathods = ~s") list-of-method)
961		;;;
962	855	(if (= 0 num-args)
963	856	;; we assume the signature is regular, thus, constants has only one
964	857	;; declaration and it has no declaration for erro sort.

994	887	(push m res))))))
995	888	(let ((minimal-methods (get-minimal-methods)))
996	889	(declare (type list minimal-methods))
997		;;(debug-msg ("~%minimal-methods: ~s") minimal-methods)
998	890	(let* ((num-entry (length minimal-methods))
999	891	(result (make-list num-entry)))
1000	892	(declare (type fixnum num-entry)

1004	896	(let* ((s-ms (nth x minimal-methods))
1005	897	(comparable-methods (find-comparable (car s-ms))))
1006	898	(declare (type list s-ms comparable-methods))
1007		;;(debug-msg ("~%comparable-methods: ~s") comparable-methods)
1008	899	(setf (nth x result)
1009	900	(cons (cons (car s-ms)
1010	901	(if (= arg-pos (1- num-args))

1020	911	num-args
1021	912	so)
1022	913	nil)))))
1023		result)))
1024		)))
	914	result))))))
1025	915
1026	916
1027	917	;;; FIND-OPERATOR-METHOD operator arg-sort-list & optional opinfo-table sort-order

1056	946	(when method (return-from find method))
1057	947	))))
1058	948	;; constant. only one method.
1059		method-table
1060		))
	949	method-table))
1061	950
1062	951	;;; *****************
1063	952	;;; ADDING NEW METHOD___________________________________________________________

1073	962	arity
1074	963	coarity
1075	964	&optional
1076		(module
1077		(or current-module last-module))
	965	(module (get-context-module))
1078	966	constructor
1079	967	behavioural
1080	968	coherent
1081	969	error-operator)
1082	970	(declare (type list opinfo arity)
1083	971	(type sort-struct coarity)
1084		(type module module)
1085		(type (or null t)
1086		constructor
1087		behavioural
1088		coherent
1089		error-operator)
1090		(values (or null t) method))
	972	(type (or null module) module))
1091	973	;;
1092	974	(let ((meth nil))
1093	975	(dolist (m (opinfo-methods opinfo))

1099	981	(not (eq (method-name meth )
1100	982	(method-name beh-equal)))
1101	983	(not (method-is-error-method meth)))
1102		;; (and meth on-operator-debug)
1103	984	(with-output-chaos-warning ()
1104	985	(format t "the operator of the same rank has already been declared: ")
1105	986	(print-next)
1106	987	(print-chaos-object meth)
1107	988	(print-next)
1108		(format t "~%... ignored.")
1109		;; (print-next)
1110		;; (format t "ignoring this one.")
1111		)
1112		#\|\|
1113		(return-from add-operator-declaration-to-table
1114		(values nil meth))
1115		\|\|#
1116		)
	989	(format t "~%... ignored.")))
1117	990	(let ((operator (opinfo-operator opinfo)))
1118	991	(declare (type operator operator))
1119	992	(when (and meth (not (eq (method-module meth) module)))
	993	;; the method is the imported one
1120	994	(when (and (not (method-constructor meth))
1121	995	constructor)
1122	996	(with-output-chaos-warning ()

1147	1021	(print-simple-mod-name (method-module meth))
1148	1022	(print-next)
1149	1023	(princ "but being declared as coherent in ")
1150		(print-simple-mod-name module)
1151		#\|\|
1152		(print-next)
1153		(princ "ignoring this `coherent' attribute.")
1154		\|\|#
1155		)))
	1024	(print-simple-mod-name module))))
1156	1025	(unless meth
1157	1026	(setq meth (make-operator-method :name (operator-name operator)
1158	1027	:arity arity
1159		:coarity coarity
1160		)))
	1028	:coarity coarity)))
1161	1029	(when (eq (method-module meth) module)
1162	1030	(setf (method-constructor meth) constructor)
1163	1031	(setf (method-is-behavioural meth) behavioural)
1164		;; (setf (method-is-coherent meth) coherent)
1165	1032	(setf (method-is-user-defined-error-method meth)
1166	1033	error-operator))
1167	1034	;;

1244	1111	(pushnew method (module-beh-attributes module) :test #'eq))
1245	1112	(if (sort-is-hidden (method-coarity method))
1246	1113	(pushnew method (module-non-beh-methods module) :test #'eq)
1247		(pushnew method (module-non-beh-attributes module) :test #'eq))
1248		))
1249		(pushnew method (opinfo-methods opinfo) :test #'eq)
1250		))
	1114	(pushnew method (module-non-beh-attributes module) :test #'eq))))
	1115	(pushnew method (opinfo-methods opinfo) :test #'eq)))
1251	1116
1252	1117	(defun add-method-to-table-very-fast (opinfo method module)
1253	1118	(declare (type list opinfo)

1264	1129	(if (sort-is-hidden (method-coarity method))
1265	1130	(push method (module-non-beh-methods module))
1266	1131	(push method (module-non-beh-attributes module)))))
1267		(push method (opinfo-methods opinfo))
1268		)
	1132	(push method (opinfo-methods opinfo)))
1269	1133
1270	1134	;;;
1271	1135	;;; RECREATE-METHOD

1348	1212	;;
1349	1213	(progn
1350	1214	(setf (method-theory newmeth) theory)
1351		(compute-method-theory-info-for-matching newmeth)
1352		))
	1215	(compute-method-theory-info-for-matching newmeth)))
1353	1216	;;
1354	1217	newmeth))))
1355	1218

1378	1241	(coar2 (method-coarity meth2)))
1379	1242	(or (sort< coar2 coar1 so)
1380	1243	(and (sort= coar1 coar2)
1381		(sort-list<= (method-arity meth2) (method-arity meth1) so)))
1382		))
	1244	(sort-list<= (method-arity meth2) (method-arity meth1) so)))))
1383	1245
1384	1246	;;;
1385	1247	;;; DELETE-ERROR-OPERATORS-IN
1386	1248	;;;
1387		(defun delete-error-operators-in (&optional (module (or current-module
1388		last-module)))
	1249	(defun delete-error-operators-in (&optional (module (get-context-module)))
1389	1250	(declare (type module module)
1390	1251	(values t))
1391	1252	(let ((minfo (module-opinfo-table module))

1403	1264	(delete-if #'(lambda (x)
1404	1265	(and (method-is-error-method x)
1405	1266	(not (method-is-user-defined-error-method x))))
1406		(opinfo-methods opinfo))))
1407		))
	1267	(opinfo-methods opinfo))))))
1408	1268
1409	1269	;;;
1410	1270	;;; MAKE-OPERATOR-CLUSTERS-IN
1411	1271	;;;
1412		(defun make-operator-clusters-in (&optional (module (or current-module
1413		last-module)))
	1272	(defun make-operator-clusters-in (&optional (module (get-context-module)))
1414	1273	(declare (type module module)
1415	1274	(values t))
1416	1275	(let ((result nil)

1471	1330	(let ((print-indent (+ 2 print-indent)))
1472	1331	(fresh-line)
1473	1332	(princ "-- the result : ")
1474		(print-chaos-object pre)))
1475		)
	1333	(print-chaos-object pre))))
1476	1334	(push info result))))))
1477	1335	;;
1478	1336	(setf (module-all-operators module)

1506	1364	;;;
1507	1365	(defun method-most-general-no-error (method methods
1508	1366	&optional
1509		(module (or current-module
1510		last-module)))
	1367	(module (get-context-module)))
1511	1368	(declare (type method method)
1512	1369	(type list methods)
1513	1370	(type module module)

1522	1379	;;;
1523	1380	;;; SETUP-ERROR-OPERATORS-IN
1524	1381	;;; NOTE assumption : no error operators are generated in the module yet.
1525		;;;
	1382	;;; TODO--------
1526	1383	(defun get-new-error-sort-name-in (module sort-name)
1527	1384	(declare (type module module)
1528	1385	(type (or simple-string symbol) sort-name))

1541	1398	:test #'equal))
1542	1399	(eval-ast decl)))
1543	1400
1544		(defun setup-error-operators-in (&optional (module (or current-module
1545		last-module)))
	1401	(defun setup-error-operators-in (&optional (module (or (get-context-module))))
1546	1402	(declare (type module module)
1547	1403	(values t))
1548	1404	(let ((all-error-operators nil))

1555	1411	(format t "~%[setup-error-operators-in]:BEFORE")
1556	1412	(format t "~& arity=~s" proto-arity)
1557	1413	(format t "~& coarity=~s" proto-coarity))
1558		#\|\|
1559		(setq proto-arity
1560		(mapcar #'(lambda (sref)
1561		(if (%is-sort-ref sref)
1562		(let ((name (%sort-ref-name sref)))
1563		(setf (%sort-ref-name sref)
1564		(get-new-error-sort-name-in module name)))
1565		(get-new-error-sort-name-in module sref)))
1566		proto-arity))
1567		(if (%is-sort-ref proto-coarity)
1568		(setf (%sort-ref-name proto-coarity)
1569		(get-new-error-sort-name-in module
1570		(%sort-ref-name proto-coarity)))
1571		(setq proto-coarity
1572		(get-new-error-sort-name-in module proto-coarity)))
1573		(setf (%op-decl-arity eop-decl) proto-arity)
1574		(setf (%op-decl-coarity eop-decl) proto-coarity)
1575		\|\|#
1576	1414	(when on-operator-debug
1577	1415	(format t "~%[setup-error-operators-in]: declaring user defind errr op")
1578	1416	(format t "~% by decl : ") (print-chaos-object eop-decl))

1600	1438	(print-chaos-object (car opinfo)))
1601	1439
1602	1440	;; avoid generate if there already ...
1603
1604		;;#\|\|
1605	1441	(when (some #'(lambda (x)
1606	1442	(method-is-error-method x))
1607	1443	(opinfo-methods opinfo))
1608	1444	(when on-operator-debug
1609	1445	(format t "~% * already exists"))
1610	1446	(return-from setup-error-operator nil))
1611		;;\|\|#
1612	1447	;;
1613	1448	(let ((method-info-table (module-opinfo-table module))
1614	1449	(sort-order (module-sort-order module))
1615	1450	(pre-errs (module-error-methods module))
1616		(all-errs nil)
1617		)
	1451	(all-errs nil))
1618	1452	;; NOTE:
1619	1453	;; all coarities of methods are in the same connected component.
1620	1454	(let ((proto-method nil)
1621	1455	(method-name nil)
1622	1456	(err-coarity nil)
1623	1457	(new-arities nil)
1624		(coherent nil)
1625		)
	1458	(coherent nil))
1626	1459	;;
1627	1460	(setq proto-method
1628	1461	(find-if #'(lambda (x) (method-is-universal* x))

1668	1501	(method-arity meth))))
1669	1502	(pushnew ar new-arities :test #'equal))
1670	1503	(setq coherent
1671		(or coherent (method-is-coherent meth)))
1672		)))
	1504	(or coherent (method-is-coherent meth))))))
1673	1505	(dolist (arity new-arities)
1674	1506	(when on-operator-debug
1675	1507	(format t "~% * try for arity ")

1719	1551	(compute-method-theory-info-for-matching
1720	1552	pre
1721	1553	method-info-table)
1722		(setf (method-is-coherent pre) coherent)
1723		)
	1554	(setf (method-is-coherent pre) coherent))
1724	1555	;; not yet have, generate a new one.
1725	1556	(multiple-value-bind (ent? meth)
1726	1557	(add-operator-declaration-to-table opinfo

1735	1566	(print-chaos-object meth)
1736	1567	(format t "~% -- entered? ~a" ent?))
1737	1568	(when ent?
1738		;;
1739	1569	(push meth all-errs)
1740	1570	(setf (method-theory meth method-info-table)
1741	1571	the-empty-theory

1743	1573	(method-is-behavioural proto-method))
1744	1574	(setf (method-is-coherent meth) coherent)
1745	1575	(compute-method-theory-info-for-matching
1746		meth method-info-table)
1747		)))
1748		))
	1576	meth method-info-table))))))
1749	1577	;; returns the list of error operators.
1750	1578	all-errs)))
1751	1579

1776	1604	(setf (method-theory new-meth)
1777	1605	(method-theory meth))
1778	1606	(setf (method-theory-info-for-matching new-meth)
1779		(method-theory-info-for-matching meth))
1780		)))
	1607	(method-theory-info-for-matching meth)))))
1781	1608
1782	1609	(defun make-if-then-else-op (module sort)
1783	1610	(declare (type module module)

1804	1631	(setf (method-theory new-meth)
1805	1632	(method-theory bool-if))
1806	1633	(setf (method-theory-info-for-matching new-meth)
1807		(method-theory-info-for-matching bool-if))
1808		)))
	1634	(method-theory-info-for-matching bool-if)))))
1809	1635
1810	1636	(defun setup-if-then-else-in (module)
1811	1637	(declare (type module module)

1815	1641	(dolist (es sorts)
1816	1642	(make-if-then-else-op module es)))))
1817	1643
1818		#\|\|
1819		(defun setup-sem-relations-in (module)
1820		(when (assq truth-module (module-all-submodules module))
1821		(let ((sorts (get-module-top-sorts module)))
1822		(dolist (es sorts)
1823		(if (sort-is-hidden es)
1824		(progn
1825		;; _=*=_
1826		(make-sem-relation-op module
1827		beh-equal
1828		(list es es)
1829		bool-sort)
1830		;; _=b=_
1831		(make-sem-relation-op module
1832		beh-eq-pred
1833		(list es es)
1834		bool-sort))
1835		(progn
1836		;; _==_
1837		(make-sem-relation-op module
1838		bool-equal
1839		(list es es)
1840		bool-sort)
1841		;; _=/=_
1842		(make-sem-relation-op module
1843		bool-nonequal
1844		(list es es)
1845		bool-sort)
1846		))
1847		)))
1848		(when (assq rwl-module (module-all-submodules module))
1849		;; _==>_
1850		(let ((sorts (get-module-top-sorts module)))
1851		(dolist (s sorts)
1852		(make-sem-relation-op module
1853		rwl-predicate
1854		(list s s)
1855		bool-sort))))
1856		)
1857
1858		\|\|#
1859
1860	1644	(defun setup-sem-relations-in (module)
1861	1645	(declare (type module module)
1862	1646	(values t))

1868	1652	(make-sem-relation-op module
1869	1653	beh-equal
1870	1654	(list es es)
1871		bool-sort)
1872		)))))
	1655	bool-sort))))))
1873	1656
1874	1657	(defparameter memb-predicate-name-template
1875	1658	'("_" ":" 'sort-name))

1942	1725	(unless (operator-associativity op)
1943	1726	(if (operator-is-associative op)
1944	1727	(setf (operator-associativity op)
1945		:right)))
1946		)
	1728	:right))))
1947	1729	;; set (1) lowers and highers,
1948	1730	;; (2) memo property
1949	1731	;; (3) match theory.

1960	1742	(setf (method-overloaded-methods m)
1961	1743	(compute-overloaded-methods m methods))
1962	1744	(when (eq (method-module m) current-module)
1963		#\|\|
1964		;; (2) memo is now obsolete
1965		(unless (method-has-memo m)
1966		(setf (method-has-memo m) memo))
1967		\|\|#
1968	1745	;; ** the rewrite strategy for default methods are always eager.
1969	1746	;; we set the value here.
1970	1747	(when (method-is-error-method m)

1989	1766	(setf (method-theory m method-info-table) theory)
1990	1767	(compute-method-theory-info-for-matching
1991	1768	m
1992		method-info-table))
1993		))
1994		))
1995		))
1996
1997		;; setup method lookup table.
1998		;; * NOT USED NOW *
1999		;; (setf (opinfo-method-table opinfo)
2000		;; (make-method-table (opinfo-methods opinfo)
2001		;; current-sort-order))
2002		;;
2003		#\|\|
2004		;; compute syntactic properties for each methods.
2005		(compute-method-syntactic-properties opinfo method-info-table)
2006		;; set syntactic properties for error methods.
2007		(compute-error-method-syntactic-properties opinfo
2008		method-info-table)
2009		\|\|#
2010		))
2011		))))
	1769	method-info-table))))))))))))))
2012	1770
2013	1771	(defun set-operator-syntactic-properties (module)
2014	1772	(with-in-module (module)

2018	1776	(compute-method-syntactic-properties opinfo method-info-table)
2019	1777	;; set syntactic properties for error methods.
2020	1778	(compute-error-method-syntactic-properties opinfo
2021		method-info-table)
2022		))))
	1779	method-info-table)))))
2023	1780
2024	1781	(defun make-standard-token-seq (op-name-token number-of-args)
2025	1782	(declare (type fixnum number-of-args)

2049	1806	(methods (opinfo-methods opinfo))
2050	1807	(op-prec (operator-computed-precedence op))
2051	1808	(op-assoc (operator-associativity op))
2052		(token-sequence (operator-token-sequence op))
2053		)
	1809	(token-sequence (operator-token-sequence op)))
2054	1810	(unless (operator-is-mixfix op)
2055	1811	;; operator has a standard application form.
2056	1812	(setf token-sequence (make-standard-token-seq token-sequence

2068	1824	;; assoc theory is interpreted as right-associative
2069	1825	(if (and (method-is-associative method
2070	1826	method-info-table)
2071		(null op-assoc)
2072		)
	1827	(null op-assoc))
2073	1828	':right
2074		op-assoc)))))
	1829	op-assoc)))))
2075	1830	(declare (type fixnum prec lower-prec)
2076	1831	(type symbol assoc-decl))
2077	1832	;;

2111	1866	gathering (cdr gathering)))
2112	1867	(t (push (cons 'token cur-item) res)))
2113	1868	(setq token-seq (cdr token-seq)))
2114		;;
2115		; (terpri)
2116		; (print-chaos-object method)
2117		; (format t " :form= ~S" form)
2118		;;
2119	1869	(setf (method-form method) form))))))
2120	1870
2121	1871	(defun compute-error-method-syntactic-properties (opinfo method-info-table)

2159	1909	(type list token-seq)
2160	1910	(type symbol assoc-decl)
2161	1911	(values list))
2162		;;
2163		; (terpri)
2164		; (print-chaos-object method)
2165		; (format t " : assoc=~S" (method-is-associative method))
2166		;;
2167	1912	(if assoc-decl
2168	1913	(if (eq assoc-decl ':left)
2169	1914	'(:left :right)
2170		'(:right :left))
	1915	'(:right :left))
2171	1916	;; if unary prefix use :left not :right
2172	1917	(if (not (operator-is-mixfix (method-operator method)))
2173	1918	(mapcar #'(lambda (x) (declare (ignore x)) '&) (method-arity method))

2182	1927	;;;
2183	1928	;;; CHECK-POLIMORHIC-OVERLODING-IN
2184	1929	;;;
2185		(defun check-polimorphic-overloading-in (&optional (module (or current-module
2186		last-module)))
	1930	(defun check-polimorphic-overloading-in (&optional (module (get-context-module)))
2187	1931	(declare (type module module)
2188	1932	(values t))
2189	1933	(with-in-module (module)

2358	2102	(return-from is-variable)))
2359	2103	;; come here if the occ-th argument is a variable,or
2360	2104	;; method is maximal. delay the evaluation.
2361		(push (1+ occ) end-strategy)
2362		))
	2105	(push (1+ occ) end-strategy)))
2363	2106	(setf (method-rewrite-strategy meth)
2364	2107	(complete-method-strategy meth
2365	2108	(append (reverse strategy)
2366	2109	(if (member 0 strategy) nil '(0))
2367		(reverse end-strategy))))
2368		))))))))
	2110	(reverse end-strategy))))))))))))
2369	2111
2370	2112	;;; NOTE assumes current-opinfo-table is properly bound.
2371	2113	;;;

2389	2131	(setf (method-rules-with-different-top mth)
2390	2132	(sort (method-rules-with-different-top mth)
2391	2133	#'method<=
2392		:key #'(lambda (x) (term-head (axiom-lhs x)))))
2393		;;
2394		))))
	2134	:key #'(lambda (x) (term-head (axiom-lhs x)))))))))
2395	2135
2396	2136	(defun propagate-attributes (module)
2397	2137	(declare (type module module)

2448	2188	(print-chaos-object (opinfo-operator opinfo))
2449	2189	(print-next)
2450	2190	(term-print id) (princ " -- VS. -- ")
2451		(term-print nid)))
2452		)))
2453		)))
	2191	(term-print nid)))))))))
2454	2192	;;
2455	2193	(when id
2456	2194	(let ((idsrt (term-sort id))

2474	2212	;;
2475	2213	(set-method-theory lower
2476	2214	newthy
2477		#\|\| set-method-theory calls this
2478		(check-method-theory-consistency
2479		lower
2480		newthy
2481		current-opinfo-table
2482		t)
2483		\|\|#
2484		current-opinfo-table
2485		t))
2486		))
2487		)) ; end unless
2488		) ; end dolist
2489		) ; end dolist
2490		)
2491		))
2492
	2215	t)))))))))))
2493	2216
2494	2217	;;; EOF

+2

-3

chaos/construct/sort.lisp less more

779	779	(defvar .test-term-sort-membership-in-progress. nil)
780	780
781	781	(defun test-term-sort-membership (term sort-id-const
782		&optional
783		(module (or current-module
784		last-module)))
	782	&optional (module (get-context-module)))
	783
785	784	(declare (type term term sort-id-const))
786	785	(unless module
787	786	(with-output-chaos-error ('no-context)

+14

-97

chaos/decafe/meval.lisp less more

73	73	modexp)))
74	74	(let ((mod nil)
75	75	(me (normalize-modexp modexp)))
76		(when (and (equal me "THE-LAST-MODULE")
77		last-module)
78		(return-from eval-modexp
79		(if reconstruct-if-need
80		(reconstruct-module-if-need last-module)
81		last-module)))
	76	;; "." -> current context module
82	77	(when (and (equal me ".")
83		current-module)
84		(return-from eval-modexp
85		current-module))
	78	(get-context-module))
	79	(return-from eval-modexp (get-context-module)))
86	80	(when (stringp me)
	81	;; simple name
87	82	(let ((pos (position #\. (the simple-string me) :from-end t)))
88	83	(if pos
89	84	(let ((name (subseq (the simple-string me) 0 (the fixnum pos)))

94	89	(if (modexp-is-error context)
95	90	(with-output-chaos-error ('no-such-module)
96	91	(format t "Could not evaluate modexpr ~a, " me)
97		(format t " no such module ~a" qual)
98		)
	92	(format t " no such module ~a" qual))
99	93	(setf mod (find-module-in-env name context))))
100	94	(setq mod (find-module-in-env me (if also-local
101		current-module
	95	(get-context-module)
102	96	nil))))))
103	97	(if mod
104	98	(if reconstruct-if-need

111	105	(declare (special on-autoload))
112	106	(!input-file (cdr ent)))
113	107	(setq mod (find-module-in-env me (if also-local
114		current-module
	108	(get-context-module)
115	109	nil)))
116	110	(if mod
117	111	mod

161	155
162	156	;; Internal Error!
163	157	(t (with-output-chaos-error ('invalid-modexp)
164		(format t "bad modexp form ~s" modexp)))
165		))
	158	(format t "bad modexp form ~s" modexp)))))
166	159
167	160	;;; ************************
168	161	;;; SPECIFIC MODULE CREATORS____________________________________________________

177	170	(declaim (special copy-variables))
178	171	(defvar copy-variables nil)
179	172
180		#\|\|
181		(defun create-renamed-module (mod name)
182		(let ((beh-proof-in-progress t)
183		(copy-variables t))
184		(let ((newmod (eval-ast (%module-decl* (normalize-modexp name)
185		(module-kind mod)
186		:user
187		(list (%import* :using mod))))))
188		(add-modexp-defn (module-name newmod) newmod)
189		(compile-module newmod)
190		newmod)
191		))
192		\|\|#
193	173	(defun create-renamed-module (mod name)
194	174	(let ((beh-proof-in-progress t)
195	175	(copy-variables t)

201	181	(import-module newmod :using mod)
202	182	(add-modexp-defn (module-name newmod) newmod)
203	183	(compile-module newmod)
204		newmod)
205		))
	184	newmod)))
206	185
207	186	(defun create-renamed-module-2 (mod name context-module)
208	187	(let ((copy-variables t)

214	193	(incorporate-module-copying newmod mod t nil context-module)
215	194	(add-modexp-defn (module-name newmod) newmod)
216	195	(compile-module newmod)
217		newmod)
218		))
	196	newmod)))
219	197
220	198	;;; ***********
221	199	;;; CREATE-PLUS : Modexp -> Module

264	242	;;; ********************
265	243	;;; NOTE apply-modmorph must use memo tables since mapping may affect
266	244	;;; sub-modules (e.g. with "protecting A[X <= Y]")
267		;;;
268		;;;
269		#\|\|
	245
270	246	(defun create-instantiation (modexp)
271	247	(flet ((report-error (&rest ignore)
272	248	(declare (ignore ignore))

288	264	(with-output-chaos-error ('modexp-err)
289	265	(princ "Unknown parameterized module in instantiation: ")
290	266	(when (modexp-is-error modpar)
291		(princ (cdr modpar))
292		))
293		)
294		#\|\|
295		(when (eq current-module modpar)
296		(with-output-chaos-error ('modexp-eval)
297		(princ "module ")
298		(print-mod-name current-module)
299		(princ "cannot instantiate itself")
300		))
301		\|\|#
	267	(princ (cdr modpar)))))
302	268	(unless (get-module-parameters modpar)
303	269	(with-output-chaos-error ('modexp-eval)
304	270	(princ "module ")
305	271	(print-mod-name modpar)
306		(princ " has no parameters.")
307		))
308		;;
309		(let ((args (do ((r (%instantiation-args modexp) (cdr r))
310		(res nil))
311		((null r) (nreverse res))
312		(push (eval-view-arg (car r)
313		modpar)
314		res))))
315		(let ((name (make-int-instantiation :module modpar
316		:args args))
317		(mappg (views-to-modmorph modpar args)))
318		(let ((module (apply-modmorph name mappg modpar)))
319		;; (setf (module-name module) name) ; name is set by apply-modmorph.
320		(setf (module-decl-form module) modexp)
321		module)))))))))
322		\|\|#
323
324		(defun create-instantiation (modexp)
325		(flet ((report-error (&rest ignore)
326		(declare (ignore ignore))
327		(with-output-msg ()
328		(princ "could not evaluate instantiation: ")
329		(print-modexp modexp standard-output t t)
330		(chaos-error 'modexp-error))))
331		(with-chaos-error (#'report-error)
332		(cond ((int-instantiation-p modexp) ; evaluated internal modexp.
333		(let ((mappg (views-to-modmorph (int-instantiation-module modexp)
334		(int-instantiation-args modexp))))
335		(apply-modmorph modexp mappg (int-instantiation-module modexp))))
336		(t ; not yet evaluated, build from the
337		; scratch.
338		(let* ((auto-context-change nil)
339		;; parameter module must be a global
340		(modpar (eval-modexp (%instantiation-module modexp))))
341		(unless (module-p modpar)
342		(with-output-chaos-error ('modexp-err)
343		(princ "Unknown parameterized module in instantiation: ")
344		(when (modexp-is-error modpar)
345		(princ (cdr modpar))
346		))
347		)
348		(unless (get-module-parameters modpar)
349		(with-output-chaos-error ('modexp-eval)
350		(princ "module ")
351		(print-mod-name modpar)
352		(princ " has no parameters.")
353		))
	272	(princ " has no parameters.")))
354	273	;;
355	274	(let ((args nil)
356	275	(mappg nil))

411	330	type
412	331	(if (eq type :visible)
413	332	"sort"
414		"hsort")
415		)
416		))
	333	"hsort"))))
417	334	sort))
418	335
419	336	(defun create-rename (modexp)

+2

-4

chaos/decafe/mimport-new.lisp less more

1056	1056	(defparameter import-rwl-ast
1057	1057	(%import* :protecting (%modexp* "RWL")))
1058	1058
1059		(defun include-rwl (&optional (module (or current-module last-module)))
	1059	(defun include-rwl (&optional (module (get-context-module)))
1060	1060	(when include-rwl
1061	1061	(unless (module-includes-rwl module)
1062	1062	(with-in-module (module)
1063		(eval-import-modexp import-rwl-ast)
1064		)))
1065		)
	1063	(eval-import-modexp import-rwl-ast)))))
1066	1064
1067	1065	;;;
1068	1066	;;; IMPORT-VARIABLES

+19

-170

chaos/decafe/mimport.lisp less more

134	134	(return-from import-module-internal nil))
135	135	(when (eq module submodule)
136	136	(with-output-chaos-error ('invalid-import)
137		(princ "module cannot import itself!")
138		))
	137	(princ "module cannot import itself!")))
139	138
140	139	;; compile submodule if need
141	140	(compile-module submodule)

150	149	(nm (cdr al)))
151	150	(add-module-alias module mod nm)))
152	151	;;
153		#\|\|
154		(when (and include-bool
155		(assq bool-module
156		(module-all-submodules submodule)))
157		(include-bool module))
158		\|\|#
159		;;
160	152	(with-in-module (module)
161		;;
162		;;
163	153	(if parameter
164	154	;; PARAMETERIZED MODULE IMPORTATION.
165	155	;; We carete a new module with name `(formal-name "::" module-object)'

207	197	(progn
208	198	(when on-import-debug
209	199	(format t "~&module is already imported, skipping.."))
210		(return-from import-module-internal t)
211		))
212		))
	200	(return-from import-module-internal t)))))
213	201	(when check-import-mode
214	202	;; other more complex importation check.
215	203	;; checks confliction among shared submodules.

277	265	(add-imported-module newmod (cdr par)(cdar par))
278	266	(incorporate-module newmod (cdr par) (cdar par)))
279	267	(unless chaos-quiet (princ ")" error-output))
280		newmod)))
281		))))
	268	newmod)))))))
282	269
283	270	;;; INCORPORATE-MODULE : Module Mode SubModule -> Module'
284	271	;;; Do the importation.

334	321	:test #'eq))
335	322	(let ((opinfos (module-all-operators submodule)))
336	323	(dolist (opinfo opinfos)
337		(transfer-operator module submodule opinfo nil theory-mod))
338		)
339		;; #\|\|
	324	(transfer-operator module submodule opinfo nil theory-mod)))
340	325	;; import error operators which might be reused.
341	326	;; (dolist (em (module-error-methods submodule))
342	327	;; (when (method-is-user-defined-error-method em)
343	328	;; (pushnew em (module-error-methods module) :test #'eq)))
344	329	(dolist (em (module-error-methods submodule))
345	330	(pushnew em (module-error-methods module) :test #'eq))
346		;; \|\|#
347		;; user defined error ops -----
348		#\|\|
349		(when (module-error-op-decl submodule)
350		(format t "~&** importing error operator decl.")
351		(setf (module-error-op-decl module)
352		(nconc (module-error-op-decl module)
353		(copy-tree (module-error-op-decl submodule)))))
354		\|\|#
355		#\|\|
356		(dolist (edecl (module-error-op-decl submodule))
357		(eval-ast edecl))
358		\|\|#
359	331	;; import macros
360	332	(dolist (macro (module-macros submodule))
361	333	(add-macro-to-module module macro))

389	361	(using-find-sort (_sort)
390	362	(or (cdr (assq _sort import-sort-map)) _sort))
391	363
392		;; for debug
393		#\|\|
394		(!using-find-sort (_sort)
395		(or (cdr (assq _sort import-sort-map))
396		(progn (break) _sort)))
397		\|\|#
398	364	(using-import-var (var)
399	365	(let ((nm (variable-name var))
400	366	(sort (using-find-sort (variable-sort var))))

408	374	(setq val (make-variable-term sort nm))
409	375	(when copy-variables
410	376	(push (cons nm val) (module-variables module)))
411		(push (cons nm val) import-local-vars)
412		)))))
	377	(push (cons nm val) import-local-vars))))))
413	378	;;
414	379	(using-find-sort-err (s)
415	380	(let ((sort (cdr (assq s import-sort-map))))

517	482	mode
518	483	s
519	484	nil
520		(or theory-module submodule)))
521		))))
	485	(or theory-module submodule)))))))
522	486	(using-import-subs (smod)
523	487	(dolist (s (reverse (module-direct-submodules smod)))
524	488	(using-import-sub (car s) (cdr s))))

632	596	;;
633	597	;; import error operator declarations
634	598	;;
635		#\|\|
636		(when (module-error-op-decl submodule)
637		(setf (module-error-op-decl module)
638		(nconc (module-error-op-decl module)
639		(copy-tree (module-error-op-decl submodule)))))
640		\|\|#
641	599	(dolist (eop (module-error-op-decl submodule))
642	600	(when on-import-debug
643	601	(with-output-msg ()

648	606
649	607	;;
650	608	;; import variable declarations of error sorts
651		;;
652		#\|\|
653		(when (module-error-var-decl submodule)
654		(setf (module-error-var-decl module)
655		(nconc (module-error-var-decl module)
656		(copy-tree (module-error-var-decl submodule)))))
657		\|\|#
	609	;; nothing todo ... NO TODO
	610
658	611	;;
659	612	;; copy macros
660	613	;;

666	619	;; (print macro)
667	620	(add-macro-to-module module new-macro)))
668	621
669		;;(eval-psort-declaration (module-psort-declaration submodule)
670		;; module)
671	622	;;
672	623	;; import equations & rules copying
673	624	;;

718	669	(to-opinfo (module-opinfo-table module))
719	670	(so (module-sort-order module)))
720	671	;; find the method group to be inserted
721		#\|\|
722		(dolist (method (opinfo-methods opinfo))
723		(when (or (method-is-user-defined-error-method method)
724		(and (not (method-is-error-method method))
725		(not (method-is-for-regularity? method from-module))))
726		(setq new-opinfo
727		(dolist (x opinfos nil)
728		(when (or (null (method-arity method))
729		(is-in-same-connected-component*
730		(method-coarity method)
731		(method-coarity (or (cadr (opinfo-methods x))
732		(car (opinfo-methods x))))
733		so))
734		(return x))))
735		(return nil)))
736		\|\|#
737	672	(dolist (method (opinfo-methods opinfo))
738	673	(when (and (not (method-is-error-method method))
739	674	(not (method-is-for-regularity? method from-module)))

749	684	(return nil)))
750	685	;; create new operaotr info if could not find.
751	686	(cond (new-opinfo
752		(setq new-op (opinfo-operator new-opinfo))
753		)
	687	(setq new-op (opinfo-operator new-opinfo)))
754	688	(t
755	689	(when on-import-debug
756	690	(format t "~%* creating new opinfo for operator ~s : "

773	707	(when on-import-debug
774	708	(format t "~&-- importing method ~s : " method)
775	709	(print-chaos-object method))
776		;;
777		#\|\|
778		(when (modexp-add-method-to-table new-opinfo method module)
779		(when on-import-debug
780		(format t "~&-- importing method-theory ~s:"
781		(method-theory method from-opinfo))
782		(finish-output error-output)))
783		\|\|#
784	710	(modexp-add-method-to-table new-opinfo method module)
785	711	(transfer-operator-attributes method module from-module theory-mod)
786	712	;; import axioms

797	723	(print-chaos-object method)))
798	724	(add-rule-to-method (check-axiom-error-method module rule)
799	725	method to-opinfo)
800		(pushnew rule (module-all-rules module) :test #'rule-is-similar?)
801		)
802		)
	726	(pushnew rule (module-all-rules module) :test #'rule-is-similar?)))
803	727	;;
804	728	(dolist (r (reverse (method-rules-with-different-top method
805	729	from-opinfo)))

815	739	method to-opinfo)
816	740	(pushnew r (module-all-rules module) :test #'rule-is-similar?)))
817	741	)))
818
819		;;
820		#\|\|
821		(dolist (method (reverse (opinfo-methods opinfo)))
822		(when (and ;; (not (method-is-error-method method))
823		(not (method-is-for-regularity? method from-module)))
824		(when on-import-debug
825		(format t "~&-- importing method ~s : " method)
826		(print-chaos-object method))
827		;;
828		;;#\|\|
829		(when (modexp-add-method-to-table new-opinfo method module)
830		(when on-import-debug
831		(format t "~&-- importing method-theory ~s:"
832		(method-theory method from-opinfo))
833		(finish-output error-output)))
834		;; \|\|#
835		(modexp-add-method-to-table new-opinfo method module)
836		(transfer-operator-attributes method module from-module theory-mod)
837		;; import axioms
838		(let ((all-rules (module-all-rules module)))
839		(dolist (rule (rule-ring-to-list
840		(method-rules-with-same-top method from-opinfo)))
841		(when (or (not (memq rule all-rules))
842		(eq method (term-head (axiom-lhs rule))))
843		(when on-import-debug
844		(with-in-module (from-module)
845		(format t "~%-- importing axiom ")
846		(print-chaos-object rule)
847		(format t "~% for method : ")
848		(print-chaos-object method)))
849		(add-rule-to-method (check-axiom-error-method module rule)
850		method to-opinfo)
851		(pushnew rule (module-all-rules module) :test #'rule-is-similar?)
852		)
853		)
854		;;
855		(dolist (r (reverse (method-rules-with-different-top method
856		from-opinfo)))
857		(when (or (not (memq r all-rules))
858		(eq method (term-head (axiom-lhs r))))
859		(when on-import-debug
860		(with-in-module (from-module)
861		(format t "~%-- importing axiom ")
862		(print-chaos-object r)
863		(format t "~% for method : ")
864		(print-chaos-object method)))
865		(add-rule-to-method (check-axiom-error-method module r)
866		method to-opinfo)
867		(pushnew r (module-all-rules module) :test #'rule-is-similar?)))
868		)))
869		\|\|#
870		;;
871	742	(when on-import-debug
872		(format t "~&* done transfer-operator"))
873		))
874		))
	743	(format t "~&* done transfer-operator"))))))
875	744
876	745	(defun modexp-add-method-to-table (opinfo method module)
877	746	(let ((pmeth (find method (opinfo-methods opinfo)

881	750	(sort= (method-coarity x)
882	751	(method-coarity y))))))
883	752	(method-info-table (module-opinfo-table module)))
884		(if (eq pmeth method) ; (or (eq pmeth method)
885		; ;; dirty kludge!
886		; (and pmeth (method-is-of-same-operator-safe method rwl-predicate)))
	753	(if (eq pmeth method)
887	754	nil
888	755	(progn
889	756	(setf (get-method-info method method-info-table)

915	782	(setf (method-theory method (module-opinfo-table to-module))
916	783	new-theory)
917	784	(compute-method-theory-info-for-matching method
918		(module-opinfo-table to-module))
919		)))
	785	(module-opinfo-table to-module)))))
920	786
921	787	(defun modexp-merge-operator-theory (method to-module from-module
922	788	&optional theory-mod)

937	803	(setq meta-demod (method-is-meta-demod meth)))
938	804	(with-in-module (to-module)
939	805	(setf (method-is-coherent meth) coh)
940		(setf (method-is-meta-demod meth) meta-demod))
941		))
	806	(setf (method-is-meta-demod meth) meta-demod))))
942	807
943	808	;;; *****************************************
944	809	;;; AUTOMATIC IMPORATION OF BUILT-IN MODULES.___________________________________

955	820	(unless (memq syntax-err-sort (module-all-sorts module))
956	821	(with-in-module (module)
957	822	(eval-import-modexp import-hard-wired-ast))))
958
959		#\|\|
960		(defun include-BOOL (&optional (module current-module))
961		(when include-BOOL
962		(unless (memq Bool-sort
963		(module-all-sorts module))
964		(with-in-module (module)
965		(eval-import-modexp import-bool-ast))))
966		(include-chaos-module)
967		)
968		\|\|#
969	823
970	824	(defun include-BOOL (&optional (module current-module))
971	825	(when include-BOOL

973	827	(module-all-submodules module))
974	828	(with-in-module (module)
975	829	(eval-import-modexp import-bool-ast))))
976		(include-chaos-module)
977		)
	830	(include-chaos-module))
978	831
979	832	(defparameter import-object-ast
980	833	(%import* :extending (%modexp* "OBJECT")))

982	835	(defun include-object ()
983	836	(unless (memq class-id-sort
984	837	(module-all-sorts current-module))
985		(eval-import-modexp import-object-ast)
986		))
	838	(eval-import-modexp import-object-ast)))
987	839
988	840	(defparameter import-record-ast
989	841	(%import* :extending (%modexp* "RECORD-STRUCTURE")))

996	848	(defparameter import-rwl-ast
997	849	(%import* :protecting (%modexp* "RWL")))
998	850
999		(defun include-rwl (&optional (module (or current-module last-module)))
	851	(defun include-rwl (&optional (module (get-context-module)))
1000	852	(when include-rwl
1001	853	(unless (module-includes-rwl module)
1002	854	(with-in-module (module)
1003		(eval-import-modexp import-rwl-ast)
1004		)))
1005		)
	855	(eval-import-modexp import-rwl-ast)))))
1006	856
1007	857	;;;
1008	858	;;; IMPORT-VARIABLES

1018	868	(with-output-chaos-warning ()
1019	869	(format t "importing variable ~a, could not find sort ~a"
1020	870	name
1021		(sort-id (variable-sort v)))))))
1022		))
	871	(sort-id (variable-sort v)))))))))
1023	872
1024	873	;;; EOF

+41

-263

chaos/decafe/modmorph.lisp less more

103	103	;; some cases the real module compilation is not done
104	104	;; while evaluating modexprs, and we also want
105	105	;; psort-declaration for consistency.
106		(setf (module-principal-sort newmod) s-mapped)
107		))
108		)
	106	(setf (module-principal-sort newmod) s-mapped))))
109	107	;;
110	108	(when chaos-verbose (princ "[")) ; now we begin.
111	109	(when on-modexp-debug

199	197	(inherit-principal-sort x sortim)
200	198	(unless (eq x sortim)
201	199	(push (cons x sortim) sortmap)
202		(setf (modmorph-sort map) sortmap))
203		)
204		(inherit-principal-sort x x))
205		)))
206		)))
	200	(setf (modmorph-sort map) sortmap)))
	201	(inherit-principal-sort x x))))))))
207	202	;;
208	203	(if chaos-verbose
209	204	(print-in-progress "s") ; done mapping sorts

229	224	(with-output-msg ()
230	225	(format t " generating error sorts")))
231	226	(generate-err-sorts so)
232		(setq no-error-sort t)
233		)
	227	(setq no-error-sort t))
234	228	;;
235	229	(if chaos-verbose
236	230	(print-in-progress "<") ; done mapping sort relations

255	249	(not (memq method
256	250	(module-methods-for-regularity mod)))))
257	251	(unless (assq method opmap)
258		(modmorph-recreate-method mod newmod sortmap method))
259		)))
	252	(modmorph-recreate-method mod newmod sortmap method)))))
260	253	;;
261	254	(if chaos-verbose
262	255	(print-in-progress "o") ; done mapping operators

292	285	(print-in-progress ","))
293	286
294	287	;; THEOREMS ---------------------------------------------------------
295		#\|\| NO YET
296		(setf (module-theorems newmod)
297		(append
298		(mapcar #'(lambda (r)
299		(modmorph-recreate-axiom newmod sortmap
300		opmap modmap r))
301		(module-theorems mod))
302		(module-theorems newmod)))
303		\|\|#
	288	;; NO YET
304	289
305	290	;; OK we've done, nothing to be done here already.
306	291	;;

325	310	(modmorph-update-theory mod map opinfo))
326	311	(propagate-attributes mod)
327	312	(update-parse-information mod)
328		(mark-module-ready-for-parsing mod)
329		)
	313	(mark-module-ready-for-parsing mod))
330	314
331	315	(defun fix-operator-mapping (mod map)
332	316	(let ((opmap (modmorph-op map))

357	341	(t nil))))
358	342	opmap)))
359	343
360		#\|\|
361		(defun modmorph-find-error-method (module method opmap &optional sortmap)
362		(declare (type module module)
363		(type method method)
364		(type list opmap sortmap)
365		(values (or null method)))
366		(or (car (memq method (module-error-methods module)))
367		(let* ((alen (length (method-arity method)))
368		(opinfos (find-operators-in-module (method-symbol method)
369		alen
370		module)))
371		(declare (type fixnum alen)
372		(type list opinfos))
373		;;
374		(unless opinfos
375		(let* ((name (method-symbol method))
376		(mapped? (find-if #'(lambda (x)
377		(and (equal (method-symbol
378		(the method (car x)))
379		name)
380		(= (the fixnum
381		(length (method-arity (car x))))
382		alen)))
383		opmap)))
384		(when mapped?
385		;; (method :simple-map . method)
386		;; (mehtod :replacement pvars term)
387		(setq name (if (memq (second mapped?)
388		'(:simple-map :simple-error-map))
389		(method-symbol (the method (cddr mapped?)))
390		(method-symbol (term-head (cadddr mapped?)))))
391		(setq opinfos (find-operators-in-module name alen module)))))
392		;;
393		(let ((opinfo nil)
394		(err-method nil))
395		(let* ((ar (mapcar #'(lambda (x)
396		(declare (type sort* x))
397		(if (err-sort-p x)
398		(find-compatible-err-sort x module sortmap)
399		x))
400		(method-arity method)))
401		#\|\|
402		(ar-names (mapcar #'(lambda(x)
403		(declare (type sort* x))
404		(sort-id x))
405		ar))
406		\|\|#
407		(cr (if (err-sort-p (method-coarity method))
408		(find-compatible-err-sort (method-coarity method)
409		module
410		sortmap)
411		(method-coarity method)))
412		#\|\|
413		(cr-name (sort-id cr))
414		\|\|#
415		)
416		(declare (type sort* cr))
417		(block find-method
418		(dolist (oi opinfos)
419		(declare (type list oi))
420		(dolist (cand (opinfo-methods oi))
421		(declare (type method cand))
422		(when (and (sort-list= ar (method-arity cand))
423		(sort= cr (method-coarity cand)))
424		(setq opinfo oi)
425		(setq err-method cand)
426		(return-from find-method nil))
427		)))
428		;;
429		(unless opinfo
430		;; failed!....
431		;; this means we need error method which are not generated
432		;; yet. -- really?
433		;; (break)
434		(let ((arity (mapcar #'(lambda (x)
435		(declare (type sort* x))
436		(if (err-sort-p x)
437		(let ((compo
438		(err-sort-components x)))
439		(mapcar #'(lambda(y)
440		(modmorph-assoc-image
441		sortmap
442		y))
443		compo))
444		(list (modmorph-assoc-image
445		sortmap
446		x))))
447		ar))
448		(coarity (let ((c cr))
449		(if (err-sort-p c)
450		(let ((compo (err-sort-components c)))
451		(mapcar #'(lambda (s)
452		(modmorph-assoc-image sortmap s))
453		compo))
454		(list (modmorph-assoc-image sortmap c)))))
455		(so (module-sort-order module)))
456		(declare (type sort-order so))
457		;;
458		;; (break)
459		;;
460		(when (block
461		find-opinfo
462		(dolist (oi opinfos)
463		(declare (type list oi))
464		(let ((mm (opinfo-methods oi)))
465		(dolist (m mm)
466		(declare (type method m))
467		(block try1
468		(let ((xarity (method-arity m))
469		(xcoarity (method-coarity m)))
470		(declare (type list xarity)
471		(type sort* xcoarity))
472		(dotimes (pos (length xarity))
473		(declare (type fixnum pos))
474		(unless (some #'(lambda (y)
475		(declare (type sort* y))
476		(sort<= (the sort*
477		(nth pos xarity))
478		y
479		so))
480		(nth pos arity))
481		(return-from try1 nil)))
482		(unless (some #'(lambda (y)
483		(declare (type sort* y))
484		(sort<= xcoarity y so))
485		coarity)
486		(return-from try1 nil))
487		(setq opinfo oi)
488		(return-from find-opinfo t))
489		)))))
490		;;
491		(setup-error-operator opinfo module)
492		(setq err-method (car (opinfo-methods opinfo)))
493		)))
494		)
495		;;
496		(when on-modexp-debug
497		(format t "~%-- finding error method for : ")
498		(print-chaos-object method)
499		(format t "~% found : ")
500		(print-chaos-object err-method))
501		;;
502		err-method))))
503		\|\|#
504
505	344	(defun modmorph-find-mapped-sorts (module sort-l sortmap)
506	345	(mapcar #'(lambda (x)
507	346	(declare (type sort* x))

533	372	(method-has-memo to) memo
534	373	(method-associativity to) assoc
535	374	(method-constructor to) constr)
536		(set-method-theory to theory)
537		))
538		))
	375	(set-method-theory to theory)))))
539	376
540	377
541	378	(defun modmorph-find-user-defined-error-method (method module sortmap)

568	405	sortmap))
569	406	(cr (car (modmorph-find-mapped-sorts module
570	407	(list (method-coarity method))
571		sortmap)))
572		)
	408	sortmap))))
573	409	(declare (type sort* cr))
574	410	(block find-method
575	411	(dolist (oi opinfos)

581	417	(sort= cr (method-coarity cand)))
582	418	(setq opinfo oi)
583	419	(setq err-method cand)
584		(return-from find-method nil))
585		)))
	420	(return-from find-method nil)))))
586	421	;;
587	422	(unless opinfo
588	423	;; failed!....

641	476	coarity)
642	477	(return-from try1 nil))
643	478	(setq opinfo oi)
644		(return-from find-opinfo t))
645		)))))
	479	(return-from find-opinfo t)))))))
646	480	;;
647	481	(setup-error-operator opinfo module)
648		(setq err-method (car (opinfo-methods opinfo)))
649		)
	482	(setq err-method (car (opinfo-methods opinfo))))
650	483	(unless err-method
651	484	;; this means that the original method should be an
652	485	;; user defined error-method...

656	489	(err-sort-p x))
657	490	ar)
658	491	(err-sort-p coarity))
659		;; so bad ...
660		#\|\|
661		(with-output-panic-message ()
662		(format t "well ... could not find proper error method for ")
663		(print-chaos-object method))
664		\|\|#
665	492	(with-output-chaos-warning ()
666	493	(format t "well ... could not find proper error method for ")
667	494	(print-chaos-object method))
668		(return-from modmorph-find-proper-error-method method)
669		)
	495	(return-from modmorph-find-proper-error-method method))
670	496	;; we declare err-method
671		;; (format t "~&declaring new error method...")
672	497	(multiple-value-bind (o m)
673	498	(declare-operator-in-module
674	499	(method-symbol method)

680	505	nil
681	506	t) ; error method?
682	507	(declare (ignore o))
683		(setq err-method m))
684		) ; end case no err-method
685		)
686		) ; end case no op-info
687		)
	508	(setq err-method m))) ; end case no err-method
	509	)))
688	510	;;
689	511	(when on-modexp-debug
690	512	(format t "~%-- finding error method for : ")

744	566	; user defined one.
745	567	(modmorph-find-user-defined-error-method method
746	568	module
747		sortmap)))
748		)))
	569	sortmap))))))
749	570
750	571
751	572	(defun replace-error-method (mod term op-map sort-map)

789	610	(some #'(lambda (x)
790	611	(or (modmorph-module-is-mapped modmap (car x))
791	612	(modmorph-submodule-is-mapped modmap (car x))))
792		(module-submodules mod))
793		)
	613	(module-submodules mod)))
794	614
795	615	;;;=============================================================================
796	616	;;; MOD-MORPH-IMPORT-SUBMODULES : MODULE NEW-MODULE MAP

834	654	;;
835	655	(if (eq ':using mode)
836	656	(modmorph-import-submodules mod newmod map submodule-image)
837		#\|\|
838		(if (module-is-parameter-theory submodule-image)
839		(let* ((mod-name (module-name submodule-image))
840		(formal-name (first mod-name))
841		(real-sub (third mod-name)))
842		(import-module newmod mode real-sub formal-name))
843		(import-module newmod mode submodule-image))
844		\|\|#
845		(import-module newmod mode submodule-image)
846		)
847		))
	657	(import-module newmod mode submodule-image))))
848	658
849	659	;;;-----------------------------------------------------------------------------
850	660	;;; MODMORPH-MAP-SUBMODULE

891	701	args)))
892	702	(let ((new-name (%instantiation* smod args)))
893	703	;; * * *
894		(apply-modmorph (normalize-modexp new-name) map smod)
895		)))
	704	(apply-modmorph (normalize-modexp new-name) map smod))))
896	705	;;
897	706	(t (let ((nm (modmorph-construct-name map
898	707	;; (module-name smod)

951	760	,(parameter-module-context smod))))
952	761	(t (normalize-modexp
953	762	(%rename* s-name
954		(%rename-map (modmorph-name map)))))
955		)))
	763	(%rename-map (modmorph-name map))))))))
956	764	(t (let ((modmorph-expanded nil))
957	765	(let ((val (modmorph-reconstruct-name map
958	766	(if (module-p smod)

968	776	;;; want result in canonical form
969	777	(defun modmorph-reconstruct-name (map me)
970	778	(when on-modexp-debug
971		(format t "~%[modmorph-reconstruct-name]:")
972		#\|\|
973		(format t "~%-- given map ")
974		(print-mapping map)
975		(format t "~%-- given modexp ")
976		(print-chaos-object me)
977		\|\|#
978		)
	779	(format t "~%[modmorph-reconstruct-name]:"))
979	780	;;
980	781	(when (modexp-is-?name? me)
981	782	(when on-modexp-debug

1107	908	(setf (view-decl-form view) (view-decl-form me))
1108	909	view))
1109	910	;;
1110		(t (break "modmorph-reconstruct-name: missing case"))
1111		))
	911	(t (break "modmorph-reconstruct-name: missing case"))))
1112	912
1113	913	(defun target-of-view-arg (vw)
1114	914	(when (modexp-is-?name? vw)

1117	917	((module-p vw) vw)
1118	918	((view-p vw) (view-target vw))
1119	919	((%is-view vw) (%view-target vw))
1120		(t (break "target-of-view-arg: unknown view argument"))
1121		))
	920	(t (break "target-of-view-arg: unknown view argument"))))
1122	921
1123	922	(eval-when (:execute :compile-toplevel :load-toplevel)
1124	923	(declaim (type fixnum anon-view-name))

1167	966	(when on-modexp-debug
1168	967	(format t "~&*result view=")
1169	968	(print-chaos-object view))
1170		(%!arg* arg-name view)))
1171		))
	969	(%!arg* arg-name view)))))
1172	970
1173	971	(defun modmorph-reconstruct-view-sort-mapping (mod map s-maps)
1174	972	(declare (ignore mod))

1410	1208	(string (sort-id s1)))
1411	1209	(print-chaos-object module)
1412	1210	;; (break)
1413		(return-from modmorph-sort-image nil)))
1414		)))
1415		)))
	1211	(return-from modmorph-sort-image nil)))))))))
1416	1212
1417	1213	(defun modmorph-sorts-image (module sortmap sortlist)
1418	1214	(mapcar #'(lambda (x) (modmorph-sort-image module sortmap x))

1449	1245	op-symbol
1450	1246	arity
1451	1247	coarity
1452		sortmap))
1453		))))
	1248	sortmap))))))
1454	1249
1455	1250	(defun modmorph-recreate-method-aux-1 (oldmodule module
1456	1251	method

1458	1253	arity
1459	1254	coarity
1460	1255	sort-map)
1461		(recreate-method oldmodule method module op-symbol arity coarity sort-map)
1462		)
	1256	(recreate-method oldmodule method module op-symbol arity coarity sort-map))
1463	1257
1464	1258	(defun modmorph-recreate-method-aux-2 (oldmodule module sortmap method)
1465	1259	(declare (ignore sortmap))

1494	1288	(cdr idinf)))))
1495	1289	thy)))
1496	1290	(t thy)))
1497		(compute-method-theory-info-for-matching method minfo))
1498		) ; dolist
	1291	(compute-method-theory-info-for-matching method minfo))) ; dolist
1499	1292	)))
1500	1293
1501	1294	;;; TERMS

1536	1329	(when on-modexp-debug
1537	1330	(format t "~& variable not found in modmorph-local-vars"))
1538	1331	(push new-var modmorph-local-vars)
1539		new-var))))
1540		))
	1332	new-var))))))
1541	1333	(t (let ((head (term-head term))
1542	1334	(new-head nil))
1543	1335	;; look in the mapping

1586	1378	(method-arity head))
1587	1379	(modmorph-sort-image lookmod
1588	1380	sortmap
1589		(method-coarity head)))
1590		))))))
	1381	(method-coarity head)))))))))
1591	1382	;;
1592	1383	(unless new-head
1593	1384	(with-output-chaos-error ('no-such-operator)

1613	1404	modmap
1614	1405	tm))
1615	1406	(term-subterms term))
1616		module))
1617		)))))
	1407	module)))))))
1618	1408
1619	1409	;;; AXIOMS
1620	1410

1670	1460	(if (atom (car nm2)) (list nm2) nm2))
1671	1461	(modmorph-merge-assoc (modmorph-sort m1) (modmorph-sort m2) warn)
1672	1462	(modmorph-merge-op-assoc (modmorph-op m1) (modmorph-op m2) warn)
1673		(modmorph-merge-assoc (modmorph-module m1) (modmorph-module m2) warn))
1674		))
	1463	(modmorph-merge-assoc (modmorph-module m1) (modmorph-module m2) warn))))
1675	1464
1676	1465	(defun modmorph-merge-assoc (a1 a2 &optional warn)
1677	1466	(let ((res a2))

1696	1485	(print-chaos-object (cdr m))
1697	1486	(print-next)
1698	1487	(print-chaos-object (cdr im)))
1699		)))
1700		;; (push (cons (car m) (cdr im)) res)
1701		)
1702		(push m res))
1703		))
1704		res
1705		))
	1488	))))
	1489	(push m res))))
	1490	res))
1706	1491
1707	1492	(defun modmorph-op-map-is-ident (map)
1708	1493	(if (eq :simple-map (second map))

1742	1527	(print-chaos-object (caddr m))
1743	1528	(print-next)
1744	1529	(print-chaos-object (caddr m)))))
1745		)))
1746		;; (push (cons (car m) (cdr im)) res)
1747		)
1748		(push m res))
1749		))
1750		res
1751		))
	1530	))))
	1531	(push m res))))
	1532	res))
1752	1533
1753	1534	;; im1 & im2 are of the form
1754	1535	;;; (:simple-map . method) -- or --

1826	1607	;;;
1827	1608	(defvar .mapping-debug. nil)
1828	1609
1829		(defun mapping-image (term-list term &optional (module (or current-module
1830		last-module)))
	1610	(defun mapping-image (term-list term &optional (module (get-context-module)))
1831	1611	(when .mapping-debug.
1832	1612	(format t "~&[mapping-image] term = ")
1833	1613	(print-chaos-object term)

1846	1626	(term-head term)
1847	1627	(mapcar #'(lambda (st) (mapping-image term-list st))
1848	1628	(term-subterms term))
1849		module)
1850		)))
	1629	module))))
1851	1630
1852	1631	(defun mapping-image-2 (map term_list term)
1853	1632	(cond ((term-is-variable? term)

1886	1665	(term-subterms term))
1887	1666	(if (module-p as)
1888	1667	as
1889		om))
1890		))))
	1668	om))))))
1891	1669
1892	1670	;;;
1893	1671	(defun view-get-image-of-axioms (view)

+1

-2

chaos/decafe/modmorph2.lisp less more

1819	1819	;;;
1820	1820	(defvar .mapping-debug. nil)
1821	1821
1822		(defun mapping-image (term-list term &optional (module (or current-module
1823		last-module)))
	1822	(defun mapping-image (term-list term &optional (module (get-context-module)))
1824	1823	(when .mapping-debug.
1825	1824	(format t "~&[mapping-image] term = ")
1826	1825	(print-chaos-object term)

+3

-4

chaos/eval/chaos-top.lisp less more

137	137	(fresh-all)
138	138	(flush-all)
139	139	(format t "~&[")
140		(if last-module
141		(print-simple-mod-name last-module)
	140	(if (get-context-module)
	141	(print-simple-mod-name (get-context-module))
142	142	(princ "*"))
143		(princ "]> ")
144		))
	143	(princ "]> ")))
145	144
146	145	(defun handle-chaos-error (val)
147	146	(if chaos-input-source

+9

-192

chaos/eval/eval-ast.lisp less more

217	217	body))
218	218	current-module
219	219	hidden )))
220
221		;;;-----------------------------------------------------------------------------
222		;;; DECLARE-RECORD
223		;;;
224		(defun declare-record (record-decl)
225		(I-miss-current-module declare-record)
226		(include-BOOL)
227		(include-RECORD)
228		(let ((rsort (declare-record-in-module current-module
229		(%record-decl-name record-decl)
230		(%record-decl-supers record-decl)
231		(%record-decl-attributes
232		record-decl)
233		(%record-decl-hidden record-decl))))
234		(set-needs-parse)
235		(set-needs-rule)
236		rsort))
237
238		;;;-----------------------------------------------------------------------------
239		;;; DECLARE-CLASS
240		;;;
241		(defun declare-class (class-decl)
242		(I-miss-current-module declare-class)
243		(include-BOOL)
244		(include-OBJECT)
245		(let ((csort (declare-class-in-module current-module
246		(%class-decl-name class-decl)
247		(%class-decl-supers class-decl)
248		(%class-decl-attributes class-decl)
249		(%class-decl-hidden class-decl))))
250		(set-needs-parse)
251		(set-needs-rule)
252		csort))
253	220
254	221	;;;=============================================================================
255	222	;;; OPERATOR, OPERATOR ATTRIBUTES

375	342	(set-needs-rule)
376	343	meth)
377	344	nil))))
378
379		;;; DECLARE-OPERATOR-ATTRIBUTES : decl -> operator
380		;;; returns operator if success, otherwise nil.
381		;;;
382		#\|\|
383		(defun declare-operator-attributes (decl)
384		(I-miss-current-module declare-operator-attributes)
385		;; NOTE qualifier in opref is ignored, is it OK?
386		(let ((name (%opref-name (%opattr-decl-opref decl)))
387		(num-args (%opref-num-args (%opattr-decl-opref decl)))
388		(attr (%opattr-decl-attribute decl)))
389		(let ((opinfo (find-qual-operator-in current-module name num-args)))
390		(unless opinfo
391		(with-output-chaos-error ('operator-not-found)
392		(format t "declaring attributes, could not found unique operator ~a."
393		name)
394		))
395		(let ((op (opinfo-operator opinfo))
396		(memo (%opattrs-memo attr))
397		(theory (%opattrs-theory attr))
398		(assoc (%opattrs-assoc attr))
399		(prec (%opattrs-prec attr))
400		(strat (%opattrs-strat attr)))
401		;; (when memo (declare-operator-memo-attr op memo))
402		(when memo
403		(with-output-chaos-warning ()
404		(format t "memo attribute is now obsolate.")))
405		(when theory (declare-operator-theory op theory))
406		(when assoc (declare-operator-associativity op assoc))
407		(when prec (declare-operator-precedence op prec))
408		(when strat (declare-operator-strategy op strat))
409		(set-needs-parse)
410		(set-needs-rule)
411		;; save the declaration form.
412		(push decl (module-opattrs current-module))
413		op))))
414		\|\|#
415	345
416	346	;;;=============================================================================
417	347	;;; AXIOMS, VARIABLES

781	711	;;; DECLARE-MODULE : module-declaration-form -> module
782	712	;;;
783	713	(defun declare-module (decl)
784		;; need not current-module
785	714	(let ((mod nil) ; will bound created module.
786	715	(name (%module-decl-name decl))
787	716	(kind (%module-decl-kind decl))

828	757	;;
829	758	(propagate-module-change modval)
830	759	;;
831		(when (eq modval last-module)
832		(setq last-module nil)
	760	(when (eq modval (get-context-module))
	761	(reset-context-module)
833	762	(setq recover-same-context t))
834	763
835	764	(when (eq modval memoized-module)

844	773	$$term-context nil
845	774	$$subterm nil
846	775	$$action-stack nil
847		$$selection-stack nil))
848		)
	776	$$selection-stack nil)))
849	777
850	778	;; process declaration forms.
851	779	(setf mod (create-module name))

877	805	(let ((real-mod (find-module-in-env name nil)))
878	806	(final-setup real-mod)
879	807	(if recover-same-context
880		(setq last-module real-mod)
881		(if auto-context?
882		(change-context last-module real-mod)))
	808	(reset-context-module real-mod)
	809	(if auto-context?
	810	(change-context (get-context-module) real-mod)))
883	811	;;
884	812	(unless (module-is-parameter-theory real-mod)
885	813	(print-in-progress " done."))

938	866	(parameter (%import-parameter decl))
939	867	(alias (%import-alias decl))
940	868	(new-mod nil))
941		(when (and (%is-modexp modexp)
942		(equal (%modexp-value modexp) "THE-LAST-MODULE"))
943		(setf (%modexp-value modexp) last-module))
944		(setf new-mod (import-module current-module mode modexp parameter alias))
	869	(setf new-mod (import-module (get-context-module) mode modexp parameter alias))
945	870	new-mod))
946	871
947	872	;;; !ADD-US
948	873	;;;-----------------------------------------------------------------------------
949	874	;;; NOT YET
950
951		#\|\|
952		(defun !add-us (e)
953		;; expansion top-level-eval
954		(let ((mepars (parse-modexp (third e))))
955		(if (and (consp mepars) (eq 'with (car mepars)))
956		(!add-using-with current-module mepars)
957		(let ((val (eval-modexp mepars nil nil)))
958		(if (eq TRUTH-module val)
959		(with-output-chaos-warning ()
960		(princ "using TRUTH not allowed, replaced by extending")
961		(print-next)
962		(princ "in module ") (print-mod-name current-module)
963		(import-module current-module :extending val))
964		(if (eq current-module val)
965		(with-output-chaos-warning ()
966		(princ "module cannot use itself (ignored)."))
967		(import-module current-module :using val))))
968		)))
969		\|\|#
970
971		#\|\|
972		;;; handle using X with A and B
973		(defun !add-using-with (module mepars)
974		(let ((mod (eval-modexp (cadr mepars))))
975		(when (modexp-is-error mod)
976		(with-output-chaos-error ()
977		(princ "cannot evaluate module: ")
978		(print-modexp (cadr mepars))
979		(chaos-to-top)))
980		(let ((submods (let ((current-module mod))
981		(mapcar #'(lambda (me)
982		(let ((val (eval-modexp me)))
983		(when (modexp-is-error val)
984		(with-output-chaos-error ()
985		(princ "cannot evaluate module: ")
986		(print-modexp me)
987		(terpri)
988		(chaos-to-top)))
989		val))
990		(if (equal '(nil) (caddr mepars))
991		nil
992		(caddr mepars))))))
993		(incorporate-using-with module mod submods))))
994	875
995	876	;;; Labels in Axioms env.
996	877	;;;-----------------------------------------------------------------------------

1010	891	(princ "label ")
1011	892	(princ l)
1012	893	(princ " contains an initial digit (ignored)") (terpri))
1013		(push l res)))
1014		)
1015		(nreverse res)
1016		))
1017
1018
1019		;;;=============================================================================
1020		;;; MISC.
1021
1022		;;; AS
1023		;;;-----------------------------------------------------------------------------
1024		;;; !ADD-AS
1025		;;;
1026		(defun !add-as (e)
1027		(unless (module-is-prepare-for-parsing current-module)
1028		(prepare-for-parsing current-module))
1029		(with-in-module (current-module)
1030		(let* ((so (module-sort-order current-module))
1031		(sort (find-sort-in current-module (nth 1 e)))
1032		(tm (parser$parses current-module (nth 3 e)
1033		(if sort sort cosmos)))
1034		(cnd (parser$parses current-module (nth 5 e))))
1035		(when (null sort)
1036		(princ "Unknown sort in sort constraint"))
1037		(when (null tm)
1038		(princ "No parse for term in sort constraint") (terpri))
1039		(when (or (null cnd) (not (null (cdr cnd))))
1040		(princ "No single parse for condition in sort constraint") (terpri))
1041		(if (and tm (not (null (cdr tm))))
1042		(when tm (princ "Term in sort constraint is ambiguous") (terpri))
1043		(when (and tm (null (cdr tm)))
1044		(when (and sort tm)
1045		(unless (sort-order$is-included-in so sort (term$sort (car tm)))
1046		(princ "Specified sort and sort of term incompatible")))
1047		(when (and tm cnd (null (cdr tm)) (null (cdr cnd)))
1048		(unless (subsetp (term$vars (car cnd)) (term$vars (car tm)))
1049		(princ "Condition variables not subset of those in term") (terpri)))
1050		)))
1051		(error "** Error: general sort constraint not currently handled (ignored)")
1052		(terpri)
1053		(princ " ")
1054		(princ "as ")
1055		(simple-princ-open (nth 1 e))
1056		(princ " : ")
1057		(simple-princ-open (nth 3 e))
1058		(princ " if ")
1059		(simple-princ-open (nth 5 e))
1060		(princ " .")
1061		(terpri)
1062		))
1063
1064		;;; OP-AS
1065		(defun !add-op-as (e)
1066		;(!add-sort-constraint
1067		; (nth 7 e) (nth 5 e) (nth 9 e))
1068		(with-output-chaos-warning ()
1069		(princ "operator assertion being treated simply as a")
1070		(princ " declaration") (print-next)
1071		(princ "for operator: ") (print-simple-princ-open (nth 1 e)) (terpri))
1072		(!add-op
1073		`("op" ,(nth 1 e) ":" ,(nth 3 e) "->" ,(nth 5 e)
1074		,@(if (equal "." (nth 10 e)) nil (list (nth 10 e)))
1075		"."))
1076		)
1077
1078		\|\|#
	894	(push l res))))
	895	(nreverse res)))
1079	896
1080	897	;;; EOF

+67

-183

chaos/eval/eval-ast2.lisp less more

147	147	(number-matches nil))
148	148	(let ((mod (if modexp
149	149	(eval-modexp modexp)
150		last-module)))
151		(unless (eq mod last-module)
	150	(get-context-module))))
	151	(unless (eq mod (get-context-module))
152	152	(clear-term-memo-table term-memo-table))
153	153	(if (or (null mod) (modexp-is-error mod))
154	154	(if (null mod)
155	155	(with-output-chaos-error ('no-context)
156		(princ "no module expression provided and no selected(current) module.")
157		)
	156	(princ "no module expression provided and no selected(current) module."))
158	157	(with-output-chaos-error ('no-such-module)
159	158	(princ "incorrect module expression, no such module ")
160		(print-chaos-object modexp)
161		))
	159	(print-chaos-object modexp)))
162	160	(progn
163		(context-push-and-move last-module mod)
	161	(context-push-and-move (get-context-module) mod)
	162	(when auto-context-change
	163	(change-context (get-context-module) mod))
164	164	(with-in-module (mod)
165		(when auto-context-change
166		(change-context last-module mod))
167	165	(!setup-reduction mod)
168	166	(setq $$mod current-module)
169	167	(setq sort cosmos)

177	175	(when (or (null (term-sort term))
178	176	(sort<= (term-sort term) syntax-err-sort chaos-sort-order))
179	177	(return-from perform-reduction* nil))
180		#\|\|
181		(setq term (car (canonicalize-variables (list term) mod)))
182		\|\|#
183	178	(when rewrite-stepping (setq steps-to-be-done 1))
184	179	(when show-stats
185	180	(setq time2 (get-internal-run-time))
186	181	(setf time-for-parse
187	182	(format nil "~,3f sec"
188		;; (/ (float (- time2 time1)) internal-time-units-per-second)
189		(elapsed-time-in-seconds time1 time2)
190		)))
	183	(elapsed-time-in-seconds time1 time2))))
191	184	(unless chaos-quiet
192		;; (fresh-all)
193	185	(flush-all)
194	186	(if (eq mode :exec) ; rewrite-exec-mode
195	187	(format t "~%-- execute in ")

197	189	(format t "~%-- execute! in ")
198	190	(if (eq mode :red)
199	191	(format t "~%-- reduce in ")
200		(format t"~%-- behavioural reduce in "))
201		))
	192	(format t"~%-- behavioural reduce in "))))
202	193	(print-simple-mod-name current-module)
203	194	(princ " : ")
204	195	(let ((print-indent (+ 4 print-indent)))

206	197	(term-print-with-sort term))
207	198	(flush-all))
208	199	;; ********
209		(reset-target-term term last-module mod)
	200	(reset-target-term term (get-context-module) mod)
210	201	;; ********
211	202	(setq $$matches 0)
212	203	(setq time1 (get-internal-run-time))

219	210	cexec-normalize)
220	211	(rewrite-exec term current-module mode)
221	212	(rewrite term current-module mode))))
222		;;
223		#\|\| ============= TODO
224		(when (term-op-contains-theory $$term)
225		(reset-reduced-flag $$term)
226		(setq term $$term)
227		(catch 'rewrite-abort
228		(let ((do-empty-match nil))
229		(if (and rewrite-exec-mode
230		cexec-normalize)
231		(rewrite-exec term current-module mode)
232		(rewrite term current-module mode)))))
233		\|\|#
234		;;
235	213	(setq res $$term)
236	214	(when mel-sort
237		(setq res (setq $$term (apply-sort-memb res mod)))
238		)
	215	(setq res (setq $$term (apply-sort-memb res mod))))
239	216	;;
240	217	(setq time2 (get-internal-run-time))
241	218	(setf time-for-reduction

275	252	(format t ")~%")
276	253	(format t ", ~d memo hits)~%"
277	254	term-memo-hash-hit)))
278		(flush-all)
279		;; (terpri)
280		))
281		))
282		))
	255	(flush-all)))))))
283	256	(context-pop-and-recover))))))
284	257
285	258	(defun perform-meta-reduction (pre-term &optional modexp mode)

289	262	sort)
290	263	(let ((mod (if modexp
291	264	(eval-modexp modexp)
292		last-module)))
	265	(get-context-module))))
293	266	(if (or (null mod) (modexp-is-error mod))
294	267	(if (null mod)
295	268	(with-output-chaos-error ('no-context)

298	271	(princ "incorrect module expression, no such module ")
299	272	(print-chaos-object modexp)))
300	273	(progn
301		(context-push-and-move last-module mod)
	274	(context-push-and-move (get-context-module) mod)
302	275	(setq sort cosmos)
	276	(when auto-context-change
	277	(change-context (get-context-module) mod)) ;;; what?
303	278	(with-in-module (mod)
304		;;
305		(change-context last-module mod)
306		;;
307		(!setup-reduction mod)
	279	(!setup-reduction current-module)
308	280	(setq $$mod current-module)
309	281	(setq rewrite-semantic-reduce
310	282	(and (eq mode :red)

364	336	(defun do-parse-term* (preterm &optional modexp)
365	337	(let ((mod (if modexp
366	338	(eval-modexp modexp)
367		last-module)))
	339	(get-context-module))))
368	340	(unless mod
369	341	(with-output-chaos-error ('no-context)
370	342	(princ "no module expression provided and no selected(current) module.")))

373	345	(princ "incorrect module expression, not such module: ")
374	346	(print-chaos-object modexp)))
375	347	;;
376		(context-push-and-move last-module mod)
	348	(context-push-and-move (get-context-module) mod)
377	349	(with-in-module (mod)
378	350	(prepare-for-parsing current-module)
379	351	(let ((parse-variables nil))

384	356	(!setup-reduction mod)
385	357	(setq res (apply-sort-memb res
386	358	mod)))
387		(reset-target-term res last-module mod)
	359	(reset-target-term res current-module mod)
388	360	;; ********
389	361	(format t "~&")
390	362	(term-print-with-sort res standard-output)
391		(flush-all)
392		;; (break "...")
393		#\|\|
394		(when chaos-verbose
395		(print-term-tree res t))
396		\|\|#
397		)))
	363	(flush-all))))
398	364	(context-pop-and-recover)))
399	365
400	366	;;; TODO

402	368	(declare (ignore mod prompt))
403	369	(with-output-simple-msg ()
404	370	(princ "sorry, red-loop is not implemented yet.."))
405		(return-from red-loop nil)
406		#\|\|
407		(setq $$trials 1)
408		(setq mod (eval-modexp-top mod))
409		(if (modexp-is-error mod)
410		(with-output-chaos-error ('no-such-module)
411		(princ "undefined module")
412		)
413		(let (in
414		(flag nil)
415		(top-level (at-top-level)))
416		(!setup-reduction mod)
417		(loop
418		(chaos-init)
419		(when (and prompt top-level)
420		(terpri)
421		(print-mod-name mod) (princ "> "))
422		(let ((cur (!set-single-reader '("[" "]" "_"))))
423		(progn
424		(setq in (read-seq-of-term '(\|.\|)))
425		(!set-reader cur)))
426		(when (null in) (return))
427		(unless top-level
428		(if flag
429		(progn (princ "---------------------------------------")
430		(terpri))
431		(setq flag t)))
432		(perform-reduction in) ; should ...
433		)))
434		:done
435		\|\|#
436		)
	371	(return-from red-loop nil))
437	372
438	373	(defun check-bad-rules (mod)
439	374	(declare (ignore mod))

457	392	(defun under-debug-rewrite ()
458	393	(or $$trace-rewrite $$trace-rewrite-whole rewrite-stepping
459	394	rewrite-count-limit rewrite-stop-pattern))
460
461		#\|\|
462		(defun rewrite-debug-on ()
463		(setf (symbol-function 'apply-one-rule)
464		(symbol-function 'apply-one-rule-dbg)))
465
466		(defun rewrite-debug-off ()
467		(unless (under-debug-rewrite)
468		(setf (symbol-function 'apply-one-rule)
469		(symbol-function 'apply-one-rule-simple))))
470		\|\|#
471	395
472	396	(defun rewrite-debug-on () ())
473	397	(defun rewrite-debug-off () ())

500	424	(if (= len (length count))
501	425	(set-rewrite-count-limit num)
502	426	(with-output-chaos-error ('invalid-value)
503		(format t "invalid rewrite count limit ~a" count)
504		))))))
	427	(format t "invalid rewrite count limit ~a" count)))))))
505	428
506	429	(defun set-rewrite-count-limit (num)
507	430	(if (integerp num)

563	486	(if (or (null pat)
564	487	(member pat '(("none") ("off") ("nil") ("null"))))
565	488	(set-rewrite-stop-pattern 'none)
566		(let ((mod (or current-module
567		last-module
	489	(let ((mod (or (get-context-module)
568	490	(with-output-chaos-error ('no-context)
569		(princ "no context (current) module is specified.")))
570		))
	491	(princ "no context (current) module is specified.")))))
571	492	(let* ((parse-variables (module-variables mod))
572	493	(term (simple-parse mod
573	494	pat cosmos)))

617	538	(when (modexp-is-error mod)
618	539	(with-output-chaos-error ('no-such-module)
619	540	(format t "incorrect module expression, unknown module?")
620		(print-modexp modexp)
621		))
	541	(print-modexp modexp)))
622	542	(describe-module mod)))
623	543
624	544

630	550	;; (current-module nil)
631	551	mod)
632	552	(setf mod (if (null modexp)
633		last-module
	553	(get-context-module)
634	554	(eval-modexp modexp)))
635	555	(when (modexp-is-error mod)
636	556	(with-output-chaos-error ('no-such-module)
637	557	(princ "incorrect module expression or uknown module")
638		(print-modexp modexp)
639		))
	558	(print-modexp modexp)))
640	559	;;
641	560	(unless mod
642	561	(with-output-chaos-error ('no-context)
643		(princ "no module to be opened!")
644		))
	562	(princ "no module to be opened!")))
645	563	;;
646	564	(unless chaos-quiet
647	565	(fresh-all)

653	571	(!open-module mod)
654	572	(unless chaos-quiet
655	573	(print-in-progress ". done.")
656		(terpri)
657		)
658		))
	574	(terpri))))
659	575
660	576	(defparameter module-open-form
661	577	(%module-decl* "%"

672	588	(princ "closing this module...") (print-next)
673	589	(eval-close-module nil)))
674	590	(setq open-module mod)
675		(setq last-before-open last-module)
676		(setq last-module mod)
	591	(setq last-before-open (get-context-module))
677	592	(clear-term-memo-table term-memo-table)
678	593	(let ((chaos-quiet t)
679		(copy-variables t))
	594	(copy-variables t)
	595	open-mod)
680	596	(setf (%module-decl-kind module-open-form) (module-kind mod))
681		(setq last-module (eval-ast module-open-form))
682		(import-module last-module :using mod)
683		;; (import-module last-module :including mod)
684		;; (import-variables mod last-module)
685		(compile-module last-module))
686		(change-context last-before-open last-module)
687		last-module))
	597	(setq open-mod (eval-ast module-open-form))
	598	(import-module open-mod :using mod)
	599	(compile-module open-mod)
	600	(change-context last-before-open open-mod)
	601	open-mod)))
688	602
689	603	;;; ************
690	604	;;; CLOSE-MODULE

692	606	(defun eval-close-module (&rest ast)
693	607	(declare (ignore ast))
694	608	(if open-module
695		(let ((saved-open open-module))
696		(when (and saved-open (equal "%" (module-name saved-open)))
697		;; (delete-module-all saved-open)
698		;; discard all resources
699		(initialize-module open-module)
700		(setq open-module nil))
701		(change-context last-module last-before-open)
	609	(let ((omod (eval-modexp "%")))
	610	(initialize-module omod)
	611	(when (eq omod (get-context-module))
	612	(change-context (get-context-module) last-before-open))
702	613	(setq open-module nil)
703		(when current-module
704		(change-current-module last-module))
705	614	(setq last-before-open nil))
706	615	(with-output-chaos-warning ()
707		(princ "no module is open.")
708		)))
709
	616	(princ "no module is open."))))
710	617
711	618	;;; ***********
712	619	;;; SAVE SYSTEM

758	665	(print-centering
759	666	"* NOTE : DO NOT MODIFY THIS FILE ULESS YOU REALLY KNOW WHAT YOU ARE DOING!."
760	667	.fill-space.
761		stream)
762		)
	668	stream))
763	669	(terpri stream)
764	670	(princ "\|#" stream)
765	671	(format stream "~&(in-package \"CHAOS\")")

862	768	(when msg?
863	769	(with-output-simple-msg ()
864	770	(format t "~&** done restting system.")
865		(force-output)))
866		))
	771	(force-output)))))
867	772
868	773	;;; **********
869	774	;;; FULL-RESET

894	799	;;
895	800	(when msg?
896	801	(print-in-progress " done")
897		(terpri)
898		)
	802	(terpri))
899	803	(setq chaos-features nil)
900	804	(setq open-module nil)
901	805	(setq last-before-open nil)

1360	1264
1361	1265	;; operator strictness
1362	1266	(:strictness
1363		(let ((mod (if last-module last-module
1364		(if current-module
1365		current-module
	1267	(let ((mod (or (get-context-module)
1366	1268	(with-output-chaos-error ('no-context)
1367		(princ "no context (current) module.")
1368		)))))
	1269	(princ "no context (current) module.")))))
1369	1270	;;
1370	1271	(!setup-reduction mod)
1371	1272	(with-in-module (mod)

1377	1278	(check-operator-strictness op mod t))
1378	1279	(with-output-chaos-error ('no-such-operator)
1379	1280	(princ "no such operator")
1380		(print-chaos-object parsedop)
1381		))
1382		))
	1281	(print-chaos-object parsedop)))))
1383	1282	(check-operator-strictness-whole mod t)))))
1384	1283
1385	1284	;; TRS compatibility

1400	1299	(format t "~&- rewrite rule")
1401	1300	(let ((print-indent (+ 2 print-indent)))
1402	1301	(print-next)
1403		(print-chaos-object (car r-ms))
1404		)
	1302	(print-chaos-object (car r-ms)))
1405	1303	(format t "~& violates the compatibility,")
1406	1304	(format t "~& and following operator(s) can possibly be affected:")
1407	1305	(let ((print-indent (+ 2 print-indent)))

1411	1309	(with-output-simple-msg ()
1412	1310	(format t ">> module is compatible."))))))
1413	1311	;;;
1414		;;;
1415		;;;
1416	1312	(:coherency
1417		(let ((mod (if last-module last-module
1418		(if current-module
1419		current-module
	1313	(let ((mod (or (get-context-module)
1420	1314	(with-output-chaos-error ('no-context)
1421		(princ "no context (current) module.")
1422		)))))
	1315	(princ "no context (current) module.")))))
1423	1316	;;
1424	1317	(!setup-reduction mod)
1425	1318	(with-in-module (mod)

1431	1324	(check-operator-coherency op mod t))
1432	1325	(with-output-chaos-error ('no-such-operator)
1433	1326	(princ "no such operator")
1434		(print-chaos-object parsedop)
1435		))
1436		))
	1327	(print-chaos-object parsedop)))))
1437	1328	(check-operator-coherency-whole mod)))))
1438	1329	;;
1439	1330	;; SENSIBILITY of the signature

1467	1358	(pn-check-refinement args))
1468	1359	;; unknown
1469	1360	(t (with-output-chaos-error ('invalid-arg)
1470		(format t "unknown option to check: ~a" (%check-what ast))
1471		)))))
	1361	(format t "unknown option to check: ~a" (%check-what ast)))))))
1472	1362
1473	1363	;;; *************
1474	1364	;;; TRAM COMPILER

1485	1375	;; first we check the context
1486	1376	(let ((mod (if modexp
1487	1377	(eval-modexp modexp)
1488		last-module)))
	1378	(get-context-module))))
1489	1379	;;
1490	1380	(when (or (null mod) (modexp-is-error mod))
1491	1381	(if (null mod)

1528	1418	(princ (cadr result)))
1529	1419	(force-output))
1530	1420	(progn
1531		(context-push-and-move last-module mod)
	1421	(context-push-and-move (get-context-module) mod)
1532	1422	(let ((print-indent (+ 4 print-indent)))
1533	1423	(with-in-module (mod)
1534	1424	(setq $$term (car result))

1545	1435	(terpri)
1546	1436	(princ (cadr result)))
1547	1437	(force-output)
1548		(reset-target-term $$term last-module mod)))
	1438	(reset-target-term $$term (get-context-module) mod)))
1549	1439	(context-pop-and-recover)))))
1550	1440	;;
1551	1441	(otherwise (with-output-panic-message ()
1552	1442	(format t "internal error, unknown tram command ~a"
1553	1443	command)
1554		(chaos-error 'panic))))
1555		)))
	1444	(chaos-error 'panic)))))))
1556	1445
1557	1446	;;; ********
1558	1447	;;; AUTOLOAD

1563	1452	(let ((entry (assoc modname autoload-alist :test #'equal)))
1564	1453	(if entry
1565	1454	(setf (cdr entry) file)
1566		(push (cons modname file) autoload-alist)))
1567		))
	1455	(push (cons modname file) autoload-alist)))))
1568	1456
1569	1457	;;; *********************
1570	1458	;;; MISC SUPOORT ROUTINES

1611	1499	(number-matches 0))
1612	1500	(let ((mod (if modexp
1613	1501	(eval-modexp modexp)
1614		last-module)))
1615		(unless (eq mod last-module)
	1502	(get-context-module))))
	1503	(unless (eq mod (get-context-module))
1616	1504	(clear-term-memo-table term-memo-table))
1617	1505	(when (or (null mod) (modexp-is-error mod))
1618	1506	(if (null mod)

1621	1509	(with-output-chaos-error ('no-such-module)
1622	1510	(princ "no such module: ")
1623	1511	(print-chaos-object modexp))))
1624		;;
1625		(context-push-and-move last-module mod)
	1512	(context-push-and-move (get-context-module) mod)
	1513	(when auto-context-change
	1514	(change-context (get-context-module) mod))
1626	1515	(with-in-module (mod)
1627		(when auto-context-change
1628		(change-context last-module mod))
1629	1516	(!setup-reduction mod)
1630	1517	(setq $$mod current-module)
1631	1518	(setq sort cosmos)

1655	1542	(print-simple-mod-name current-module)
1656	1543	(print-check 0 3)
1657	1544	(princ " : ")
1658		;; (print-check)
1659	1545	(let ((print-indent (+ 4 print-indent)))
1660	1546	(term-print lhs)
1661	1547	(print-check 0 4)
1662	1548	(princ " == ")
1663		;; (print-check)
1664	1549	(term-print rhs))
1665	1550	(flush-all))
1666		;;
1667	1551	(setq $$matches 0)
1668	1552	(setq time1 (get-internal-run-time))
1669	1553

1713	1597	(let ((modexp (%inspect-modexp ast))
1714	1598	mod)
1715	1599	(setf mod (if (null modexp)
1716		last-module
	1600	(get-context-module)
1717	1601	(eval-modexp modexp)))
1718	1602	(when (modexp-is-error mod)
1719	1603	(with-output-chaos-error ('no-such-module)

1734	1618	(modexp (%what-is-module ast))
1735	1619	(mod nil))
1736	1620	(setf mod (if (null modexp)
1737		last-module
	1621	(get-context-module)
1738	1622	(eval-modexp modexp)))
1739	1623	(when (modexp-is-error mod)
1740	1624	(with-output-chaos-error ('no-such-module))

1753	1637	(modexp (%look-up-module ast))
1754	1638	(mod nil))
1755	1639	(setf mod (if (null modexp)
1756		(or last-module
	1640	(or (get-context-module)
1757	1641	(with-output-chaos-error ('no-context)
1758	1642	(format t "~%No context module is set.")))
1759	1643	(eval-modexp modexp)))

+12

-23

chaos/eval/eval-mod.lisp less more

46	46	;;;
47	47	(defun modexp-top-level-eval (modexp)
48	48	(let ((meparse (parse-modexp modexp)))
49		(if (equal "THE-LAST-MODULE" meparse)
50		(if last-module
51		last-module
52		(with-output-chaos-error ('no-context)
53		(princ "no context (current) module")
54		))
55		(eval-modexp-top (normalize-modexp meparse)))
56		))
	49	(eval-modexp-top (normalize-modexp meparse))))
57	50
58	51	;;; EVAL-MOD
59	52	;;; similar to MODEXP-TOP-LEVEL-EVAL.

61	54	;;;
62	55	(defun eval-mod (toks &optional (change-context auto-context-change))
63	56	(if (null toks)
64		(if last-module
65		last-module
	57	(or (get-context-module)
66	58	(with-output-chaos-error ('no-context)
67		(princ "no selected(current) module.")
68		))
	59	(princ "no selected(current) module.")))
69	60	(if (equal '("%") toks)
70	61	(if open-module
71	62	(let ((mod (find-module-in-env (normalize-modexp "%"))))

74	65	(princ "could not find % module!!!!")
75	66	(chaos-error 'panic)))
76	67	(when change-context
77		(change-context last-module mod))
	68	(change-context (get-context-module) mod))
78	69	mod)
79	70	(with-output-chaos-warning ()
80	71	(princ "no module is opening.")

88	79	(if (integerp val)
89	80	(let ((nmod (print-nth-mod val))) ;;; !!!
90	81	(when change-context
91		(change-context last-module nmod))
	82	(change-context (get-context-module) nmod))
92	83	nmod)
93	84	(with-output-chaos-error ('no-such-module)
94		(format t "could not evaluate the modexp ~a" toks)
95		)))
	85	(format t "could not evaluate the modexp ~a" toks))))
96	86	(with-output-chaos-error ('no-such-module)
97	87	(format t "undefined module? ~a" toks)
98	88	))
99	89	(progn
100	90	(when change-context
101		(change-context last-module val))
	91	(change-context (get-context-module) val))
102	92	val))))))
103	93
104	94	;;; what to do with this one?

131	121	(sub (nth-sub (1- no) mod)))
132	122	(if sub
133	123	(when change-context
134		(change-context last-module sub))
	124	(change-context (get-context-module) sub))
135	125	(progn (princ "** Waring : No such sub-module") (terpri) nil))))
136	126	((and (equal "param" it)
137	127	(cadr toks)

142	132	(param (nth (1- no) params)))
143	133	(if param
144	134	(when change-context
145		(change-context last-module (cdr param)))
	135	(change-context (get-context-module) (cdr param)))
146	136	(with-output-chaos-error ('no-such-parameter)
147	137	(princ "No such parameter")
148	138	))))
149	139	((and (null toks) change-context force?)
150		(when last-module
151		(change-context last-module nil)))
152		(t (eval-mod toks change-context))
153		)))
	140	(when (get-context-module)
	141	(change-context (get-context-module) nil)))
	142	(t (eval-mod toks change-context)))))
154	143
155	144	;;; EOF

+1

-3

chaos/maude/maude.lisp less more

143	143	;;;
144	144	;;; SHOW-FMOD*
145	145	;;;
146		(defun show-fmod* (&optional (module (or last-module
147		current-module)))
	146	(defun show-fmod* (&optional (module (get-context-module)))
148	147	(let ((trs (get-module-trs module)))
149		;;
150	148	(princ "fmod ")
151	149	(print-mod-name module standard-output nil t)
152	150	(princ " is ")

+1

-152

chaos/primitives/baxioms.lisp less more

47	47	;;; ************
48	48	;;; REWRITE RULE : internal use only
49	49	;;; ************
50
51		#\|\|
52		(defterm rewrite-rule (object)
53		:visible (type ; type, either ':equation or ':rule
54		lhs ;
55		rhs
56		condition
57		behavioural
58		id-condition
59		first-match-method
60		next-match-method
61		labels
62		trace-flag)
63		:int-printer print-rule-object
64		:print print-rule-internal)
65		\|\|#
66	50
67	51	(defstruct (rewrite-rule (:include object (-type 'rewreite-rule))
68	52	(:copier nil)

126	110
127	111	;;; Extended rewrite rule
128	112	;;;
129		#\|\|
130		(defterm ex-rewrite-rule (rewrite-rule)
131		:visible (type
132		lhs
133		rhs
134		condition
135		behavioural
136		id-condition
137		first-match-method
138		next-match-method
139		extensions)
140		:int-printer print-rule-object
141		:print print-rule-internal)
142		\|\|#
143	113
144	114	(defstruct (ex-rewrite-rule (:include rewrite-rule (-type 'ex-rewrite-rule))
145	115	(:copier nil)

194	164	;;; *****
195	165	;;; definition of axiom structure.
196	166	;;;
197		#\|\|
198
199		(defterm axiom (rewrite-rule)
200		:visible (type ; :equation, :rule
201		lhs ; left hand side.
202		rhs ; right hand side.
203		condition ; condition
204		behavioural ; t iff axiom is behavioural
205		)
206		:hidden (kind ; internaly categorized kind name of an
207		;; ac-extension :
208		;; a-extensions : these are now local to module.
209		)
210		:int-printer print-axiom-object
211		:print print-axiom-internal
212		)
213
214		\|\|#
215
216	167	(defstruct (axiom (:include rewrite-rule (-type 'axiom))
217	168	(:copier nil)
218	169	(:constructor make-axiom)

228	179	(setf (symbol-function 'is-axiom) (symbol-function 'axiom-p))
229	180	)
230	181
231		#\|\|
232		(defstruct (axiom-exts (:type list))
233		(ac-extension nil)
234		(a-extensions nil))
235		\|\|#
236
237	182	(defun print-axiom-object (obj stream &rest ignore)
238	183	(declare (ignore ignore))
239	184	(if current-module

246	191	(defmacro is-axiom? (--obj) `(is-axiom ,--obj))
247	192
248	193	;;; Primitive structure accessors ----------------------------------------------
249
250		;;; (defmacro axiom-lhs (_a) `(%axiom-lhs ,_a))
251		;;; (defmacro axiom-rhs (_a) `(%axiom-rhs ,_a))
252		;;; (defmacro axiom-condition (_a) `(%axiom-condition ,_a))
253		;;; (defmacro axiom-type (_a) `(%axiom-type ,_a))
254		;;; (defmacro axiom-id-condition (_a) `(%axiom-id-condition ,_a))
255		;;; (defmacro axiom-ac-extension (_a) `(%axiom-ac-extension ,_a))
256		;;; (defmacro axiom-a-extensions (_a) `(%axiom-a-extensions ,_a))
257		;;; (defmacro axiom-kind (_a) `(%axiom-kind ,_a))
258		;;; (defmacro axiom-first-match-method (_a) `(%axiom-first-match-method ,_a))
259		;;; (defmacro axiom-next-match-method (_a) `(%axiom-next-match-method ,_a))
260		;;; (defmacro axiom-labels (_a) `(%axiom-labels ,_a))
261	194
262	195	(defmacro axiom-is-behavioural (_a) `(axiom-behavioural ,_a))
263	196

288	221	(list (cons axiom extensions)))))
289	222	extensions))
290	223
291		;; the following two macros are now just a synonym to axiom-extensions
292		#\|\|
293		(defmacro axiom-ac-extension (_x &optional
294		(ext-rule-table 'current-ext-rule-table))
295		`(axiom-exts-ac-extension (gethash ,_x ,ext-rule-table)))
296
297		(defmacro axiom-a-extensions (_x &optional
298		(ext-rule-table 'current-ext-rule-table))
299		`(axiom-exts-a-extensions (gethash ,_x ,ext-rule-table)))
300
301		\|\|#
302	224	(defmacro axiom-ac-extension (_x &optional
303	225	(_ext-rule-table 'current-ext-rule-table))
304	226	`(axiom-extensions ,_x ,_ext-rule-table))

315	237	(_ext-rule-table 'current-ext-rule-table))
316	238	`(axiom-extensions ,_ax ,_ext-rule-table))
317	239
318		#\|\|
319		(defun !axiom-a-extensions (ax &optional
320		(ext-rule-table current-ext-rule-table))
321		(let ((exts (axiom-extensions ax ext-rule-table)))
322		(if exts
323		(axiom-exts-a-extensions exts)
324		nil)))
325
326		(defsetf !axiom-a-extensions (_ax &optional
327		(ext-rule-table 'current-ext-rule-table))
328		(_value)
329		` (let ((exts (axiom-extensions ,_ax ,ext-rule-table)))
330		(unless exts
331		(setf (axiom-extensions ,_ax ,ext-rule-table)
332		(make-axiom-exts)))
333		(setf (axiom-exts-a-extensions exts) ,_value)))
334
335		\|\|#
336
337
338	240	;;; the basic constructor
339	241	;;; create-axiom
340	242	;;;
341		#\|\|
342		(defun create-axiom (lhs rhs condition type behavioural id-condition
343		ac-extension
344		a-extensions kind first-match-method next-match-method
345		labels)
346		(let ((r (axiom* type lhs rhs condition behavioural)))
347		(setf (axiom-id-condition r) id-condition)
348		(when (or ac-extension a-extensions)
349		(setf (axiom-extensions r) (make-axiom-exts)))
350		(if ac-extension
351		(setf (axiom-ac-extension r) ac-extension))
352		(if a-extensions
353		(setf (axiom-a-extensions r) a-extensions))
354		(setf (axiom-kind r) kind)
355		(setf (axiom-first-match-method r) first-match-method)
356		(setf (axiom-next-match-method r) next-match-method)
357		(setf (axiom-labels r) labels)
358		r))
359		\|\|#
360
361	243	(defun create-axiom (lhs
362	244	rhs
363	245	condition

384	266	(setf (axiom-next-match-method r) next-match-method)
385	267	(setf (axiom-labels r) labels)
386	268	(setf (axiom-meta-and-or r) meta-and-or)
387		(set-context-module r)
	269	(set-object-context-module r)
388	270	r))
389	271
390	272	(defmacro rule-is-builtin (_rule_)
391	273	` (term$is-lisp-code? (term-body (rule-rhs ,_rule_))))
392
393		#\|\|
394		(defun deallocate-axiom (ax)
395		(deallocate-non-var (axiom-lhs ax))
396		(deallocate-non-var (axiom-rhs ax))
397		(let ((cond (axiom-condition ax)))
398		(when (and cond
399		(not (or (eq bool-true cond)
400		(eq bool-false cond))))
401		(deallocate-non-var cond)))
402		(when (axiom-ac-extension ax)
403		(deallocate-axiom (axiom-ac-extension ax)))
404		(mapc #'deallocate-axiom (axiom-a-extensions ax)))
405		\|\|#
406	274
407	275	;;; AXIOM-CONTAINS-ERROR-METHOD? : Axiom -> Bool
408	276	;;; retrurns true iff the axiom contains terms with error-method as top.

428	296
429	297	;;; NOT YET
430	298
431		#\|
432		(defterm theorem (object)
433		:visible (value) ; the theorem itself
434		:hidden (type ; type of thorem
435		; :eq = equation
436		; :rule = rule
437		; :fop = first order predicate
438		; :hol = higher order predicate
439		module ; module object in which the theorem is
440		; specified.
441		valid ; flag
442		; nil = unknown.
443		; :valid = the thorem is poved to be valid.
444		; :invalid = the theorem is proved to be
445		; invalid.
446		))
447		\|#
448
449
450	299	;;; EOF

+1

-1

chaos/primitives/bmacro.lisp less more

42	42
43	43	(defun print-macro (macro stream &rest ignore)
44	44	(declare (ignore ignore))
45		(let ((mod (or last-module current-module)))
	45	(let ((mod (get-context-module)))
46	46	(if mod
47	47	(with-in-module (mod)
48	48	(term-print (macro-lhs macro) stream)

+24

-236

chaos/primitives/bmodule2.lisp less more

48	48	;;; MODULE __________________________________________________________________
49	49	;;; STRUCTURE
50	50	;;; *********
51		#\|\|
52		(defterm module (top-object)
53		:visible (name) ; module name (modexpr).
54		:hidden (signature ; own signature.
55		axiom-set ; set of own axioms.
56		theorems ; set of own theorems, not used yet.
57		parse-dictionary ; infos for term parsing.
58		ex-info ; various compiled informations.
59		trs ; corresponding semi-compiled TRS.
60		context ; run time context
61		)
62		:int-printer print-module-object
63		:print print-module-internal)
64
65		(defstruct (module (:include top-object (-type 'module))
66		(:conc-name "MODULE-")
67		(:constructor make-module)
68		(:constructor module* (name))
69		(:print-function print-module-object)
70		)
71		(signature nil :type (or null signature-struct))
72		; own signature.
73		(axiom-set nil :type (or null axiom-set))
74		; set of own axioms.
75		(theorems nil :type list) ; set of own theorems, not used yet.
76		(parse-dictionary nil :type (or null parse-dictionary))
77		; infos for term parsing.
78		(ex-info nil :type list) ; various compiled informations.
79		(trs nil :type (or null trs)) ; corresponding semi-compiled TRS.
80		(context nil
81		:type (or null module-context))
82		; run time context
83		(alias nil :type list)
84		)
85
86		(eval-when (:execute :load-toplevel)
87		(setf (get 'module :type-predicate) (symbol-function 'module-p))
88		(setf (get 'module :eval) nil)
89		(setf (get 'module :print) 'print-module-internal)
90		)
91
92		\|\|#
93
94		;;; type predicate
95
96		;;; (defmacro module-p (_object) `(is-module ,_object))
97	51
98	52	;;; module name
99	53	;;; name ::= string

249	203	(return-from get-importing-path
250	204	(nconc path im2))))))))))
251	205
252		(defun get-real-importing-mode (module2 &optional (module (or current-module
253		last-module)))
	206	(defun get-real-importing-mode (module2 &optional (module (get-context-module)))
254	207	(declare (type module module2 module)
255	208	(values symbol))
256		;;
257	209	(let ((path (get-importing-path module2 module)))
258	210	(let ((mode nil))
259	211	(dolist (e path mode)

418	370	;;; gathers own signature infomations of a module. stored in module's `signature'
419	371	;;; slot.
420	372
421		#\|\|
422		(defstruct (signature-struct (:conc-name "SIGNATURE$")
423		;; #+gcl (:static t)
424		)
425		(sorts nil :type list) ; list of own sorts.
426		(sort-relations nil :type list) ; list of subsort relations.
427		(operators nil :type list) ; list of operators declared in the
428		; module.
429		(opattrs nil :type list) ; explicitly declared operator
430		; attributes in a form of AST.
431		(principal-sort nil :type atom) ; principal sort of the module.
432		)
433
434		\|\|#
435	373
436	374	;;; accessors via module, all are setf'able.
437	375

466	404	;;; *********
467	405	;;; gathers own axioms and explicitly declared variables of a module.
468	406	;;; stored in module's `axioms' slot.
469
470		#\|\|
471		(defstruct (axiom-set (:conc-name "AXIOM-SET$")
472		;; #+gcl (:static t)
473		)
474		(variables nil :type list) ; assoc list of explicitly declared
475		; variables.
476		; ((variable-name . variable) ...)
477		(equations nil :type list) ; list of equtions declared in the module.
478		(rules nil :type list) ; list of rules declared in the module.
479		)
480
481		\|\|#
482	407
483	408	;;; accessors from module object, all are setf'able.
484	409

516	441	;;; builtin-info part of builtin sorts.
517	442	;;;
518	443
519		#\|\|
520		(defstruct (parse-dictionary (:conc-name "DICTIONARY-")
521		;; #+gcl (:static t)
522		)
523		(table (make-hash-table :test #'equal :size 50)
524		:type (or null hash-table))
525		(builtins nil :type list)
526		(juxtaposition nil :type list) ; list of juxtaposition methods.
527		)
528		\|\|#
529
530	444	;;; accessors via module, all are setf'able
531	445
532	446	(defmacro module-dictionary-table (_mod) `(dictionary-table

565	479	;;; ***
566	480	;;; TRS________________________________________________________________________
567	481	;;; ***
568
569		#\|\|
570		(let ((.ext-rule-table-symbol-num. 0))
571		(declare (type fixnum .ext-rule-table-symbol-num.))
572		(defun make-ext-rule-table-name ()
573		(declare (values symbol))
574		(intern (format nil "ext-rule-table-~d" (incf .ext-rule-table-symbol-num.))))
575		)
576
577		;;; The structure TRS is a representative of flattened module.
578
579		(defstruct (TRS (:conc-name trs$)
580		;; #+gcl (:static t)
581		)
582		(module nil :type (or null module)) ; the reverse pointer
583		;; SIGNATURE INFO
584		(opinfo-table (make-hash-table :test #'eq)
585		:type (or null hash-table))
586		; operator infos
587		(sort-order (make-hash-table :test #'eq)
588		:type (or null hash-table))
589		; transitive closure of sort-relations
590		;; (ext-rule-table (make-hash-table :test #'eq))
591		(ext-rule-table (make-ext-rule-table-name)
592		:type symbol)
593		; assoc table of rule A,AC extensions
594		;;
595		(sorts nil :type list) ; list of all sorts
596		(operators nil :type list) ; list of all operators
597		;; REWRITE RULES
598		(rules nil :type list) ; list of all rewrite rules.
599		;; INFO FOR EXTERNAL INTERFACE -----------------------------------
600		(sort-name-map nil :type list)
601		(op-info-map nil :type list)
602		(op-rev-table nil :type list)
603		;; GENERATED OPS & AXIOMS for equalities & if_then_else_fi
604		;; for proof support system.
605		(sort-graph nil :type list)
606		(err-sorts nil :type list)
607		(dummy-methods nil :type list)
608		(sem-relations nil :type list) ; without error sorts
609		(sem-axioms nil :type list) ; ditto
610		;; a status TRAM interface generated?
611		(tram nil :type symbol) ; nil,:eq, or :all
612		)
613
614		\|\|#
615	482
616	483	;;; accessor via module, all are setf'able.
617	484	(defmacro module-rewrite-rules (_mod) `(trs$rules (module-trs ,_mod)))

706	573	(if (trs$opinfo-table trs)
707	574	(clrhash (trs$opinfo-table trs)))
708	575	(setf (trs$opinfo-table trs) nil)
709		#\|\|
710		(if (trs$ext-rule-table trs)
711		(clrhash (trs$ext-rule-table trs)))
712		\|\|#
713	576	(setf (get (trs$ext-rule-table trs) :ext-rules) nil)
714	577	)
715	578

717	580	;;; CONTEXT_____________________________________________________________________
718	581	;;; *******
719	582	;;; holds some run time context infos.
720
721		#\|\|
722		(defstruct (module-context
723		;; #+gcl (:static t)
724		)
725		(bindings nil :type list) ; top level let binding
726		(special-bindings nil :type list) ; users $$variables ...
727		($$term nil :type list) ; $$term
728		($$subterm nil :type list) ; $$subterm
729		($$action-stack nil :type list) ; action stack for apply
730		($$selection-stack nil :type list) ; selection stack for choose
731		($$stop-pattern nil :type list) ; stop pattern
732		)
733		\|\|#
734
735	583	;;; accessors via module, all are setf'able.
736	584
737	585	(defmacro module-bindings (_mod) `(module-context-bindings (module-context

748	596
749	597	;;; intialization
750	598	(defun initialize-module-context (context)
751		(declare (type module-context context)
	599	(declare (type module-dyn-context context)
752	600	(values t))
753	601	(setf (module-context-bindings context) nil
754	602	(module-context-special-bindings context) nil

760	608	)
761	609
762	610	(defun clean-up-context (context)
763		(declare (type module-context context)
	611	(declare (type module-dyn-context context)
764	612	(values t))
765	613	(initialize-module-context context))
766	614

794	642	;;; beh-axioms-prooved nil ;
795	643	;;; psort-decl ; declaration form of principal sort
796	644	;;; error-op-decl ; declaration forms of explicit error
797		;;; ; operators. may contain illegual ones.
798		;;; macros
799		;;;
	645
800	646	(defun module-infos (mod) (object-misc-info mod))
	647
801	648	(defsetf module-infos (mod) (values)
802	649	`(setf (object-misc-info ,mod) ,values))
803	650

823	670	(defmacro module-hidden (_mod)
824	671	` (getf (object-misc-info ,_mod) ':module-hidden))
825	672
826		;;; KIND
827		(defmacro module-kind (_mod)
828		`(getf (object-misc-info ,_mod) ':module-kind))
829
830		(defmacro module-is-theory (_mod_) `(eq :theory (module-kind ,_mod_)))
831
832		(defmacro module-is-object (_mod_) `(eq :object (module-kind ,_mod_)))
833
834		(defmacro module-is-final (_mod_) `(eq :theory (module-kind ,_mod_)))
835
836		(defmacro module-is-loose (_mod_)
837		` (memq (module-kind ,_mod_) '(:module :ots)))
838
839		(defmacro module-is-initial (_mod_) `(eq (module-kind ,_mod_) :object))
840
841	673	;;; REGULARITY
842	674	(defmacro module-is-regular (_mod)
843	675	`(getf (object-misc-info ,_mod) ':modle-is-regular))
844
845		;;; ALL-SUBMODULES-LIST -- cached data
846		;;; OBSOLETE
847		;;; (defun module-all-submodules-list (mod)
848		;;; (or (object-misc-info-all-submodules-list (object-misc-info mod))
849		;;; (setf (object-misc-info-all-submodules-list (object-misc-info mod))
850		;;; (mapcar #'car (module-all-submodules mod)))))
851	676
852	677	;;; ADD-IMPORTED-MODULE : module mode submodule [alias] -> void
853	678	;;; (for downward comatibility.)

1074	899	(defmacro module-ambig-sorts (_m) `(getf (object-misc-info ,_m) ':ambig-sorts))
1075	900	(defmacro module-ambig-ops (_m) `(getf (object-misc-info ,_m) ':ambig-ops))
1076	901
1077		;;; EX-INFO INITIALIZATION -----------------------------------------------------
1078		;;; OBSOLETE
1079
1080		#\|\|
1081		(defun initialize-module-ex-info (ex-info)
1082		(setf (module-ex-info-protected-modules ex-info) nil
1083		(module-ex-info-hard-wired ex-info) nil
1084		(module-ex-info-kind ex-info) nil
1085		(module-ex-info-all-submodules-list ex-info) nil
1086		(module-ex-info-infos ex-info) nil))
1087
1088		(defun clean-up-ex-info (ex-info)
1089		(initialize-module-ex-info ex-info))
1090
1091		\|\|#
1092
1093	902	;;; *************
1094	903	;;; Module status_______________________________________________________________
1095	904	;;; *************

1099	908	;;; 1 : regularized -- NOT USED.
1100	909	;;; 2 : prepared for parsing
1101	910	;;; 3 : prepared for rewriting
1102		;;;
	911	(defparameter module-initial -1)
	912	(defparameter module-inconsistent 0)
	913	(defparameter module-regularized 1)
	914	(defparameter module-ready-parsing 2)
	915	(defparameter module-ready-rewriting 3)
	916
1103	917	;;; o Adding new sort or operator declarations makes the module status to 0.
1104	918	;;; o Adding new rule makes the module status to at most 2.
1105	919	;;; o Some changes in any submodule makes the status to 0.
1106	920	;;; (should be more fine grained checking for statu change).
1107		;;;
1108		;;; (defmacro module-status (_mod) `(object-status ,_mod))
1109	921
1110	922	;;; initial inconsistent status
1111	923
1112		(defmacro module-is-inconsistent (_module)
1113		`(object-is-inconsistent ,_module))
	924	(defun module-is-inconsistent (_module)
	925	(object-is-inconsistent _module))
1114	926
1115	927	(defun mark-module-as-inconsistent (_module)
1116	928	(mark-object-as-inconsistent _module))

1118	930	;;; parsing preparation
1119	931
1120	932	(defmacro need-parsing-preparation (_module)
1121		`(< (module-status ,_module) 2))
	933	`(< (module-status ,_module) module-ready-parsing))
1122	934
1123	935	(defmacro module-is-ready-for-parsing (_module)
1124		`(>= (module-status ,_module) 2))
	936	`(>= (module-status ,_module) module-ready-parsing))
1125	937
1126	938	(defmacro mark-module-ready-for-parsing (_module)
1127		`(setf (module-status ,_module) (max 2 (module-status ,_module))))
	939	`(setf (module-status ,_module) (max module-ready-parsing (module-status ,_module))))
1128	940
1129	941	(defmacro mark-need-parsing-preparation (_module)
1130		`(setf (module-status ,_module) (min 1 (module-status ,_module))))
	942	`(setf (module-status ,_module) (min module-regularized (module-status ,_module))))
1131	943
1132	944	;;; rewriting preparation
1133	945
1134	946	(defmacro need-rewriting-preparation (_module)
1135		`(< (module-status ,_module) 3))
	947	`(< (module-status ,_module) module-ready-rewriting))
1136	948
1137	949	(defmacro module-is-ready-for-rewriting (_module)
1138		`(>= (module-status ,_module) 3))
	950	`(>= (module-status ,_module) module-ready-rewriting))
1139	951
1140	952	(defmacro mark-module-as-consistent (_module)
1141		`(setf (module-status ,_module) 3))
	953	`(setf (module-status ,_module) module-ready-rewriting))
1142	954
1143	955	(defmacro mark-module-ready-for-rewriting (_module)
1144	956	`(mark-module-as-consistent ,_module))
1145	957
1146	958	(defmacro mark-module-need-rewriting-preparation (_module)
1147		`(setf (module-status ,_module) (min 2 (module-status ,_module))))
	959	`(setf (module-status ,_module) (min module-ready-parsing (module-status ,_module))))
1148	960
1149	961	;;; some handy procs.
1150	962

1157	969	(defmacro needs-rule (&optional (_module 'current-module))
1158	970	`(compile-module ,_module))
1159	971
1160		;;; *******
1161		;;; PRINTER
1162		;;; *******
1163
1164		(defun print-module-object (obj stream &rest ignore)
1165		(declare (ignore ignore)
1166		(type module obj)
1167		(type stream stream)
1168		(values t))
1169		(if (or (module-is-inconsistent obj)
1170		(null (module-name obj)))
1171		(format stream "[:module \"~a\"]" (module-name obj))
1172		(cond ((module-is-object obj)
1173		(format stream ":mod![\"~a\"]" (module-print-name obj)))
1174		((module-is-theory obj)
1175		(format stream ":mod*[\"~a\"]" (module-print-name obj)))
1176		(t (format stream ":mod[\"~a\"]" (module-print-name obj))))))
1177
1178	972	;;; *********************************
1179	973	;;; Constructing RUN TIME ENVIRONMENT -----------------------------------------
1180	974	;;; *********************************

1185	979	;;; module.
1186	980	;;; current-opinfo-table : operator information table of the current module .
1187	981	;;;
1188
1189	982	(defmacro with-in-module ((_module_) &body body)
1190	983	(once-only (_module_)
1191	984	` (block with-in-module

1393	1186	(defun initialize-module (mod)
1394	1187	(declare (type module mod)
1395	1188	(values t))
1396		;;
1397		(setf (module-status mod) -1) ; initial state.
	1189	(setf (module-status mod) module-initial) ; initial state.
1398	1190	(setf (module-decl-form mod) nil)
1399	1191	;; interface
1400	1192	(if (the (or null ex-interface) (module-interface mod))

1416	1208	(setf (module-parse-dictionary mod) (make-parse-dictionary)))
1417	1209	;; misc infos
1418	1210	(setf (object-misc-info mod) nil)
1419		;;; (if (object-misc-info mod)
1420		;;; (initialize-module-ex-info (module-ex-info mod))
1421		;;; (setf (module-ex-info mod) (make-module-ex-info)))
1422	1211	;; trs
1423	1212	(if (the (or null trs) (module-trs mod))
1424	1213	(initialize-trs (module-trs mod) mod)
1425	1214	(setf (module-trs mod) (make-trs :module mod)))
1426	1215	;; context
1427		(if (the (or null module-context) (module-context mod))
	1216	(if (the (or null module-dyn-context) (module-context mod))
1428	1217	(initialize-module-context (module-context mod))
1429		(setf (module-context mod) (make-module-context)))
	1218	(setf (module-context mod) (make-module-dyn-context :object mod)))
1430	1219	;; symbol table
1431	1220	(setf (module-alias mod) nil)
1432	1221	(setf (module-symbol-table mod) (make-symbol-table))
1433	1222	;; print name
1434		;; (setf (module-print-name mod) (make-module-print-name2 mod))
1435	1223	(setf (module-print-name mod) (make-module-print-name mod))
1436	1224	;;
1437	1225	(clear-tmp-sort-cache)

+62

-122

chaos/primitives/bobject2.lisp less more

52	52	;;; definition of semantic object & internal data structure.
53	53	;;; all objects defined in this file inherits either %object or %int-object.
54	54
55		#\|\|
56		;;; term structure of semantic object of Chaos.
57		(defterm object () :category ':object)
58
59		(defterm static-object () :category ':static-object)
60
61		;;; structure of internal object of Chaos.
62		(defterm int-object () :category ':int-object)
63
64		(defterm static-int-object () :category ':static-int-object)
65		\|\|#
66
67	55	(defstruct (object (:conc-name "OBJECT-")
68	56	(:constructor make-object)
69	57	(:constructor object* nil)

76	64	(defmacro object-info (_obj _info)
77	65	` (getf (object-misc-info ,_obj) ,_info))
78	66
79		(defun set-context-module (obj &optional (mod current-module))
80		(setf (object-context-mod obj) mod))
81
82		(eval-when (:execute :load-toplevel)
83		(setf (symbol-function 'is-object)(symbol-function 'object-p))
84		(setf (get 'object ':type-predicate) (symbol-function 'is-object))
85		(setf (get 'object :eval) nil)
86		(setf (get 'object :print) nil))
	67	(defun set-object-context-module (obj &optional (context-mod (get-context-module)))
	68	(setf (object-context-mod obj) context-mod))
	69
	70	; (eval-when (:execute :load-toplevel)
	71	; (setf (symbol-function 'is-object)(symbol-function 'object-p))
	72	; (setf (get 'object ':type-predicate) (symbol-function 'is-object))
	73	; (setf (get 'object :eval) nil)
	74	; (setf (get 'object :print) nil))
87	75
88	76	;;; *********
89	77	;;; INTERFACE

127	115	((module-p nm) (canonicalize-object-name (module-name nm)))
128	116	(t
129	117	;; do nothing
130		;; (error "internal error, illegal name object ~s" nm)
131	118	)))
132	119
133	120	(defun symbol-table-add (table nm obj)

156	143	(t (pushnew obj (stable-unknowns tbl))))
157	144	tbl)))
158	145
159		(defun symbol-table-get (name &optional (module current-module))
	146	(defun symbol-table-get (name &optional (module (get-context-module)))
160	147	(let ((gname (canonicalize-object-name name)))
161	148	(gethash gname (symbol-table-map
162	149	(module-symbol-table module)))))
163	150
164		#\|\|
165		(defun pr-symbol-table (st stream &rest ignore)
166		(let ((names (copy-list (symbol-table-names st))))
167		(setq names (sort names #'ob<))
168		(dolist (name names)
169		(pr-name name (gethash name (symbol-table-map st)) stream))))
170
171		(defun get-object-type (obj)
172		(cond ((module-p obj) :module)
173		((sort-p obj) :sort)
174		((operator-p obj) :operator)
175		((axiom-p obj) :axiom)
176		((term-is-variable? obj) :variable)
177		(t :unknown)))
178
179		(defun get-obj-info (obj)
180		(let ((type (get-object-type obj)))
181		(cond ((or (eq type :variable)
182		(eq (object-context-mod obj) current-module))
183		(list obj type "of the current module"))
184		((eq type :unknown)
185		(list obj type "unknown type of object"))
186		((object-context-mod obj)
187		(list obj
188		type
189		(concatenate 'string "of module "
190		(with-output-to-string (str)
191		(print-mod-name (object-context-mod obj)
192		str
193		t)))))
194		(t (list obj type "")))))
195
196		(defun pr-name (name objs stream)
197		(format stream "~&~A~8T" name)
198		(dolist (obj objs)
199		(let ((info (get-obj-info obj)))
200		(format stream ": ~A ~A~%" (second info) (third info)))))
201		\|\|#
202
203	151	;;;=============================================================================
204	152	;;; TOP-OBJECT _________________________________________________________________
205	153	;;; **********
206	154
207	155	;;; represents common structure of top-level semantic objects.
208	156	;;;
209		#\|\|
210		(defterm top-object (object) ; was (static-object)
211		:visible (name) ; name.
212		:hidden (interface ; external interface.
213		status ; object status.
214		decl-form ; declaration form
215		)
216		)
217		\|\|#
218	157	(defstruct (top-object (:conc-name "TOP-OBJECT-")
219	158	(:constructor make-top-object)
220	159	(:constructor top-object* (name))

226	165	(decl-form nil :type list)
227	166	(symbol-table (make-symbol-table) :type symbol-table))
228	167
229		(eval-when (:execute :load-toplevel)
230		(setf (symbol-function 'is-top-object)(symbol-function 'top-object-p))
231		(setf (get 'top-object ':type-predicate) (symbol-function 'is-top-object))
232		(setf (get 'top-object :eval) nil)
233		(setf (get 'top-object :print) nil))
	168	; (eval-when (:execute :load-toplevel)
	169	; (setf (symbol-function 'is-top-object)(symbol-function 'top-object-p))
	170	; (setf (get 'top-object ':type-predicate) (symbol-function 'is-top-object))
	171	; (setf (get 'top-object :eval) nil)
	172	; (setf (get 'top-object :print) nil))
234	173
235	174	;;;
236	175	;;; basic accessors via top-object

333	272	(declare (type ex-interface interface)
334	273	(values t))
335	274	(setf (interface$parameters interface) nil)
336		(setf (interface$exporting-objects interface) nil)
337		)
	275	(setf (interface$exporting-objects interface) nil))
338	276
339	277	(defun clean-up-ex-interface (interface)
340	278	(declare (type ex-interface interface)
341	279	(values t))
342	280	(setf (interface$dag interface) nil)
343	281	(setf (interface$parameters interface) nil)
344		(setf (interface$exporting-objects interface) nil)
345		)
	282	(setf (interface$exporting-objects interface) nil))
346	283
347	284	;;;
348	285	;;; setting dependency

364	301	(dag-node-subnodes sub-dag))))
365	302	(push s-node (dag-node-subnodes dag)))))
366	303	;; make exporting relation
367		;; (pushnew (cons object mode) (object-exporting-objects subobject) :test #'equal)
368		(pushnew (cons object mode) (object-exporting-objects subobject) :test #'equal)
369		)
	304	(pushnew (cons object mode) (object-exporting-objects subobject) :test #'equal))
370	305
371	306	;;; ******
372	307	;;; STATUS

435	370	;;; builtin-info part of builtin sorts.
436	371	;;;
437	372
438		(defstruct (parse-dictionary (:conc-name "DICTIONARY-")
439		;; #+gcl (:static t)
440		)
	373	(defstruct (parse-dictionary (:conc-name "DICTIONARY-"))
441	374	(table (make-hash-table :test #'equal :size 50)
442	375	:type (or null hash-table))
443	376	(builtins nil :type list)

540	473	(let ((mod (trs$module obj)))
541	474	(format stream "'[:trs \"~a\"]" (make-module-print-name2 mod))))
542	475
543		;;; *******
544		;;; CONTEXT_____________________________________________________________________
545		;;; *******
546		;;; holds some run time context infos.
547
548		(defstruct (module-context
549		;; #+gcl (:static t)
550		)
	476	;;; ******************
	477	;;; MODULE-DYN-CONTEXT___________________________________________________________
	478	;;; ******************
	479	;;; holds run time dynamic infomation of a module.
	480
	481	(defstruct (module-dyn-context (:conc-name "MODULE-CONTEXT-"))
	482	(object nil :type (or null object)) ; module
551	483	(bindings nil :type list) ; top level let binding
552	484	(special-bindings nil :type list) ; users $$variables ...
553	485	($$term nil :type list) ; $$term

563	495	;;; MODULE __________________________________________________________________
564	496	;;; STRUCTURE
565	497	;;; *********
566		#\|\|
567		(defterm module (top-object)
568		:visible (name) ; module name (modexpr).
569		:hidden (signature ; own signature.
570		axiom-set ; set of own axioms.
571		theorems ; set of own theorems, not used yet.
572		parse-dictionary ; infos for term parsing.
573		ex-info ; various compiled informations.
574		trs ; corresponding semi-compiled TRS.
575		context ; run time context
576		)
577		:int-printer print-module-object
578		:print print-module-internal)
579		\|\|#
580
581	498	(defstruct (module (:include top-object (-type 'module))
582	499	(:conc-name "MODULE-")
583	500	(:constructor make-module)
584	501	(:constructor module* (name))
585		(:print-function print-module-object)
586		)
	502	(:print-function print-module-object))
587	503	(print-name "" :type string)
588	504	(signature nil :type (or null signature-struct))
589	505	; own signature.

592	508	(theorems nil :type list) ; set of own theorems, not used yet.
593	509	(parse-dictionary nil :type (or null parse-dictionary))
594	510	; infos for term parsing.
595		;; (ex-info nil :type list) ; various compiled informations.
596		(trs nil :type (or null trs)) ; corresponding semi-compiled TRS.
	511	(trs nil :type (or null trs)) ; corresponding semi-compiled TRS.
597	512	(context nil
598		:type (or null module-context))
	513	:type (or null module-dyn-context))
599	514	; run time context
600		(alias nil :type list)
601		)
602
603		(eval-when (:execute :load-toplevel)
604		(setf (get 'module :type-predicate) (symbol-function 'module-p))
605		(setf (get 'module :eval) nil)
606		(setf (get 'module :print) 'print-module-internal)
607		)
	515	(alias nil :type list) ; alias names for a module generated from complex modexpr
	516	)
	517
	518	;;; KIND
	519	(defmacro module-kind (_mod)
	520	`(getf (object-misc-info ,_mod) ':module-kind))
	521
	522	(defmacro module-is-theory (_mod_) `(eq :theory (module-kind ,_mod_)))
	523
	524	(defmacro module-is-object (_mod_) `(eq :object (module-kind ,_mod_)))
	525
	526	(defmacro module-is-final (_mod_) `(eq :theory (module-kind ,_mod_)))
	527
	528	(defmacro module-is-loose (_mod_)
	529	` (memq (module-kind ,_mod_) '(:module :ots)))
	530
	531	(defmacro module-is-initial (_mod_) `(eq (module-kind ,_mod_) :object))
	532
	533	;;; PRINTER
	534
	535	(defun print-module-object (obj stream &rest ignore)
	536	(declare (ignore ignore)
	537	(type module obj)
	538	(type stream stream)
	539	(values t))
	540	(if (or (module-is-inconsistent obj)
	541	(null (module-name obj)))
	542	(format stream ":module[\"~a\"]" (module-name obj))
	543	(cond ((module-is-object obj)
	544	(format stream ":mod![\"~a\"]" (module-print-name obj)))
	545	((module-is-theory obj)
	546	(format stream ":mod*[\"~a\"]" (module-print-name obj)))
	547	(t (format stream ":mod[\"~a\"]" (module-print-name obj))))))
608	548
609	549	;;; ****
610	550	;;; VIEW _______________________________________________________________________

633	573
634	574	(defun print-view-struct-object (obj stream &rest ignore)
635	575	(declare (ignore ignore))
636		(format stream "#<view ~a: ~s => ~s \| ~s>"
	576	(format stream ":view[~a: ~s => ~s \| ~s]"
637	577	(view-struct-name obj)
638	578	(view-struct-src obj)
639	579	(view-struct-target obj)

+15

-295

chaos/primitives/boperator.lisp less more

124	124	;;; ********
125	125	;;; OPERATOR __________________________________________________________________
126	126	;;; ********
127		#\|\|
128		(defterm operator (object) ; (static-object)
129		:visible (name) ; list of `symbol' & `number of arguments'.
130		:hidden (module
131		strategy
132		theory
133		syntax
134		memo
135		print-name
136		hidden
137		)
138		:int-printer print-operator-object
139		:print print-operator-internal)
140
141		\|\|#
142
143	127	(defstruct (operator (:include object (-type 'operator))
144	128	(:constructor make-operator)
145	129	(:constructor operator* (name))
146	130	(:copier nil)
147	131	(:print-function print-operator-object))
148	132	(name nil :type list)
149		(module nil :type (or null module))
150	133	(strategy nil :type list)
151	134	(theory nil :type (or null op-theory))
152	135	(syntax nil :type (or null opsyntax))

161	144
162	145	(defun print-operator-object (obj stream &rest ignore)
163	146	(declare (ignore ignore))
164		(format stream "(:op ~s : ~x)" (operator-name obj) (addr-of obj))
165		)
166
167		;;; (defmacro operator-p (_o) `(is-operator ,_o))
	147	(format stream ":op[~s : ~x]" (operator-name obj) (addr-of obj)))
168	148
169	149	;;; Basic accessors ----------------------------------------------------------
170
171		;;; (defmacro operator-name (_operator) `(%operator-name ,_operator))
	150	(defmacro operator-module (op)
	151	`(object-context-mod ,op))
172	152	(defmacro operator-symbol (_operator) `(car (operator-name ,_operator)))
173	153	(defmacro operator-num-args (_operator) `(cdr (operator-name ,_operator)))
174		;;; (defmacro operator-module (_operator) `(%operator-module ,_operator))
175		;;; (defmacro operator-hidden (_operator) `(%operator-hidden ,_operator))
176	154
177	155	;;; id = (name . module)
178	156	(defmacro operator-id (__operator)

180	158	`(cons (operator-name ,__operator) (operator-module ,__operator))))
181	159	(defmacro operator-module-id (__operator) `(module-name (operator-module
182	160	,__operator)))
183		;;; (defmacro operator-strategy (__operator) `(%operator-strategy ,__operator))
184	161	(defmacro operator-rewrite-strategy (__operator)
185	162	`(operator-strategy ,__operator))
186		;;; (defmacro operator-theory (__operator) `(%operator-theory ,__operator))
187		;;; (defmacro operator-syntax (__operator) `(%operator-syntax ,__operator))
188		;;; (defmacro operator-print-name (__operator) `(%operator-print-name ,__operator))
189		;;; (defmacro operator-memo (__operator) `(%operator-memo ,__operator))
190	163
191	164	(defun explode-operator-name (op-symbol)
192	165	(declare (type list op-symbol)

241	214
242	215	;;; Constructor of Operator body.-----------------------------------------------
243	216	(defvar opname-table nil)
244		#\|\|
245		(eval-when (:execute :load-toplevel)
246		(setf opname-table (make-hash-table :test #'equal)))
247		\|\|#
248	217
249	218	(defun canonicalize-op-name (name)
250	219	(declare (type list name)

253	222	(prog1
254	223	name
255	224	(push (cons name name) opname-table))))
256
257		#\|\|
258		(defvar .operator-recycler.)
259		(eval-when (:execute :load-toplevel)
260		(setq .operator-recycler. (make-hash-table :test #'equal)))
261
262		(defun allocate-operator (name num-args module)
263		(let* ((name (canonicalize-op-name (cons name num-args)))
264		(key (cons name module))
265		(op (gethash key .operator-recycler.)))
266		(if op
267		op
268		(progn
269		(setq op (operator* name))
270		(setf (operator-module op) module)
271		(when (modexp-is-simple-name (module-name module))
272		(setf (gethash key .operator-recycler.) op))
273		op))))
274
275		\|\|#
276	225
277	226	(defun allocate-operator (name num-args module)
278	227	(declare (type list name)

301	250	(operator-syntax o) syntax
302	251	(operator-print-name o) print-name)
303	252	o))
304
305	253
306	254	;;; accessors of an operator's syntax via operator.
307	255	;;;

457	405	;;; *****************************************************************************
458	406
459	407	;;; * NOTE* The slots defined here are all module idependent.
460		#\|\|
461		(defterm method (object)
462		:visible (name ; operator name (canonicalized).
463		arity ; arity, list of argument sorts.
464		coarity) ; coarity
465		:hidden (module ; the module it belongs.
466		constructor ; flag, t iff the method is a
467		; constructor. not yet used.
468		supplied-strategy ; user supplied rewrite strategy.
469		form ; describes the form of a term with the
470		; method as top. used for parsing.
471		precedence ; precedence used for parsing.
472		associativity ; associative info used for parsing.
473		memo ; t iff the rewriting will be memoized.
474		behavioural ; t iff the method is behavioural method.
475		coherent ; t iff the method is behaviourally coherent.
476		error ; t iff the method is error method and user
477		; defined.
478		)
479		:int-printer print-method-object
480		:print print-method-internal)
481		\|\|#
482	408
483	409	(defstruct (method (:include object (-type 'method))
484	410	(:constructor make-method)

488	414	(name nil :type list) ; operator name (canonicalized).
489	415	(arity nil :type list) ; arity, list of argument sorts.
490	416	(coarity nil :type (or null sort*)) ; coarity
491		(module nil :type (or null module)) ; the module it belongs.
492	417	(constructor nil :type (or null t)) ; flag, t iff the method is a
493	418	; constructor. not yet used.
494	419	(supplied-strategy nil :type list) ; user supplied rewrite strategy.

498	423	; precedence used for parsing.
499	424	(associativity nil :type symbol) ; associative info used for parsing.
500	425	(behavioural nil :type (or null t)) ; t iff the method is behavioural method.
501		;; (coherent nil :type (or null t)) ; t iff the method is behaviourally coherent.
502	426	(error nil :type (or null t)) ; t iff the method is error method and user
503	427	; defined.
504	428	(derived-from nil :type (or null method))
505	429	(has-memo nil :type (or null t))
506		(id-symbol nil :type symbol)
507		)
	430	(id-symbol nil :type symbol))
508	431
509	432	(eval-when (:execute :load-toplevel)
510	433	(setf (symbol-function 'is-method) (symbol-function 'method-p))

513	436
514	437	(defun print-method-object (obj stream &rest ignore)
515	438	(declare (ignore ignore))
516		(format stream "[:operator ~a]" (method-name obj)))
	439	(format stream ":op[~a]" (method-name obj)))
517	440
518	441	;;; Primitive constructor ------------------------------------------------------
519	442

521	444	;;;
522	445	(defmacro create-operator-method (_name _arity _coarity)
523	446	`(let ((meth (method* ,_name ,_arity ,_coarity)))
524		(set-context-module meth)
	447	(set-object-context-module meth)
525	448	meth))
526	449
527	450	;;; Primitive type predicate ---------------------------------------------------

530	453
531	454	;;; Primitive accessors --------------------------------------------------------
532	455
533		;;; (defmacro method-name (_m) `(%method-name ,_m))
	456	(defmacro method-module (m)
	457	`(object-context-mod ,m))
	458
534	459	(defmacro method-symbol (_m) `(car (method-name ,_m)))
535		;;; (defmacro method-arity (_m) `(%method-arity ,_m))
536		;;; (defmacro method-coarity (_m) `(%method-coarity ,_m))
537		;;; (defmacro method-constructor (_m) `(%method-constructor ,_m))
538		;;; (defmacro method-form (_m) `(%method-form ,_m))
539		;;; (defmacro method-supplied-strategy (_m) `(%method-supplied-strategy ,_m))
540		;;; (defmacro method-precedence (_m) `(%method-precedence ,_m))
541		;;; (defmacro method-memo (_m) `(%method-memo ,_m))
542		;;; (defmacro method-module (_m) `(%method-module ,_m))
543		;;; (defmacro method-associativity (_m) `(%method-associativity ,_m))
544		;;; (defmacro method-behavioural (_m) `(%method-behavioural ,_m))
	460
545	461	(defmacro method-is-behavioural (_m) `(method-behavioural ,_m)) ; synonym
546		;;; (defmacro method-is-coherent (_m) `(method-coherent ,_m))
	462
547	463	(defmacro method-is-user-defined-error-method (_m)
548	464	`(method-error ,_m))
549	465

578	494	(type list arity)
579	495	(type sort* coarity)
580	496	(values method))
581		#\|\|
582		(let ((key (list name arity coarity)))
583		(or (gethash key .operator-method-recycler.)
584		(let ((meth (method* name arity coarity)))
585		(setf (gethash key .operator-method-recycler.) meth)
586		meth)))
587		\|\|#
588		(create-operator-method name arity coarity)
589		)
	497	(create-operator-method name arity coarity))
590	498
591	499	(defun make-method-id-symbol (method)
592	500	(let* ((nam (method-name method))

603	511	(values method))
604	512	(let ((meth (allocate-operator-method name arity coarity)))
605	513	(declare (type method meth))
606		(setf (method-module meth) current-module
	514	(setf (method-module meth) (get-context-module)
607	515	(method-constructor meth) nil
608	516	(method-supplied-strategy meth) nil
609	517	(method-precedence meth) nil

624	532
625	533	;;; The same object.
626	534	(defmacro method= (_meth1 _meth2) `(eq ,_meth1 ,_meth2))
	535
627	536	(defun method-w= (m1 m2)
628	537	(or (method= m1 m2)
629	538	(when (and (sort= (method-coarity m1) sort-id-sort)

675	584	;;; ***********
676	585	;;; Internal structure constaining module dependent infos of a method.
677	586	;;; does not appear explicitly in Chaos program.
678
679		#\|\|
680		(defterm !method-info (int-object) ; (static-int-object) ; internal term.
681		:hidden (operator ; pointer to the operator.
682		theory ; equational theory.
683		lower-methods ; list of lower comparable methods,
684		; sorted lower->higher, exclusive.
685		overloaded-methods ; list of overloaded methods,
686		; sortd higher->lower, exclusive.
687		rules-with-same-top ; rewrite rules with lhs and rhs have a
688		; common top method.
689		rules-with-different-top ; rewrite rules with lhs and rhs have
690		; different top method.
691		strictly-overloaded ; t iff the method is strictly
692		; overloaded ,i.e., has no incomparable
693		; overloaded method.
694		rew-strategy ; rewrite strategy.
695		has-trans ; flag, t iff the method has transitivity
696		; axioms.
697		))
698
699		\|\|#
700
701	587	(defstruct (!method-info (:include object (-type '!method-info))
702	588	(:copier nil)
703	589	(:constructor make-!method-info)

736	622	;;;
737	623	;;; GET-METHOD-INFO
738	624	;;;
739		#\|\|
740		(defun get-method-info (method &optional (opinfo-table current-opinfo-table))
741		(if (and (eq method .method1.) (eq opinfo-table .method-tab1.))
742		.method-val1.
743		(if (and (eq method .method2.) (eq opinfo-table .method-tab2.))
744		.method-val2.
745		(let ((res (gethash method opinfo-table)))
746		(if res
747		(progn
748		(setq .method2. .method1.
749		.method-tab2. .method-tab1.
750		.method-val2. .method-val1.)
751		(setq .method1. method
752		.method-tab1. opinfo-table
753		.method-val1. res)
754		res)
755		#\|\|
756		(with-output-chaos-error ()
757		(format t "context is inconsistent, could not get info for operator:")
758		(format t "~& ~a" (method-name method))
759		(chaos-to-top))
760		\|\|#
761		nil
762		)))))
763		\|\|#
764
765	625	(declaim (inline get-method-info))
766	626
767	627	(#+GCL si::define-inline-function #-GCL defun

839	699	`(!method-info-coherent (get-method-info ,_m ,_info-table)))
840	700
841	701	;;; CONSTRUCTOR ----------------------------------------------------------------
842
843		#\|\|
844		(defvar .method-info-recycler. (make-hash-table :test #'equal))
845		(defun allocate-method-info (method module)
846		(let* ((key (list method module))
847		(minfo (gethash key .method-info-recycler.)))
848		(if minfo
849		minfo
850		(progn
851		(setq minfo (!method-info*))
852		(when (modexp-is-simple-name (module-name module))
853		(setf (gethash key .method-info-recycler.) minfo))
854		minfo))))
855		\|\|#
856	702
857	703	(defun allocate-method-info (meth mod)
858	704	(declare (ignore meth mod)

880	726	;;;
881	727	;;; METHOD-THEORY-INFO-FOR-MATCHING
882	728	;;;
883		#\|\|
884		(defun method-theory-info-for-matching (method &optional (info-table
885		current-opinfo-table))
886		(declare (type method method)
887		(type hash-table info-table)
888		(values theory-info))
889		(let* ((th (method-theory method info-table))
890		(info (theory-info th)))
891		(declare (type op-theory th)
892		(type theory-info info))
893		(if (zero-rule-only th)
894		(%svref theory-info-array
895		(logandc2 (the fixnum (theory-info-code info)) .Z.))
896		info)))
897		\|\|#
898
899	729	(defun compute-method-theory-info-for-matching (method &optional
900	730	(info-table
901	731	current-opinfo-table))

1146	976	(if (err-sort-p a)
1147	977	(return-from method-is-error-method t))))))
1148	978
1149		#\|\|
1150		(defun method-is-universal (method)
1151		(and (method-arity method)
1152		(every #'(lambda (x) (or (sort= x universal-sort)
1153		(sort= x huniversal-sort)
1154		(sort= x cosmos)))
1155		(method-arity method))))
1156		\|\|#
1157
1158	979	(defun method-is-universal (method)
1159	980	(declare (type method method)
1160	981	(values (or null t)))

1328	1149	;;; NOTE second method is assumed to be just associative.
1329	1150	;;;
1330	1151	#-GCL (declaim (inline method-is-associative-restriction-of))
1331		#\|\|
1332		(defun method-is-associative-restriction-of (meth1
1333		meth2
1334		&optional
1335		(so current-sort-order)
1336		(info current-opinfo-table))
1337		(declare (type method meth1 meth2)
1338		(type sort-order so)
1339		(type hash-table info)
1340		(values (or null t)))
1341		(or (method= meth1 meth2)
1342		(and (eq (method-name meth1) (method-name meth2))
1343		(sort<= (method-coarity meth1)
1344		(method-coarity meth2)
1345		so)
1346		(sort-list<= (method-arity meth1)
1347		(method-arity meth2)
1348		so)
1349		(theory-contains-associativity (method-theory meth1 info)))))
1350		\|\|#
1351	1152	#-GCL
1352	1153	(defun method-is-associative-restriction-of (meth1
1353	1154	meth2)

1373	1174	;;;
1374	1175	;;; NOTE second method is assumed to be associative-commutive.
1375	1176	;;;
1376		#\|\|
1377		(defun method-is-AC-restriction-of (meth1
1378		meth2
1379		&optional
1380		(so current-sort-order)
1381		(info current-opinfo-table))
1382		(declare (type method meth1 meth2)
1383		(type sort-order so)
1384		(type hash-table info)
1385		(values (or null t)))
1386		(or (method= meth1 meth2)
1387		(and (eq (method-name meth1) (method-name meth2))
1388		(sort<= (method-coarity meth1)
1389		(method-coarity meth2)
1390		so)
1391		(sort-list<= (method-arity meth1)
1392		(method-arity meth2)
1393		so)
1394		(theory-contains-AC (method-theory meth1 info)))))
1395		\|\|#
1396
1397	1177	#-GCL (declaim (inline method-is-ac-restriction-of))
1398
1399	1178	#-GCL
1400	1179	(defun method-is-AC-restriction-of (meth1
1401	1180	meth2

1422	1201	;;;
1423	1202	;;; NOTE second method is assumed to be just commutive.
1424	1203	;;;
1425		#\|\|
1426		(defun method-is-commutative-restriction-of (meth1
1427		meth2
1428		&optional
1429		(so current-sort-order)
1430		(info current-opinfo-table))
1431		(declare (type method meth1 meth2)
1432		(type sort-order so)
1433		(type hash-table info)
1434		(values (or null t)))
1435		(or (method= meth1 meth2)
1436		(and (eq (method-name meth1) (method-name meth2))
1437		(sort<= (method-coarity meth1)
1438		(method-coarity meth2)
1439		so)
1440		(sort-list<= (method-arity meth1)
1441		(method-arity meth2)
1442		so)
1443		(theory-contains-commutativity (method-theory meth1 info)))))
1444		\|\|#
1445
1446	1204	#-GCL (declaim (inline method-is-commutative-restriction-of))
1447
1448	1205	#-GCL
1449	1206	(defun method-is-commutative-restriction-of (meth1 meth2)
1450	1207	(declare (type method meth1 meth2)

1772	1529	method)
1773	1530	(car res)))
1774	1531	(return-from lowest-method! method))))))
1775
1776		#\|\|
1777		(defun lowest-method! (method lower-bound &optional (module current-module))
1778		(declare (type method method)
1779		(type list lower-bound)
1780		(type module module)
1781		(values (or null method)))
1782		(let ((current-sort-order (module-sort-order module))
1783		(current-opinfo-table (module-opinfo-table module))
1784		(res nil))
1785		(declare (type hash-table current-sort-order current-opinfo-table))
1786		(let ((over-methods (method-overloaded-methods method current-opinfo-table)))
1787		(declare (type list over-methods))
1788		(when on-debug
1789		(format t "~%* lowest-method! : over-methods =")
1790		(dolist (m over-methods)
1791		(terpri)
1792		(princ " ")
1793		(print-chaos-object m)))
1794		;;
1795		(if over-methods
1796		(progn
1797		(dolist (meth over-methods)
1798		(declare (type method meth))
1799		(when (and (sort-list<= lower-bound (method-arity meth))
1800		(not (member
1801		meth
1802		res
1803		:test #'(lambda (x y)
1804		(method-is-instance-of y
1805		x
1806		current-sort-order)))))
1807		(push meth res)))
1808		(or (choose-lowest-op res)
1809		method))
1810		(return-from lowest-method! method)))))
1811		\|\|#
1812	1532
1813	1533	(defun lowest-method* (method &optional lower-bound (module current-module))
1814	1534	(declare (type method method)

1987	1707	(setf (operator-associativity op) nil)
1988	1708	(setf (operator-computed-precedence op) nil)
1989	1709	(setf (operator-theory op) the-empty-theory)
1990		(set-context-module op module)
	1710	(set-object-context-module op module)
1991	1711	op)))
1992	1712
1993	1713	;;; EOF

+12

-35

chaos/primitives/bsort.lisp less more

57	57	;;; never be created as a term body (abstract class).
58	58	;;;
59	59
60		#\|\|
61		(defterm sort-struct (object) ; (static-object)
62		;; :name ""
63		:visible (id ; sort name, symbol.
64		hidden) ; flag, t iff the sort is hidden sort.
65
66		:hidden (module ; module in which the sort is declared.
67		; type = module object.
68		constructor ; the list of constructor methods of the
69		; sort. not used.
70		inhabited ; temporary flag used for regularizing
71		; the signature of a module.
72		)
73		:int-printer print-sort-internal
74		:print print-sort-internal)
75		\|\|#
76
77	60	(defstruct (sort-struct (:conc-name "SORT-STRUCT-")
78	61	(:include object (-type 'sort-struct))
79	62	(:copier nil)

82	65	(:constructor sort-struct* (id hidden)))
83	66	(id nil :type symbol)
84	67	(hidden nil :type (or null t))
85		(module nil :type (or null module))
86	68	(constructor nil :type list)
87	69	(inhabited nil :type (or null t))
88		(derived-from nil :type (or null sort-struct))
89		)
	70	(derived-from nil :type (or null sort-struct)))
	71
	72	(eval-when (:execute :load-toplevel :compile-toplevel)
	73	(defmacro sort-module (sort)
	74	`(object-context-mod ,sort))
	75	)
90	76
91	77	(eval-when (:execute :load-toplevel)
92	78	(setf (symbol-function 'sort-sort-struct) (symbol-function 'sort-struct-p))

173	159	(type (or null t) hidden))
174	160	(let ((sort (sort* id hidden)))
175	161	(setf (sort-module sort) module)
176		(set-context-module sort module)
	162	(set-object-context-module sort module)
177	163	sort))
178	164
179	165	;;; SORT-TABLE
180		#\|\|
181		(defvar sort-table (make-hash-table :test #'equal))
182		(defmacro get-sort-named (sort-name_ module_)
183		`(gethash (cons ,sort-name_ ,module_) sort-table))
184		(defun clear-all-sorts () (clrhash sort-table))
185		(defun register-sort (sort)
186		(setf (gethash (cons (sort-id sort) (sort-module sort)) sort-table) sort))
187
188		\|\|#
189	166
190	167	(defvar sort-table nil)
191	168	(defun get-sort-named (sort-name module)

326	303	(setf (crsort-maker s) (if (eq p-type 'class-sort)
327	304	(list nil nil nil nil)
328	305	(list nil nil)))
329		(set-context-module s module)
	306	(set-object-context-module s module)
330	307	s))
331	308
332	309	(defun new-record-sort (id module &optional hidden)

430	407	(let ((bs (bsort* id hidden)))
431	408	(setf (sort-module bs) module
432	409	(bsort-info bs) info)
433		(set-context-module bs module)
	410	(set-object-context-module bs module)
434	411	bs))
435	412
436	413	;;; Predicate ------------------------------------------------------------------

513	490	(let ((as (and-sort* id hidden)))
514	491	(setf (sort-module as) module
515	492	(and-sort-components as) and-components)
516		(set-context-module as module)
	493	(set-object-context-module as module)
517	494	as))
518	495
519	496	;;; Predicates -----------------------------------------------------------------

567	544	(let ((os (or-sort* id hidden)))
568	545	(setf (sort-module os) module
569	546	(or-sort-components os) or-components)
570		(set-context-module os module)
	547	(set-object-context-module os module)
571	548	os))
572	549
573	550	;;; Predicate ------------------------------------------------------------------

618	595	(setf (sort-module es) module
619	596	(err-sort-components es) components
620	597	(err-sort-lowers es) lowers)
621		(set-context-module es module)
	598	(set-object-context-module es module)
622	599	es))
623	600
624	601	;;; Predicates ----------------------------------------------------------------

+33

-80

chaos/primitives/context.lisp less more

40	40	;;; all the functions which handle module's context.
41	41	;;;
42	42
43		;;; INSTANCE DB ****************************************************************
44		;;; instance db stores all the instances of class sort.
45		;;; made for persistent object
46		;;; we store term-body of an instance in the instance db.
47		;;; retrieving the instance always creates new term.
48		;;; this is for avoiding destructive replacement of term body.
49		;;;
50
51		;;; (defvar instance-db (make-hash-table :test #'equal))
52		;;; (defun clear-instance-db () (clrhash instance-db))
53
54		(defmacro make-id-key (___id)
55		(once-only (___id)
56		` (cond ((term-is-builtin-constant? ,___id)
57		(term-builtin-value ,___id))
58		(t (method-symbol (term-method ,___id))))))
59
60		(defun find-instance (id &optional class (module current-module))
61		(or (find-instance-aux id module class)
62		(dolist (sub (module-all-submodules module) nil)
63		(when (not (eq (cdr sub) :using))
64		(let ((inst (find-instance-aux id (car sub) class)))
65		(if inst (return-from find-instance inst)))))))
66
67		(defun find-instance-aux (id module &optional class)
68		(let ((db (module-instance-db module)))
69		(unless db (return-from find-instance-aux nil))
70		(let ((body (gethash (make-id-key id) db)))
71		(if body
72		(progn
73		(term$unset-reduced-flag body)
74		(when class
75		(unless (sort<= (term$sort body) class (module-sort-order module))
76		(return-from find-instance-aux nil)))
77		(list body))
78		nil))))
79
80		(defun register-instance (object)
81		(unless (term-eq void-object object)
82		(let ((module (sort-module (term-sort object)))
83		(id (term-arg-1 object)))
84		(let ((db (module-instance-db module)))
85		(unless db
86		(initialize-module-instance-db module)
87		(setq db (module-instance-db module)))
88		(setf (gethash (make-id-key id) db) (term-body object))))))
89
90		(defun delete-instance (object)
91		(unless (term-eq void-object object)
92		(let ((module (sort-module (term-sort object))))
93		(let ((db (module-instance-db module)))
94		(unless db
95		(return-from delete-instance nil))
96		(remhash (make-id-key (term-arg-1 object)) db)))))
	43	;;; GET-CONTEXT : null \| module
	44	(defun get-context ()
	45	(if current-module
	46	(module-context current-module)
	47	nil))
	48
	49	;;; GET-CONTEXT-MODULE
	50	(defun get-context-module ()
	51	current-module)
	52
	53	;;; RESET-CONTEXT-MODULE
	54	(defun reset-context-module (&optional (mod nil))
	55	(setf current-module mod))
	56
	57	;;; GET-OBJECT-CONTEXT object -> null \| module
	58	;;;
	59	(defun get-object-context (obj)
	60	(or (get-context-module) (object-context-mod obj)))
97	61
98	62	;;; BINDINGS *******************************************************************
99	63
100		;;; GET BOUND VALUES
	64	;;; GET-BOUND-VALUE : let-symbol -> value (a term) \| null
	65
101	66	(defun is-special-let-variable? (name)
102	67	(declare (values (or null t)))
103	68	(and (>= (length (the simple-string name)) 3)

110	75	:test #'(lambda (x y)
111	76	(eq x (car y))))))
112	77
113		(defun get-bound-value (let-sym &optional (mod current-module))
	78	(defun get-bound-value (let-sym &optional (mod (get-context-module)))
114	79	(or (cdr (assoc let-sym (module-bindings mod) :test #'equal))
115	80	(when allow-$$term
116	81	(cond ((equal let-sym "$$term")

137	102	(cdr (assoc let-sym (module-bindings mod) :test #'equal)))
138	103	(t nil)))))
139	104
140		(defun set-bound-value (let-sym value &optional (mod current-module))
	105	(defun set-bound-value (let-sym value &optional (mod (get-context-module)))
141	106	(when (or (equal let-sym "$$term")
142	107	(equal let-sym "$$subterm"))
143	108	(with-output-chaos-error ('misc-error)

175	140	(module-context-$$subterm context) $$subterm
176	141	(module-context-$$action-stack context) $$action-stack
177	142	(module-context-$$selection-stack context) $$selection-stack
178		(module-context-$$stop-pattern context) rewrite-stop-pattern
179		;; (module-context-$$ptree context) proof-tree
180		))))
	143	(module-context-$$stop-pattern context) rewrite-stop-pattern))))
181	144
182	145	(defun new-context (mod)
183	146	(unless mod

186	149	$$action-stack nil
187	150	$$selection-stack nil
188	151	$$term-context nil
189		last-module nil
190		;; !!!
191	152	current-module nil
192		rewrite-stop-pattern nil
193		;; proof-tree nil
194		)
	153	rewrite-stop-pattern nil)
195	154	(return-from new-context nil))
196		;;
197	155	(let ((context (module-context mod)))
198	156	(setf $$term (module-context-$$term context)
199	157	$$subterm (module-context-$$subterm context)
200	158	$$action-stack (module-context-$$action-stack context)
201	159	$$selection-stack (module-context-$$selection-stack context)
202		rewrite-stop-pattern (module-context-$$stop-pattern context)
203		;;proof-tree (module-context-$$ptree context)
204		)
	160	rewrite-stop-pattern (module-context-$$stop-pattern context))
205	161	(setf $$term-context mod)
206		(setq last-module mod)
207		;; !!!!!
208		(setq current-module mod)
209		;; !!!!!
	162	(reset-context-module mod)
210	163	(clear-method-info-hash)
211	164	t))
212	165

222	175	;; save current context
223	176	(save-context from)
224	177	;; restore new context
225		(new-context to)
226		)
	178	(new-context to))
227	179
228	180	(defun reset-target-term (term old-mod mod)
229	181	(if (eq mod old-mod)

233	185	$$selection-stack nil)
234	186	(save-context mod)
235	187	(new-context mod))
236		;; we do not change globals, instead set in context of mod.
237		(save-context mod)))
	188	;; we do not change globals, instead set in context of mod.
	189	(save-context mod)))
238	190	;;;
239	191	(defun context-push (mod)
240	192	(push mod old-context))

247	199	(change-context old new))
248	200
249	201	(defun context-pop-and-recover ()
250		(when (or last-module current-module)
	202	(when (get-context-module)
251	203	(let ((old (context-pop)))
252		(unless (member old (list last-module current-module))
	204	(unless (eq old (get-context-module))
253	205	;; eval-mod may change the current context implicitly.
254	206	;; in this case we do not recover context.
255		(change-context last-module old)))))
	207	(change-context (get-context-module) old)))))
256	208
257	209	;;; EOF
	210

+1

-29

chaos/primitives/find.lisp less more

96	96
97	97	;;; FIND-SORTS-IN-MODULE
98	98
99		(defun find-sorts-in-module (sort-name &optional (module (or current-module
100		last-module)))
	99	(defun find-sorts-in-module (sort-name &optional (module (get-context-module)))
101	100	(declare (type symbol sort-name)
102	101	(type module module))
103	102	(let ((res nil))

107	106
108	107	;;; FIND-SORT
109	108	;;;
110		#\|\|
111		(defun find-sort (sort-name-or-name-ref &optional (module (or current-module
112		last-module)))
113		(unless module
114		(error "Internal error,module is not specified: find-sort"))
115		(unless (module-p module)
116		(error "Internal error, find-sort: invalid module ~A" module))
117		(let ((sort (get-sort-named sort-name-or-name-ref module)))
118		(if sort sort
119		(let ((ambig-sorts (find-sorts-in-module sort-name-or-name-ref module)))
120		(cond ((= (length ambig-sorts) 1) (car ambig-sorts))
121		((> (length ambig-sorts) 1)
122		(with-output-chaos-warning ()
123		(princ "sort name ")
124		(princ sort-name-or-name-ref)
125		(princ " is ambiguous, arbitrary take ")
126		(print-chaos-object (setf sort (car (nreverse ambig-sorts))))
127		(princ " as the resolved name.")
128		)
129		sort)
130		(t (or (get-sort-named sort-name-or-name-ref 'chaos-module)
131		(with-output-chaos-warning ()
132		(princ "no such sort ")
133		(princ sort-name-or-name-ref)
134		nil))))))))
135
136		\|\|#
137	109
138	110	;;; FIND-SORT-IN : Module Sort-Name -> Sort
139	111	;;;

+1

-4

chaos/primitives/gen-eval.lisp less more

80	80	(and (fboundp (car ast))
81	81	(symbol-function (car ast))))))
82	82	(cond (evaluator
83		(let ((module (or ;; (chaos-eval-context ast)
84		;; chaos-eval-context
85		current-module
86		last-module)))
	83	(let ((module (get-context-module)))
87	84	(when (and module (not (module-p module)))
88	85	(setq module (find-module-in-env
89	86	(normalize-modexp (string module)))))

+3

-4

chaos/primitives/gen-print.lisp less more

590	590	(cond ((chaos-ast? object)
591	591	(let ((printer (ast-printer object)))
592	592	(if printer
593		(let ((mod (or current-module last-module)))
	593	(let ((mod (get-context-module)))
594	594	(if mod
595	595	(with-in-module (mod)
596	596	(funcall printer object stream))

601	601	((and (chaos-object? object) (not (stringp object)))
602	602	(let ((printer (object-printer object)))
603	603	(if printer
604		(let ((mod (or current-module
605		last-module)))
	604	(let ((mod (get-context-module)))
606	605	(if mod
607	606	(with-in-module (mod)
608	607	(funcall printer object stream))

611	610	(print-pretty nil))
612	611	(prin1 object stream)))))
613	612	((term? object)
614		(let ((mod (or current-module last-module)))
	613	(let ((mod (get-context-module)))
615	614	(if mod
616	615	(with-in-module (mod)
617	616	(term-print object stream))

+1

-2

chaos/primitives/junk/bmodule.lisp less more

227	227	(return-from get-importing-path
228	228	(nconc path im2))))))))))
229	229
230		(defun get-real-importing-mode (module2 &optional (module (or current-module
231		last-module)))
	230	(defun get-real-importing-mode (module2 &optional (module (get-context-module)))
232	231	(declare (type module module2 module)
233	232	(values symbol))
234	233	;;

+2

-5

chaos/primitives/normodexp.lisp less more

77	77	(setq modexp (car modexp)))
78	78	;;
79	79	(when (and (equal modexp "the-current-module")
80		current-module)
81		(setq modexp current-module))
82		;; (when (and (equal modexp "THE-LAST-MODULE") last-module)
83		;; (setq modexp last-module))
84		;;
	80	(get-context-module))
	81	(setq modexp (get-context-module)))
85	82	(cond ((module-p modexp) (normalize-modexp (module-name modexp)))
86	83	((stringp modexp) (canonicalize-simple-module-name modexp))
87	84	((atom modexp) modexp)

+16

-31

chaos/primitives/print-object.lisp less more

297	297
298	298	;;; top level modexp printer ---------------------------------------------------
299	299
300		#\|\|
301	300	(defun get-context-name (obj)
302		(let ((context-mod (object-context-mod obj)))
303		(if context-mod
304		(with-output-to-string (str)
305		(print-mod-name context-mod str t))
306		nil)))
307		\|\|#
308
309		(defun get-context-name (obj)
310		(let ((context-mod (object-context-mod obj)))
	301	(let ((context-mod (get-object-context obj)))
311	302	(if context-mod
312	303	(get-module-print-name context-mod)
313	304	nil)))
314	305
315		(defun get-context-name-extended (obj &optional (context current-module))
	306	(defun get-context-name-extended (obj &optional (context (get-context-module)))
316	307	(let ((cmod (object-context-mod obj)))
	308	(declare (type (or null module) cmod))
317	309	(unless cmod (return-from get-context-name-extended nil))
318		;;
319		(when context
320		(let ((als (assoc cmod (module-alias context))))
321		(when als
322		(return-from get-context-name-extended (cdr als)))))
323		;;
	310	(let ((als (assoc cmod (module-alias context))))
	311	(when als
	312	(return-from get-context-name-extended (cdr als))))
324	313	(let ((name (get-module-print-name cmod)))
325	314	(unless (module-is-parameter-theory cmod)
326	315	(cond ((modexp-is-simple-name name)

878	867
879	868	(defun print-sort-internal (sort &optional (stream standard-output) ignore)
880	869	(declare (ignore ignore))
881		(print-sort-name sort (or current-module last-module) stream))
	870	(print-sort-name sort (get-object-context sort) stream))
882	871
883	872	(defun print-record-internal (sort &optional (stream standard-output) ignore)
884	873	(declare (ignore ignore))
885		(print-sort-name sort (or current-module last-module) stream))
	874	(print-sort-name sort (get-object-context sort) stream))
886	875
887	876	(defun print-class-internal (sort &optional (stream standard-output) ignore)
888	877	(declare (ignore ignore))
889		(print-sort-name sort (or current-module last-module) stream))
	878	(print-sort-name sort (get-object-context sort) stream))
890	879
891	880	(defun print-bsort-internal (sort &optional (stream standard-output) ignore)
892	881	(declare (ignore ignore))
893		(print-sort-name sort (or current-module last-module) stream))
	882	(print-sort-name sort (get-object-context sort) stream))
894	883
895	884	(defun print-and-sort-internal (sort &optional (stream standard-output) ignore)
896	885	(declare (ignore ignore))
897		(print-sort-name sort (or current-module last-module) stream))
	886	(print-sort-name sort (get-object-context sort) stream))
898	887
899	888	(defun print-or-sort-internal (sort &optional (stream standard-output) ignore)
900	889	(declare (ignore ignore))
901		(print-sort-name sort (or current-module last-module) stream))
	890	(print-sort-name sort (get-object-context sort) stream))
902	891
903	892	(defun print-err-sort-internal (sort &optional (stream standard-output) ignore)
904	893	(declare (ignore ignore))
905		(print-sort-name sort (or current-module last-module) stream))
	894	(print-sort-name sort (get-object-context sort) stream))
906	895
907	896	;;; MODULE ************
908
909		;;; (defun print-module-internal (module &optional (stream standard-output))
910		;;; (print-mod-name module stream t t))
911	897
912	898	(defun print-module-internal (module &optional (stream standard-output) ignore)
913	899	(declare (ignore ignore))

957	943
958	944	(defun print-method-internal (meth &optional (stream standard-output) ignore)
959	945	(declare (ignore ignore))
960		(let ((mod (or current-module last-module))
	946	(let ((mod (get-object-context meth))
961	947	(.file-col. .file-col.))
962	948	(format stream "~{~A~} :" (method-symbol meth))
963	949	(setq .file-col. (file-column stream))

1195	1181
1196	1182	;;; PRINT-SORT-NAME : sort &optional module stream -> Void
1197	1183	;;;
1198		(defun print-sort-name (s &optional
1199		(module (or current-module last-module))
1200		(stream standard-output))
	1184	(defun print-sort-name (s &optional (module (get-object-context s))
	1185	(stream standard-output))
1201	1186	(unless (sort-struct-p s) (break "print-sort-name: given non sort: ~s" s))
1202	1187	(let ((standard-output stream)
1203	1188	(mod-name (get-module-print-name (sort-module s))))

+12

-54

chaos/primitives/term-utils.lisp less more

59	59	(defun make-applform (sort meth &optional args)
60	60	(declare (type sort* sort)
61	61	(type method meth)
62		(type list args)
63		(values term))
64		(if consider-object
65		(if (method-is-object-constructor meth)
66		(let ((id (car args)) ; the first argument is always an object
67		; identifier.
68		(class sort))
69		#+:debug-term
70		(progn
71		(format t "~&object construction: ")
72		(print-object meth)
73		(force-output))
74		(if (not (term-is-variable? id)) ; non variable means the term
75		; denotes a concrete instance.
76		(let ((instance nil))
77		(setf instance (find-instance id class))
78		(if instance
79		(progn (setf (term-arg-3 instance) (third args))
80		instance)
81		(progn (setf instance
82		(make-applform-simple sort meth args))
83		(register-instance instance)
84		instance)))
85		(make-applform-simple sort meth args)
86		))
87		(make-applform-simple sort meth args) )
88		(make-applform-simple sort meth args)))
	62	(type list args))
	63	(make-applform-simple sort meth args))
89	64
90	65	;;; ******************
91	66	;;; RESET-REDUCED-FLAG

288	263	(term-print-with-sort term)))))
289	264	(if (term$is-builtin-constant? body)
290	265	;; built-in constant term
291		(let ((so (module-sort-order
292		(if current-module
293		current-module
294		(or last-module
295		(sort-module (term$sort body))))))
296		(isrt (term$sort body))
297		(val (term$builtin-value body)))
	266	(let* ((isrt (term$sort body))
	267	(cm (get-object-context isrt))
	268	(so (if cm
	269	(module-sort-order cm)
	270	(with-output-chaos-error ('internal-error)
	271	(format t "Internal Error, No context module [ULP]."))))
	272	(val (term$builtin-value body)))
298	273	(declare (type sort-order so)
299	274	(type sort* isrt)
300	275	(type t val))

314	289
315	290	;; application form
316	291	(let* ((head (term$head body))
317		(mod (if current-module
318		current-module
319		(or last-module
320		(operator-module (method-operator head)))))
	292	(mod (get-object-context (method-operator head)))
321	293	(son nil)
322	294	(t1 nil)
323	295	(t2 nil)

325	297	(new-head nil))
326	298	(declare (type method head)
327	299	(type module mod))
328		;; #\|\|
329		(when (method-is-error-method head)
330		(when term-debug
331		(with-output-msg ()
332		(format t "ULP:ERR_TERM: ")
333		(term-print-with-sort term)))
334		;; recursively
335		(dolist (sub (term-subterms term))
336		(update-lowest-parse sub)))
337		;; \|\|#
338
339	300	;; ----------------------------
340	301	;; special case if_then_else_fi
341	302	;; ----------------------------

824	785	;;; method, otherwise, given method is used.
825	786	(defvar sa-debug nil)
826	787	(defun make-term-with-sort-check (meth subterms
827		&optional (module (or current-module
828		last-module)))
	788	&optional (module (get-context-module)))
829	789	(declare (type method meth)
830	790	(type list subterms)
831	791	(type module module))

1466	1426	(sort-is-hidden x))
1467	1427	(mapcar #'(lambda (y) (term-sort y))
1468	1428	(term-subterms term)))
1469		;; patch Tue May 26 10:11:22 JST 1998
1470	1429	(or (method-is-behavioural (term-head term))
1471	1430	(method-is-coherent (term-head term)))
1472	1431	t)
1473		(every #'term-can-be-in-beh-axiom? (term-subterms term))))
1474		)
	1432	(every #'term-can-be-in-beh-axiom? (term-subterms term)))))
1475	1433	(t t)))
1476	1434
1477	1435	(defun term-is-non-behavioural? (term)

+2

-6

chaos/term-parser/parse-engine.lisp less more

170	170	(term-subterms term)))
171	171	(simple-copy-term term))))
172	172
173		(defun get-qualified-op-pattern (tok &optional (module (or current-module
174		last-module)))
	173	(defun get-qualified-op-pattern (tok &optional (module (get-context-module)))
175	174	(labels ((destruct-op-name (expr)
176	175	(let ((pos (position #\_ expr)))
177	176	(declare (type (or null fixnum) pos))

1682	1681	(print-terletox-list terletox-list))
1683	1682	terletox-list))
1684	1683
1685		(defun test-sort-memb-predicate (term &optional (module (or current-module
1686		last-module)))
	1684	(defun test-sort-memb-predicate (term &optional (module (get-context-module)))
1687	1685	(unless module
1688	1686	(with-output-chaos-error ('no-context)
1689	1687	(princ "checking _:_, no context module is given!")))
1690	1688	(with-in-module (module)
1691	1689	(let ((arg1 (term-arg-1 term))
1692	1690	(id-const (term-arg-2 term)))
1693		;; (format t "~&arg1 = ")(print arg1)
1694		;; (format t "~&id-const = ") (print id-const)
1695	1691	(let ((sorts (gather-sorts-with-id id-const module))
1696	1692	(term-sort (term-sort arg1)))
1697	1693	(unless sorts

+1

-2

chaos/term-parser/parse-macro.lisp less more

73	73	(term-is-congruent-2? (macro-rhs macro1)
74	74	(macro-rhs macro2))))
75	75
76		(defun expand-macro (term &optional (module (or current-module
77		last-module)))
	76	(defun expand-macro (term &optional (module (get-context-module)))
78	77	(labels ((apply-macro-rule (macro term)
79	78	(block the-end
80	79	(multiple-value-bind (global-state subst no-match E-equal)

+1

-1

chaos/term-parser/parse-top.lisp less more

368	368	;;; parse-convert : term -> term'
369	369	;;;
370	370	(defun parse-convert (term
371		&optional (module (or current-module last-module)))
	371	&optional (module (get-context-module)))
372	372	;; #define macro expand
373	373	(when macroexpand
374	374	(setq term (expand-macro term module)))

+2

-4

chaos/tools/compat.lisp less more

39	39	;;;
40	40	;;; CHECK COMPATIBILITY
41	41	;;;
42		(defun check-compatibility (&optional (module (or last-module
43		current-module)))
	42	(defun check-compatibility (&optional (module (get-context-module)))
44	43	(unless module
45	44	(with-output-chaos-error ('no-context)
46		(princ "no context (current) module is specified!")
47		))
	45	(princ "no context (current) module is specified!")))
48	46	;;
49	47	(unless on-preparing-for-parsing
50	48	(prepare-for-parsing module))

+12

-22

chaos/tools/op-check.lisp less more

48	48	;;; 1. constants(operations free from axioms) are always strict.
49	49	;;;
50	50	(defun check-method-strictness (meth &optional
51		(module (or current-module
52		last-module
53		))
	51	(module (get-context-module))
54	52	report?)
55	53
56	54	(unless module
57	55	(with-output-chaos-error ('no-cntext)
58		(princ "checking lazyness: no context module is specified!")
59		))
	56	(princ "checking lazyness: no context module is specified!")))
60	57	;;
61	58	(with-in-module (module)
62	59	(cond ((and (null (method-rules-with-different-top meth))

144	141	(values (reverse strategy) (reverse end-strategy)))))
145	142	)))
146	143
147		(defun check-operator-strictness (op &optional (module (or last-module
148		current-module))
149		report?)
	144	(defun check-operator-strictness (op &optional (module (get-context-module))
	145	report?)
150	146	(unless module
151	147	(with-output-chaos-error ('no-context)
152		(princ "no context (current) module is given!")
153		))
	148	(princ "no context (current) module is given!")))
154	149	;;
155	150	(let* ((opinfo (if (opinfo-p op)
156	151	(prog1 op (setq op (opinfo-operator op)))

179	174	(push (list meth str-list1 str-list2) res))))
180	175	(nreverse res)))
181	176
182		(defun check-operator-strictness-whole (&optional (module (or last-module
183		current-module))
	177	(defun check-operator-strictness-whole (&optional (module (get-context-module))
184	178	report?)
185	179	(unless module
186	180	(with-output-chaos-error ('no-context)
187		(princ "no context (current) module is specified!")
188		))
	181	(princ "no context (current) module is specified!")))
189	182	;;
190	183	(let ((result nil))
191	184	(dolist (opinfo (ops-to-be-shown module))

243	236	nil))))
244	237
245	238	(defun check-method-coherency (meth &optional
246		(module (or current-module last-module))
	239	(module (get-context-module))
247	240	(warn t))
248	241	(unless module
249	242	(with-output-chaos-error ('no-cntext)

520	513
521	514	(defun check-operator-coherency (op
522	515	&optional
523		(module (or current-module last-module))
524		(warn t)
525		)
	516	(module (get-context-module))
	517	(warn t))
526	518
527	519	(unless module
528	520	(with-output-chaos-error ('no-context)
529		(princ "no context (current) module is given!")
530		))
	521	(princ "no context (current) module is given!")))
531	522	;;
532	523	(let* ((opinfo (if (opinfo-p op)
533	524	(prog1 op (setq op (opinfo-operator op)))

616	607	))
617	608
618	609	(defun check-method-congruency (meth iobservers
619		&optional (module (or current-module
620		last-module)))
	610	&optional (module (get-context-module)))
621	611	(unless module
622	612	(with-output-panic-message ()
623	613	(princ "congruence check: no context module!")))

+2

-4

chaos/tools/regcheck.lisp less more

54	54	(non-empties nil) ; non-empty methods.
55	55	)
56	56
57		(defun print-sop (sop &optional (module (or current-module
58		last-module)))
	57	(defun print-sop (sop &optional (module (get-context-module)))
59	58	(with-in-module (module)
60	59	(format t "~%** SOP : operator ")
61	60	(print-chaos-object (sop-operator sop))

600	599	(cadr m)))
601	600
602	601	(defun check-method-redundancy (arity coarity method-list
603		&optional (module (or current-module
604		last-module)))
	602	&optional (module (get-context-module)))
605	603	(let ((so (module-sort-order module))
606	604	(redundant-methods nil)
607	605	(not-tobe-added? nil))

+10

-26

chaos/tools/show.lisp less more

49	49	(with-output-msg ()
50	50	(princ "no current context, `select' some module first."))
51	51	(return-from show-context nil))
52		(if (eq last-module mod)
	52	(if (eq (get-context-module) mod)
53	53	(format t "~&-- current context :")
54	54	(progn (format t "~&-- context of : ")
55	55	(print-chaos-object mod)))
56		(context-push-and-move last-module mod)
	56	(context-push-and-move (get-context-module) mod)
57	57	(with-in-module (mod)
58	58	(format t "~&[module] ")
59	59	(print-chaos-object current-module)

79	79
80	80	;;; SHOW BINDINGS
81	81
82		(defun show-bindings (&optional (module last-module))
	82	(defun show-bindings (&optional (module (get-context-module)))
83	83	(unless module
84	84	(with-output-msg ()
85	85	(princ "no context (current module) is specified.")

106	106
107	107	;;; show apply selection
108	108
109		(defun show-apply-selection (&optional (module last-module))
	109	(defun show-apply-selection (&optional (module (get-context-module)))
110	110	(unless module
111	111	(with-output-msg ()
112	112	(princ "no context (current module) is specified.")

137	137	(terpri)
138	138	(incf depth)))))
139	139
140		;; (format t "~&[selections] ~{~a~^ of ~}" $$selection-stack)
141
142	140	;;;
143	141	;;; print-pending
144	142	;;;
145		(defun print-pending (&optional (module last-module))
	143	(defun print-pending (&optional (module (get-context-module)))
146	144	(unless module
147	145	(with-output-msg ()
148	146	(princ "no context (current module) is specified.")

184	182	(with-output-chaos-warning ()
185	183	(format t "unknown option for `show term' : ~a" tree?))
186	184	(return-from show-term nil))
187		(unless last-module
	185	(unless (get-context-module)
188	186	(with-output-msg ()
189	187	(princ "no current context, `select' some module first.")
190	188	(return-from show-term nil)))
191	189	(unless target
192	190	(setq target "$$term"))
193		(with-in-module (last-module)
	191	(with-in-module ((get-context-module))
194	192	(when (stringp target)
195	193	;; let variable
196	194	(catch 'term-context-error

389	387	(check-qualified-sort-name sort)
390	388	(cond (modexp
391	389	(setq mod (eval-modexp modexp))
392		#\|\|
393		(find-module-in-env-ext modexp (or
394		current-module
395		last-module)
396		:no-error)
397		\|\|#
398	390	(unless (module-p mod)
399	391	(with-output-msg ()
400	392	(format t "no such module ~a" modexp)
401	393	(return-from show-sort nil))))
402		(t (setq mod (or current-module
403		last-module))
	394	(t (setq mod (get-context-module))
404	395	(unless (module-p mod)
405	396	(with-output-msg ()
406	397	(princ "no context(current) module, select some first.")

434	425	(defun get-module-from-opref (parsedop)
435	426	(let ((mod nil))
436	427	(cond ((%opref-module parsedop)
437		#\|\|
438		(setq mod (find-module-in-env-ext (%opref-module parsedop)
439		(or current-module
440		last-module)
441		:no-error))
442		\|\|#
443	428	(setq mod (%opref-module parsedop))
444	429	(unless (module-p mod)
445	430	(setq mod (eval-modexp (%opref-module parsedop)))

450	435	(print-next)
451	436	(princ "no such module ")
452	437	(princ (%opref-module parsedop))))))
453		(t (setq mod (or current-module
454		last-module))
	438	(t (setq mod (get-context-module))
455	439	(unless mod
456	440	(with-output-chaos-error ('no-context)
457	441	(princ "no context module is given.")))))

506	490	(defun show-param (toks no &optional describe)
507	491	(let ((mod (if toks
508	492	(eval-mod-ext toks)
509		(or last-module current-module))))
	493	(get-context-module))))
510	494	(unless mod
511	495	(with-output-msg ()
512	496	(format t "no context (current module) is specified.")

+5

-5

chaos/tools/sort-tree.lisp less more

58	58	kinds)
59	59	kinds)))
60	60
61		(defun make-sort-tree (sort &optional (mod (or current-module last-module)))
	61	(defun make-sort-tree (sort &optional (mod (get-object-context sort)))
62	62	(let* ((so (module-sort-order mod))
63	63	(kind (the-err-sort sort so))
64	64	(sls (module-sort-relations mod))

76	76
77	77	(defun print-sort-tree (sort &optional
78	78	(stream standard-output)
79		(mod (or current-module last-module)))
	79	(mod (get-object-context sort)))
80	80	(!print-sort-tree sort stream mod nil))
81	81
82	82	(defun print-sort-graph (sort &optional
83	83	(stream standard-output)
84		(mod (or current-module last-module)))
	84	(mod (get-object-context sort)))
85	85	(!print-sort-tree sort stream mod t))
86	86
87	87	(defun !print-sort-tree (sort stream mod show-as-graph)

103	103
104	104	;;; PRINT-MODULE-SORT-TREE
105	105
106		(defun print-module-sort-tree (&optional (mod (or current-module last-module))
	106	(defun print-module-sort-tree (&optional (mod (get-context-module))
107	107	(stream standard-output))
108	108	(!print-module-sort-tree mod stream nil))
109	109
110		(defun print-module-sort-graph (&optional (mod (or current-module last-module))
	110	(defun print-module-sort-graph (&optional (mod (get-context-module))
111	111	(stream standard-output))
112	112	(!print-module-sort-tree mod stream t))
113	113

+7

-19

chaos/tram/tram.lisp less more

144	144	;;
145	145	(with-output-chaos-error ('tram-fail)
146	146	(format t "failed to invoke TRAM compiler")
147		(when last-module
148		(context-pop-and-recover))
149		))
	147	(when (get-context-module)
	148	(context-pop-and-recover))))
150	149
151	150	;;
152	151	(setq tram_in_file in-file
153	152	tram_out_file out-file)
154	153
155		#\|\|
156		;; wait for a while untill i/o files are prepared
157		(dotimes (x 30)
158		x
159		(sleep 1)
160		(when (probe-file in-file) (return nil)))
161		\|\|#
162
163	154	;; try open streams
164	155	(setq out-stream (open out-file
165	156	:direction :output

171	162	(unless (and in-stream out-stream)
172	163	(with-output-chaos-error ('tram-fail)
173	164	(format t "failed to open TRAM I/O streams")
174		(when last-module
175		(context-pop-and-recover))
176		))
177		(setq tram-process (cons in-stream out-stream))
178		))
	165	(when (get-context-module)
	166	(context-pop-and-recover))))
	167	(setq tram-process (cons in-stream out-stream))))
179	168
180	169	(defun kill-tram-process ()
181	170	(setq tram-last-module nil)

289	278	(format t "Unkonwn TRAM term ~s is returned.~
290	279	~% This can happen if signature is not regular..."
291	280	tram-term)
292		(when last-module
	281	(when (get-context-module)
293	282	(context-pop-and-recover))
294	283	(chaos-error 'tram-panic)))))))
295	284

751	740	;;; TRAM-COMPILE-CHAOS-MODULE
752	741	;;;
753	742	(defun tram-compile-chaos-module (&optional all?
754		(module (or current-module
755		last-module))
	743	(module (get-context-module))
756	744	debug)
757	745	;;
758	746	(unless debug (run-tram-process-if-need))

+0

-6

comlib/globals.lisp less more

72	72
73	73	(defvar top-level-definition-in-progress nil)
74	74
75		;;; last-module bounds the module object which was the target of the operation
76		;;; in the last time, i.e., whenever the context is swithced, last-module
77		;;; bounds the last `current module'.
78	75	;;; open-module bounds the 'opening' module.
79	76	;;;
80	77	(declaim (special open-module ; the module crrently opened.
81		last-module ; the module which was the current last
82		; time.
83	78	last-before-open ; the module which was last before the
84	79	; currently opened module.
85	80	))

89	84	(defvar current-opinfo-table nil)
90	85	(defvar current-ext-rule-table nil)
91	86	(defvar open-module nil)
92		(defvar last-module nil)
93	87	(defvar last-before-open nil)
94	88
95	89	;;; Feature for require & provide

+9

-5

doc/examples/ASIP/zz.mod less more

3	3	-- imperative program", MIT Press.
4	4	-- * program codes are converted from OBJ to CafeOBJ
5	5	--
6		"ZZ extends CafeoBJ's built-in representation of the integers with an
	6
	7	#\|------------------------------
	8	ZZ extends CafeoBJ's built-in representation of the integers with an
7	9	equality predicate, _is_, and with some equations that are useful for
8	10	manipulating inequalities. In paricular, these equations are useful
9	11	as lemmas in the correctness proof given in the book. For example,

18	20	lemma for the proof. In fact, there is not set of equations that can allow
19	21	the automatic verification of all properties of integer expressions which
20	22	contain indeterminate values such as `s[['X]]'; in other words, first order
21		arithmetic is \"undecidable\".
22		"
	23	arithmetic is "undecidable".
	24	--------------------------\|#
23	25
24	26	module ZZ {
25	27	imports {
26	28	protecting (INT)
27	29	}
28	30	signature {
29		"The predicate _is_ is intended to represent equality on integers.
	31	#\|
	32	The predicate _is_ is intended to represent equality on integers.
30	33	The reason for introducing a new equality predicate rather then
31	34	using CafeOBJ's builtin equality _==_ is that we want to use
32	35	integer expressions which indeterminate values in program
33		correctness proofs (cf. Section 2.1.1 of Chapter2). "
	36	correctness proofs (cf. Section 2.1.1 of Chapter2).
	37	\|#
34	38	op _is_ : Int Int -> Bool
35	39	}
36	40	axioms {

+0

-1

sysdef.asd less more

124	124	(:file "match-method")
125	125	(:file "axiom")
126	126	(:file "gen-rule")
127		(:file "cr")
128	127	(:file "rwl")
129	128	(:file "beh")
130	129	(:file "module")

+0

-1

sysdef.cl less more

160	160	"construct/match-method"
161	161	"construct/axiom"
162	162	"construct/gen-rule"
163		"construct/cr"
164	163	"construct/rwl"
165	164	"construct/beh"
166	165	"construct/module"

+2

-3

thstuff/basics.lisp less more

87	87	nil))))
88	88
89	89	(defun disp-term (x)
90		(with-in-module (last-module)
	90	(with-in-module ((get-context-module))
91	91	(term-print x)
92	92	(princ " : ")
93	93	(print-sort-name (term-sort x) current-module)))

513	513	trmtoks
514	514	avar
515	515	aterm)
516		;; (!setup-parse last-module)
517		(with-in-module (last-module)
	516	(with-in-module ((get-context-module))
518	517	(loop (when (null substtoks) (return))
519	518	;; <varid> = <term>
520	519	(setq varnm (cadr substtoks))

+1

-1

thstuff/cexec.lisp less more

1420	1420	(bind nil)
1421	1421	;; the followings are experimental
1422	1422	(if nil))
1423		(let ((module (or current-module last-module))
	1423	(let ((module (get-context-module))
1424	1424	max-r
1425	1425	max-d)
1426	1426	(unless module

+22

-26

thstuff/eval-apply.lisp less more

41	41	;;; *****
42	42
43	43	(defun eval-start-command (ast)
44		(do-eval-start-th (%start-target ast) last-module))
	44	(do-eval-start-th (%start-target ast) (get-context-module)))
45	45
46	46	(defun do-eval-start-th (pre-term &optional context)
47	47	(catch 'apply-context-error
48	48	(let ((mod (if context
49	49	(eval-modexp context)
50		last-module)))
	50	(get-context-module))))
51	51	(if (or (null mod) (modexp-is-error mod))
52	52	(if (null mod)
53	53	(with-output-chaos-error ('invalid-module)

64	64	(setq target (get-bound-value (car pre-term))))
65	65	(unless target
66	66	(return-from do-eval-start-th nil))
67		(when (eq mod last-module)
	67	(when (eq mod (get-context-module))
68	68	(setq $$action-stack nil))
69	69	(reset-reduced-flag target)
70		(reset-target-term target last-module mod)))
	70	(reset-target-term target current-module mod)))
71	71	(t
72	72	(let ((parse-variables nil))
73	73	(let ((res (simple-parse current-module

75	75	cosmos)))
76	76	(when (term-is-an-error res)
77	77	(return-from do-eval-start-th nil))
78		(when (eq last-module mod)
	78	(when (eq (get-context-module) mod)
79	79	(setq $$action-stack nil))
80		(reset-target-term res last-module mod))))))
	80	(reset-target-term res current-module mod))))))
81	81	;; try use $$term
82	82	(progn
83	83	(when (or (null $$term) (eq 'void $$term))

85	85	(format t "no target term is given!")
86	86	(return-from do-eval-start-th nil)))
87	87	(check-apply-context mod)
88		(when (eq last-module mod)
	88	(when (eq (get-context-module) mod)
89	89	(setq $$action-stack nil))
90	90	(reset-reduced-flag $$term)
91		(reset-target-term $$term last-module mod)
92		)))
93		;; (clear-found-rules)
	91	(reset-target-term $$term (get-context-module) mod))))
94	92	(when (command-final) (command-display))
95	93	t)))
96	94

111	109	(setq $$subterm $$term)
112	110	(setq $$selection-stack nil)
113	111	(return-from eval-choose-command nil))
114		(with-in-module (last-module)
	112	(with-in-module ((get-context-module))
115	113	(multiple-value-bind (subterm-sort subterm)
116	114	(compute-selection $$subterm selectors)
117	115	(declare (ignore subterm-sort))

156	154	(with-output-chaos-error ('invalid-term)
157	155	(princ "term to be applied is not defined.")
158	156	))
159		(unless last-module
	157	(unless (get-context-module)
160	158	(with-output-chaos-error ('no-context-module)
161		(princ "no current module.")
162		))
	159	(princ "no current module.")))
163	160	;; real work begins here ------------------------------
164		(with-in-module (last-module)
	161	(with-in-module ((get-context-module))
165	162	(multiple-value-bind (subterm-sort subterm)
166	163	(compute-selection $$term selectors)
167	164	(setq -applied- t)
168	165	(case action
169	166	(:reduce ; full reduction on selections.
170		(!setup-reduction last-module)
	167	(!setup-reduction current-module)
171	168	(let ((rewrite-semantic-reduce
172		(module-has-behavioural-axioms last-module))
	169	(module-has-behavioural-axioms current-module))
173	170	(rewrite-exec-mode nil))
174	171	(term-replace subterm (@copy-term subterm))
175	172	(reset-reduced-flag subterm)
176		(rewrite subterm last-module)))
	173	(rewrite subterm current-module)))
177	174	(:breduce
178		(!setup-reduction last-module)
	175	(!setup-reduction current-module)
179	176	(let ((rewrite-semantic-reduce nil)
180	177	(rewrite-exec-mode nil))
181	178	(term-replace subterm (@copy-term subterm))
182	179	(reset-reduced-flag subterm)
183		(rewrite subterm last-module)))
	180	(rewrite subterm current-module)))
184	181	(:exec
185		(!setup-reduction last-module)
	182	(!setup-reduction current-module)
186	183	(let ((rewrite-semantic-reduce
187		(module-has-behavioural-axioms last-module))
	184	(module-has-behavioural-axioms current-module))
188	185	(rewrite-exec-mode t))
189	186	(term-replace subterm (@copy-term subterm))
190	187	(reset-reduced-flag subterm)
191		(rewrite subterm last-module)))
	188	(rewrite subterm current-module)))
192	189	;;
193	190	(:print ; print selections.
194	191	(format t "~&term ")

214	211	(update-lowest-parse $$term)
215	212	(when (nth 2 rule-spec) ; reverse order
216	213	(setq $$term (@copy-term $$term)))
217		(reset-target-term $$term last-module last-module))
218		) ; end :apply
	214	(reset-target-term $$term current-module current-module))) ; end :apply
219	215	(t (with-output-panic-message ()
220	216	(format t "unknown apply action : ~a" action)
221	217	(chaos-error 'unknown-action))))

450	446	(when (and rev (or (rule-is-builtin rule)
451	447	(eq (axiom-type rule) :rule)))
452	448	(format t "~&This rule cannot be applied reversed."))
453		(when (and last-module
	449	(when (and (get-context-module)
454	450	(not (rule-is-builtin rule)))
455	451	(format t "~&(This rule rewrites up.)"))))))))
456	452	t))

+9

-9

thstuff/eval-match.lisp less more

46	46	;;; ******
47	47
48	48	(defun eval-match-command (ast)
49		(unless last-module
	49	(unless (get-context-module)
50	50	(with-output-chaos-error ('no-current-module)
51	51	(princ "no current module.")))
52	52	(let ((type (%match-type ast))

57	57	$$subterm
58	58	$$term))
59	59	(t (let* ((parse-variables nil)
60		(parsed (with-in-module (last-module)
	60	(parsed (with-in-module ((get-context-module))
61	61	(simple-parse current-module
62	62	(%match-target ast)
63	63	cosmos))))

84	84
85	85	(defun find-rewrite-rules-top (target what &optional (type :match))
86	86	(let* ((real-target (supply-psuedo-variables target))
87		(patterns (find-matching-rules what real-target last-module type)))
	87	(patterns (find-matching-rules what real-target (get-context-module) type)))
88	88	(unless patterns
89		(with-in-module (last-module)
	89	(with-in-module ((get-context-module))
90	90	(format t "~&no rules found for term : ")
91	91	(term-print target))
92	92	(return-from find-rewrite-rules-top nil))
93	93	;; report the result
94	94	(format t "~&== matching rules to term : ")
95		(with-in-module (last-module)
	95	(with-in-module ((get-context-module))
96	96	(let ((fancy-print nil))
97	97	(term-print target))
98	98	(dolist (pat patterns)

127	127
128	128	(defun find-rewrite-rules-all (target what &optional (type :match))
129	129	(let* ((real-target (supply-psuedo-variables target))
130		(patterns (find-matching-rules-all what real-target last-module type)))
	130	(patterns (find-matching-rules-all what real-target (get-context-module) type)))
131	131	(unless patterns
132		(with-in-module (last-module)
	132	(with-in-module ((get-context-module))
133	133	(format t "~&no rules found for term : ")
134	134	(term-print target))
135	135	(return-from find-rewrite-rules-all nil))
136	136	;; report the result
137	137	(format t "~&== matching rules to term : ")
138		(with-in-module (last-module)
	138	(with-in-module ((get-context-module))
139	139	(let ((fancy-print nil))
140	140	(term-print target))
141	141	(dolist (pat patterns)

192	192	nil
193	193	'next-match)
194	194	'next-unify)))
195		(with-in-module (last-module)
	195	(with-in-module ((get-context-module))
196	196	(let* ((parse-variables (mapcar #'(lambda (x)
197	197	(cons (variable-name x) x))
198	198	(term-variables target)))