Codebase list cafeobj / 551a495
Introduced a new switch ':spoiler' for citp. When on, system does not perform implicit tactics. Added new tactics 'nf' and 'ct'. 'nf' normalize assumptions and goals. 'ct' check contradiction. tswd 8 years ago
5 changed file(s) with 554 addition(s) and 232 deletion(s). Raw diff Collapse all Expand all
+16
-13
cafeobj/creader.lisp less more
0 ;;;-*- Mode: Lisp; Syntax:CommonLisp; Package:CHAOS; Base:10 -*-
0 ;;;-*- Mode: Lisp; Syntax:Common-Lisp; Package:CHAOS; Base:10 -*-
11 ;;;
22 ;;; Copyright (c) 2000-2014, Toshimi Sawada. All rights reserved.
33 ;;;
799799 ((:+ |:red| |lred| |:lred| |:exec| |:bred|)
800800 (:rdr #..term-delimiting-chars. (:if-present in :symbol |:|)) (:seq-of :term) |.|)
801801 (|:verbose| :symbol)
802 (|:normalize| :symbol)
803 (|:ctf| |{| (:one-of #.EqDeclaration
804 #.RlDeclaration
805 #.BeqDeclaration
806 #.BRLDeclaration
807 #.FoplAXDeclaration)
808 |}|)
809 (|:csp| |{| (:many-of #.EqDeclaration
810 #.RlDeclaration
811 #.BeqDeclaration
812 #.BRLDeclaration
813 #.FoplAXDeclaration)
802 ;; (|:normalize| :symbol)
803 ((:+ |:ctf| |:ctf-|)
804 (:one-of (|{| (:one-of #.EqDeclaration
805 #.BeqDeclaration
806 #.FoplAXDeclaration)
807
808 |}|)
809 (\[ :term |.| \])))
810 ((:+ |:csp| |:csp-|)
811 |{| (:many-of #.EqDeclaration
812 #.RlDeclaration
813 #.BeqDeclaration
814 #.BRLDeclaration
815 #.FoplAXDeclaration)
814816 |}|)
815817 ((:+ |:show| |:sh| |:describe| |:desc|) :args)
818 (|:spoiler| (:one-of (on) (off) (|.|)))
816819 )) ; end Top-Form
817820
818821 ;; some separated definitions of non-terminals.
+14
-16
chaos/primitives/find.lisp less more
345345 (push opinfo res))))))
346346 (nreverse res)))
347347
348 ;;; *NOTE* not used now.....
349 #|
350 (defun simple-find-operator (operator-symbol num-args module-id)
351 (if (module-p module-id)
352 (setf module-id (module-name module-id)))
353 (get-operator-unique (list operator-symbol module-id) num-args))
354 |#
355
356348 (defun match-op-symbol (sym1 sym2)
357349 (let ((s1 sym1)
358350 (s2 sym2))
723715 (sort-id (method-coarity cand))))
724716 ;; (setq opinfo oi)
725717 (setq err-method cand)
726 (return-from find-method t))
727 ))))
728 #||
729 (with-output-panic-message ()
730 (princ "could not find error operator! : ")
731 (print-chaos-object method)
732 (chaos-error 'panic))
733 ||#
718 (return-from find-method t))))))
734719 (return-from find-error-method-in method))
735720 ;;
736721 err-method))))
722
723 ;;; FIND-CONSTRUCTORS-IN : module sort -> list(method)
724 ;;;
725 (defun find-sort-constructors-in (module sort)
726 (declare (type module module))
727 (with-in-module (module)
728 (let ((ops nil))
729 (dolist (opinfo (module-all-operators *current-module*))
730 (dolist (meth (opinfo-methods opinfo))
731 (when (and (method-is-constructor? meth)
732 (sort<= (method-coarity meth) sort (module-sort-order *current-module*)))
733 (push meth ops))))
734 (sort ops #'(lambda (x y) (< (length (method-arity x)) (length (method-arity y))))))))
737735
738736 ;;; VARIABLES ------------------------------------------------------------------
739737
+490
-194
thstuff/apply-tactic.lisp less more
5151 ,@body))))
5252
5353 )
54
55 ;;; This variable controlls implicit applications of tactics.
56 ;;; 'true' means CITP cares application of implicite applicatins of tactics
57 ;;; such as 'normalization of the goal', 'contradiction check ('true = false')'.
58 ;;; if this is 'false', CITP does only introduces proof schems defined.
59 (defvar *citp-spoiler* t)
5460
5561 ;;; *****************************************************************************
5662 ;;; UTILITIES
215221 ;;; NOTE: given axiom is preserved (not changed).
216222 ;;;
217223 (defun normalize-sentence (ax module)
218 (with-in-module (module)
219 (let* ((target (rule-copy-canonicalized ax module))
220 (lhs (rule-lhs target))
221 (rhs (rule-rhs target))
222 (condition (rule-condition target))
223 (reduction-mode (if (eq (rule-type ax) :equation)
224 :red
225 :exec))
226 (applied nil)
227 (app? nil))
228 (flet ((set-applied (val)
229 (or app? (setq app? val))))
230 (with-citp-debug ()
231 (with-in-module (module)
232 (format t "~%[NF] target:")
233 (print-next)
234 (print-axiom-brief target)))
235 ;; normalize lhs
236 (multiple-value-setq (lhs applied)
237 (normalize-term-in module (reset-reduced-flag lhs) :red))
238 (set-applied applied)
239 (when (eq reduction-mode :exec)
240 (multiple-value-setq (lhs applied) (normalize-term-in module (reset-reduced-flag lhs) :exec))
241 (set-applied applied))
242 ;; normalize rhs
243 (multiple-value-setq (rhs applied) (normalize-term-in module (reset-reduced-flag rhs)))
244 (set-applied applied)
245 ;; normalize condition
246 (unless (is-true? condition)
247 (multiple-value-setq (condition applied)
248 (normalize-term-in module (reset-reduced-flag condition) :red))
249 (set-applied applied))
250 (setf (rule-lhs target) lhs)
251 (setf (rule-rhs target) rhs)
252 (setf (rule-condition target) condition)
253 ;;
254 (with-citp-debug ()
255 (if (not app?)
256 (format t "~% ...not applied: ")
257 (progn
258 (print-next)
259 (princ "==> ") (print-axiom-brief target))))
260 ;;
261 (values target app?)))))
224 (let ((target (rule-copy-canonicalized ax module)))
225 (if *citp-spoiler*
226 (with-in-module (module)
227 (let ((lhs (rule-lhs target))
228 (rhs (rule-rhs target))
229 (condition (rule-condition target))
230 (reduction-mode (if (eq (rule-type ax) :equation)
231 :red
232 :exec))
233 (applied nil)
234 (app? nil))
235 (flet ((set-applied (val)
236 (or app? (setq app? val))))
237 (with-citp-debug ()
238 (with-in-module (module)
239 (format t "~%[NF] target:")
240 (print-next)
241 (print-axiom-brief target)))
242 ;; normalize lhs
243 (multiple-value-setq (lhs applied)
244 (normalize-term-in module (reset-reduced-flag lhs) :red))
245 (set-applied applied)
246 (when (eq reduction-mode :exec)
247 (multiple-value-setq (lhs applied)
248 (normalize-term-in module (reset-reduced-flag lhs) :exec))
249 (set-applied applied))
250 ;; normalize rhs
251 (multiple-value-setq (rhs applied)
252 (normalize-term-in module (reset-reduced-flag rhs)))
253 (set-applied applied)
254 ;; normalize condition
255 (unless (is-true? condition)
256 (multiple-value-setq (condition applied)
257 (normalize-term-in module (reset-reduced-flag condition) :red))
258 (set-applied applied))
259 (setf (rule-lhs target) lhs)
260 (setf (rule-rhs target) rhs)
261 (setf (rule-condition target) condition)
262 ;;
263 (with-citp-debug ()
264 (if (not app?)
265 (format t "~% ...not applied: ")
266 (progn
267 (print-next)
268 (princ "==> ") (print-axiom-brief target))))
269 ;;
270 (values target app?))))
271 (values target nil))))
262272
263273 ;;;
264274 ;;; is-contradiction : term term -> Bool
301311 (print-axiom-brief norm-sen))
302312 (values result norm-sen)))))
303313
304 ;;; check-contradiction : module -> Bool
305 ;;; check if 'true => false' or 'false => true' can happen or not
306 ;;;
307
314 ;;; check-contradiction : goal -> Bool
315 ;;; check if
316 ;;; * 'true => false' or
317 ;;; * 'false => true' or
318 ;;; * (t = t) = false
308319 (defun check-true<=>false (module &optional (report-header nil))
309320 (with-in-module (module)
310321 (let ((t-rules (method-rules-with-different-top *bool-true-meth*))
331342 (print-axiom-brief ct-rule)))
332343 ct-rule)))
333344
334 (defun check-contradiction (module &optional (report-header nil))
335 (or (check-true<=>false module report-header)
336 (with-in-module (module)
337 (let ((true-term (make-applform-simple *bool-sort* *bool-true-meth* nil))
338 (false-term (make-applform-simple *bool-sort* *bool-false-meth* nil)))
345 (defun check-contradictory-assumptions (goal &optional (report-header nil))
346 (let ((ams (goal-assumptions goal))
347 (contra? nil))
348 (with-in-module ((goal-context goal))
349 (dolist (ax ams)
350 (when (and (is-false? (rule-rhs ax))
351 (term-is-similar? (rule-lhs ax) (rule-rhs ax)))
352 (when report-header
353 (format t "~%[~a] contradictory assumption: " report-header)
354 (print-next)
355 (print-axiom-brief ax))
356 (setf contra? t)))
357 contra?)))
358
359 (defun check-contradiction (goal &optional (report-header nil))
360 (let ((module (goal-context goal)))
361 (or (check-true<=>false module report-header)
362 (check-contradictory-assumptions goal report-header)
363 (with-in-module (module)
364 (let ((true-term (make-applform-simple *bool-sort* *bool-true-meth* nil))
365 (false-term (make-applform-simple *bool-sort* *bool-false-meth* nil)))
339366 (let ((true=false (make-applform-simple *bool-sort* *eql-op* (list true-term false-term))))
340367 (multiple-value-bind (t-result t-applied?)
341368 (normalize-term-in module true=false)
345372 (print-next)
346373 (format t " `true = false' can be derived!"))
347374 (return-from check-contradiction t))))))
348 nil))
375 nil)))
349376
350377 ;;;
351378 ;;; check-le : goal -> goal'
415442 (do-check le-r (term-head .le-pat.))))))))
416443
417444 ;;;
418 ;;; make-new-assumption : module term [label] -> axiom
419 ;;;
445 ;;; make-new-assumption : module lhs rhs -> new-lhs new-rhs axiom-type
446 ;;;
447 (defun boolean-constant? (term)
448 (or (is-true? term)(is-false? term)))
449
450 (defun simplify-boolean-axiom (lhs rhs)
451 (let ((r-lhs lhs)
452 (r-rhs rhs)
453 (type :equation))
454 (with-citp-debug ()
455 (format t "~%== simplify: ")
456 (format t "~% lhs = ")(term-print-with-sort lhs)
457 (format t "~% rhs = ")(term-print-with-sort rhs))
458 (cond ((method= *eql-op* (term-method lhs))
459 (with-citp-debug ()
460 (format t "~%** case _=_"))
461 ;; (T1 = T2) = true/false ==> T1 = T2
462 (let* ((arg1 (term-arg-1 lhs))
463 (arg2 (term-arg-2 lhs))
464 (arg1-is-bconstant (boolean-constant? arg1))
465 (arg2-is-bconstant (boolean-constant? arg2)))
466 (cond ((is-true? rhs)
467 (with-citp-debug ()
468 (format t "~%-- (T1 = T2) = true"))
469 ;; (T1 = T2) = true
470 (cond ((method= (term-head arg1) (term-head arg2))
471 ;; (T1 = T1) = true : dangerous tautology
472 (with-citp-debug ()
473 (format t "~%-- (T = T) = true, tautology."))
474 (let ((*chaos-quiet* nil))
475 (with-output-chaos-warning ()
476 (format t "Found the new assumption is tautology:")
477 (print-next)
478 (format t "LHS: ") (term-print-with-sort arg1)
479 (print-next)
480 (format t "RHS: ") (term-print-with-sort arg2)
481 (format t "~%... ignored.")))
482 (setf r-lhs nil
483 r-rhs nil))
484 ((and arg1-is-bconstant arg2-is-bconstant)
485 (with-citp-debug ()
486 (format t "~%-- (true = false) = true, (false = true) = true."))
487 ;; (true = false), (false = true) = true .
488 ;; contradiction
489 (setf r-lhs arg1
490 r-rhs arg2)
491 (let ((*print-indent* (+ 2 *print-indent*)))
492 (let ((*chaos-quiet* nil))
493 (with-output-chaos-warning ()
494 (format t "Caution!, you are introducing contradiction:")
495 (print-next)
496 (format t "LHS: ") (term-print-with-sort r-lhs)
497 (print-next)
498 (format t "RHS: ") (term-print-with-sort r-rhs)))))
499 (t
500 ;; (T1 = T2) = true --> T1 = T2
501 (with-citp-debug ()
502 (format t "~% trying to simplify.."))
503 (setf r-lhs (if arg1-is-bconstant
504 arg2
505 arg1))
506 (setf r-rhs (if arg1-is-bconstant
507 arg1
508 arg2)))))
509 ((is-false? rhs)
510 ;; (T1 = T2) = false
511 (with-citp-debug ()
512 (format t "~%-- (T1 = T2) = false"))
513 (cond ((method= (term-head arg1) (term-head arg2))
514 ;; (T = T) = false
515 ;; contradiction
516 (with-citp-debug ()
517 (format t "~% (T = T) = false, contradiction!"))
518 (let ((*print-indent* (+ 2 *print-indent*))
519 (*chaos-quiet* nil))
520 (with-output-chaos-warning ()
521 (format t "Caution! you are introducing contradiction:")
522 (print-next)
523 (format t "LHS: ") (term-print-with-sort lhs)
524 (print-next)
525 (format t "RHS: ") (term-print-with-sort rhs))))
526 ((and arg1-is-bconstant arg2-is-bconstant)
527 ;; (true = false) = false, (false = true) = false
528 (with-citp-debug ()
529 (format t "~%(true = false) = false, (false = true) = false"))
530 (let ((*print-indent* (+ 2 *print-indent*))
531 (*chaos-quiet* nil))
532 (with-output-chaos-warning ()
533 (format t "Redundant assumption: ")
534 (print-next)
535 (format t "LHS: ") (term-print-with-sort lhs)
536 (print-next)
537 (format t "RHS: ") (term-print-with-sort rhs))
538 (format t "~%... ignored."))
539 (setf r-lhs nil
540 r-rhs nil))
541 (t
542 ;;
543 (with-citp-debug ()
544 (format t "-- trying to simplify.."))
545 (if (is-true? arg1)
546 (setf r-lhs arg2
547 r-rhs *bool-false*)
548 (if (is-true? arg2)
549 (setf r-lhs arg1
550 r-rhs *bool-false*)
551 (if (is-false? arg1)
552 (setf r-lhs arg2
553 r-rhs *bool-true*)
554 (if (is-false? arg2)
555 (setf r-lhs arg1
556 r-rhs *bool-true*)
557 (setf r-lhs lhs
558 r-rhs rhs)))))))))))
559 ((method= *bool-match* (term-method lhs))
560 ;; (T1 := T2) = true ==> T2 = T1
561 (setf r-lhs (term-arg-2 lhs)
562 r-rhs (term-arg-1 lhs)))
563 ((method= *rwl-predicate* (term-method lhs))
564 ;; (T1 => T2) = true ==> T1 => T2
565 (setf r-lhs (term-arg-1 lhs)
566 r-rhs (term-arg-2 lhs))
567 (setq type :rule)))
568
569 (with-citp-debug ()
570 (when r-lhs
571 (format t "~%=> ")
572 (format t "~%LHS: ")(term-print-with-sort r-lhs)
573 (format t "~%RHS: ")(term-print-with-sort r-rhs)
574 (format t "~%type: ") type))
575 (if r-lhs
576 (values r-lhs r-rhs type)
577 (values nil nil nil))))
578
420579 (defun make-new-assumption (module lhs &optional (label-prefix nil))
421580 (with-in-module (module)
422581 (let ((r-lhs lhs)
541700
542701 ;;; check-sentence&mark-label : sentence module -> (<result> <normalized-sentence> <origina-sentence>)
543702 ;;;
544 (defun check-sentence&mark-label (sentence module &optional (report-header nil))
703 (defun check-sentence&mark-label (sentence goal &optional (report-header nil))
545704 (flet ((make-st-label ()
546705 (let ((lbl (or report-header 'st)))
547706 (cons lbl (rule-labels sentence))))
556715 'ic)))
557716 (cons lbl (rule-labels sentence)))))
558717 ;;
559 (with-in-module (module)
560 (let ((target sentence)
561 (res nil)
562 (*print-indent* (+ 2 *print-indent*))
563 (*print-line-limit* 80)
564 (*print-xmode* :fancy))
565 (if (check-contradiction module report-header)
566 (setq res :ct)
567 (multiple-value-setq (res target)
568 (sentence-is-satisfied sentence module)))
569 (when res
570 ;; discharged by certain reson
571 (setq sentence (rule-copy-canonicalized sentence *current-module*)))
572 (with-in-module (module)
573 ;; check how we did dischage.
574 (case res
575 (:st (when report-header
576 (format t "~%[~a] discharged: " report-header)
577 (print-next)
578 (print-axiom-brief sentence))
579 (setf (rule-labels sentence) (make-st-label))
580 (values :st target sentence))
581 (:ct (when report-header
582 (format t "~%[~a] discharged: " report-header)
583 (print-next)
584 (print-axiom-brief sentence))
585 (setf (rule-labels sentence) (make-ct-label))
586 (values :ct target sentence))
587 (:ic (when report-header
588 (format t "~%[~a] discharged: " report-header)
589 (print-next)
590 (print-axiom-brief sentence))
591 (setf (rule-labels sentence) (make-ic-label))
592 (values :ic target sentence))
593 ;; could not discharge
594 (otherwise (values nil target sentence))))))))
718 (let ((module (goal-context goal)))
719 (with-in-module (module)
720 (let ((target sentence)
721 (res nil)
722 (*print-indent* (+ 2 *print-indent*))
723 (*print-line-limit* 80)
724 (*print-xmode* :fancy))
725 (if (check-contradiction goal report-header)
726 (setq res :ct)
727 (multiple-value-setq (res target)
728 (sentence-is-satisfied sentence module)))
729 (when res
730 ;; discharged by certain reson
731 (setq sentence (rule-copy-canonicalized sentence *current-module*)))
732 (with-in-module (module)
733 ;; check how we did dischage.
734 (case res
735 (:st (when report-header
736 (format t "~%[~a] discharged: " report-header)
737 (print-next)
738 (print-axiom-brief sentence))
739 (setf (rule-labels sentence) (make-st-label))
740 (values :st target sentence))
741 (:ct (when report-header
742 (format t "~%[~a] discharged: " report-header)
743 (print-next)
744 (print-axiom-brief sentence))
745 (setf (rule-labels sentence) (make-ct-label))
746 (values :ct target sentence))
747 (:ic (when report-header
748 (format t "~%[~a] discharged: " report-header)
749 (print-next)
750 (print-axiom-brief sentence))
751 (setf (rule-labels sentence) (make-ic-label))
752 (values :ic target sentence))
753 ;; could not discharge
754 (otherwise (values nil target sentence)))))))))
595755
596756 ;;;
597757 ;;; set-operator-rewrite-rule : module axiom -> void
607767 (when (cdr (goal-targets goal))
608768 (with-output-chaos-error ('invalid-proof-seq)
609769 (format t "Internal error. more than one target!")))
610 (let ((target (car (goal-targets goal))))
611 (multiple-value-bind (discharged normalized-target original-target)
612 (do-check-sentence target goal report-header)
613 (when discharged
614 (setf (goal-targets goal) nil
615 (goal-proved goal) (list original-target)))
616 (values discharged normalized-target original-target))))
617
770 (if *citp-spoiler*
771 (let ((target (car (goal-targets goal))))
772 (multiple-value-bind (discharged normalized-target original-target)
773 (do-check-sentence target goal report-header)
774 (when discharged
775 (setf (goal-targets goal) nil
776 (goal-proved goal) (list original-target)))
777 (values discharged normalized-target original-target)))
778 (values nil nil (car (goal-targets goal)))))
618779
619780 (defun do-check-sentence (target goal &optional report-header)
620781 (let ((mod (goal-context goal)))
621782 (multiple-value-bind (result norm-target marked-target)
622 (check-sentence&mark-label target mod report-header)
783 (check-sentence&mark-label target goal report-header)
623784 (cond (result
624785 ;; goal has been dischared already by some reason
625786 )
632793 (rule-rhs target)))
633794 (rule-rhs target) *bool-true*)
634795 (multiple-value-bind (res-2 norm-target-2 marked-target-2)
635 (check-sentence&mark-label target mod report-header)
796 (check-sentence&mark-label target goal report-header)
636797 (declare (ignore norm-target-2 marked-target-2))
637798 (when res-2
638799 (setf result res-2))))
645806 ;;;
646807 (defparameter .trial-context-module. (%module-decl* "trial-dummy" :object :user nil))
647808
648 (defun try-prove-with-axioms (module axioms target &optional (report-header nil))
649 (let ((*chaos-quiet* t))
650 (let ((tmodule (eval-ast .trial-context-module.)))
651 (import-module tmodule :including module)
652 (with-in-module (tmodule)
653 (dolist (ax axioms)
654 (adjoin-axiom-to-module tmodule ax)
655 (set-operator-rewrite-rule tmodule ax))
656 (compile-module tmodule t)
657 ;; first we check contradiction
658 (if (check-contradiction tmodule report-header)
659 :ct
660 ;; the module is consistent, try
661 (sentence-is-satisfied target tmodule))))))
809 (defun try-prove-with-axioms (goal axioms target &optional (report-header nil))
810 (let ((module (goal-context goal)))
811 (let ((*chaos-quiet* t))
812 (let ((tmodule (eval-ast .trial-context-module.)))
813 (import-module tmodule :including module)
814 (with-in-module (tmodule)
815 (dolist (ax axioms)
816 (adjoin-axiom-to-module tmodule ax)
817 (set-operator-rewrite-rule tmodule ax))
818 (compile-module tmodule t)
819 ;; first we check contradiction
820 (if (check-contradiction goal report-header)
821 :ct
822 ;; the module is consistent, try
823 (sentence-is-satisfied target tmodule)))))))
662824
663825 ;;; ****************************************************************************
664826 ;;; Tactic executors
12721434 ;;; =======================
12731435 (defun do-apply-rd (cur-goal tactic)
12741436 (let ((cur-targets (goal-targets cur-goal))
1275 (reduced-targets nil)
1276 (discharged nil)
1277 (result nil))
1278 (when cur-targets
1279 (compile-module (goal-context cur-goal) t)
1280 (dolist (target cur-targets)
1281 (multiple-value-bind (c-result cur-target original-sentence)
1282 (do-check-sentence target cur-goal tactic)
1283 (cond (c-result ; satisfied or contradition
1284 (setq result t)
1285 (push original-sentence discharged))
1286 (t (push cur-target reduced-targets)))))
1287 (setf (goal-targets cur-goal) (nreverse reduced-targets))
1288 (setf (goal-proved cur-goal) (nreverse discharged))
1289 (unless reduced-targets
1290 (format t "~%[~a] discharged goal ~s." tactic (goal-name cur-goal))))
1291 (values result nil)))
1437 (reduced-targets nil)
1438 (discharged nil)
1439 (result nil))
1440 (when cur-targets
1441 (compile-module (goal-context cur-goal) t)
1442 (dolist (target cur-targets)
1443 (multiple-value-bind (c-result cur-target original-sentence)
1444 (do-check-sentence target cur-goal tactic)
1445 (cond (c-result ; satisfied or contradition
1446 (setq result t)
1447 (push original-sentence discharged))
1448 (t (push cur-target reduced-targets)))))
1449 (setf (goal-targets cur-goal) (nreverse reduced-targets))
1450 (setf (goal-proved cur-goal) (nreverse discharged))
1451 (unless reduced-targets
1452 (format t "~%[~a] discharged goal ~s." tactic (goal-name cur-goal))))
1453 (values result nil)))
12921454
12931455 (defun apply-rd (ptree-node &optional (tactic 'rd))
12941456 (declare (type ptree-node ptree-node))
1295 (do-apply-rd (ptree-node-goal ptree-node) tactic))
1457 (let ((*citp-spoiler* t))
1458 (do-apply-rd (ptree-node-goal ptree-node) tactic)))
12961459
12971460 ;;; ==========================
12981461 ;;; TACTIC: Case Analysis [CA]
13701533 ;;;
13711534 (defvar .duplicated. nil)
13721535 (defvar .subst-so-far. nil)
1536
13731537
13741538 (defun find-gterm-matching-conditionals (goal gterm conditional-rules idx)
13751539 (declare (type goal goal)
18141978 ;;
18151979 (setq instance (make-axiom-instance *current-module* subst target-axiom))
18161980 ;; we normalize the LHS of the instance
1817 (when *citp-normalize-instance*
1981 (when *citp-spoiler*
18181982 (multiple-value-bind (n-lhs applied?)
18191983 (normalize-term-in *current-module* (axiom-lhs instance))
18201984 (when applied?
20842248 ;; do rewriting
20852249 (perform-reduction* token-seq (goal-context (ptree-node-goal next-goal-node)) mode)))
20862250
2087 ;;; :ctf
2088 ;;;
2089 (defun do-apply-ctf (cur-node equation)
2251 ;;; ===========
2252 ;;; TACTIC: :NF
2253 ;;; compute normal form of targets and assumptions.
2254 ;;; ===========
2255 (defun apply-nf (ptree-node)
2256 (declare (type ptree-node ptree-node))
2257 (let ((.cur-goal. (ptree-node-goal ptree-node)))
2258 (when (goal-is-discharged .cur-goal.)
2259 (with-output-chaos-warning ()
2260 (format t "** The goal ~s has already been proved!."
2261 (goal-name .cur-goal.)))
2262 (return-from apply-nf nil))
2263 (with-in-module ((goal-context .cur-goal.))
2264 (let ((n-targets nil)
2265 (*citp-spoiler* t)
2266 (*chaos-quiet* t)
2267 (n-assumptions nil))
2268 ;; first nomalize assumptions
2269 (dolist (as (goal-assumptions .cur-goal.))
2270 (multiple-value-bind (ns app?)
2271 (normalize-sentence as *current-module*)
2272 (when app?
2273 (adjoin-axiom-to-module (goal-context .cur-goal.) ns)
2274 (set-operator-rewrite-rule (goal-context .cur-goal.) ns)
2275 (push ns n-assumptions))))
2276 (when n-assumptions
2277 (setf (goal-assumptions .cur-goal.)
2278 (append (goal-assumptions .cur-goal.) (nreverse n-assumptions))))
2279 ;; normalize goal sentences
2280 (dolist (sen (goal-targets .cur-goal.))
2281 (multiple-value-bind (ngoal app?)
2282 (normalize-sentence sen *current-module*)
2283 (if app?
2284 (push ngoal n-targets)
2285 (push sen n-targets))))
2286 (setf (goal-targets .cur-goal.) (nreverse n-targets))
2287 t))))
2288
2289 ;;; ===========
2290 ;;; TACTIC: :CT
2291 ;;; do contradiction check, can dischage the goal
2292 ;;; ===========
2293 (defun apply-ct (ptree-node)
2294 (declare (type ptree-node ptree-node))
2295 (let ((.cur-goal. (ptree-node-goal ptree-node)))
2296 (when (goal-is-discharged .cur-goal.)
2297 (with-output-chaos-warning ()
2298 (format t "** The goal ~s has already been proved!."
2299 (goal-name .cur-goal.)))
2300 (return-from apply-ct nil))
2301 ;;
2302 (with-in-module ((goal-context .cur-goal.))
2303 (let ((*chaos-quiet* t)
2304 (*citp-spoiler* t))
2305 (when (check-contradiction .cur-goal. 'ct)
2306 (with-in-module ((goal-context .cur-goal.))
2307 (format t "%[ct] dischaged:")
2308 (dolist (target (goal-targets .cur-goal.))
2309 (print-next)
2310 (print-axiom-brief target))
2311 (setf (goal-proved .cur-goal.) (goal-targets .cur-goal.))
2312 (setf (goal-targets .cur-goal.) nil)))))
2313 t))
2314
2315 ;;; :ctf or :ctf-
2316 ;;;
2317 (defun do-apply-ctf (cur-node term-or-equation)
20902318 (let ((*chaos-quiet* t)
20912319 (*rwl-search-no-state-report* t)
20922320 (cur-goal (ptree-node-goal cur-node)))
20932321 (when (goal-is-discharged cur-goal)
20942322 (with-output-chaos-warning ()
2095 (format t "** The goal ~s has been proved!." (goal-name (ptree-node-goal cur-node)))
2096 (return-from do-apply-ctf nil)))
2097 (let ((t-goal (prepare-next-goal cur-node .tactic-ctf.))
2098 (f-goal (prepare-next-goal cur-node .tactic-ctf.)))
2099 ;; true case
2100 (with-in-module ((goal-context t-goal))
2101 (adjoin-axiom-to-module *current-module* equation)
2102 (set-operator-rewrite-rule *current-module* equation)
2323 (format t "** The goal ~s has already been proved!."
2324 (goal-name cur-goal)))
2325 (return-from do-apply-ctf nil))
2326 (if (termp term-or-equation)
2327 (do-apply-ctf-with-constructors cur-node term-or-equation)
2328 (do-apply-ctf-to-equation cur-node term-or-equation))))
2329
2330 (defun make-ctf-constructor-pattern (const-op)
2331 (when (method-arity const-op)
2332 (with-output-chaos-warning ()
2333 (format t "Constructor with arguments is not supported yet. Sorry!")
2334 (return-from make-ctf-constructor-pattern nil)))
2335 (make-applform-simple (method-coarity const-op) const-op nil))
2336
2337 (defun do-apply-ctf-with-constructors (cur-node term)
2338 (let ((cur-goal (ptree-node-goal cur-node))
2339 (sort (term-sort term))
2340 (goals nil))
2341 (let ((constructors (find-sort-constructors-in *current-module* sort)))
2342 (unless constructors
2343 (with-output-chaos-error ('no-constructors)
2344 (format t "Sort ~a has no constructors." (sort-name sort))))
2345 (dolist (const constructors)
2346 (let ((n-goal nil)
2347 (const-pat (make-ctf-constructor-pattern const)))
2348 (when const-pat
2349 (setq n-goal (prepare-next-goal cur-node .tactic-ctf.))
2350 (with-in-module ((goal-context n-goal))
2351 (multiple-value-bind (lhs rhs type)
2352 (if (sort= (term-sort term) *bool-sort*)
2353 (simplify-boolean-axiom term const-pat)
2354 (values term const-pat :equation))
2355 (when lhs
2356 (let ((ax (make-rule :lhs lhs
2357 :rhs rhs
2358 :condition *bool-true*
2359 :type type
2360 :behavioural nil)))
2361 (adjoin-axiom-to-module *current-module* ax)
2362 (set-operator-rewrite-rule *current-module* ax)
2363 (compile-module *current-module*)
2364 (push n-goal goals)
2365 (setf (goal-targets n-goal) (goal-targets cur-goal))
2366 (setf (goal-assumptions n-goal)
2367 (append (goal-assumptions cur-goal) (list ax))))))))))
2368 (if goals
2369 (values t (nreverse goals))
2370 (values nil nil)))))
2371
2372 (defun do-apply-ctf-to-equation (cur-node equation)
2373 (let* ((cur-goal (ptree-node-goal cur-node))
2374 (t-goal (prepare-next-goal cur-node .tactic-ctf.))
2375 (f-goal (prepare-next-goal cur-node .tactic-ctf.)))
2376 ;; true case
2377 (with-in-module ((goal-context t-goal))
2378 (adjoin-axiom-to-module *current-module* equation)
2379 (set-operator-rewrite-rule *current-module* equation)
2380 (compile-module *current-module*))
2381 (setf (goal-targets t-goal) (goal-targets cur-goal))
2382 (setf (goal-assumptions t-goal) (append (goal-assumptions cur-goal) (list equation)))
2383 ;; false case
2384 (let ((f-ax nil))
2385 (with-in-module ((goal-context f-goal))
2386 (setq f-ax (make-rule :lhs (make-applform-simple *bool-sort*
2387 *eql-op*
2388 (list (rule-lhs equation)
2389 (rule-rhs equation)))
2390 :rhs *bool-false*
2391 :condition *bool-true*
2392 :type :equation
2393 :behavioural nil))
2394 (adjoin-axiom-to-module *current-module* f-ax)
2395 (set-operator-rewrite-rule *current-module* f-ax)
21032396 (compile-module *current-module*))
2104 (setf (goal-targets t-goal) (goal-targets cur-goal))
2105 (setf (goal-assumptions t-goal) (append (goal-assumptions cur-goal) (list equation)))
2106 ;; false case
2107 (let ((f-ax nil))
2108 (with-in-module ((goal-context f-goal))
2109 (setq f-ax (make-rule :lhs (make-applform-simple *bool-sort*
2110 *eql-op*
2111 (list (rule-lhs equation)
2112 (rule-rhs equation)))
2113 :rhs *bool-false*
2114 :condition *bool-true*
2115 :type :equation
2116 :behavioural nil))
2117 (adjoin-axiom-to-module *current-module* f-ax)
2118 (set-operator-rewrite-rule *current-module* f-ax)
2119 (compile-module *current-module*))
2120 (setf (goal-targets f-goal) (goal-targets cur-goal))
2121 (setf (goal-assumptions f-goal) (append (goal-assumptions cur-goal) (list f-ax)))
2122 (values t (list t-goal f-goal))))))
2123
2124 (defun apply-ctf (s-form &optional (verbose *citp-verbose*))
2397 (setf (goal-targets f-goal) (goal-targets cur-goal))
2398 (setf (goal-assumptions f-goal) (append (goal-assumptions cur-goal) (list f-ax)))
2399 (values t (list t-goal f-goal)))))
2400
2401 (defun parse-axiom-or-term (form term?)
2402 (if term?
2403 (let ((*parse-variables* nil))
2404 (let ((res (simple-parse *current-module* form *cosmos*)))
2405 res))
2406 (parse-axiom-declaration (parse-module-element-1 form))))
2407
2408 (defun apply-ctf (s-form term? dash? &optional (verbose *citp-verbose*))
21252409 (let ((ptree-node (get-next-proof-context *proof-tree*)))
21262410 (with-in-module ((goal-context (ptree-node-goal ptree-node)))
21272411 (let ((*chaos-quiet* t)
2128 (equation (parse-axiom-declaration (parse-module-element-1 s-form))))
2412 (form (parse-axiom-or-term s-form term?)))
21292413 (multiple-value-bind (applied next-goals)
2130 (do-apply-ctf ptree-node equation)
2414 (do-apply-ctf ptree-node form)
21312415 (declare (ignore applied))
21322416 (unless next-goals
21332417 (return-from apply-ctf nil))
21342418 (format t "~%** Generated ~d goal~p" (length next-goals) (length next-goals))
2135 ;; apply implicit rd
2136 (dolist (ngoal next-goals)
2137 (do-apply-rd ngoal 'ctf))
2419 (when *citp-spoiler*
2420 ;; apply implicit rd
2421 (dolist (ngoal next-goals)
2422 (do-apply-rd ngoal 'ctf)
2423 (when (and dash? (goal-targets ngoal))
2424 ;; reset target
2425 (setf (goal-targets ngoal)
2426 (goal-targets (ptree-node-goal ptree-node))))))
21382427 ;; add generated nodes as children
21392428 (add-ptree-children ptree-node next-goals)
21402429 (when verbose
21432432 (ptree-node-subnodes ptree-node))))))
21442433
21452434 ;;; -----------------------------------------------------
2146 ;;; :csp
2435 ;;; :csp or :csp-
2436 ;;;
21472437 (defun do-apply-csp (cur-node axs)
21482438 (let ((*chaos-quiet* t)
21492439 (*rwl-search-no-state-report* t)
21502440 (cur-goal (ptree-node-goal cur-node)))
21512441 (when (goal-is-discharged cur-goal)
21522442 (with-output-chaos-warning ()
2153 (format t "** The goal ~s has been proved!." (goal-name (ptree-node-goal cur-node)))
2443 (format t "** The goal ~s has already been proved!." (goal-name (ptree-node-goal cur-node)))
21542444 (return-from do-apply-csp nil)))
21552445 (let ((ngoals nil))
21562446 (dolist (ax axs)
21652455 (push n-goal ngoals)))
21662456 (values t (nreverse ngoals)))))
21672457
2168 (defun apply-csp (ax-forms &optional (verbose *citp-verbose*))
2458 (defun apply-csp (ax-forms dash? &optional (verbose *citp-verbose*))
21692459 (let ((ptree-node (get-next-proof-context *proof-tree*)))
21702460 (with-in-module ((goal-context (ptree-node-goal ptree-node)))
21712461 (let ((*chaos-quiet* t)
21782468 (unless next-goals
21792469 (return-from apply-csp nil))
21802470 (format t "~%** Generated ~d goal~p" (length next-goals) (length next-goals))
2181 ;; apply implicit rd
2182 (dolist (ngoal next-goals)
2183 (do-apply-rd ngoal 'csp))
2471 (when *citp-spoiler*
2472 ;; apply implicit rd
2473 (dolist (ngoal next-goals)
2474 (do-apply-rd ngoal 'csp)
2475 (when (and dash? (goal-targets ngoal))
2476 ;; reset target
2477 (setf (goal-targets ngoal)
2478 (goal-targets (ptree-node-goal ptree-node))))))
21842479 ;; add generated node as children
21852480 (add-ptree-children ptree-node next-goals)
21862481 (when verbose
22052500 (*rwl-search-no-state-report* t))
22062501 (when (goal-is-discharged (ptree-node-goal ptree-node))
22072502 (with-output-chaos-warning ()
2208 (format t "** The goal ~s has been proved!." (goal-name (ptree-node-goal ptree-node)))
2503 (format t "** The goal ~s has already been proved!." (goal-name (ptree-node-goal ptree-node)))
22092504 (return-from apply-tactic nil)))
22102505 ;;
22112506 (format t "~%~a=> :goal{~a}" tactic (goal-name (ptree-node-goal ptree-node)))
22602555 ;;; apply-auto
22612556 ;;;
22622557 (defun apply-auto (ptree &optional (tactics .default-tactics.) (verbose *citp-verbose*))
2263 (reset-rewrite-counters)
2264 (begin-rewrite)
2265 (if (next-proof-target-is-specified?)
2266 (apply-tactics-to-node (get-next-proof-context ptree) tactics verbose)
2267 (let ((target-nodes (get-unproved-nodes ptree)))
2268 (unless target-nodes
2269 (format t "~%**> All goals have been proved!")
2270 (return-from apply-auto nil))
2271 (dolist (tactic tactics)
2272 (dolist (target-node (get-unproved-nodes ptree))
2273 (apply-tactic target-node tactic verbose)))))
2274 (end-rewrite)
2275 (report-citp-stat)
2276 (check-success ptree))
2558 (let ((*citp-spoiler* t))
2559 (reset-rewrite-counters)
2560 (begin-rewrite)
2561 (if (next-proof-target-is-specified?)
2562 (apply-tactics-to-node (get-next-proof-context ptree) tactics verbose)
2563 (let ((target-nodes (get-unproved-nodes ptree)))
2564 (unless target-nodes
2565 (format t "~%**> All goals have been proved!")
2566 (return-from apply-auto nil))
2567 (dolist (tactic tactics)
2568 (dolist (target-node (get-unproved-nodes ptree))
2569 (apply-tactic target-node tactic verbose)))))
2570 (end-rewrite)
2571 (report-citp-stat)
2572 (check-success ptree)))
22772573
22782574 ;;;
22792575 ;;; apply-tactics-to-goal
+27
-8
thstuff/citp.lisp less more
202202
203203 ;;; citp-parse-ctf
204204 ;;; :ctf { eq <term> = <term> .}
205 ;;; (":ctf" ("{" ("eq" ("1" ">" "2") "=" ("true") ".") "}"))
206 ;;; :ctf [ <term> . ]
207 ;;; (":ctf" ("[" ("1" ">" "2") "." "]"))
208 ;;; ==> (form . (term? . :ctf-?))
205209 ;;;
206210 (defun citp-parse-ctf (args)
207 (let ((ax-form (third args)))
208 (with-citp-debug ()
209 (format t "~%[:ctf] target = ~s" ax-form))
210 ax-form))
211 (let ((form (second (second args)))
212 (term? (equal (first (second args)) "[")))
213 (if (equal (first args) ":ctf-")
214 (cons form (cons term? :dash))
215 (cons form (cons term? nil)))))
211216
212217 ;;; citp-parse-csp
213218 ;;; :csp { <axiom> ... }
214219 ;;;
215220 (defun citp-parse-csp (args)
216 (let ((ax-decls nil))
221 (let ((ax-decls nil)
222 (dash? (equal (car args) ":csp-")))
217223 (dolist (elem (third args))
218224 (push elem ax-decls))
219 (nreverse ax-decls)))
225 (cons (nreverse ax-decls) dash?)))
220226
221227 ;;; { :show | :describe } <something>
222228 ;;;
232238 (format t "Internal error, unknown citp command ~s" tag))))
233239 (cons com args)))
234240
241 ;;; :spoiler { on | off }
242 ;;;
243 (defun citp-parse-spoiler (form)
244 (let ((on-off (second form)))
245 (if (equal on-off '("on"))
246 (setq *citp-spoiler* t)
247 (if (equal on-off '("off"))
248 (setq *citp-spoiler* nil)
249 ;;
250 (format t "~&:spoiler flag is ~s" (if *citp-spoiler* "on" "off"))))
251 t))
252
235253 ;;; ================================
236254 ;;; CITP related command evaluators
237255 ;;; ================================
337355 (format t ":nomalize instance: unknown parameter ~s." token))))))
338356
339357 ;;; :ctf
358 ;;; ax-form ::= (form . (term? . :ctf-?))
340359 ;;;
341360 (defun eval-citp-ctf (ax-form)
342361 (check-ptree)
343362 (with-in-module (*current-module*)
344363 (reset-rewrite-counters)
345364 (begin-rewrite)
346 (apply-ctf ax-form)
365 (apply-ctf (car ax-form) (cadr ax-form) (cddr ax-form))
347366 (end-rewrite)
348367 (report-citp-stat)
349368 (check-success *proof-tree*)))
354373 (with-in-module (*current-module*)
355374 (reset-rewrite-counters)
356375 (begin-rewrite)
357 (apply-csp (nreverse goal-ax-decls))
376 (apply-csp (car goal-ax-decls) (cdr goal-ax-decls))
358377 (end-rewrite)
359378 (report-citp-stat)
360379 (check-success *proof-tree*)))
+7
-1
thstuff/proof-struct.lisp less more
6161 (defparameter .tactic-rd. (make-tactic :name :rd
6262 :executor 'apply-rd)) ; Reduction
6363
64 (defparameter .tactic-nf. (make-tactic :name :nf
65 :executor 'apply-nf)) ; nomalize goals, assumptions
66
67 (defparameter .tactic-ct. (make-tactic :name :ct
68 :executor 'apply-ct)) ; check contradiction
69
6470 (defparameter .tactic-nil. (make-tactic :name :nop
6571 :executor 'apply-nil)) ; Do nothing, used internally.
6672
67 (defparameter .all-builtin-tactics. (list .tactic-si. .tactic-ca. .tactic-tc. .tactic-ip. .tactic-cs. .tactic-rd.))
73 (defparameter .all-builtin-tactics. (list .tactic-si. .tactic-ca. .tactic-tc. .tactic-ip. .tactic-cs. .tactic-rd. .tactic-nf. .tactic-ct.))
6874
6975 ;; default tatics is a seriase of SI CA CS TC IP.
7076 (defparameter .default-tactics. (list .tactic-si. .tactic-ca. .tactic-cs. .tactic-tc. .tactic-ip. .tactic-rd.))