Codebase list cafeobj / 33df65f
Implemented boolean term inspect command (:binspect, binspect) ':show proof' now shows the proof tree in horizontal. tswd 8 years ago
6 changed file(s) with 137 addition(s) and 56 deletion(s). Raw diff Collapse all Expand all
+3
-1
cafeobj/creader.lisp less more
818818 |}|)
819819 ((:+ |:show| |:sh| |:describe| |:desc|) :args)
820820 (|:spoiler| (:one-of (on) (off) (|.|)))
821 ((:+ |:binspect|)
821 (|:binspect|
822822 (:rdr #..term-delimiting-chars. (:if-present in :symbol |:|)) (:seq-of :term) |.|)
823 (binspect
824 (:rdr #..term-delimiting-chars. (:if-present in :modexp |:|)) (:seq-of :term) |.|)
823825 )) ; end Top-Form
824826
825827 ;; some separated definitions of non-terminals.
+15
-0
chaos/primitives/term-utils.lisp less more
15281528 (declare (ignore list-new-var))
15291529 list-copied-term)))
15301530
1531 ;;; print-term-struct
1532 ;;;
1533 (defun print-term-struct (term module &optional (stream *standard-output*))
1534 (with-in-module (module)
1535 (let ((*standard-output* stream))
1536 (print-next)
1537 (cond ((term-is-applform? term)
1538 (format t "~a" (method-name (term-head term)))
1539 (dotimes (x (length (term-subterms term)))
1540 (let ((*print-indent* (+ 2 *print-indent*)))
1541 (print-term-struct (term-arg-n term x) module))))
1542 ((term-is-builtin-constant? term)
1543 (term-print term))
1544 (t (print-chaos-object term))))))
1545
15311546 ;;; EOF
+15
-0
chaos/tools/show.lisp less more
553553 (print-mod-name *memoized-module*)
554554 (dump-term-hash *term-memo-table*)))
555555
556 ;;;
557 ;;; print-term-horizontal
558 ;;;
559 (defun print-term-horizontal (term module &optional (stream *standard-output*))
560 (with-in-module (module)
561 (let ((*standard-output* stream))
562 (print-next)
563 (cond ((term-is-applform? term)
564 (format t "~{~a~}" (method-symbol (term-head term)))
565 (dotimes (x (length (term-subterms term)))
566 (let ((*print-indent* (+ 4 *print-indent*)))
567 (print-term-horizontal (term-arg-n term x) module))))
568 ((term-is-builtin-constant? term)
569 (term-print term))
570 (t (print-chaos-object term))))))
556571 ;;; EOF
+12
-2
thstuff/apply-tactic.lisp less more
207207 (block next
208208 (when (term-is-reduced? gt)
209209 (return-from next nil))
210 #||
211 (with-citp-debug ()
212 (with-in-module (module)
213 (print-chaos-object (term-head gt))
214 (terpri)
215 (print-chaos-object module)
216 (format t "~%strat: ~a" (method-rewrite-strategy (term-head gt)))))
217 ||#
210218 (reducer-no-stat gt module reduction-mode)
211219 (unless (= rule-count-save (number-rewritings))
212220 (setq applied? t))))
14421450 (result nil))
14431451 (when cur-targets
14441452 (compile-module (goal-context cur-goal) t)
1453 (when next-goal
1454 (compile-module (goal-context next-goal) t))
14451455 (dolist (target cur-targets)
14461456 (multiple-value-bind (c-result cur-target original-sentence)
14471457 (do-check-sentence target (or next-goal cur-goal) tactic)
14681478 (goal-name cur-goal)))
14691479 (return-from apply-rd (values nil nil)))
14701480 (if (goal-targets cur-goal)
1471 (do-apply-rd cur-goal (prepare-next-goal ptree-node) tactic)
1481 (do-apply-rd cur-goal (prepare-next-goal ptree-node .tactic-rd.) tactic)
14721482 (values nil nil))))
14731483
14741484 ;;; ==========================
24922502 (dolist (ax ax-forms)
24932503 (push (parse-axiom-declaration (parse-module-element-1 ax)) axs))
24942504 (multiple-value-bind (applied next-goals)
2495 (do-apply-csp ptree-node axs)
2505 (do-apply-csp ptree-node (nreverse axs))
24962506 (declare (ignore applied))
24972507 (unless next-goals
24982508 (return-from apply-csp nil))
+63
-50
thstuff/bterm-inspector.lisp less more
199199 ;;;
200200 (defun make-and-representation (abst-and)
201201 (declare (type abst-and abst-and))
202 (make-right-assoc-normal-form *bool-and*
203 (mapcar #'car (abst-and-subst abst-and))))
202 (let ((repre (make-right-assoc-normal-form *bool-and*
203 (mapcar #'car (abst-and-subst abst-and)))))
204 (update-lowest-parse repre)
205 repre))
204206
205207 (defun make-xor-representation (bterm)
206208 (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))))
209 (let ((repre (make-right-assoc-normal-form *bool-xor*
210 (mapcar #'(lambda (x) (if (abst-and-p x)
211 (make-and-representation x)
212 (car x)))
213 (abst-bterm-subst bterm)))))
214 (update-lowest-parse repre)
215 repre))
212216
213217 (defun make-bterm-representation (bterm)
214218 (let ((subst (abst-bterm-subst bterm)))
322326 (answers nil))
323327 (dolist (subst list-subst)
324328 (let ((target (substitution-image-cp subst abst-term)))
329 (reset-reduced-flag target)
325330 (when *debug-bterm*
326331 (with-in-module ((get-context-module))
327332 (format t "~%[resolver_target] ")
328 (term-print-with-sort target)))
329 (reducer-no-stat target module :red)
333 (term-print-with-sort target)
334 (print-next)
335 (format t "~% mod = ~a" *current-module*)
336 (print-next)
337 (print-method-brief (term-head target))
338 (print-next)
339 (format t " str: ~a" (method-rewrite-strategy (term-head target)))))
340 (setq target (reducer-no-stat target module :red))
330341 (when *debug-bterm*
331342 (with-in-module ((get-context-module))
332343 (format t "~% --> ")
333 (term-print-with-sort target)))
334 (when (is-true? target)
344 (term-print-with-sort $$term)))
345 (when (is-true? $$term)
335346 (push subst answers))))
336347 answers))
337348
340351 (defvar *abst-bterm* nil)
341352 (defvar *abst-bterm-representation* nil)
342353
343 (defun try-resolve-boolean-term (term &optional (module (get-context-module)))
354 (defun try-resolve-boolean-term (term module)
344355 (unless (sort= (term-sort term) *bool-sort*)
345356 (with-output-chaos-warning ()
346357 (format t "Given term is not of sort Bool. Ignored.")
347358 (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)))))))
359 (!setup-reduction module)
360 (with-in-module (module)
361 (reset-reduced-flag term)
362 (let ((target (reducer-no-stat term module :red)))
363 ;; abstract
364 (let ((bterm (abstract-boolean-term target)))
365 (setq *abst-bterm* bterm)
366 (setq *abst-bterm-representation*
367 (make-bterm-representation bterm))
368 (let ((*print-indent* (+ 2 *print-indent*)))
369 (format t "~%** Abstracted boolean term:")
370 (with-in-module (module)
371 (print-next)
372 (term-print-with-sort *abst-bterm-representation*)
373 (print-term-graph *abst-bterm-representation* *chaos-verbose*)
374 (format t "~% where")
375 (let ((*print-indent* (+ 2 *print-indent*)))
376 (dolist (var (term-variables *abst-bterm-representation*))
377 (let ((mapping (find-bvar-subst var bterm)))
378 (unless mapping
379 (with-output-chaos-error ('internal-err)
380 (format t "Could not find the mapping of variable ~a." (variable-name var))))
381 (print-next)
382 (term-print-with-sort var)
383 (princ " |-> ")
384 (term-print-with-sort mapping))))
385 ;; find answers
386 (let ((ans (resolve-abst-bterm bterm module)))
387 (cond (ans
388 (format t "~%** The following assignment(s) can make the term 'true'.")
389 (let ((num 0))
390 (declare (type fixnum num))
391 (let ((*print-indent* (+ 2 *print-indent*)))
392 (dolist (sub ans)
393 (print-next)
394 (format t "(~d): " (incf num))
395 (print-substitution sub)))))
396 (t
397 (format t "~%** No solution was found.")))
398 (values bterm ans))))))))
386399
387400 ;;;
388401 (defun binspect-in-goal (goal-name preterm)
+29
-3
thstuff/proof-struct.lisp less more
828828 ;;;
829829 ;;; print-proof-tree
830830 ;;;
831 (defvar *show-proof-mode* :horizontal)
832
831833 (defun print-proof-tree (goal-name &optional (describe nil))
832834 (unless *proof-tree*
833835 (with-output-chaos-warning ()
840842 (ptree-root *proof-tree*))))
841843 (if describe
842844 (describe-proof-tree target-node)
843 (!print-proof-tree target-node (get-next-proof-context *proof-tree*)))))
844
845 (defun !print-proof-tree (root-node next-target &optional (stream *standard-output*))
845 (!print-proof-tree target-node (get-next-proof-context *proof-tree*) *show-proof-mode*))))
846
847 (defun !print-proof-tree (root-node next-target mode &optional (stream *standard-output*))
848 (if (eq mode :horizontal)
849 (!print-proof-horizontal root-node next-target stream)
850 (!print-proof-vertical root-node next-target stream)))
851
852 (defun !print-proof-vertical (root-node next-target stream)
846853 (let* ((leaf? #'(lambda (node) (null (dag-node-subnodes node))))
847854 (leaf-name #'(lambda (node)
848855 (with-output-to-string (s)
862869 (print-next nil *print-indent* stream)
863870 (print-trees (list (augment-tree root-node)) stream)))
864871
872 (defun !print-proof-horizontal (node next-target stream)
873 (let ((*standard-output* stream))
874 (let ((goal (ptree-node-goal node)))
875 (with-in-module ((goal-context goal))
876 (when (eq node next-target)
877 (princ ">"))
878 (if (goal-tactic goal)
879 (format t "~a ~a" (goal-tactic goal) (goal-name goal))
880 (format t "~a" (goal-name goal)))
881 (when (node-is-discharged? node)
882 (princ "*"))))
883 (let ((subnodes (ptree-node-subnodes node)))
884 (when subnodes
885 (let ((*print-indent* (+ 4 *print-indent*)))
886 (dolist (sub subnodes)
887 (print-next-prefix #\Space)
888 (!print-proof-horizontal sub next-target stream)))))))
889
890
865891 (defun describe-proof-tree (node)
866892 (declare (type ptree-node node))
867893 (flet ((proved? ()