Commit 08de427391a0238d0213553feaafd9ae87e35c9d - cafeobj

New command 'bshow [tree]', and 'bresolve'. Now 'binspect' does not try to resolve the abs bterm. tswd 8 years ago

8 changed file(s) with 119 addition(s) and 89 deletion(s). Raw diff Collapse all Expand all

-2

cafeobj/commands.lisp less more

2419	2419	:doc "TODO"
2420	2420	)
2421	2421
2422		(define ("bresolve" ":bresoleve")
	2422	(define ("bresolve" ":bresolve")
2423	2423	:category :proof
2424	2424	:parser identity
2425	2425	:evaluator bresolve
2426		:title "{binspect :binspect}"
	2426	:title "`{binspect \| :binspect}`"
2427	2427	:doc "TODO"
2428	2428	)
2429	2429
	2430	(define ("bshow" ":bshow")
	2431	:category :proof
	2432	:parser citp-parse-bshow
	2433	:evaluator bshow
	2434	:title "`{bshow \| :bshow} [tree]`"
	2435	:doc "TODO"
	2436	)
2430	2437	;;;
2431	2438
2432	2439	(define ("commands" "com")

-0

cafeobj/creader.lisp less more

823	823	(binspect
824	824	(:rdr #..term-delimiting-chars. (:if-present in :modexp \|:\|)) (:seq-of :term) \|.\|)
825	825	((:+ \|:bresolve\| bresolve))
	826	((:+ \|:bshow\| bshow) :args)
826	827	)) ; end Top-Form
827	828
828	829	;; some separated definitions of non-terminals.

-23

chaos/cafein/rengine.lisp less more

45	45	;;; MEMOIZE
46	46	;;; -------
47	47
48		(deftype term-hash-key () '(unsigned-byte 29))
49
50	48	(defconstant term-hash-mask #x1FFFFFFF)
51	49
52	50	(declaim (type fixnum term-hash-size))

56	54	`(and (method-p ,m) (method-has-memo ,m)))
57	55
58	56	#-GCL (declaim (inline term-hash-equal))
59		#-(or GCL CMU)
60		(defun term-hash-equal (x)
61		(logand term-hash-mask (sxhash x)))
62		#+CMU
63		(defun term-hash-equal (x)
64		(sxhash x))
65		#+GCL
	57
	58	#-GCL
	59	(defun term-hash-equal (x) (sxhash x))
	60
	61	#+GCL
66	62	(si:define-inline-function term-hash-equal (x) (sxhash x))
67	63
68	64	#+GCL

77	73	#-GCL
78	74	(declaim (inline term-hash-eq))
79	75	#-GCL
80		(defun term-hash-eq (object)
81		(ash (+ (the term-hash-key
82		(logand term-hash-mask
83		(the (unsigned-byte 32) (addr-of object))))
84		3)
85		-3))
	76	(defun term-hash-eq (object) (truncate (addr-of object) 4))
86	77
87	78	#-GCL
88	79	(declaim (inline term-hash-comb))
89	80	#-GCL
90	81	(defun term-hash-comb (x y)
91		;; (declare (type term-hash-key x y))
92		(the term-hash-key (logand term-hash-mask (logand term-hash-mask (+ x y)))))
	82	(logxor (ash x -5) y (ash (logand x 31) 26)))
93	83
94	84	;;;
95	85	;;; term-hash
96	86	;;;
97		;;; (defvar on-term-hash-debug nil)
98
99		(defstruct term-hash
100		(size term-hash-size :type (unsigned-byte 14) :read-only t)
101		(table nil :type (or null simple-array)) )
102
103	87	(defun hash-term (term)
104	88	(cond ((term-is-applform? term)
105	89	(let ((res (sxhash (the symbol (method-id-symbol (term-head term))))))

-1

configure less more

1739	1739
1740	1740
1741	1741
1742		VMINOR=.4b12
	1742	VMINOR=.4b13
1743	1743	VMEMO=PigNose0.99
1744	1744	PATCHLEVEL=
1745	1745

-1

configure.ac less more

31	31	AC_INIT([CafeOBJ],[1.5], [], [cafeobj], [http://www.cafeobj.org/])
32	32	AC_CONFIG_SRCDIR([make-cafeobj.lisp.in])
33	33	AC_PREREQ(2.6)
34		VMINOR=.4b12
	34	VMINOR=.4b13
35	35	VMEMO=PigNose0.99
36	36	PATCHLEVEL=
37	37	AC_SUBST(VMINOR)

+88

-59

thstuff/bterm-inspector.lisp less more

41	41	;;; Utilities to support investigating big boolean term of xor-and normal form.
42	42	;;;=============================================================================
43	43
	44	#\|\|
44	45	;;; *********
45	46	;;; TERM HASH
46	47	;;; *********

100	101	var)))))
101	102
102	103	)
	104	\|\|#
	105
	106	(defvar .bterm-assoc-table. nil)
	107	(defvar .bvar-num. 0)
	108	(declaim (type fixnum .bvar-num.))
	109
	110	(defun clear-bterm-memo-table ()
	111	(setq .bterm-assoc-table. nil))
	112
	113	(defun reset-bvar ()
	114	(setq .bvar-num. 0)
	115	(clear-bterm-memo-table))
	116
	117	(defun make-bterm-variable ()
	118	(let ((varname (intern (format nil "P-~d" (incf .bvar-num.)))))
	119	(make-variable-term bool-sort varname)))
	120
	121	(defun get-hashed-bterm-variable (term)
	122	(let ((ent (assoc term .bterm-assoc-table. :test #'term-equational-equal)))
	123	(if ent
	124	(cdr ent)
	125	(let ((var (make-bterm-variable)))
	126	(push (cons term var) .bterm-assoc-table.)
	127	var))))
103	128
104	129	;;; =======================================================================
105	130	;;; ABSTRACTED representation of a _xor_-_and_ normal form of boolean term.

108	133	;;; abstracted boolean term.
109	134	;;; each non _and_ or _xor_ boolean sub-term is abstracted by a
110	135	;;; variable.
111		(defstruct (abst-bterm (:print-function print-abst-bterm))
	136	(defstruct (abst-bterm)
112	137	(module nil) ; context module
113	138	(term nil) ; the original term
114	139	(subst nil) ; list of substitution

117	142
118	143	(defstruct (abst-and (:include abst-bterm)))
119	144
120		(defun print-abst-bterm (bt stream &rest ignore)
	145	(defun print-abst-bterm (bt &optional (stream standard-output) &rest ignore)
121	146	(declare (ignore ignore))
122		(with-in-module ((get-context-module))
123		(princ ":abt[" stream)
	147	(with-in-module ((abst-bterm-module bt))
	148	(if (abst-and-p bt)
	149	(princ ":and[" stream)
	150	(princ ":xor[" stream))
124	151	(let ((print-indent (+ 2 print-indent))
125	152	(num 0))
126	153	(declare (type fixnum print-indent num))

132	159	(progn
133	160	(let ((var (car sub))
134	161	(term (cdr sub)))
135		(term-print-with-sort var)
	162	(term-print var)
136	163	(princ " \|-> ")
137		(term-print-with-sort term))))))
	164	(term-print term))))))
138	165	(princ " ]" stream)))
139	166
140	167	;;;

142	169	(declare (type abst-bterm bterm))
143	170	(dolist (sub (abst-bterm-subst bterm))
144	171	(if (abst-bterm-p sub)
145		(find-bvar-subst var sub)
	172	(let ((subst (find-bvar-subst var sub)))
	173	(when subst (return-from find-bvar-subst subst)))
146	174	(when (variable= var (car sub))
147		(return-from find-bvar-subst (cdr sub)))))
148		nil)
	175	(return-from find-bvar-subst (cdr sub))))))
149	176
150	177	;;;
151	178	;;; abstract-boolen-term : bool-term -> abst-bterm

241	268
242	269	;;; print-bterm-tree : bterm -> void
243	270	(defun print-bterm-tree (bterm &optional (mode :vertical))
244		(declare (type abst-bterm bterm)
245		(ignore mode)) ; for NOW ** TODO for :vertical
246		(let ((aterm (make-bterm-representation bterm)))
247		(print-term-graph aterm chaos-verbose)))
	271	(declare (type abst-bterm bterm))
	272	(with-in-module ((abst-bterm-module bterm))
	273	(let ((aterm (make-bterm-representation bterm)))
	274	(if (eq mode :vertical)
	275	(print-term-graph aterm chaos-verbose)
	276	(print-term-horizontal (make-bterm-representation bterm) current-module)))))
248	277
249	278	;;; print-abs-bterm : bterm &key mode
250	279	;;; mode :simple print term representation

259	288	(:horizontal (print-bterm-tree bterm :horizontal))
260	289	(otherwise
261	290	(with-output-chaos-error ('invalid-mode)
262		(format t "Invalid print mode ~a." mode))))
263		;; shows substitution
264		(format t "~%, where")
265		(dolist (subst (abst-bterm-subst bterm))
266		(format t "~%~4T~A \|-> " (variable-name (car subst)))
267		(term-print-with-sort (cdr subst)))
268		)
	291	(format t "Invalid print mode ~a." mode)))))
269	292
270	293	;;; ===========================================================================================
271	294	;;; RESOLVER

321	344	;;; resolve-abst-bterm : bterm
322	345	;;; retuns a list of substitution which makes bterm to be true.
323	346	;;;
324		(defvar .maximum-bterm-vars. 10)
325
326	347	(defun resolve-abst-bterm (bterm &optional (module (get-context-module)))
327	348	(declare (type abst-bterm bterm))
328	349	(with-in-module (module)
329	350	(let* ((abst-term (make-bterm-representation bterm))
330	351	(variables (term-variables abst-term))
331	352	(answers nil))
332		(when (> (length variables) .maximum-bterm-vars.)
333		(with-output-chaos-warning ()
334		(format t "Sorry, but the current system can not handle more than ~d variables."
335		.maximum-bterm-vars.)
336		(return-from resolve-abst-bterm nil)))
337	353	(dolist (subst (assign-tf variables))
338	354	(let ((target (substitution-image-cp subst abst-term)))
339	355	(reset-reduced-flag target)
340		(when debug-bterm
341		(with-in-module ((get-context-module))
342		(format t "~%[resolver_target] ")
343		(term-print-with-sort target)
344		(print-next)
345		(format t "~% mod = ~a" current-module)
346		(print-next)
347		(print-method-brief (term-head target))
348		(print-next)
349		(format t " str: ~a" (method-rewrite-strategy (term-head target)))))
350		(setq target (reducer-no-stat target module :red))
351		(when debug-bterm
352		(with-in-module ((get-context-module))
353		(format t "~% --> ")
354		(term-print-with-sort $$term)))
	356	(let ((always-memo t))
	357	(setq target (reducer-no-stat target module :red)))
355	358	(when (is-true? $$term)
356	359	(push subst answers))))
357		answers)))
	360	(nreverse answers))))
358	361
359	362	;;; make-abst-boolean-term : term -> Values (abst-bterm List(substitution))
360	363	;;;

370	373	(with-in-module (module)
371	374	(reset-reduced-flag term)
372	375	(when citp-verbose
373		(format t "~%-- computing normal form of~% ")
374		(term-print term))
375		(let ((target (reducer-no-stat term module :red)))
	376	(format t "~%-- computing normal form."))
	377	(let* ((always-memo t)
	378	(target (reducer-no-stat term module :red)))
	379	(format t "~%--> ")
	380	(term-print term)
376	381	;; abstract
377	382	(when citp-verbose
378	383	(format t "~%-- starting abstraction"))

384	389	(format t "~%** Abstracted boolean term:")
385	390	(with-in-module (module)
386	391	(print-next)
387		(print-term-horizontal abst-bterm-representation module)
388		(format t "~% where")
389		(let ((print-indent (+ 2 print-indent)))
390		(dolist (var (nreverse (term-variables abst-bterm-representation)))
391		(let ((mapping (find-bvar-subst var bterm)))
392		(unless mapping
393		(with-output-chaos-error ('internal-err)
394		(format t "Could not find the mapping of variable ~a." (variable-name var))))
395		(print-next)
396		(term-print-with-sort var)
397		(princ " \|-> ")
398		(term-print-with-sort mapping))))))))))
	392	(term-print abst-bterm-representation)
	393	(when citp-verbose
	394	(print-term-horizontal abst-bterm-representation module))
	395	(print-bterm-substitution bterm abst-bterm-representation)))))))
	396
	397	(defun print-bterm-substitution (bterm &optional
	398	(term-representation abst-bterm-representation))
	399	(declare (type abst-bterm bterm))
	400	(with-in-module ((abst-bterm-module bterm))
	401	(print-next)
	402	(princ "where")
	403	(let ((print-indent (+ 2 print-indent)))
	404	(dolist (var (nreverse (term-variables term-representation)))
	405	(let ((mapping (find-bvar-subst var bterm)))
	406	(unless mapping
	407	(with-output-chaos-error ('internal-err)
	408	(format t "Could not find the mapping of variable ~a." (variable-name var))))
	409	(print-next)
	410	(term-print var)
	411	(princ " \|-> ")
	412	(term-print mapping)))))
	413	(terpri))
399	414
400	415	;;; try-resolve-bterm
401	416	;;;

413	428	(let ((num 0))
414	429	(declare (type fixnum num))
415	430	(let ((print-indent (+ 2 print-indent)))
416		(dolist (sub (reverse ans))
	431	(dolist (sub ans)
417	432	(print-next)
418	433	(format t "(~d): " (incf num))
419	434	(print-substitution sub))))))

446	461	(defun bresolve ()
447	462	(try-resolve-bterm))
448	463
	464	;;; bshow
	465	;;;
	466	(defun bshow (tree?)
	467	(unless abst-bterm
	468	(return-from bshow nil))
	469	(with-in-module ((abst-bterm-module abst-bterm))
	470	(if (equal tree? "tree")
	471	(print-term-horizontal abst-bterm-representation current-module)
	472	(if (equal tree? ".")
	473	(term-print abst-bterm-representation)
	474	(with-output-chaos-error ('invalid-parameter)
	475	(format t "Unknown option ~s" tree?))))
	476	(print-bterm-substitution abst-bterm abst-bterm-representation)))
	477
449	478	;;; EOF

-0

thstuff/citp.lisp less more

280	280	(setq goal-name nil)
281	281	(setq preterm (nth 1 args))))
282	282	(list mode goal-name preterm)))
	283
	284	;;; bshow \| :bshow
	285	;;;
	286	(defun citp-parse-bshow (args)
	287	(let ((param (cadr args)))
	288	(or param ".")))
283	289
284	290
285	291

-3

thstuff/proof-struct.lisp less more

911	911	(print-xmode :fancy))
912	912	(dolist (as assumptions)
913	913	(print-next)
914		(print-axiom-brief as)))))
	914	(print-axiom-brief as)
	915	(princ " .")))))
915	916	(let ((proved (goal-proved goal)))
916	917	(when proved
917	918	(print-next)

919	920	(let ((print-indent (+ 2 print-indent)))
920	921	(dolist (ax proved)
921	922	(print-next)
922		(print-axiom-brief ax)))))
	923	(print-axiom-brief ax)
	924	(princ " .")))))
923	925	(let ((targets (goal-targets goal)))
924	926	(when targets
925	927	(print-next)

929	931	(let ((print-indent (+ 2 print-indent)))
930	932	(dolist (target targets)
931	933	(print-next)
932		(print-axiom-brief target)))))))
	934	(print-axiom-brief target)
	935	(princ " .")))))))
933	936	(let ((subnodes (ptree-node-subnodes node)))
934	937	(when subnodes
935	938	(let ((print-indent (+ 2 print-indent)))