Commit b280d0e614cf4a7bfd42425a62f4f09e13646c75 - cafeobj

+1

-1

BigPink/codes/butils.lisp less more

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

+6

-10

BigPink/codes/commands.lisp less more

579	579	;;;
580	580	(defun eval-resolve (ast)
581	581	(let ((eval-context (get-context-module)))
582		(unless eval-context
583		(with-output-chaos-error ('no-context)
584		(princ "no context (current module) is set!")))
585	582	(let ((out-file (%resolve-arg ast)))
586	583	(if (and out-file (not (equal out-file ".")))
587	584	(with-open-file (stream out-file :direction :output

712	709	(result-as-text (%demod-return-text ast)))
713	710	(perform-demodulation* preterm modexp mode result-as-text)))
714	711
	712	;;; * TODO *
	713	;;; use reducer.
715	714	(defun perform-demodulation* (preterm &optional modexp mode (result-as-text nil))
716	715	(let ((consider-object t)
717	716	(rewrite-exec-mode (eq mode :exec))

724	723	(number-matches nil))
725	724	(let ((mod (if modexp
726	725	(eval-modexp modexp)
727		(get-context-module))))
728		(unless (eq mod (get-context-module))
	726	(get-context-module t))))
	727	(unless (eq mod (get-context-module t))
729	728	(clear-term-memo-table term-memo-table))
730	729	(if (or (null mod) (modexp-is-error mod))
731	730	(if (null mod)

735	734	(princ "incorrect module expression, no such module ")
736	735	(print-chaos-object modexp)))
737	736	(progn
738		(context-push-and-move (get-context-module) mod)
	737	(context-push-and-move (get-context-module t) mod)
739	738	(with-in-module (mod)
740	739	(auto-db-reset mod))
741	740	(with-proof-context (mod)
742	741	(when auto-context-change
743		(change-context (get-context-module) mod))
	742	(change-context (get-context-module t) mod))
744	743	(!setup-reduction mod)
745	744	(setq $$mod (get-context-module))
746	745	(setq sort cosmos)

867	866
868	867	;;; LEX
869	868	(defun eval-pn-lex (ast)
870		(unless (get-context-module)
871		(with-output-chaos-error ('no-context)
872		(princ "no context(current) module is specified.")))
873	869	(compile-module (get-context-module))
874	870	(with-in-module ((get-context-module))
875	871	(let ((optokens (%pn-lex-ops ast))

+1

-5

BigPink/codes/inv.lisp less more

771	771	(defun pn-check-invariance (args)
772	772	(declare (type list args))
773	773	(let ((target-module (get-context-module)))
774		(declare (type (or null module) target-module))
775		(unless target-module
776		(with-output-chaos-error ('no-context)
777		(princ "check invariance: no context module is specified!")))
778		;;
	774	(declare (type module target-module))
779	775	(compile-module target-module)
780	776	(multiple-value-bind (pred-name object-pat init-name loop-after
781	777	loop-after-sub

+2

-2

cafeobj/command-top.lisp less more

234	234	;;; CafeOBJ INTERPRETER TOPLEVEL HELP
235	235	;;;
236	236	(defun print-context-info ()
237		(let ((cmod (get-context-module)))
	237	(let ((cmod (get-context-module t)))
238	238	(cond ((null cmod)
239	239	(format t "~&You are at top level, no context module is set."))
240	240	(open-module

385	385	(defun print-cafeobj-prompt ()
386	386	(fresh-all)
387	387	(flush-all)
388		(let ((cur-module (get-context-module)))
	388	(let ((cur-module (get-context-module t)))
389	389	(cond ((eq prompt 'system)
390	390	(if cur-module
391	391	(if (module-is-inconsistent cur-module)

+44

-4

cafeobj/commands.lisp less more

2309	2309	:category :proof
2310	2310	:parser citp-parse-red
2311	2311	:evaluator eval-citp-red
2312		:title "`{ :red \| :exec \| :bred } <term> .`"
2313		:doc "TODO"
	2312	:title "`{ :red \| :exec \| :bred } [in <goal-name> :] <term> .`"
	2313	:doc "reduce the term in specified goal <goal-name>. "
2314	2314	)
2315	2315
2316	2316	(define (":verbose")

2342	2342	:parser citp-parse-ctf
2343	2343	:evaluator eval-citp-ctf
2344	2344	:title "`:ctf { eq [ <label-exp> ] <term> = <term> .}`"
	2345	:doc "TODO"
	2346	)
	2347
	2348	(define (":pctf")
	2349	:category :proof
	2350	:parser citp-parse-pctf
	2351	:evaluator eval-citp-pctf
	2352	:title "`:pctf { <bool-term> . ... <bool-term> .}`"
	2353	:doc "TODO"
	2354	)
	2355
	2356	(define (":pctf-")
	2357	:category :proof
	2358	:parser citp-parse-pctf
	2359	:evaluator eval-citp-pctf
	2360	:title "`:pctf- { <bool-term> . ... <bool-term> . }`"
2345	2361	:doc "TODO"
2346	2362	)
2347	2363

2383	2399	:category :proof
2384	2400	:parser citp-parse-spoiler
2385	2401	:evaluator identity
2386		:title "`:spoiler { on \| off}"
	2402	:title "`:spoiler { on \| off}`"
2387	2403	:doc "TODO"
2388	2404	)
	2405
	2406	(define (":binspect")
	2407	:category :proof
	2408	:parser parse-citp-binspect
	2409	:evaluator eval-citp-binspect
	2410	:title "`:binspect [in <goal-name> :] <boolean-term> .`"
	2411	:doc "TODO"
	2412	)
	2413
	2414	(define ("binspect")
	2415	:category :proof
	2416	:parser parse-citp-binspect
	2417	:evaluator eval-citp-binspect
	2418	:title "`binspect [in <module-name> :] <boolean-term> .`"
	2419	:doc "TODO"
	2420	)
	2421
	2422	; (define ("binspect")
	2423	; :cateogory :proof
	2424	; :parser parse-citp-binspect
	2425	; :evaluator eval-citp-binspect
	2426	; :title "`binspect [in <module-name> :] <boolean-term> .`"
	2427	; :doc "TODO"
	2428	; )
2389	2429
2390	2430	;;;
2391	2431

2410	2450	")
2411	2451
2412	2452	;;;
2413		) ; end eval-when
	2453	) ; end eval-when
2414	2454	;;; EOF

+4

-0

cafeobj/creader.lisp less more

807	807
808	808	\|}\|)
809	809	(\[ :term \|.\| \])))
	810	((:+ \|:pctf\| \|:pctf-\|)
	811	\|{\| (:many-of (\[ :term \|.\| \])) \|}\|)
810	812	((:+ \|:csp\| \|:csp-\|)
811	813	\|{\| (:many-of #.EqDeclaration
812	814	#.RlDeclaration

816	818	\|}\|)
817	819	((:+ \|:show\| \|:sh\| \|:describe\| \|:desc\|) :args)
818	820	(\|:spoiler\| (:one-of (on) (off) (\|.\|)))
	821	((:+ \|:binspect\|)
	822	(:rdr #..term-delimiting-chars. (:if-present in :symbol \|:\|)) (:seq-of :term) \|.\|)
819	823	)) ; end Top-Form
820	824
821	825	;; some separated definitions of non-terminals.

+3

-1

chaos/cafein/reducer.lisp less more

60	60	(rule-count 0)
61	61	(term-memo-hash-hit 0)
62	62	($$term nil)
	63	($$term-context nil)
63	64	($$cond nil)
64	65	($$target-term nil)
65	66	($$norm nil)

81	82	term-memo-hash-hit
82	83	$$target-term
83	84	$$term
	85	$$term-context
84	86	$$cond
85	87	$$target-term
86	88	$$norm

171	173
172	174	;; reset-term-memo-table
173	175	(defun reset-term-memo-table (module)
174		(unless (eq module (get-context-module))
	176	(unless (eq module (get-context-module t))
175	177	(clear-term-memo-table term-memo-table)))
176	178
177	179	;; prepare-reduction-env

+1

-0

chaos/cafein/rengine.lisp less more

49	49
50	50	(defconstant term-hash-mask #x1FFFFFFF)
51	51
	52	(declaim (type fixnum term-hash-size))
52	53	(defconstant term-hash-size 9001)
53	54
54	55	(defmacro method-has-memo-safe (m)

+1

-1

chaos/construct/axiom.lisp less more

894	894	(with-output-chaos-error ('invalid-rule-spec)
895	895	(format t "No rule number or name is specified.")))
896	896	;; get module in which the specified rule is looked up
897		(let ((cur-context (get-context-module)))
	897	(let ((cur-context (get-context-module t)))
898	898	(if (equal "" mod)
899	899	(setq mod cur-context)
900	900	(if (and cur-context

+2

-2

chaos/construct/operator.lisp less more

969	969	error-operator)
970	970	(declare (type list opinfo arity)
971	971	(type sort-struct coarity)
972		(type (or null module) module))
	972	(type module module))
973	973	;;
974	974	(let ((meth nil))
975	975	(dolist (m (opinfo-methods opinfo))

1398	1398	:test #'equal))
1399	1399	(eval-ast decl)))
1400	1400
1401		(defun setup-error-operators-in (&optional (module (or (get-context-module))))
	1401	(defun setup-error-operators-in (&optional (module (get-context-module)))
1402	1402	(declare (type module module)
1403	1403	(values t))
1404	1404	(let ((all-error-operators nil))

+4

-4

chaos/decafe/meval.lisp less more

75	75	(me (normalize-modexp modexp)))
76	76	;; "." -> current context module
77	77	(when (and (equal me ".")
78		(get-context-module))
79		(return-from eval-modexp (get-context-module)))
	78	(get-context-module t))
	79	(return-from eval-modexp (get-context-module t)))
80	80	(when (stringp me)
81	81	;; simple name
82	82	(let ((pos (position #\. (the simple-string me) :from-end t)))

93	93	(format t "~% no such module ~s" qual)))
94	94	(setf mod (find-module-in-env name context))))
95	95	(setq mod (find-module-in-env me (if also-local
96		(get-context-module)
	96	(get-context-module t)
97	97	nil))))))
98	98	(if mod
99	99	(if reconstruct-if-need

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

+1

-1

chaos/eval/chaos-top.lisp less more

137	137	(fresh-all)
138	138	(flush-all)
139	139	(format t "~%[")
140		(if (get-context-module)
	140	(if (get-context-module t)
141	141	(print-simple-mod-name (get-context-module))
142	142	(princ "*"))
143	143	(princ "]> ")))

+2

-2

chaos/eval/eval-ast.lisp less more

753	753	;;
754	754	(propagate-module-change modval)
755	755	;;
756		(when (eq modval (get-context-module))
	756	(when (eq modval (get-context-module t))
757	757	(reset-context-module)
758	758	(setq recover-same-context t))
759	759

803	803	(if recover-same-context
804	804	(reset-context-module real-mod)
805	805	(if auto-context?
806		(change-context (get-context-module) real-mod)))
	806	(change-context (get-context-module t) real-mod)))
807	807	;;
808	808	(unless (module-is-parameter-theory real-mod)
809	809	(print-in-progress " done."))

+43

-68

chaos/eval/eval-ast2.lisp less more

135	135	stat-form ; statistics in string
136	136	term-form) ; normalized term in string form
137	137	;; prepare rewriting context
138		(when (or (null mod) (modexp-is-error mod))
139		(if mod
140		(with-output-chaos-error ('no-such-module)
141		(princ "Incorrect module expression, no such module ")
142		(print-chaos-object modexp))
143		(with-output-chaos-error ('no-context)
144		(princ "No module expression provided, and no selected (current) module."))))
	138	(when (modexp-is-error mod)
	139	(with-output-chaos-error ('no-such-module)
	140	(princ "Incorrect module expression, no such module ")
	141	(print-chaos-object modexp)))
	142	;; set rewrting context
	143	(context-push-and-move (get-context-module t) mod)
	144	(when auto-context-change
	145	(change-context (get-context-module t) mod))
145	146	;; parse target term
146	147	(setq term (prepare-term preterm mod))
147		;; set rewrting context
148		(context-push-and-move (get-context-module) mod)
149		(when auto-context-change
150		(change-context (get-context-module) mod))
151	148	;; print out prelude message
152	149	(unless chaos-quiet
153	150	(with-in-module (mod)

192	189	(let ((mod (if modexp
193	190	(eval-modexp modexp)
194	191	(get-context-module))))
195		(if (or (null mod) (modexp-is-error mod))
196		(if (null mod)
197		(with-output-chaos-error ('no-context)
198		(princ "no module expression provided and no selected(current) module."))
199		(with-output-chaos-error ('no-such-module)
200		(princ "incorrect module expression, no such module ")
201		(print-chaos-object modexp)))
	192	(if (modexp-is-error mod)
	193	(with-output-chaos-error ('no-such-module)
	194	(princ "incorrect module expression, no such module ")
	195	(print-chaos-object modexp))
202	196	(progn
203		(context-push-and-move (get-context-module) mod)
	197	(context-push-and-move (get-context-module t) mod)
204	198	(setq sort cosmos)
205	199	(when auto-context-change
206		(change-context (get-context-module) mod)) ;;; what?
	200	(change-context (get-context-module t) mod)) ;;; what?
207	201	(with-in-module (mod)
208	202	(!setup-reduction current-module)
209	203	(setq $$mod current-module)

265	259	(defun do-parse-term* (preterm &optional modexp)
266	260	(let ((mod (if modexp
267	261	(eval-modexp modexp)
268		(get-context-module))))
269		(unless mod
270		(with-output-chaos-error ('no-context)
271		(princ "no module expression provided and no selected(current) module.")))
	262	(get-context-module)))
	263	(target-term nil))
272	264	(when (modexp-is-error mod)
273	265	(with-output-chaos-error ('no-such-module)
274	266	(princ "incorrect module expression, not such module: ")
275	267	(print-chaos-object modexp)))
276	268	;;
277		(context-push-and-move (get-context-module) mod)
	269	(context-push-and-move (get-context-module t) mod)
278	270	(with-in-module (mod)
279	271	(prepare-for-parsing current-module)
280	272	(let ((parse-variables nil))
281		(let ((res (simple-parse current-module preterm cosmos)))
282		(setq res (car (canonicalize-variables (list res) mod)))
283		;; ******** MEL
284		(when mel-sort
285		(!setup-reduction mod)
286		(setq res (apply-sort-memb res
287		mod)))
288		(reset-target-term res current-module mod)
289		;; ********
290		(format t "~%")
291		(term-print-with-sort res standard-output)
292		(flush-all))))
293		(context-pop-and-recover)))
	273	(setq target-term (car (canonicalize-variables (list (simple-parse current-module preterm cosmos)) mod)))
	274	;; ******** MEL
	275	(when mel-sort
	276	(!setup-reduction mod)
	277	(setq target-term (apply-sort-memb target-term mod)))
	278	(reset-target-term target-term current-module mod)
	279	;; ********
	280	(format t "~%")
	281	(term-print-with-sort target-term standard-output)
	282	(flush-all)))
	283	(context-pop-and-recover)
	284	(values target-term mod)))
294	285
295	286	;;; TODO
296	287	(defun red-loop (mod &optional prompt)

415	406	(if (or (null pat)
416	407	(member pat '(("none") ("off") ("nil") ("null"))))
417	408	(set-rewrite-stop-pattern 'none)
418		(let ((mod (or (get-context-module)
419		(with-output-chaos-error ('no-context)
420		(princ "no context (current) module is specified.")))))
	409	(let ((mod (get-context-module)))
421	410	(let* ((parse-variables (module-variables mod))
422	411	(term (simple-parse mod
423	412	pat cosmos)))

517	506	(princ "closing this module...") (print-next)
518	507	(eval-close-module nil)))
519	508	(setq open-module mod)
520		(setq last-before-open (get-context-module))
	509	(setq last-before-open (get-context-module t))
521	510	(clear-term-memo-table term-memo-table)
522	511	(let ((chaos-quiet t)
523	512	(copy-variables t)

537	526	(if open-module
538	527	(let ((omod (eval-modexp "%")))
539	528	(initialize-module omod)
540		(when (eq omod (get-context-module))
541		(change-context (get-context-module) last-before-open))
	529	(when (eq omod (get-context-module t))
	530	(change-context (get-context-module t) last-before-open))
542	531	(setq open-module nil)
543	532	(setq last-before-open nil))
544	533	(with-output-chaos-warning ()

1199	1188
1200	1189	;; operator strictness
1201	1190	(:strictness
1202		(let ((mod (or (get-context-module)
1203		(with-output-chaos-error ('no-context)
1204		(princ "no context (current) module.")))))
1205		;;
	1191	(let ((mod (get-context-module)))
1206	1192	(!setup-reduction mod)
1207	1193	(with-in-module (mod)
1208	1194	(if args

1245	1231	(format t ">> module is compatible."))))))
1246	1232	;;;
1247	1233	(:coherency
1248		(let ((mod (or (get-context-module)
1249		(with-output-chaos-error ('no-context)
1250		(princ "no context (current) module.")))))
1251		;;
	1234	(let ((mod (get-context-module)))
1252	1235	(!setup-reduction mod)
1253	1236	(with-in-module (mod)
1254	1237	(if args

1311	1294	(let ((mod (if modexp
1312	1295	(eval-modexp modexp)
1313	1296	(get-context-module))))
1314		;;
1315		(when (or (null mod) (modexp-is-error mod))
1316		(if (null mod)
1317		(with-output-chaos-error ('no-context)
1318		(princ "no module expression provided and no selected(current) module.")
1319		)
	1297	(when (modexp-is-error mod)
1320	1298	(with-output-chaos-error ('no-such-module)
1321	1299	(princ "incorrect module expression, no such module ")
1322		(print-chaos-object modexp)
1323		)))
	1300	(print-chaos-object modexp)))
1324	1301	;; process specified command
1325	1302	(case command
1326	1303	((:compile :compile-all)

1353	1330	(princ (cadr result)))
1354	1331	(force-output))
1355	1332	(progn
1356		(context-push-and-move (get-context-module) mod)
	1333	(context-push-and-move (get-context-module t) mod)
1357	1334	(let ((print-indent (+ 4 print-indent)))
1358	1335	(with-in-module (mod)
1359	1336	(setq $$term (car result))

1370	1347	(terpri)
1371	1348	(princ (cadr result)))
1372	1349	(force-output)
1373		(reset-target-term $$term (get-context-module) mod)))
	1350	(reset-target-term $$term (get-context-module t) mod)))
1374	1351	(context-pop-and-recover)))))
1375	1352	;;
1376	1353	(otherwise (with-output-panic-message ()

1446	1423	(number-matches 0))
1447	1424	(let ((mod (if modexp
1448	1425	(eval-modexp modexp)
1449		(get-context-module))))
	1426	(get-context-module t))))
1450	1427	(unless (eq mod (get-context-module))
1451	1428	(clear-term-memo-table term-memo-table))
1452	1429	(when (or (null mod) (modexp-is-error mod))

1456	1433	(with-output-chaos-error ('no-such-module)
1457	1434	(princ "no such module: ")
1458	1435	(print-chaos-object modexp))))
1459		(context-push-and-move (get-context-module) mod)
	1436	(context-push-and-move (get-context-module t) mod)
1460	1437	(when auto-context-change
1461		(change-context (get-context-module) mod))
	1438	(change-context (get-context-module t) mod))
1462	1439	(with-in-module (mod)
1463	1440	(!setup-reduction mod)
1464	1441	(setq $$mod current-module)

1584	1561	(modexp (%look-up-module ast))
1585	1562	(mod nil))
1586	1563	(setf mod (if (null modexp)
1587		(or (get-context-module)
1588		(with-output-chaos-error ('no-context)
1589		(format t "~%No context module is set.")))
	1564	(get-context-module)
1590	1565	(eval-modexp modexp)))
1591	1566	(when (modexp-is-error mod)
1592	1567	(with-output-chaos-error ('no-such-module)

+35

-38

chaos/eval/eval-mod.lisp less more

54	54	;;;
55	55	(defun eval-mod (toks &optional (change-context auto-context-change))
56	56	(if (null toks)
57		(or (get-context-module)
58		(with-output-chaos-error ('no-context)
59		(princ "no selected(current) module.")))
60		(if (equal '("%") toks)
61		(if open-module
62		(let ((mod (find-module-in-env (normalize-modexp "%"))))
63		(unless mod
64		(with-output-panic-message ()
65		(princ "could not find % module!!!!")
66		(chaos-error 'panic)))
67		(when change-context
68		(change-context (get-context-module) mod))
69		mod)
70		(with-output-chaos-warning ()
71		(princ "no module is opening.")
72		(chaos-error 'no-open-module)))
73		(let ((val (modexp-top-level-eval toks)))
74		(if (modexp-is-error val)
75		(if (and (null (cdr toks))
76		(<= 4 (length (car toks)))
77		(equal "MOD" (subseq (car toks) 0 3)))
78		(let ((val (read-from-string (subseq (car toks) 3))))
79		(if (integerp val)
80		(let ((nmod (print-nth-mod val))) ;;; !!!
81		(when change-context
82		(change-context (get-context-module) nmod))
83		nmod)
84		(with-output-chaos-error ('no-such-module)
85		(format t "could not evaluate the modexp ~a" toks))))
	57	(get-context-module)
	58	(if (equal '("%") toks)
	59	(if open-module
	60	(let ((mod (find-module-in-env (normalize-modexp "%"))))
	61	(unless mod
	62	(with-output-panic-message ()
	63	(princ "could not find % module!!!!")
	64	(chaos-error 'panic)))
	65	(when change-context
	66	(change-context (get-context-module t) mod))
	67	mod)
	68	(with-output-chaos-warning ()
	69	(princ "no module is opening.")
	70	(chaos-error 'no-open-module)))
	71	(let ((val (modexp-top-level-eval toks)))
	72	(if (modexp-is-error val)
	73	(if (and (null (cdr toks))
	74	(<= 4 (length (car toks)))
	75	(equal "MOD" (subseq (car toks) 0 3)))
	76	(let ((val (read-from-string (subseq (car toks) 3))))
	77	(if (integerp val)
	78	(let ((nmod (print-nth-mod val))) ;;; !!!
	79	(when change-context
	80	(change-context (get-context-module t) nmod))
	81	nmod)
86	82	(with-output-chaos-error ('no-such-module)
87		(format t "undefined module? ~a" toks)
88		))
89		(progn
90		(when change-context
91		(change-context (get-context-module) val))
92		val))))))
	83	(format t "could not evaluate the modexp ~a" toks))))
	84	(with-output-chaos-error ('no-such-module)
	85	(format t "undefined module? ~a" toks)))
	86	(progn
	87	(when change-context
	88	(change-context (get-context-module t) val))
	89	val))))))
93	90
94	91	;;; what to do with this one?
95	92

121	118	(sub (nth-sub (1- no) mod)))
122	119	(if sub
123	120	(when change-context
124		(change-context (get-context-module) sub))
	121	(change-context (get-context-module t) sub))
125	122	(progn (princ "** Waring : No such sub-module") (terpri) nil))))
126	123	((and (equal "param" it)
127	124	(cadr toks)

132	129	(param (nth (1- no) params)))
133	130	(if param
134	131	(when change-context
135		(change-context (get-context-module) (cdr param)))
	132	(change-context (get-context-module t) (cdr param)))
136	133	(with-output-chaos-error ('no-such-parameter)
137	134	(princ "No such parameter")
138	135	))))
139	136	((and (null toks) change-context force?)
140		(when (get-context-module)
	137	(when (get-context-module t)
141	138	(change-context (get-context-module) nil)))
142	139	(t (eval-mod toks change-context)))))
143	140

+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 (get-context-module)))
	45	(let ((mod (get-context-module t)))
46	46	(if mod
47	47	(with-in-module (mod)
48	48	(term-print (macro-lhs macro) stream)

+17

-13

chaos/primitives/context.lisp less more

47	47	nil))
48	48
49	49	;;; GET-CONTEXT-MODULE
50		(defun get-context-module ()
51		current-module)
	50	(defun get-context-module (&optional no-error)
	51	(or current-module
	52	(if no-error
	53	nil
	54	(with-output-chaos-error ('no-context)
	55	(format t "No context module is set.")))))
52	56
53	57	;;; RESET-CONTEXT-MODULE
54	58	(defun reset-context-module (&optional (mod nil))

57	61	;;; GET-OBJECT-CONTEXT object -> null \| module
58	62	;;;
59	63	(defun get-object-context (obj)
60		(or (get-context-module) (object-context-mod obj)))
	64	(or (get-context-module t) (object-context-mod obj)))
61	65
62	66	;;; BINDINGS *******************************************************************
63	67

106	110	(when (or (equal let-sym "$$term")
107	111	(equal let-sym "$$subterm"))
108	112	(with-output-chaos-error ('misc-error)
109		(princ "sorry, but you cannot use \"$$term\" or \"$$subterm\" as let variable.")
110		))
	113	(princ "sorry, but you cannot use \"$$term\" or \"$$subterm\" as let variable.")))
111	114	;;
112	115	(let* ((special nil)
113	116	(bindings (if (is-special-let-variable? let-sym)

148	151	$$subterm nil
149	152	$$action-stack nil
150	153	$$selection-stack nil
151		$$term-context nil
152	154	current-module nil
153	155	rewrite-stop-pattern nil)
154	156	(return-from new-context nil))

181	183	(if (eq mod old-mod)
182	184	(progn
183	185	(setq $$term term
	186	$$term-context mod
184	187	$$subterm term
185	188	$$selection-stack nil)
186	189	(save-context mod)
187	190	(new-context mod))
188	191	;; we do not change globals, instead set in context of mod.
189		(save-context mod)))
	192	(progn
	193	(setq $$term-context mod)
	194	(save-context mod))))
190	195	;;;
191	196	(defun context-push (mod)
192	197	(push mod old-context))

199	204	(change-context old new))
200	205
201	206	(defun context-pop-and-recover ()
202		(when (get-context-module)
203		(let ((old (context-pop)))
204		(unless (eq old (get-context-module))
205		;; eval-mod may change the current context implicitly.
206		;; in this case we do not recover context.
207		(change-context (get-context-module) old)))))
	207	(let ((old (context-pop)))
	208	(unless (eq old (get-context-module t))
	209	;; eval-mod may change the current context implicitly.
	210	;; in this case we do not recover context.
	211	(change-context (get-context-module t) old))))
208	212
209	213	;;; EOF
210	214

+1

-1

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 (get-context-module)))
	83	(let ((module (get-context-module t)))
84	84	(when (and module (not (module-p module)))
85	85	(setq module (find-module-in-env
86	86	(normalize-modexp (string module)))))

+3

-3

chaos/primitives/gen-print.lisp less more

595	595	(cond ((chaos-ast? object)
596	596	(let ((printer (ast-printer object)))
597	597	(if printer
598		(let ((mod (get-context-module)))
	598	(let ((mod (get-context-module t)))
599	599	(if mod
600	600	(with-in-module (mod)
601	601	(funcall printer object stream))

606	606	((and (chaos-object? object) (not (stringp object)))
607	607	(let ((printer (object-printer object)))
608	608	(if printer
609		(let ((mod (get-context-module)))
	609	(let ((mod (get-context-module t)))
610	610	(if mod
611	611	(with-in-module (mod)
612	612	(funcall printer object stream))

615	615	(print-pretty nil))
616	616	(prin1 object stream)))))
617	617	((term? object)
618		(let ((mod (get-context-module)))
	618	(let ((mod (get-context-module t)))
619	619	(if mod
620	620	(with-in-module (mod)
621	621	(term-print object stream))

+1

-1

chaos/primitives/normodexp.lisp less more

77	77	(setq modexp (car modexp)))
78	78	;;
79	79	(when (and (equal modexp "the-current-module")
80		(get-context-module))
	80	(get-context-module t))
81	81	(setq modexp (get-context-module)))
82	82	(cond ((module-p modexp) (normalize-modexp (module-name modexp)))
83	83	((stringp modexp) (canonicalize-simple-module-name modexp))

+1

-1

chaos/primitives/term-utils.lisp less more

823	823	;;; same as make-term-with-sort-check, but specialized to binary operators.
824	824
825	825	(defun make-term-with-sort-check-bin (meth subterms
826		&optional (module current-module))
	826	&optional (module (get-context-module)))
827	827	(declare (type method meth)
828	828	(type list subterms)
829	829	(type (or null module) module)

+0

-3

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

1681	1681	terletox-list))
1682	1682
1683	1683	(defun test-sort-memb-predicate (term &optional (module (get-context-module)))
1684		(unless module
1685		(with-output-chaos-error ('no-context)
1686		(princ "checking _:_, no context module is given!")))
1687	1684	(with-in-module (module)
1688	1685	(let ((arg1 (term-arg-1 term))
1689	1686	(id-const (term-arg-2 term)))

+0

-5

chaos/tools/compat.lisp less more

40	40	;;; CHECK COMPATIBILITY
41	41	;;;
42	42	(defun check-compatibility (&optional (module (get-context-module)))
43		(unless module
44		(with-output-chaos-error ('no-context)
45		(princ "no context (current) module is specified!")))
46		;;
47	43	(unless on-preparing-for-parsing
48	44	(prepare-for-parsing module))
49		;;
50	45	(with-in-module (module)
51	46	(let ((rules (module-all-rules module))
52	47	(non-decreasing-rules nil))

+0

-5

chaos/tools/op-check.lisp less more

50	50	(defun check-method-strictness (meth &optional
51	51	(module (get-context-module))
52	52	report?)
53
54		(unless module
55		(with-output-chaos-error ('no-cntext)
56		(princ "checking lazyness: no context module is specified!")))
57		;;
58	53	(with-in-module (module)
59	54	(cond ((and (null (method-rules-with-different-top meth))
60	55	(rule-ring-is-empty (method-rules-with-same-top meth)))

+16

-36

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 (get-context-module) mod)
	52	(if (eq (get-context-module t) 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 (get-context-module) mod)
	56	(context-push-and-move (get-context-module t) mod)
57	57	(with-in-module (mod)
58	58	(format t "~%[module] ")
59	59	(print-chaos-object current-module)

80	80	;;; SHOW BINDINGS
81	81
82	82	(defun show-bindings (&optional (module (get-context-module)))
83		(unless module
84		(with-output-msg ()
85		(princ "no context (current module) is specified.")
86		(return-from show-bindings nil)))
87	83	(with-in-module (module)
88	84	(let ((bindings (module-bindings current-module)))
89	85	(format t "~&[bindings] ")

107	103	;;; show apply selection
108	104
109	105	(defun show-apply-selection (&optional (module (get-context-module)))
110		(unless module
111		(with-output-msg ()
112		(princ "no context (current module) is specified.")
113		(return-from show-apply-selection nil)))
	106	(declare (ignore module)) ; TODO
114	107	(when $$term-context
115	108	(with-in-module ($$term-context)
116	109	(format t "$$subterm = ")

141	134	;;; print-pending
142	135	;;;
143	136	(defun print-pending (&optional (module (get-context-module)))
144		(unless module
145		(with-output-msg ()
146		(princ "no context (current module) is specified.")
147		(return-from print-pending nil)))
148	137	(with-in-module (module)
149	138	(format t"~&[pending actions] ")
150	139	(if (null $$action-stack)

182	171	(with-output-chaos-warning ()
183	172	(format t "unknown option for `show term' : ~a" tree?))
184	173	(return-from show-term nil))
185		(unless (get-context-module)
	174	(unless (get-context-module t)
186	175	(with-output-msg ()
187	176	(princ "no current context, `select' some module first.")
188	177	(return-from show-term nil)))

381	370	(with-output-msg ()
382	371	(format t "no such module ~a" modexp)
383	372	(return-from show-sort nil))))
384		(t (setq mod (get-context-module))
385		(unless (module-p mod)
386		(with-output-msg ()
387		(princ "no context(current) module, select some first.")
388		(return-from show-sort nil)))))
	373	(t (setq mod (get-context-module))))
389	374	(with-in-module (mod)
390	375	(let ((srt (find-sort-in mod sort-n)))
391	376	(if srt

429	414	(print-next)
430	415	(princ "no such module ")
431	416	(princ (%opref-module parsedop))))))
432		(t (setq mod (get-context-module))
433		(unless mod
434		(with-output-chaos-error ('no-context)
435		(princ "no context module is given.")))))
	417	(t (setq mod (get-context-module))))
436	418	mod))
437	419
438	420	(defun resolve-operator-reference (opref &optional (no-error nil))

489	471	(let ((mod (if toks
490	472	(eval-mod-ext toks)
491	473	(get-context-module))))
492		(unless mod
493		(with-output-msg ()
494		(format t "no context (current module) is specified.")
495		(return-from show-param nil)))
	474	(when (modexp-is-error mod)
	475	(with-output-chaos-error ('invalid-modexp)
	476	(format t "Invalid module expression: ~s" toks)))
496	477	(let ((param (find-parameterized-submodule no mod)))
497	478	(if (and param (not (modexp-is-error param)))
498	479	(progn
499	480	(with-in-module (param)
500	481	(if describe
501	482	(describe-module param)
502		(show-module param)))
	483	(show-module param)))
503	484	(terpri))
504		(with-output-msg ()
505		(if (null (module-parameters mod))
506		(princ "module has no parameters.")
507		(format t "no such parameter ~a" (if (integerp no)
508		(1+ no)
509		no))))))
510		))
	485	(with-output-msg ()
	486	(if (null (module-parameters mod))
	487	(princ "module has no parameters.")
	488	(format t "no such parameter ~a" (if (integerp no)
	489	(1+ no)
	490	no))))))))
511	491
512	492	;;; ************
513	493	;;; SHOW MODULES

+2

-1

sysdef.asd less more

187	187	(:file "case")
188	188	(:file "proof-struct")
189	189	(:file "apply-tactic")
190		(:file "citp")))
	190	(:file "citp")
	191	(:file "bterm-inspector")))
191	192	(:module "BigPink"
192	193	:components ((:module codes
193	194	:serial t

+2

-1

sysdef.cl less more

233	233	"thstuff/case"
234	234	"thstuff/proof-struct"
235	235	"thstuff/apply-tactic"
236		"thstuff/citp"))
	236	"thstuff/citp"
	237	"thstuff/bterm-inspector"))
237	238	(:module-group :bigpink
238	239	(:definitions
239	240	"BigPink/codes/types"

+10

-8

thstuff/apply-tactic.lisp less more

2251	2251	(defun reduce-in-goal (mode goal-name token-seq)
2252	2252	(with-citp-debug ()
2253	2253	(format t "~%~s in ~s : ~s" (string mode) goal-name token-seq))
2254		(let ((next-goal-node (if goal-name
2255		(find-goal-node proof-tree goal-name)
2256		(get-next-proof-context proof-tree))))
2257		(unless next-goal-node
2258		(with-output-chaos-error ('no-target)
2259		(if goal-name
2260		(format t ":~a could not find the goal ~s." mode goal-name)
2261		(format t "No default target goal."))))
	2254	(let ((next-goal-node (get-target-goal-node goal-name)))
2262	2255	;; do rewriting
2263	2256	(perform-reduction* token-seq (goal-context (ptree-node-goal next-goal-node)) mode)))
2264	2257

2458	2451	(pr-goal (ptree-node-goal gn))))
2459	2452	(ptree-node-subnodes ptree-node))))))
2460	2453
	2454	;;; :pctf or :pctf-
	2455	;;;
	2456	(defun apply-pctf (s-forms dash? &optional (verbose citp-verbose))
	2457	;; TODO
	2458	s-forms
	2459	dash?
	2460	verbose
	2461	)
	2462
2461	2463	;;; -----------------------------------------------------
2462	2464	;;; :csp or :csp-
2463	2465	;;;

+408

-0

thstuff/bterm-inspector.lisp less more

	0	;;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
	1	;;;
	2	;;; Copyright (c) 2000-2014, Toshimi Sawada. All rights reserved.
	3	;;;
	4	;;; Redistribution and use in source and binary forms, with or without
	5	;;; modification, are permitted provided that the following conditions
	6	;;; are met:
	7	;;;
	8	;;; * Redistributions of source code must retain the above copyright
	9	;;; notice, this list of conditions and the following disclaimer.
	10	;;;
	11	;;; * Redistributions in binary form must reproduce the above
	12	;;; copyright notice, this list of conditions and the following
	13	;;; disclaimer in the documentation and/or other materials
	14	;;; provided with the distribution.
	15	;;;
	16	;;; THIS SOFTWARE IS PROVIDED BY THE AUTHOR 'AS IS' AND ANY EXPRESSED
	17	;;; OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
	18	;;; WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
	19	;;; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
	20	;;; DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
	21	;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
	22	;;; GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
	23	;;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
	24	;;; WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
	25	;;; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
	26	;;; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
	27	;;;
	28	(in-package :chaos)
	29	#\|=============================================================================
	30	System:CHAOS
	31	Module:thstuff
	32	File:bool-term.lisp
	33	=============================================================================\|#
	34	#-:chaos-debug
	35	(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
	36	#+:chaos-debug
	37	(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
	38
	39	(defvar debug-bterm nil)
	40	;;;=============================================================================
	41	;;; Utilities to support investigating big boolean term of xor-and normal form.
	42	;;;=============================================================================
	43
	44	;;; *********
	45	;;; TERM HASH
	46	;;; *********
	47	(declaim (type fixnum bterm-hash-size))
	48	(defconstant bterm-hash-size 1001)
	49
	50	(let ((.bterm-hash. nil)
	51	(bvar-num 0))
	52	(declare (type fixnum bvar-num))
	53
	54	(defun clear-bterm-memo-table ()
	55	(dotimes (x bterm-hash-size)
	56	(setf (svref .bterm-hash. x) nil)))
	57
	58	(defun bterm-hash ()
	59	.bterm-hash.)
	60
	61	(defun bterm-hash-ref (index)
	62	(declare (type fixnum index))
	63	(svref .bterm-hash. index))
	64
	65	(defun dump-bterm-hash ()
	66	(with-in-module ((get-context-module))
	67	(dotimes (x bterm-hash-size)
	68	(let ((ent (svref .bterm-hash. x)))
	69	(when ent
	70	(format t "~%(~d): " x)
	71	(let ((print-indent (+ print-indent 2)))
	72	(dolist (elt ent)
	73	(print-next)
	74	(term-print-with-sort (car elt))
	75	(princ " \|-> ")
	76	(term-print-with-sort (cdr elt)))))))))
	77
	78	(defun reset-bvar ()
	79	(setq bvar-num 0)
	80	(unless .bterm-hash.
	81	(setq .bterm-hash. (alloc-svec bterm-hash-size)))
	82	(clear-bterm-memo-table))
	83
	84	(defun make-bterm-variable ()
	85	(let ((varname (intern (format nil "P-~d" (incf bvar-num)))))
	86	(make-variable-term bool-sort varname)))
	87
	88	(defun get-hashed-bterm-variable (term)
	89	(let ((val (hash-term term))
	90	(var nil))
	91	(declare (type fixnum val))
	92	(let* ((ind (mod val bterm-hash-size))
	93	(ent (svref .bterm-hash. ind)))
	94	(setq var (cdr (assoc term ent :test #'term-is-similar?)))
	95	(if var
	96	var
	97	(progn
	98	(setf var (make-bterm-variable))
	99	(setf (svref .bterm-hash. ind) (cons (cons term var) ent))
	100	var)))))
	101
	102	)
	103
	104	;;; =======================================================================
	105	;;; ABSTRACTED representation of a _xor_-_and_ normal form of boolean term.
	106
	107	;;; ABS-BTERM:
	108	;;; abstracted boolean term.
	109	;;; each non _and_ or _xor_ boolean sub-term is abstracted by a
	110	;;; variable.
	111	(defstruct (abst-bterm (:print-function print-abst-bterm))
	112	; by variables
	113	(term nil) ; the original term
	114	(subst nil) ; list of substitution
	115	; or instance of abst-bterm(for _and_ abstraction)
	116	)
	117
	118	(defstruct (abst-and (:include abst-bterm)))
	119
	120	(defun print-abst-bterm (bt stream &rest ignore)
	121	(declare (ignore ignore))
	122	(with-in-module ((get-context-module))
	123	(princ ":abt[" stream)
	124	(let ((print-indent (+ 2 print-indent))
	125	(num 0))
	126	(declare (type fixnum print-indent num))
	127	(dolist (sub (abst-bterm-subst bt))
	128	(print-next nil print-indent stream)
	129	(format stream "(~d) " (incf num))
	130	(if (abst-bterm-p sub)
	131	(print-abst-bterm sub stream)
	132	(progn
	133	(let ((var (car sub))
	134	(term (cdr sub)))
	135	(term-print-with-sort var)
	136	(princ " \|-> ")
	137	(term-print-with-sort term))))))
	138	(princ " ]" stream)))
	139
	140	;;;
	141	(defun find-bvar-subst (var bterm)
	142	(declare (type abst-bterm bterm))
	143	(dolist (sub (abst-bterm-subst bterm))
	144	(if (abst-bterm-p sub)
	145	(find-bvar-subst var sub)
	146	(when (variable= var (car sub))
	147	(return-from find-bvar-subst (cdr sub)))))
	148	nil)
	149
	150	;;;
	151	;;; abstract-boolen-term : bool-term -> abst-bterm
	152	;;;
	153
	154	;;; xtract-xor-subterms : term
	155	;;; returns ac subterms of the given term iff the top op is _xor_
	156	(defun xtract-xor-subterms (term)
	157	(let ((args (if (method= (term-head term) bool-xor)
	158	(list-ac-subterms term bool-xor)
	159	nil)))
	160	args))
	161
	162	;;; xtract-and-subterms : term
	163	;;; returns ac subterms of the given term iff the top op is _and_
	164	(defun xtract-and-subterms (term)
	165	(if (method= (term-head term) bool-and)
	166	(list-ac-subterms term bool-and)
	167	nil))
	168
	169	(defun make-and-abstraction (term subterms)
	170	(let ((subst nil))
	171	(dolist (sub subterms)
	172	(push (cons (get-hashed-bterm-variable sub) sub) subst))
	173	(make-abst-and :term term :subst (nreverse subst))))
	174
	175	(defun abstract-boolean-term (term)
	176	(let ((bterm (make-abst-bterm :term term))
	177	(xor-subs (xtract-xor-subterms term))
	178	(subst nil))
	179	;; reset variable number & term hash
	180	(reset-bvar)
	181	(if xor-subs
	182	;; top operator is _xor_
	183	;; we further decompose by _and_
	184	(dolist (xs xor-subs)
	185	(let ((as (xtract-and-subterms xs)))
	186	(if as
	187	(push (make-and-abstraction xs as) subst)
	188	(push (cons (get-hashed-bterm-variable xs) xs) subst))))
	189	;; top operator is not xor
	190	(let ((as (xtract-and-subterms term)))
	191	(when as
	192	(push (make-and-abstraction term as) subst))))
	193	(setf (abst-bterm-subst bterm) (nreverse subst))
	194	bterm))
	195
	196	;;;
	197	;;; make-bterm-representation : bterm -> boolen term
	198	;;; from bterm make a concrete representation of abstracted boolean term
	199	;;;
	200	(defun make-and-representation (abst-and)
	201	(declare (type abst-and abst-and))
	202	(make-right-assoc-normal-form bool-and
	203	(mapcar #'car (abst-and-subst abst-and))))
	204
	205	(defun make-xor-representation (bterm)
	206	(declare (type abst-bterm bterm))
	207	(make-right-assoc-normal-form bool-xor
	208	(mapcar #'(lambda (x) (if (abst-and-p x)
	209	(make-and-representation x)
	210	(car x)))
	211	(abst-bterm-subst bterm))))
	212
	213	(defun make-bterm-representation (bterm)
	214	(let ((subst (abst-bterm-subst bterm)))
	215	;; no _xor nor _and_ ops in original term
	216	(unless subst
	217	(return-from make-bterm-representation (abst-bterm-term bterm)))
	218	;; sole _and_ term.
	219	(when (and (null (cdr subst))
	220	(abst-and-p (car subst)))
	221	(return-from make-bterm-representation (make-and-representation (car subst))))
	222	;; _xor_ normal form
	223	(make-xor-representation bterm)))
	224
	225	;;; ===========================================================================================
	226	;;; PRINTERS
	227	;;; abst-bterm printers
	228
	229	;;; simple-print-bterm : bterm -> void
	230	(defun simple-print-bterm (bterm)
	231	(declare (type abst-bterm bterm))
	232	(let ((aterm (make-bterm-representation bterm)))
	233	(term-print-with-sort aterm)))
	234
	235	;;; print-bterm-tree : bterm -> void
	236	(defun print-bterm-tree (bterm &optional (mode :vertical))
	237	(declare (type abst-bterm bterm)
	238	(ignore mode)) ; for NOW ** TODO for :vertical
	239	(let ((aterm (make-bterm-representation bterm)))
	240	(print-term-graph aterm chaos-verbose)))
	241
	242	;;; print-abs-bterm : bterm &key mode
	243	;;; mode :simple print term representation
	244	;;; :tree print term representation as vertical tree structure
	245	;;; :horizontal print term representation horizontal tree structure
	246	;;; also shows a substitution used for abstruction.
	247	;;;
	248	(defun print-abs-bterm (bterm &key (mode :simple))
	249	(case mode
	250	(:simple (simple-print-bterm bterm))
	251	(:tree (print-bterm-tree bterm))
	252	(:horizontal (print-bterm-tree bterm :horizontal))
	253	(otherwise
	254	(with-output-chaos-error ('invalid-mode)
	255	(format t "Invalid print mode ~a." mode))))
	256	;; shows substitution
	257	(format t "~%, where")
	258	(dolist (subst (abst-bterm-subst bterm))
	259	(format t "~%~4T~A \|-> " (variable-name (car subst)))
	260	(term-print-with-sort (cdr subst)))
	261	)
	262
	263	;;; ===========================================================================================
	264	;;; RESOLVER
	265	;;; computes possible solutions (assignments) which makes abstracted boolean term to be 'true.'
	266	;;;
	267
	268	;;; assign-tf
	269	;;; make all posssible variable substitutions with the domain {'true' ,'false'}.
	270	;;;
	271	(defun make-tf-combination (rows columns)
	272	(let ((assignment nil)
	273	(subst (make-array (list rows columns))))
	274	(flet ((change-parity ()
	275	(if (is-true? assignment)
	276	(setq assignment bool-false)
	277	(setq assignment bool-true))))
	278	(dotimes (c columns)
	279	(setq assignment nil)
	280	(let ((cycle (expt 2 c)))
	281	(dotimes (r rows)
	282	(if (not assignment)
	283	(setq assignment bool-true)
	284	(if (= 0 (mod r cycle))
	285	(change-parity)))
	286	#\|\|
	287	(when debug-bterm
	288	(format t "~%cycle=~d, columns=~d, row=~d: ~s" cycle c r (if (is-true? assignment)
	289	"true"
	290	"false")))
	291	\|\|#
	292	(setf (aref subst r c) assignment))))
	293	subst)))
	294
	295	(defun assign-tf (list-vars)
	296	(let* ((columns (length list-vars))
	297	(rows (expt 2 columns))
	298	(assignments (make-tf-combination rows columns))
	299	(l-subst nil))
	300	(dotimes (r rows)
	301	(let ((subst nil))
	302	(dotimes (c columns)
	303	(push (cons (nth c list-vars) (aref assignments r c)) subst))
	304	(push (nreverse subst) l-subst)))
	305	(when debug-bterm
	306	(with-in-module ((get-context-module))
	307	(let ((num 0))
	308	(dolist (sub (reverse l-subst))
	309	(format t "~%(~d): " (incf num))
	310	(print-substitution sub)))))
	311	(nreverse l-subst)))
	312
	313	;;;
	314	;;; resolve-abst-bterm : bterm
	315	;;; retuns a list of substitution which makes bterm to be true.
	316	;;;
	317	(defun resolve-abst-bterm (bterm &optional (module (get-context-module)))
	318	(declare (type abst-bterm bterm))
	319	(let* ((abst-term (make-bterm-representation bterm))
	320	(variables (term-variables abst-term))
	321	(list-subst (assign-tf variables))
	322	(answers nil))
	323	(dolist (subst list-subst)
	324	(let ((target (substitution-image-cp subst abst-term)))
	325	(when debug-bterm
	326	(with-in-module ((get-context-module))
	327	(format t "~%[resolver_target] ")
	328	(term-print-with-sort target)))
	329	(reducer-no-stat target module :red)
	330	(when debug-bterm
	331	(with-in-module ((get-context-module))
	332	(format t "~% --> ")
	333	(term-print-with-sort target)))
	334	(when (is-true? target)
	335	(push subst answers))))
	336	answers))
	337
	338	;;; try-resolve-boolean-term : term -> Values (abst-bterm List(substitution))
	339	;;;
	340	(defvar abst-bterm nil)
	341	(defvar abst-bterm-representation nil)
	342
	343	(defun try-resolve-boolean-term (term &optional (module (get-context-module)))
	344	(unless (sort= (term-sort term) bool-sort)
	345	(with-output-chaos-warning ()
	346	(format t "Given term is not of sort Bool. Ignored.")
	347	(return-from try-resolve-boolean-term nil)))
	348	(multiple-value-bind (target app?)
	349	(normalize-term-in module term)
	350	(declare (ignore app?))
	351	;; abstract
	352	(let ((bterm (abstract-boolean-term target)))
	353	(setq abst-bterm bterm)
	354	(setq abst-bterm-representation
	355	(make-bterm-representation bterm))
	356	(let ((print-indent (+ 2 print-indent)))
	357	(format t "~%** Abstracted boolean term:")
	358	(with-in-module (module)
	359	(print-next)
	360	(term-print-with-sort abst-bterm-representation)
	361	(format t "~%,where")
	362	(let ((print-indent (+ 2 print-indent)))
	363	(dolist (var (term-variables abst-bterm-representation))
	364	(let ((mapping (find-bvar-subst var bterm)))
	365	(unless mapping
	366	(with-output-chaos-error ('internal-err)
	367	(format t "Could not find the mapping of variable ~a." (variable-name var))))
	368	(print-next)
	369	(term-print-with-sort var)
	370	(princ " \|-> ")
	371	(term-print-with-sort mapping))))
	372	;; find answers
	373	(let ((ans (resolve-abst-bterm bterm module)))
	374	(cond (ans
	375	(format t "~%** The following assignment(s) can make the term 'true'.")
	376	(let ((num 0))
	377	(declare (type fixnum num))
	378	(let ((print-indent (+ 2 print-indent)))
	379	(dolist (sub ans)
	380	(print-next)
	381	(format t "(~d): " (incf num))
	382	(print-substitution sub)))))
	383	(t
	384	(format t "~%** No solution was found.")))
	385	(values bterm ans)))))))
	386
	387	;;;
	388	(defun binspect-in-goal (goal-name preterm)
	389	(let* ((goal-node (get-target-goal-node goal-name))
	390	(context-module (goal-context (ptree-node-goal goal-node)))
	391	(target (do-parse-term* preterm context-module)))
	392	(try-resolve-boolean-term target context-module)))
	393
	394	(defun binspect-in-module (mod-name preterm)
	395	(multiple-value-bind (target context-module)
	396	(do-parse-term* preterm mod-name)
	397	(try-resolve-boolean-term target context-module)))
	398
	399	;;; TOP LEVEL FUNCTION
	400	;;; binspect-in
	401	(defun binspect-in (mode goal-or-module-name preterm)
	402	(cond ((eq mode :citp)
	403	(binspect-in-goal goal-or-module-name preterm))
	404	(t
	405	(binspect-in-module goal-or-module-name preterm))))
	406
	407	;;; EOF

+0

-3

thstuff/cexec.lisp less more

1322	1322	(let ((module (get-context-module))
1323	1323	max-r
1324	1324	max-d)
1325		(unless module
1326		(with-output-chaos-error ('no-context)
1327		(format t "no context module..")))
1328	1325	(if (integerp max-result)
1329	1326	(setq max-r max-result)
1330	1327	(if (term-is-builtin-constant? max-result)

+58

-1

thstuff/citp.lisp less more

181	181	((":bred") (setq mode :bred)))
182	182	(if (= 4 (length e))
183	183	(progn
184		(setq goal-name (cadr (cadr e))); (find-goal-node proof-tree (cadr (cadr e)))
	184	(setq goal-name (cadr (cadr e)))
185	185	(setq preterm (nth 2 e)))
186	186	(progn
187	187	(setq goal-name nil)

213	213	(if (equal (first args) ":ctf-")
214	214	(cons form (cons term? :dash))
215	215	(cons form (cons term? nil)))))
	216
	217	;;; citp-parse-pctf
	218	;;; :pctf { [<term> .] ... [<term> . ] }
	219	;;; (":pctf" "{" (("[" (<Term>1) "." "]") ... ("[" (<Termn>) "." "]")) "}")
	220	;;; ==> (:pctf-? <Term1> ... <Termn>)
	221	(defun citp-parse-pctf (args)
	222	(let ((pctf-minus? (equal (car args) ":pctf-"))
	223	(list-terms (third args))
	224	(pre-terms nil))
	225	(print list-terms)
	226	(dolist (lt list-terms)
	227	(push (second lt) pre-terms))
	228	(cons pctf-minus? (nreverse pre-terms))))
216	229
217	230	;;; citp-parse-csp
218	231	;;; :csp { <axiom> ... }

250	263	(format t "~&:spoiler flag is ~s" (if citp-spoiler "on" "off"))))
251	264	t))
252	265
	266	;;;
	267	;;; {:binspect \| binspect} [in <goal-name> : ] <boolean-term> .
	268	;;;
	269	(defun parse-citp-binspect (args)
	270	(let (mode
	271	goal-name
	272	preterm)
	273	(if (equal (first args) ":binspect")
	274	(setq mode :citp)
	275	(setq mode :general))
	276	(if (= 4 (length args))
	277	(progn
	278	(setq goal-name (cadr (cadr args)))
	279	(setq preterm (nth 2 args)))
	280	(progn
	281	(setq goal-name nil)
	282	(setq preterm (nth 1 args))))
	283	(list mode goal-name preterm)))
	284
	285
	286
253	287	;;; ================================
254	288	;;; CITP related command evaluators
255	289	;;; ================================

363	397	(reset-rewrite-counters)
364	398	(begin-rewrite)
365	399	(apply-ctf (car ax-form) (cadr ax-form) (cddr ax-form))
	400	(end-rewrite)
	401	(report-citp-stat)
	402	(check-success proof-tree)))
	403
	404	;;; :pctf
	405	;;;
	406	(defun eval-citp-pctf (ax-form)
	407	(check-ptree)
	408	(with-in-module (current-module)
	409	(reset-rewrite-counters)
	410	(begin-rewrite)
	411	;; TODO
	412	ax-form
	413	;; (apply-pctf (car ax-form) (cadr ax-form) (cddr ax-form))
366	414	(end-rewrite)
367	415	(report-citp-stat)
368	416	(check-success proof-tree)))

402	450	(t (with-output-chaos-error ('unknown)
403	451	(format t "Unknown parameter to :show/:describe ~S" target))))))
404	452
	453
	454	;;; :binspect
	455	;;;
	456	(defun eval-citp-binspect (args)
	457	(let ((mode (first args))
	458	(goal-or-mod (second args))
	459	(preterm (third args)))
	460	(binspect-in mode goal-or-mod preterm)))
	461
405	462	;;; EOF

+76

-83

thstuff/eval-apply.lisp less more

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 (get-context-module))
68		(setq $$action-stack nil))
	67	(setq $$action-stack nil)
69	68	(reset-reduced-flag target)
70	69	(reset-target-term target current-module mod)))
71	70	(t

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

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

146	143	(where-spec (%apply-where-spec ast))
147	144	(selectors (%apply-selectors ast)))
148	145	(catch 'apply-context-error
149		(if (eq action :help)
150		(apply-help)
151		(progn
152		;; check some evaluation env
153		(when (or (null $$term) (eq 'void $$term))
154		(with-output-chaos-error ('invalid-term)
155		(princ "term to be applied is not defined.")
156		))
157		(unless (get-context-module)
158		(with-output-chaos-error ('no-context-module)
159		(princ "no current module.")))
160		;; real work begins here ------------------------------
161		(with-in-module ((get-context-module))
162		(multiple-value-bind (subterm-sort subterm)
163		(compute-selection $$term selectors)
164		(setq -applied- t)
165		(case action
166		(:reduce ; full reduction on selections.
167		(!setup-reduction current-module)
168		(let ((rewrite-semantic-reduce
169		(module-has-behavioural-axioms current-module))
170		(rewrite-exec-mode nil))
171		(term-replace subterm (@copy-term subterm))
172		(reset-reduced-flag subterm)
173		(rewrite subterm current-module)))
174		(:breduce
175		(!setup-reduction current-module)
176		(let ((rewrite-semantic-reduce nil)
177		(rewrite-exec-mode nil))
178		(term-replace subterm (@copy-term subterm))
179		(reset-reduced-flag subterm)
180		(rewrite subterm current-module)))
181		(:exec
182		(!setup-reduction current-module)
183		(let ((rewrite-semantic-reduce
184		(module-has-behavioural-axioms current-module))
185		(rewrite-exec-mode t))
186		(term-replace subterm (@copy-term subterm))
187		(reset-reduced-flag subterm)
188		(rewrite subterm current-module)))
189		;;
190		(:print ; print selections.
191		(format t "~%term ")
192		(disp-term subterm)
193		(format t "~&tree form")
194		(print-term-tree subterm))
195		(:apply ; apply specified rule.
196		(setq -applied- nil)
197		(let* ((actrule (compute-action-rule rule-spec
198		substitution
199		selectors))
200		(-inside-apply-with-extensions-
201		(and
202		(let ((arlhs (rule-lhs actrule)))
203		(and (term-is-application-form? arlhs)
204		(method-is-associative (term-head arlhs)))))))
205		(if (eq :within where-spec)
206		(let ((-inside-apply-all- t))
207		(catch 'apply-all-quit
208		(@apply-all actrule subterm-sort subterm)))
209		(@apply-rule actrule subterm-sort subterm)))
210		(when -applied-
211		(update-lowest-parse $$term)
212		(when (nth 2 rule-spec) ; reverse order
213		(setq $$term (@copy-term $$term)))
214		(reset-target-term $$term current-module current-module))) ; end :apply
215		(t (with-output-panic-message ()
216		(format t "unknown apply action : ~a" action)
217		(chaos-error 'unknown-action))))
218		;;
219		(unless -applied-
220		(with-output-chaos-warning ()
221		(princ "rule not applied")))
222		;;
223		(command-final)
224		(command-display))))))))
	146	(when (eq action :help)
	147	(apply-help)
	148	(return-from eval-apply-command nil))
	149	;; check some evaluation env
	150	(when (or (null $$term) (eq 'void $$term))
	151	(with-output-chaos-error ('invalid-term)
	152	(princ "term to be applied is not defined.")))
	153	;; real work begins here ------------------------------
	154	(with-in-module ((get-context-module))
	155	(multiple-value-bind (subterm-sort subterm)
	156	(compute-selection $$term selectors)
	157	(setq -applied- t)
	158	(case action
	159	(:reduce ; full reduction on selections.
	160	(!setup-reduction current-module)
	161	(let ((rewrite-semantic-reduce
	162	(module-has-behavioural-axioms current-module))
	163	(rewrite-exec-mode nil))
	164	(term-replace subterm (@copy-term subterm))
	165	(reset-reduced-flag subterm)
	166	(rewrite subterm current-module)))
	167	(:breduce
	168	(!setup-reduction current-module)
	169	(let ((rewrite-semantic-reduce nil)
	170	(rewrite-exec-mode nil))
	171	(term-replace subterm (@copy-term subterm))
	172	(reset-reduced-flag subterm)
	173	(rewrite subterm current-module)))
	174	(:exec
	175	(!setup-reduction current-module)
	176	(let ((rewrite-semantic-reduce
	177	(module-has-behavioural-axioms current-module))
	178	(rewrite-exec-mode t))
	179	(term-replace subterm (@copy-term subterm))
	180	(reset-reduced-flag subterm)
	181	(rewrite subterm current-module)))
	182	;;
	183	(:print ; print selections.
	184	(format t "~%term ")
	185	(disp-term subterm)
	186	(format t "~&tree form")
	187	(print-term-tree subterm))
	188	(:apply ; apply specified rule.
	189	(setq -applied- nil)
	190	(let* ((actrule (compute-action-rule rule-spec
	191	substitution
	192	selectors))
	193	(-inside-apply-with-extensions-
	194	(and
	195	(let ((arlhs (rule-lhs actrule)))
	196	(and (term-is-application-form? arlhs)
	197	(method-is-associative (term-head arlhs)))))))
	198	(if (eq :within where-spec)
	199	(let ((-inside-apply-all- t))
	200	(catch 'apply-all-quit
	201	(@apply-all actrule subterm-sort subterm)))
	202	(@apply-rule actrule subterm-sort subterm)))
	203	(when -applied-
	204	(update-lowest-parse $$term)
	205	(when (nth 2 rule-spec) ; reverse order
	206	(setq $$term (@copy-term $$term)))
	207	(reset-target-term $$term current-module current-module))) ; end :apply
	208	(t (with-output-panic-message ()
	209	(format t "unknown apply action : ~a" action)
	210	(chaos-error 'unknown-action))))
	211	;;
	212	(unless -applied-
	213	(with-output-chaos-warning ()
	214	(princ "rule not applied")))
	215	;;
	216	(command-final)
	217	(command-display))))))
225	218
226	219	(defvar copy-conditions)
227	220	(declaim (special copy-conditons))

446	439	(when (and rev (or (rule-is-builtin rule)
447	440	(eq (axiom-type rule) :rule)))
448	441	(format t "~%This rule cannot be applied reversed."))
449		(when (and (get-context-module)
	442	(when (and (get-context-module t)
450	443	(not (rule-is-builtin rule)))
451	444	(format t "~%(This rule rewrites up.)"))))))))
452	445	t))

+0

-3

thstuff/eval-match.lisp less more

46	46	;;; ******
47	47
48	48	(defun eval-match-command (ast)
49		(unless (get-context-module)
50		(with-output-chaos-error ('no-current-module)
51		(princ "no current module.")))
52	49	(let ((type (%match-type ast))
53	50	(target (case (%match-target ast)
54	51	(:top $$term)

+14

-3

thstuff/proof-struct.lisp less more

700	700	(push x nodes))))
701	701	(nreverse nodes)))
702	702
703		;;;
704	703	;;; get-unproved-goals : ptree -> List(goal)
705	704	;;;
706	705	(defun get-unproved-goals (ptree)
707	706	(mapcar #'(lambda (y) (ptree-node-goal y)) (get-unproved-nodes ptree)))
708	707
709		;;;
710	708	;;; print-unproved-goals
711	709	;;;
712	710	(defun print-unproved-goals (ptree &optional (stream standard-output))

717	715	(dolist (goal (get-unproved-goals ptree))
718	716	(pr-goal goal stream)))
719	717
720		;;;
721	718	;;; get-next-pfoof-context : ptree -> ptree-node
722	719	;;;
723	720	(defun get-next-proof-context (ptree)

726	723
727	724	(defun next-proof-target-is-specified? ()
728	725	next-default-proof-node)
	726
	727	;;; get-target-goal-node
	728	;;; given goal-name or NULL, returns the next targetted goal node.
	729	;;;
	730	(defun get-target-goal-node (&optional goal-name)
	731	(let ((next-goal-node (if goal-name
	732	(find-goal-node proof-tree goal-name)
	733	(get-next-proof-context proof-tree))))
	734	(unless next-goal-node
	735	(with-output-chaos-error ('no-target)
	736	(if goal-name
	737	(format t "Could not find the goal ~s." goal-name)
	738	(format t "No default target goal."))))
	739	next-goal-node))
729	740
730	741	;;;
731	742	;;; select-next-goal : goal-name