| 30 | 30 |
|
| 31 | 31 |
)
|
| 32 | 32 |
|
| 33 | |
;;; ==============
|
| 34 | |
;;; some utilities
|
| 35 | |
;;; ==============
|
| 36 | |
|
| 37 | |
;;;
|
|
33 |
;;; *****************************************************************************
|
|
34 |
;;; UTILITIES
|
|
35 |
;;; ****************************************************************************
|
|
36 |
|
|
37 |
;;; distribute-sentences : ptree-node List(axiom) -> List(goal)
|
|
38 |
;;; if there are multiple sentences, distribute them into newly genereted goals for each
|
|
39 |
;;;
|
|
40 |
(defun distribute-sentences (parent axioms tactic)
|
|
41 |
(declare (type ptree-node parent))
|
|
42 |
(let ((new-goals nil)
|
|
43 |
(goal nil))
|
|
44 |
(cond ((cdr axioms)
|
|
45 |
(dolist (ax axioms)
|
|
46 |
(setq goal (prepare-next-goal parent tactic))
|
|
47 |
(setf (goal-targets goal) (list ax))
|
|
48 |
(push goal new-goals)))
|
|
49 |
(t (push (ptree-node-goal parent) new-goals)))
|
|
50 |
(nreverse new-goals)))
|
|
51 |
|
|
52 |
#||
|
|
53 |
(defun distribute-sentences (parent axioms tactic)
|
|
54 |
(declare (type ptree-node parent))
|
|
55 |
(let ((new-goals nil)
|
|
56 |
(goal nil))
|
|
57 |
(dolist (ax axioms)
|
|
58 |
(setq goal (prepare-next-goal parent tactic))
|
|
59 |
(setf (goal-targets goal) (list ax))
|
|
60 |
(push goal new-goals))
|
|
61 |
(nreverse new-goals)))
|
|
62 |
||#
|
|
63 |
|
| 38 | 64 |
;;; rule-copy-cononicalized : rule module -> rule
|
| 39 | 65 |
;;; copy rule with all variables are renewed and noralized.
|
| 40 | 66 |
;;;
|
|
| 48 | 74 |
(rule-rhs new-rule) (second canon)
|
| 49 | 75 |
(rule-condition new-rule) (third canon))
|
| 50 | 76 |
new-rule))
|
|
77 |
|
|
78 |
;;;
|
|
79 |
;;; apply-substitution-to-axiom : subst axiom module -> axiom'
|
|
80 |
;;;
|
|
81 |
(defun apply-substitution-to-axiom (subst axiom &optional label)
|
|
82 |
(setf (rule-lhs axiom) (substitution-image-simplifying subst (rule-lhs axiom))
|
|
83 |
(rule-rhs axiom) (substitution-image-simplifying subst (rule-rhs axiom))
|
|
84 |
(rule-condition axiom) (if (is-true? (rule-condition axiom))
|
|
85 |
*bool-true*
|
|
86 |
(substitution-image-simplifying subst (rule-condition axiom))))
|
|
87 |
(when label
|
|
88 |
(setf (rule-labels axiom) label))
|
|
89 |
axiom)
|
| 51 | 90 |
|
| 52 | 91 |
;;; intro-const-returns-subst : module name variable -> (variable . constant-term)
|
| 53 | 92 |
;;; introduces a new constant of sort(variable) into a module.
|
|
| 180 | 219 |
(setq result (append (term-variables lhs)
|
| 181 | 220 |
(append (term-variables rhs)
|
| 182 | 221 |
(term-variables cond))))
|
|
222 |
#||
|
| 183 | 223 |
(with-citp-debug ()
|
| 184 | 224 |
(dolist (v result)
|
| 185 | 225 |
(print-next) (term-print-with-sort v)))
|
|
226 |
||#
|
| 186 | 227 |
(delete-duplicates result :test #'variable-equal)))
|
| 187 | 228 |
|
| 188 | 229 |
;;;
|
|
| 202 | 243 |
|
| 203 | 244 |
;;; normalize-term-in : module term -> term applied
|
| 204 | 245 |
;;;
|
| 205 | |
(defun normalize-term-in (module term)
|
| 206 | |
(with-in-module (module)
|
| 207 | |
(setq $$matches 0)
|
| 208 | |
(let ((*perform-on-demand-reduction* t)
|
| 209 | |
(*rule-count* 0))
|
| 210 | |
(unless (term-variables term)
|
| 211 | |
;; we only targets ground term
|
| 212 | |
(rewrite term *current-module* :red))
|
| 213 | |
(values term (not (= 0 *rule-count*))))))
|
|
246 |
(defun normalize-term-in (module term &optional (reduction-mode :red))
|
|
247 |
(let ((gterms (get-gterms term))
|
|
248 |
(applied? nil))
|
|
249 |
(if gterms
|
|
250 |
(with-in-module (module)
|
|
251 |
(dolist (gt gterms)
|
|
252 |
(setq $$matches 0)
|
|
253 |
(let ((*perform-on-demand-reduction* t)
|
|
254 |
(*rule-count* 0))
|
|
255 |
(rewrite gt *current-module* reduction-mode)
|
|
256 |
(unless (= 0 *rule-count*)
|
|
257 |
(setq applied? t))))
|
|
258 |
(values term applied?))
|
|
259 |
(values term nil))))
|
| 214 | 260 |
|
| 215 | 261 |
;;; normalize-sentence : axiom module -> axiom' Bool
|
| 216 | 262 |
;;; [NF]
|
|
| 223 | 269 |
(lhs (rule-lhs target))
|
| 224 | 270 |
(rhs (rule-rhs target))
|
| 225 | 271 |
(condition (rule-condition target))
|
|
272 |
(reduction-mode (if (eq (rule-type ax) :equation)
|
|
273 |
:red
|
|
274 |
:exec))
|
| 226 | 275 |
(app? nil))
|
| 227 | |
(with-citp-debug ()
|
| 228 | |
(with-in-module (module)
|
| 229 | |
(format t "~%[NF]: target")
|
| 230 | |
(print-next)
|
| 231 | |
(print-axiom-brief target)))
|
| 232 | |
;;
|
| 233 | |
(multiple-value-bind (result applied)
|
| 234 | |
(normalize-term-in module lhs)
|
| 235 | |
;; (declare (ignore result))
|
| 236 | |
(or app? (setq app? applied))
|
| 237 | |
(multiple-value-setq (result applied) (normalize-term-in module rhs))
|
| 238 | |
(or app? (setq app? applied))
|
| 239 | |
(unless (is-true? condition)
|
| 240 | |
(multiple-value-setq (result applied)
|
| 241 | |
(normalize-term-in module condition))
|
| 242 | |
(or app? (setq app? applied)))
|
| 243 | |
;;
|
|
276 |
(flet ((set-applied (val)
|
|
277 |
(or app? (setq app? val))))
|
| 244 | 278 |
(with-citp-debug ()
|
| 245 | |
(if (not app?)
|
| 246 | |
(format t "~% ...not applied.")
|
| 247 | |
(progn
|
| 248 | |
(print-next)
|
| 249 | |
(princ "==> ") (print-axiom-brief target))))
|
|
279 |
(with-in-module (module)
|
|
280 |
(format t "~%[NF]: target")
|
|
281 |
(print-next)
|
|
282 |
(print-axiom-brief target)))
|
| 250 | 283 |
;;
|
| 251 | |
(values target app?)))))
|
|
284 |
(multiple-value-bind (result applied)
|
|
285 |
(normalize-term-in module lhs :red)
|
|
286 |
(set-applied applied)
|
|
287 |
(when (eq reduction-mode :exec)
|
|
288 |
(multiple-value-setq (result applied) (normalize-term-in module lhs :exec))
|
|
289 |
(set-applied applied))
|
|
290 |
(multiple-value-setq (result applied) (normalize-term-in module rhs))
|
|
291 |
(set-applied applied)
|
|
292 |
(unless (is-true? condition)
|
|
293 |
(multiple-value-setq (result applied)
|
|
294 |
(normalize-term-in module condition :red))
|
|
295 |
(set-applied applied))
|
|
296 |
;;
|
|
297 |
(with-citp-debug ()
|
|
298 |
(if (not app?)
|
|
299 |
(format t "~% ...not applied.")
|
|
300 |
(progn
|
|
301 |
(print-next)
|
|
302 |
result
|
|
303 |
(princ "==> ") (print-axiom-brief target))))
|
|
304 |
;;
|
|
305 |
(values target app?))))))
|
| 252 | 306 |
|
| 253 | 307 |
;;;
|
| 254 | 308 |
;;; is-contradiction : term term -> Bool
|
|
| 274 | 328 |
;;; check-contradiction : module -> Bool
|
| 275 | 329 |
;;; check if 'true => false' or 'false => true'
|
| 276 | 330 |
;;;
|
|
331 |
(defun check-true<=>false (module &optional (report-header nil))
|
|
332 |
(with-in-module (module)
|
|
333 |
(let ((t-rules (method-rules-with-different-top *bool-true-meth*))
|
|
334 |
(f-rules (method-rules-with-different-top *bool-false-meth*))
|
|
335 |
(ct-rules nil))
|
|
336 |
(dolist (rule (append t-rules f-rules))
|
|
337 |
(when (is-true? (rule-condition rule))
|
|
338 |
(push rule ct-rules)))
|
|
339 |
(when (and ct-rules report-header)
|
|
340 |
(format t "~%[~a]: contradiction " report-header)
|
|
341 |
(let ((*print-indent* (+ 2 *print-indent*)))
|
|
342 |
(dolist (ax (reverse ct-rules))
|
|
343 |
(print-next)
|
|
344 |
(print-axiom-brief ax))))
|
|
345 |
(nreverse ct-rules))))
|
|
346 |
|
| 277 | 347 |
(defun check-contradiction (module &optional (report-header nil))
|
| 278 | |
(with-in-module (module)
|
| 279 | |
(let ((cont-axs (or (method-rules-with-different-top *bool-true-meth*)
|
| 280 | |
(method-rules-with-different-top *bool-false-meth*))))
|
| 281 | |
(when cont-axs
|
| 282 | |
(when report-header
|
| 283 | |
(dolist (ax cont-axs)
|
| 284 | |
(format t "~%[~a]: contradiction " report-header)
|
| 285 | |
(let ((*print-indent* (+ 2 *print-indent*)))
|
| 286 | |
(print-next)
|
| 287 | |
(print-axiom-brief ax))))
|
| 288 | |
(return-from check-contradiction t)))
|
| 289 | |
(let ((true-term (make-applform-simple *bool-sort* *bool-true-meth* nil))
|
| 290 | |
(false-term (make-applform-simple *bool-sort* *bool-false-meth* nil)))
|
| 291 | |
(let ((true=false (make-applform-simple *bool-sort* *eql-op* (list true-term false-term))))
|
| 292 | |
(multiple-value-bind (t-result t-applied?)
|
| 293 | |
(normalize-term-in module true=false)
|
| 294 | |
(when (and t-applied? (is-true? t-result))
|
| 295 | |
(when report-header
|
| 296 | |
(format t "~%[~a]: contradiction " report-header)
|
| 297 | |
(print-next)
|
| 298 | |
(format t " `true = false' can be derived!"))
|
| 299 | |
(return-from check-contradiction t))))
|
| 300 | |
nil)))
|
| 301 | |
|
| 302 | |
;;; check-sentence&mark-label sentence
|
| 303 | |
;;;
|
|
348 |
(or (check-true<=>false module report-header)
|
|
349 |
(with-in-module (module)
|
|
350 |
(let ((true-term (make-applform-simple *bool-sort* *bool-true-meth* nil))
|
|
351 |
(false-term (make-applform-simple *bool-sort* *bool-false-meth* nil)))
|
|
352 |
(let ((true=false (make-applform-simple *bool-sort* *eql-op* (list true-term false-term))))
|
|
353 |
(multiple-value-bind (t-result t-applied?)
|
|
354 |
(normalize-term-in module true=false)
|
|
355 |
(when (and t-applied? (is-true? t-result))
|
|
356 |
(when report-header
|
|
357 |
(format t "~%[~a]: contradiction " report-header)
|
|
358 |
(print-next)
|
|
359 |
(format t " `true = false' can be derived!"))
|
|
360 |
(return-from check-contradiction t))))))
|
|
361 |
nil))
|
|
362 |
|
|
363 |
;;; check-sentence&mark-label : sentence module -> (<result> <normalized-sentence> <origina-sentence>)
|
|
364 |
;;;
|
| 304 | 365 |
(defun check-sentence&mark-label (sentence module &optional (report-header nil))
|
| 305 | 366 |
(with-in-module (module)
|
| 306 | 367 |
(let ((target sentence)
|
|
| 327 | 388 |
(otherwise (values nil target sentence))))))
|
| 328 | 389 |
|
| 329 | 390 |
;;;
|
|
391 |
;;; set-operator-rewrite-rule : module axiom -> void
|
|
392 |
;;;
|
|
393 |
(defun set-operator-rewrite-rule (module axiom)
|
|
394 |
(when (term-is-applform? (rule-lhs axiom))
|
|
395 |
(add-rule-to-method axiom (term-head (rule-lhs axiom)) (module-opinfo-table module))))
|
|
396 |
|
|
397 |
;;;
|
|
398 |
;;; check-goal-is-satisfied : goal -> ( <result> <normalized-target> <possibly-marked-target> )
|
|
399 |
;;;
|
|
400 |
(defun check-goal-is-satisfied (goal &optional (report-header nil))
|
|
401 |
(when (cdr (goal-targets goal))
|
|
402 |
(with-output-chaos-error ('invalid-proof-seq)
|
|
403 |
(format t "Internal error. more than one target!")))
|
|
404 |
(with-in-module ((goal-context goal))
|
|
405 |
(let ((target (car (goal-targets goal)))
|
|
406 |
(context (goal-context goal)))
|
|
407 |
(multiple-value-bind (result norm-target marked-target)
|
|
408 |
(check-sentence&mark-label target context report-header)
|
|
409 |
(cond (result
|
|
410 |
;; dischared by some reason
|
|
411 |
(setf (goal-targets goal) nil)
|
|
412 |
(setf (goal-proved goal) (list marked-target)))
|
|
413 |
((and (is-true? (rule-condition target))
|
|
414 |
(eq (rule-type target) :equation))
|
|
415 |
(setf target (rule-copy-canonicalized target context))
|
|
416 |
(setf (rule-lhs target) (make-applform-simple *bool-sort*
|
|
417 |
*eql-op*
|
|
418 |
(list (rule-lhs target)
|
|
419 |
(rule-rhs target)))
|
|
420 |
(rule-rhs target) *bool-true*)
|
|
421 |
(multiple-value-bind (res-2 norm-target-2 marked-target-2)
|
|
422 |
(check-sentence&mark-label target context report-header)
|
|
423 |
(declare (ignore norm-target-2 marked-target-2))
|
|
424 |
(when res-2
|
|
425 |
(setf (goal-targets goal) nil)
|
|
426 |
(setf (goal-proved goal) (list marked-target)))))
|
|
427 |
(t ;; nothing to do
|
|
428 |
))
|
|
429 |
(values result norm-target marked-target target)))))
|
|
430 |
;;;
|
| 330 | 431 |
;;; try-prove-with-axioms : module List(axiom) axiom : -> { :satisfied | :ct | nil }
|
| 331 | 432 |
;;;
|
| 332 | 433 |
(defparameter .trial-context-module. (%module-decl* "trial-dummy" :object :user nil))
|
|
| 338 | 439 |
(with-in-module (tmodule)
|
| 339 | 440 |
(dolist (ax axioms)
|
| 340 | 441 |
(adjoin-axiom-to-module tmodule ax)
|
| 341 | |
(add-rule-to-method ax
|
| 342 | |
(term-method (rule-lhs ax))
|
| 343 | |
(module-opinfo-table tmodule)))
|
|
442 |
(set-operator-rewrite-rule tmodule ax))
|
| 344 | 443 |
(compile-module tmodule t)
|
| 345 | 444 |
;; first we check contradiction
|
| 346 | 445 |
(if (check-contradiction tmodule report-header)
|
|
| 351 | 450 |
(if applied
|
| 352 | 451 |
(sentence-is-satisfied res)
|
| 353 | 452 |
nil)))))))
|
|
453 |
|
|
454 |
;;; ****************************************************************************
|
|
455 |
;;; Tactic executors
|
|
456 |
;;; ****************************************************************************
|
|
457 |
|
|
458 |
;;; ===========
|
|
459 |
;;; TACTIC: NIL
|
|
460 |
;;; do nothing
|
|
461 |
;;; ===========
|
|
462 |
|
|
463 |
(defun apply-nil (node)
|
|
464 |
(declare (ignore node))
|
|
465 |
(with-output-chaos-warning ()
|
|
466 |
(format t "~%Tactic [NIL] does nothing."))
|
|
467 |
(values nil nil))
|
|
468 |
|
|
469 |
(defun apply-nil-internal (node sentences &optional (all-together nil) (tactic .tactic-nil.))
|
|
470 |
(declare (type ptree-node node)
|
|
471 |
(type list sentences))
|
|
472 |
(let ((goals nil))
|
|
473 |
(cond (all-together
|
|
474 |
(let ((ngoal (prepare-next-goal node tactic)))
|
|
475 |
(setf (goal-targets ngoal) sentences)
|
|
476 |
(push ngoal goals)))
|
|
477 |
(t (dolist (sentence sentences)
|
|
478 |
(let ((ngoal (prepare-next-goal node tactic)))
|
|
479 |
(setf (goal-targets ngoal) (list sentence))
|
|
480 |
(push ngoal goals)))))
|
|
481 |
(values goals (nreverse goals))))
|
| 354 | 482 |
|
| 355 | 483 |
;;; =======================
|
| 356 | 484 |
;;; TACTIC: IMPLICATION[IP]
|
|
| 367 | 495 |
(push (term-copy-and-returns-list-variables sub) cps)))
|
| 368 | 496 |
(setq cps (list (term-copy-and-returns-list-variables condition))))
|
| 369 | 497 |
(dolist (c cps)
|
| 370 | |
(let ((new-ax (make-new-assumption c *bool-true* *bool-true* 'ip))
|
| 371 | |
#||
|
| 372 | |
(make-rule :lhs c
|
| 373 | |
:rhs *bool-true*
|
| 374 | |
:condition *bool-true*
|
| 375 | |
:type :equation
|
| 376 | |
:behavioural (axiom-behavioural axiom)
|
| 377 | |
:labels '(ip))
|
| 378 | |
||#
|
| 379 | |
)
|
|
498 |
(let ((new-ax (make-new-assumption c *bool-true* *bool-true* 'ip)))
|
| 380 | 499 |
(compute-rule-method new-ax)
|
| 381 | 500 |
(push new-ax axs)))
|
| 382 | 501 |
(with-citp-debug ()
|
|
| 389 | 508 |
(defun apply-ip (ptree-node)
|
| 390 | 509 |
(declare (type ptree-node ptree-node))
|
| 391 | 510 |
(with-in-context (ptree-node)
|
| 392 | |
(let ((inconsistent nil)
|
| 393 | |
(remaining nil)
|
| 394 | |
(discharged nil))
|
| 395 | |
(with-in-module ((goal-context .cur-goal.))
|
| 396 | |
(dolist (target .cur-targets.)
|
| 397 | |
(cond ((is-true? (rule-condition target))
|
| 398 | |
;; target has no condition part
|
| 399 | |
(push target remaining))
|
| 400 | |
(t (setq target (normalize-sentence target (goal-context .cur-goal.)))
|
| 401 | |
(let ((condition (rule-condition target)))
|
| 402 | |
(cond ((is-true? condition)
|
| 403 | |
;; target is discharged.
|
| 404 | |
(format t "~%[ip] discharged: ")
|
| 405 | |
(print-axiom-brief target)
|
| 406 | |
(push target discharged))
|
| 407 | |
((equal *bool-false* condition)
|
| 408 | |
;; IC (inconsistency)
|
| 409 | |
(format t "~%[ip] inconsistent axiom")
|
| 410 | |
(let ((*print-indent* (+ 2 *print-indent*)))
|
| 411 | |
(print-next)
|
| 412 | |
(print-axiom-brief target))
|
| 413 | |
(push target inconsistent))
|
| 414 | |
((null (term-variables condition))
|
| 415 | |
;; t = t' if C
|
| 416 | |
;; C is a ground term and is not true.
|
| 417 | |
;; try if (SP + { C } |- t = t') or not..
|
| 418 | |
;; if this is satisfied, discharge it.
|
| 419 | |
(let ((new-axs (generate-ip-derived-axioms *current-module* target))
|
| 420 | |
(next-target (rule-copy-canonicalized target *current-module*))
|
| 421 | |
(satisfied? nil))
|
| 422 | |
(setf (rule-condition next-target) *bool-true*)
|
| 423 | |
(setq satisfied? (try-prove-with-axioms *current-module*
|
| 424 | |
new-axs
|
| 425 | |
next-target
|
| 426 | |
'ip))
|
| 427 | |
(unless satisfied?
|
| 428 | |
(when (eq (rule-type next-target) :equation)
|
| 429 | |
(setf (rule-lhs next-target) (make-applform-simple *bool-sort*
|
| 430 | |
*eql-op*
|
| 431 | |
(list (rule-lhs next-target)
|
| 432 | |
(rule-rhs next-target)))
|
| 433 | |
(rule-rhs next-target) *bool-true*)
|
| 434 | |
(setq satisfied? (try-prove-with-axioms *current-module*
|
| 435 | |
new-axs
|
| 436 | |
next-target))))
|
| 437 | |
|
| 438 | |
(with-citp-debug ()
|
| 439 | |
(format t "~%[ip]: tries to prove ")
|
| 440 | |
(print-axiom-brief next-target)
|
| 441 | |
(print-next)
|
| 442 | |
(format t "with axioms")
|
| 443 | |
(let ((*print-indent* (+ 2 *print-indent*)))
|
| 444 | |
(dolist (ax new-axs)
|
| 445 | |
(print-next)
|
| 446 | |
(print-axiom-brief ax)))
|
| 447 | |
(print-next)
|
| 448 | |
(format t "-- result = ~s" satisfied?))
|
| 449 | |
|
| 450 | |
(cond ((eq satisfied? :satisfied)
|
| 451 | |
;; the target is satisfied assuming new-axs
|
| 452 | |
(push target discharged)
|
| 453 | |
(setf (rule-labels target) (cons 'ip (rule-labels target)))
|
| 454 | |
(format t "~%[ip] discharged: ")
|
| 455 | |
(print-axiom-brief target))
|
| 456 | |
((eq satisfied? :ct)
|
| 457 | |
;; contradiction
|
| 458 | |
(setf (rule-labels target) (cons 'ct (rule-labels target)))
|
| 459 | |
(push target inconsistent)
|
| 460 | |
(format t "~%[ip] discharged: ")
|
| 461 | |
(print-axiom-brief target))
|
| 462 | |
(t
|
| 463 | |
(push target remaining)
|
| 464 | |
;; generate next goal to be proved
|
| 465 | |
;; (SP + { C } |- t = t')
|
| 466 | |
(let ((next-goal (prepare-next-goal ptree-node .tactic-ip.)))
|
| 467 | |
(with-in-module ((goal-context next-goal))
|
| 468 | |
(dolist (new-ax new-axs)
|
| 469 | |
(add-rule-to-method new-ax
|
| 470 | |
(term-method (rule-lhs new-ax))
|
| 471 | |
(module-opinfo-table *current-module*))
|
| 472 | |
(adjoin-axiom-to-module *current-module* new-ax))
|
| 473 | |
(setf (goal-assumptions next-goal) (append (goal-assumptions next-goal) new-axs))
|
| 474 | |
(setf (goal-targets next-goal) (list next-target))
|
| 475 | |
(push next-goal .next-goals.)))))))
|
| 476 | |
(t ;; others
|
| 477 | |
(push target remaining)))))))
|
| 478 | |
;; done for all target
|
| 479 | |
(setf (goal-targets .cur-goal.) (nreverse remaining))
|
| 480 | |
(setf (goal-proved .cur-goal.) (nconc (reverse discharged) (reverse inconsistent))))
|
| 481 | |
;;
|
| 482 | |
(if .next-goals.
|
| 483 | |
(values t .next-goals.)
|
| 484 | |
(progn
|
| 485 | |
(when (goal-proved .cur-goal.)
|
| 486 | |
(format t "~%[ip]: discharged the goal ~s" (goal-name .cur-goal.)))
|
| 487 | |
(values nil nil))))))
|
|
511 |
(let ((original-goal (ptree-node-goal ptree-node)))
|
|
512 |
(flet ((push-next-goal (goal)
|
|
513 |
(unless (eq goal original-goal) (push goal .next-goals.))))
|
|
514 |
(let ((target-goals (distribute-sentences ptree-node .cur-targets. .tactic-ip.)))
|
|
515 |
(dolist (.cur-goal. target-goals)
|
|
516 |
(multiple-value-bind (result target otarget)
|
|
517 |
(check-goal-is-satisfied .cur-goal. 'ip)
|
|
518 |
(declare (ignore otarget))
|
|
519 |
(if result
|
|
520 |
;; discharged by som reason
|
|
521 |
(push-next-goal .cur-goal.))
|
|
522 |
(cond ((and (not (is-true? (rule-condition target)))
|
|
523 |
(null (term-variables (rule-condition target))))
|
|
524 |
;; t = t' if C
|
|
525 |
;; C is a ground term and is not true.
|
|
526 |
;; try if (SP + { C } |- t = t') or not..
|
|
527 |
;; if this is satisfied, discharge it.
|
|
528 |
(let ((ngoal (if (eq .cur-goal. original-goal)
|
|
529 |
(prepare-next-goal ptree-node .tactic-ip.)
|
|
530 |
.cur-goal.)))
|
|
531 |
(with-in-module ((goal-context ngoal))
|
|
532 |
(let ((new-axs (generate-ip-derived-axioms *current-module* target))
|
|
533 |
(next-target (rule-copy-canonicalized target *current-module*)))
|
|
534 |
;; make the target
|
|
535 |
(setf (rule-condition next-target) *bool-true*)
|
|
536 |
(setf (goal-targets ngoal)
|
|
537 |
(list (normalize-sentence next-target *current-module*)))
|
|
538 |
;; add [ip] axioms
|
|
539 |
(dolist (ax new-axs)
|
|
540 |
(adjoin-axiom-to-module *current-module* ax)
|
|
541 |
(set-operator-rewrite-rule *current-module* ax))
|
|
542 |
(setf (goal-assumptions ngoal) (reverse new-axs))
|
|
543 |
;; compile & check
|
|
544 |
(compile-module *current-module* t)
|
|
545 |
;; check-goal-isa-satisfied do all the neccessary things for us.
|
|
546 |
;; (check-goal-is-satisfied ngoal 'ip)
|
|
547 |
(push-next-goal ngoal)))))
|
|
548 |
;; nothig todo. remain the goal as is
|
|
549 |
(t ))))
|
|
550 |
;; done for all goals
|
|
551 |
(values .next-goals. (nreverse .next-goals.)))))))
|
| 488 | 552 |
|
| 489 | 553 |
;;; =================================
|
| 490 | 554 |
;;; TACTIC: Theorem of Constants [TC]
|
|
| 504 | 568 |
|
| 505 | 569 |
(defun apply-tc (ptree-node)
|
| 506 | 570 |
(declare (type ptree-node ptree-node))
|
|
571 |
;;
|
| 507 | 572 |
(with-in-context (ptree-node)
|
| 508 | |
(let ((discharged nil)
|
| 509 | |
(remaining nil))
|
| 510 | |
;; for each target sentence do TC
|
| 511 | |
(dolist (target .cur-targets.)
|
| 512 | |
(multiple-value-bind (c-result cur-target original-sentence)
|
| 513 | |
(check-sentence&mark-label target (goal-context .cur-goal.) 'tc)
|
| 514 | |
(cond (c-result ; satisfied or contradiction
|
| 515 | |
(push original-sentence discharged))
|
| 516 | |
((axiom-variables cur-target)
|
| 517 | |
;; (push target remaining)
|
| 518 | |
(let ((next-goal (prepare-next-goal ptree-node .tactic-tc.)))
|
| 519 | |
(with-in-module ((goal-context next-goal))
|
| 520 | |
(let* ((next-target (rule-copy-canonicalized cur-target *current-module*))
|
| 521 | |
(vars (axiom-variables next-target))
|
| 522 | |
(subst (make-tc-variable-substitutions next-goal vars)))
|
| 523 | |
(push next-goal .next-goals.)
|
| 524 | |
(setf (rule-lhs next-target) (substitution-image-simplifying subst (rule-lhs next-target))
|
| 525 | |
(rule-rhs next-target) (substitution-image-simplifying subst (rule-rhs next-target))
|
| 526 | |
(rule-condition next-target) (if (is-true? (rule-condition next-target))
|
| 527 | |
*bool-true*
|
| 528 | |
(substitution-image-simplifying subst (rule-condition next-target))))
|
| 529 | |
(compute-rule-method next-target)
|
| 530 | |
(setf (goal-targets next-goal) (list next-target))))))
|
| 531 | |
(t (push target remaining)))))
|
| 532 | |
(setf (goal-proved .cur-goal.) (nreverse discharged))
|
| 533 | |
(setf (goal-targets .cur-goal.) (nreverse remaining))
|
| 534 | |
(if .next-goals.
|
| 535 | |
(values t (nreverse .next-goals.))
|
| 536 | |
(if (goal-targets .cur-goal.)
|
| 537 | |
(values nil nil)
|
| 538 | |
(progn
|
| 539 | |
(format t "~%[tc]: discharged the goal ~s" (goal-name .cur-goal.))
|
| 540 | |
(values t nil)))))))
|
|
573 |
(let ((original-goal .cur-goal.))
|
|
574 |
(flet ((push-next-goal (goal)
|
|
575 |
(unless (eq goal original-goal) (push goal .next-goals.))))
|
|
576 |
(let ((target-goals (distribute-sentences ptree-node .cur-targets. .tactic-tc.)))
|
|
577 |
(dolist (cgoal target-goals)
|
|
578 |
(multiple-value-bind (res sentence osentence)
|
|
579 |
(check-goal-is-satisfied cgoal 'rd)
|
|
580 |
(declare (ignore osentence))
|
|
581 |
(cond (res
|
|
582 |
;; discharged
|
|
583 |
(push-next-goal cgoal))
|
|
584 |
((axiom-variables sentence)
|
|
585 |
(when (eq cgoal original-goal)
|
|
586 |
(setq cgoal (prepare-next-goal ptree-node .tactic-tc.)))
|
|
587 |
(push-next-goal cgoal)
|
|
588 |
(with-in-module ((goal-context cgoal))
|
|
589 |
(let* ((next-target (rule-copy-canonicalized sentence *current-module*))
|
|
590 |
(vars (axiom-variables next-target))
|
|
591 |
(subst (make-tc-variable-substitutions cgoal vars)))
|
|
592 |
(apply-substitution-to-axiom subst next-target)
|
|
593 |
(compute-rule-method next-target)
|
|
594 |
(setf (goal-targets cgoal)
|
|
595 |
(list (normalize-sentence next-target *current-module*))))))
|
|
596 |
(t ))))
|
|
597 |
(values .next-goals. (nreverse .next-goals.)))))))
|
| 541 | 598 |
|
| 542 | 599 |
;;; ===================================
|
| 543 | 600 |
;;; TACTIC: Simultaneous Induction [SI]
|
|
| 651 | 708 |
(dolist (subst all-subst)
|
| 652 | 709 |
(when (every #'(lambda (sub) (null (method-arity (cdr sub)))) subst)
|
| 653 | 710 |
(push subst res)))
|
|
711 |
(with-citp-debug ()
|
|
712 |
(format t "~%[si] base case subst")
|
|
713 |
(dolist (sub res)
|
|
714 |
(print-next)
|
|
715 |
(print-substitution sub)))
|
| 654 | 716 |
(nreverse res)))
|
| 655 | 717 |
|
| 656 | 718 |
;;;
|
|
| 661 | 723 |
(dolist (subst all-subst)
|
| 662 | 724 |
(unless (every #'(lambda (sub) (null (method-arity (cdr sub)))) subst)
|
| 663 | 725 |
(push subst res)))
|
|
726 |
(with-citp-debug ()
|
|
727 |
(format t "~%[si] get-induction-step-subsutitutions")
|
|
728 |
(dolist (sub res)
|
|
729 |
(print-next)
|
|
730 |
(print-substitution sub)))
|
| 664 | 731 |
(nreverse res)))
|
| 665 | 732 |
|
| 666 | 733 |
;;;
|
|
| 690 | 757 |
;;; generates base case axioms for a given target
|
| 691 | 758 |
;;;
|
| 692 | 759 |
(defun set-base-cases (goal target base-substitutions)
|
| 693 | |
(let ((all-targets nil))
|
|
760 |
(let ((all-targets nil)
|
|
761 |
(app? nil))
|
| 694 | 762 |
(with-in-module ((goal-context goal))
|
| 695 | 763 |
(dolist (subst base-substitutions)
|
| 696 | 764 |
(let* ((new-target (rule-copy-canonicalized target *current-module*))
|
| 697 | 765 |
(real-subst (make-real-induction-subst subst (axiom-variables new-target))))
|
| 698 | |
(setf (rule-lhs new-target) (substitution-image-simplifying real-subst (rule-lhs new-target))
|
| 699 | |
(rule-rhs new-target) (substitution-image-simplifying real-subst (rule-rhs new-target))
|
| 700 | |
(rule-condition new-target) (substitution-image-simplifying real-subst (rule-condition new-target)))
|
| 701 | |
(push new-target all-targets)))
|
| 702 | |
(setf (goal-targets goal) (nconc (goal-targets goal) all-targets)))))
|
|
766 |
(when real-subst
|
|
767 |
(setq app? t)
|
|
768 |
(apply-substitution-to-axiom real-subst new-target)
|
|
769 |
(push new-target all-targets)))))
|
|
770 |
(setf (goal-targets goal) (nconc (goal-targets goal) all-targets))
|
|
771 |
app?))
|
| 703 | 772 |
|
| 704 | 773 |
;;;
|
| 705 | 774 |
;;; make-step-constructor-term
|
|
| 718 | 787 |
res))))
|
| 719 | 788 |
|
| 720 | 789 |
;;;
|
| 721 | |
;;; make-induction-step-subst : goal axiom List((var . op)) -> substitution
|
|
790 |
;;; make-induction-step-subst : goal axiom (var . op) -> substitution
|
| 722 | 791 |
;;;
|
| 723 | 792 |
(defun make-induction-step-subst (goal target v-op-list)
|
| 724 | 793 |
;; we ignore all mapped operators are constant constructors.
|
|
| 778 | 847 |
(cons (car sub) (list (third sub))))
|
| 779 | 848 |
hypo-v-op))
|
| 780 | 849 |
(all-subst nil))
|
| 781 | |
;; return if there are no possible combinations
|
| 782 | |
(unless (cdr hypo-v-op)
|
| 783 | 850 |
(with-citp-debug ()
|
| 784 | |
(format t "~%resolve subst: no possible combinations"))
|
| 785 | |
(return-from resolve-induction-subst (list (make-proper-alist rsubsts))))
|
|
851 |
(format t "~%[si] resolve induction step: given")
|
|
852 |
(print-next) (format t "hypo-v-op: ~s" hypo-v-op)
|
|
853 |
(print-next) (princ "step-subst" )
|
|
854 |
(print-substitution step-subst))
|
|
855 |
;; return if there are no possible combinations
|
|
856 |
;; (unless (cdr hypo-v-op)
|
|
857 |
;; (return-from resolve-induction-subst (list (make-proper-alist rsubsts))))
|
| 786 | 858 |
;;
|
| 787 | 859 |
(with-citp-debug ()
|
| 788 | 860 |
(format t "~%resolve subst: given")
|
|
| 840 | 912 |
t)
|
| 841 | 913 |
|
| 842 | 914 |
(defun add-hypothesis (step-goal target hypo-subst step-subst)
|
|
915 |
(with-citp-debug ()
|
|
916 |
(format t "~%[si]: add-hypothesis")
|
|
917 |
(print-next) (princ "-- hypo-subst ")
|
|
918 |
(dolist (hp hypo-subst)
|
|
919 |
(print-next)
|
|
920 |
(print-substitution hp))
|
|
921 |
(print-next) (princ "-- step-subst ")
|
|
922 |
(print-substitution step-subst))
|
| 843 | 923 |
(dolist (osub hypo-subst)
|
| 844 | 924 |
(dolist (sub (resolve-induction-subst step-goal osub step-subst))
|
| 845 | 925 |
(unless (subst-is-equal sub step-subst)
|
|
| 847 | 927 |
(subst (make-real-induction-step-subst sub (axiom-variables hypo))))
|
| 848 | 928 |
(with-citp-debug
|
| 849 | 929 |
(format t "~%>>[applying hypo subst] ")
|
| 850 | |
(print-substitution subst))
|
| 851 | |
(setf (rule-lhs hypo) (substitution-image-simplifying subst (rule-lhs hypo))
|
| 852 | |
(rule-rhs hypo) (substitution-image-simplifying subst (rule-rhs hypo))
|
| 853 | |
(rule-condition hypo) (if (is-true? (rule-condition hypo))
|
| 854 | |
*bool-true*
|
| 855 | |
(substitution-image-simplifying subst (rule-condition hypo)))
|
| 856 | |
(rule-labels hypo) '(si)) ; (cons 'ind-hypo (rule-labels target))
|
| 857 | |
|
|
930 |
(print-substitution subst)
|
|
931 |
(print-next)
|
|
932 |
(princ "to ")
|
|
933 |
(print-axiom-brief hypo))
|
|
934 |
(apply-substitution-to-axiom subst hypo '(si))
|
| 858 | 935 |
(compute-rule-method hypo)
|
| 859 | |
(add-rule-to-method hypo (term-method (rule-lhs hypo)) (module-opinfo-table *current-module*))
|
|
936 |
(set-operator-rewrite-rule *current-module* hypo)
|
| 860 | 937 |
(adjoin-axiom-to-module *current-module* hypo)
|
|
938 |
(with-citp-debug ()
|
|
939 |
(format t "~%--> ")
|
|
940 |
(print-axiom-brief hypo))
|
| 861 | 941 |
(setf (goal-assumptions step-goal) (append (goal-assumptions step-goal) (list hypo))))))))
|
| 862 | 942 |
|
| 863 | 943 |
;;;
|
|
| 871 | 951 |
(with-citp-debug
|
| 872 | 952 |
(format t "~%>>[applying step subst] ")
|
| 873 | 953 |
(print-substitution subst))
|
| 874 | |
(setf (rule-lhs new-target) (substitution-image-simplifying subst (rule-lhs new-target))
|
| 875 | |
(rule-rhs new-target) (substitution-image-simplifying subst (rule-rhs new-target))
|
| 876 | |
(rule-condition new-target) (if (is-true? (rule-condition new-target))
|
| 877 | |
*bool-true*
|
| 878 | |
(substitution-image-simplifying subst (rule-condition new-target))))
|
|
954 |
(apply-substitution-to-axiom subst new-target)
|
| 879 | 955 |
(setf (goal-targets step-goal) (nconc (goal-targets step-goal) (list new-target))))))
|
| 880 | 956 |
|
| 881 | 957 |
;;;
|
|
| 885 | 961 |
(defun induction-cases (parent-node)
|
| 886 | 962 |
(declare (type ptree-node parent-node))
|
| 887 | 963 |
(let* ((cur-goal (ptree-node-goal parent-node))
|
| 888 | |
(cur-targets (goal-targets cur-goal))
|
|
964 |
(cur-targets nil)
|
| 889 | 965 |
(indvars (goal-indvars cur-goal))
|
| 890 | 966 |
(all-subst (make-indvar-comb-substitutions indvars
|
| 891 | 967 |
(gather-constructor-ops (goal-context cur-goal))))
|
| 892 | 968 |
(base-goal (prepare-next-goal parent-node .tactic-si.))
|
| 893 | |
(step-goals nil))
|
|
969 |
(step-goals nil)
|
|
970 |
(need-goal nil)
|
|
971 |
(base-generated nil)
|
|
972 |
(remainings nil))
|
| 894 | 973 |
;;
|
| 895 | 974 |
(with-citp-debug ()
|
|
975 |
(format t "~%[si] all possible substitutions")
|
| 896 | 976 |
(let ((num 0))
|
| 897 | 977 |
(declare (type fixnum num))
|
| 898 | 978 |
(dolist (subs all-subst)
|
| 899 | 979 |
(format t "~%subst #~d" (incf num))
|
| 900 | 980 |
(let ((*print-indent* (+ 2 *print-indent*)))
|
| 901 | 981 |
(print-next)
|
| 902 | |
;; (dolist (s subs) (print-substitution s))
|
| 903 | 982 |
(print-substitution subs)))))
|
|
983 |
|
|
984 |
;; implicit NF application
|
|
985 |
(dolist (ct (goal-targets cur-goal))
|
|
986 |
(multiple-value-bind (ntarget app?)
|
|
987 |
(normalize-sentence ct (goal-context cur-goal))
|
|
988 |
(when app? (setq need-goal t))
|
|
989 |
(push ntarget cur-targets)))
|
|
990 |
(setq cur-targets (nreverse cur-targets))
|
| 904 | 991 |
|
| 905 | 992 |
;; generate base cases
|
| 906 | 993 |
;;
|
| 907 | 994 |
(dolist (target cur-targets)
|
| 908 | |
(set-base-cases base-goal target (get-induction-base-substitutions all-subst)))
|
|
995 |
(if (not (set-base-cases base-goal target (get-induction-base-substitutions all-subst)))
|
|
996 |
(when need-goal
|
|
997 |
(push target remainings))
|
|
998 |
(setq base-generated t)))
|
|
999 |
(unless base-generated (setq base-goal nil))
|
| 909 | 1000 |
|
| 910 | 1001 |
;; generate step cases
|
| 911 | 1002 |
;; we generate all possible combinations of given induction variables.
|
|
| 920 | 1011 |
(make-induction-step-subst step-goal target subst)
|
| 921 | 1012 |
(add-hypothesis step-goal target hypo-subst-list step-subst)
|
| 922 | 1013 |
(add-step-cases step-goal target step-subst)))
|
| 923 | |
;; (!setup-reduction (goal-context step-goal))
|
| 924 | |
(push step-goal step-goals))))
|
|
1014 |
(cond ((goal-targets step-goal)
|
|
1015 |
(push step-goal step-goals))
|
|
1016 |
(t ))))) ; do nothig
|
|
1017 |
;;
|
|
1018 |
(when remainings
|
|
1019 |
(multiple-value-bind (ap? nil-goals)
|
|
1020 |
(apply-nil-internal parent-node (reverse remainings) :all-togather)
|
|
1021 |
(declare (ignore ap?))
|
|
1022 |
(dolist (ng nil-goals)
|
|
1023 |
(push ng step-goals))))
|
| 925 | 1024 |
;;
|
| 926 | |
(values t (cons base-goal (nreverse step-goals)))))
|
| 927 | |
|
| 928 | |
;;; apply-si
|
|
1025 |
(if base-goal
|
|
1026 |
(values t (cons base-goal (nreverse step-goals)))
|
|
1027 |
(if step-goals
|
|
1028 |
;; case remainings
|
|
1029 |
(values t step-goals)
|
|
1030 |
(values nil nil)))))
|
|
1031 |
|
|
1032 |
;;;
|
|
1033 |
;;; apply-si : ptree-node -> (applied? . List(goal))
|
| 929 | 1034 |
;;;
|
| 930 | 1035 |
(defun apply-si (ptree-node)
|
| 931 | 1036 |
(declare (type ptree-node ptree-node))
|
| 932 | |
;; internally apply-rd
|
| 933 | |
(apply-rd ptree-node)
|
| 934 | |
;;
|
| 935 | 1037 |
(let ((cur-goal (ptree-node-goal ptree-node)))
|
| 936 | 1038 |
(unless (and (goal-indvars cur-goal) (goal-targets cur-goal))
|
| 937 | 1039 |
(return-from apply-si nil))
|
|
| 1148 | 1250 |
(format t "~%>>[ca] adding an axiom to module ~s" (get-module-simple-name (goal-context next-goal)))
|
| 1149 | 1251 |
(print-next)
|
| 1150 | 1252 |
(print-axiom-brief axs))
|
| 1151 | |
(add-rule-to-method axs (term-method (rule-lhs axs)) (module-opinfo-table *current-module*))
|
|
1253 |
(set-operator-rewrite-rule *current-module* axs)
|
| 1152 | 1254 |
(adjoin-axiom-to-module *current-module* axs)
|
| 1153 | 1255 |
(push axs case-axioms))))
|
| 1154 | 1256 |
(setf (goal-assumptions next-goal) (append (goal-assumptions next-goal)
|
|
| 1158 | 1260 |
;;;
|
| 1159 | 1261 |
;;; generate-cases : ptree-node term List(conditional-axiom)
|
| 1160 | 1262 |
;;;
|
| 1161 | |
(defun generate-cases (ptree-node target conditional-rules)
|
| 1162 | |
(let ((gterms (get-gterms-from-axiom target))
|
| 1163 | |
(next-goals nil))
|
| 1164 | |
;; g-rs-pairs: ((gterm-1 . List(rs-pairs)) .. (gterm-n . (List(rs-pairs))))
|
| 1165 | |
;; rs-pairs : ((rule-1 . subst-1) ... (rule-m . subst-m))
|
| 1166 | |
(let ((g-rs-pairs nil))
|
| 1167 | |
(dolist (gterm gterms)
|
| 1168 | |
;; split cases for each ground term
|
| 1169 | |
;; Gterm-1 : (rs-1 rs-2) (rs-3) --> ((rs-1 rs-3) (rs-2 rs-3))
|
| 1170 | |
(let ((rs-pairs (find-gterm-matching-conditionals gterm conditional-rules)))
|
| 1171 | |
(when rs-pairs
|
| 1172 | |
(setf g-rs-pairs (nconc g-rs-pairs rs-pairs)))))
|
| 1173 | |
;; make all combinations and generate cases
|
| 1174 | |
;; Gterm-1 : (rs-1 rs-2) (rs-3) --> ((rs-1 rs-3) (rs-2 rs-3))
|
| 1175 | |
;; Gterm-2 : (rs-4) --> ((rs-4))
|
| 1176 | |
;; ==> ((rs-1 rs-3 rs-4) (rs-2 rs-3 rs-4)) <-- two groups, i.e, two next goals
|
| 1177 | |
(let ((rv-combs (select-comb-elems g-rs-pairs)))
|
| 1178 | |
(dolist (rv-com rv-combs)
|
| 1179 | |
(with-citp-debug ()
|
| 1180 | |
(dolist (rr rv-com)
|
| 1181 | |
(format t "~%>>[ca] gterm rs-pair: ")
|
| 1182 | |
(print-next)
|
| 1183 | |
(print-axiom-brief (car rr))
|
| 1184 | |
(print-next)
|
| 1185 | |
(print-substitution (cdr rr))))
|
| 1186 | |
;; rv-com ((gterm-1 . rv-pair-1-1) (gterm-2 . rvpair-2-1) .. (gterm-n . rvpair-n-1))
|
| 1187 | |
(let ((next-goal (prepare-next-goal ptree-node .tactic-ca.)))
|
| 1188 | |
(setf (goal-targets next-goal) (goal-targets (ptree-node-goal ptree-node)))
|
| 1189 | |
(generate-case-axioms next-goal rv-com)
|
| 1190 | |
(push next-goal next-goals))))
|
|
1263 |
(defun generate-cases (ptree-node target conditional-rules divide?)
|
|
1264 |
(declare (type ptree-node ptree-node)
|
|
1265 |
(list conditional-rules))
|
|
1266 |
(multiple-value-bind (norm-target app?)
|
|
1267 |
(normalize-sentence target (goal-context (ptree-node-goal ptree-node)))
|
|
1268 |
(when app?
|
|
1269 |
(setq target norm-target))
|
|
1270 |
;; then generate possible cases
|
|
1271 |
(let ((gterms (get-gterms-from-axiom target))
|
|
1272 |
(next-goals nil)
|
|
1273 |
(remainings nil))
|
|
1274 |
;; g-rs-pairs: ((gterm-1 . List(rs-pairs)) .. (gterm-n . (List(rs-pairs))))
|
|
1275 |
;; rs-pairs : ((rule-1 . subst-1) ... (rule-m . subst-m))
|
|
1276 |
(let ((g-rs-pairs nil))
|
|
1277 |
(dolist (gterm gterms)
|
|
1278 |
;; split cases for each ground term
|
|
1279 |
;; Gterm-1 : (rs-1 rs-2) (rs-3) --> ((rs-1 rs-3) (rs-2 rs-3))
|
|
1280 |
(let ((rs-pairs (find-gterm-matching-conditionals gterm conditional-rules)))
|
|
1281 |
(when rs-pairs
|
|
1282 |
(setf g-rs-pairs (nconc g-rs-pairs rs-pairs)))))
|
|
1283 |
;; make all combinations and generate cases
|
|
1284 |
;; Gterm-1 : (rs-1 rs-2) (rs-3) --> ((rs-1 rs-3) (rs-2 rs-3))
|
|
1285 |
;; Gterm-2 : (rs-4) --> ((rs-4))
|
|
1286 |
;; ==> ((rs-1 rs-3 rs-4) (rs-2 rs-3 rs-4)) <-- two groups, i.e, two next goals
|
|
1287 |
(let ((rv-combs (select-comb-elems g-rs-pairs))
|
|
1288 |
(next-goal nil))
|
|
1289 |
(cond (rv-combs
|
|
1290 |
(dolist (rv-com rv-combs)
|
|
1291 |
(with-citp-debug ()
|
|
1292 |
(dolist (rr rv-com)
|
|
1293 |
(format t "~%>>[ca] gterm rs-pair: ")
|
|
1294 |
(print-next)
|
|
1295 |
(print-axiom-brief (car rr))
|
|
1296 |
(print-next)
|
|
1297 |
(print-substitution (cdr rr))))
|
|
1298 |
;; rv-com ((gterm-1 . rv-pair-1-1) (gterm-2 . rvpair-2-1) .. (gterm-n . rvpair-n-1))
|
|
1299 |
(setq next-goal (prepare-next-goal ptree-node .tactic-ca.))
|
|
1300 |
(setf (goal-targets next-goal) (goal-targets (ptree-node-goal ptree-node)))
|
|
1301 |
(generate-case-axioms next-goal rv-com)
|
|
1302 |
(push next-goal next-goals)))
|
|
1303 |
(t (push target remainings)))))
|
|
1304 |
;;
|
|
1305 |
(when remainings
|
|
1306 |
(when (or next-goals app? divide?)
|
|
1307 |
(multiple-value-bind (app? nop-goals)
|
|
1308 |
(apply-nil-internal ptree-node (reverse remainings) nil .tactic-ca.)
|
|
1309 |
(declare (ignore app?))
|
|
1310 |
(dolist(ng nop-goals)
|
|
1311 |
(push ng next-goals)))))
|
| 1191 | 1312 |
(values next-goals (nreverse next-goals)))))
|
| 1192 | 1313 |
|
| 1193 | 1314 |
(defun apply-ca (ptree-node)
|
|
| 1195 | 1316 |
(with-in-context (ptree-node)
|
| 1196 | 1317 |
(with-in-module ((goal-context .cur-goal.))
|
| 1197 | 1318 |
(let ((crules (remove-if #'(lambda (x) (is-true? (rule-condition x)))
|
| 1198 | |
(module-all-rules (goal-context .cur-goal.)))))
|
|
1319 |
(module-all-rules (goal-context .cur-goal.))))
|
|
1320 |
(divide? (cdr .cur-targets.)))
|
| 1199 | 1321 |
(dolist (target .cur-targets.)
|
| 1200 | 1322 |
(multiple-value-bind (applied goals)
|
| 1201 | |
(generate-cases ptree-node target crules)
|
|
1323 |
(generate-cases ptree-node target crules divide?)
|
| 1202 | 1324 |
(declare (ignore applied))
|
| 1203 | 1325 |
(when goals (setq .next-goals. (nconc .next-goals. goals)))))
|
| 1204 | 1326 |
(values .next-goals. .next-goals.)))))
|
|
| 1224 | 1346 |
(t (with-in-module (module)
|
| 1225 | 1347 |
(setq ax (parse-axiom-declaration (parse-module-element-1 (cdr target-form))))
|
| 1226 | 1348 |
(when add-to-module
|
| 1227 | |
(add-rule-to-method ax (term-method (rule-lhs ax)) (module-opinfo-table module))
|
|
1349 |
(set-operator-rewrite-rule module ax)
|
| 1228 | 1350 |
(adjoin-axiom-to-module module ax)
|
| 1229 | 1351 |
(set-needs-rule)))))
|
| 1230 | 1352 |
ax))
|
|
| 1280 | 1402 |
(let ((new-axiom (rule-copy-canonicalized axiom module))
|
| 1281 | 1403 |
(rsubst nil))
|
| 1282 | 1404 |
(setq rsubst (make-real-instanciation-subst subst (axiom-variables new-axiom)))
|
| 1283 | |
(setf (rule-lhs new-axiom) (substitution-image-simplifying rsubst (rule-lhs new-axiom))
|
| 1284 | |
(rule-rhs new-axiom) (substitution-image-simplifying rsubst (rule-rhs new-axiom))
|
| 1285 | |
(rule-condition new-axiom) (substitution-image-simplifying rsubst (rule-condition new-axiom))
|
| 1286 | |
(rule-labels new-axiom) '(init))
|
|
1405 |
(apply-substitution-to-axiom rsubst new-axiom '(init))
|
|
1406 |
#||
|
| 1287 | 1407 |
(when (axiom-variables new-axiom)
|
| 1288 | 1408 |
(with-output-chaos-error ('not-ground)
|
| 1289 | 1409 |
(format t "Instanciating an axiom, not all variable substitutions are supplied.")
|
| 1290 | 1410 |
(dolist (v (axiom-variables new-axiom))
|
| 1291 | 1411 |
(print-next)
|
| 1292 | 1412 |
(term-print-with-sort v))))
|
|
1413 |
||#
|
| 1293 | 1414 |
new-axiom))
|
| 1294 | 1415 |
|
| 1295 | 1416 |
;;;
|
|
| 1315 | 1436 |
(print-axiom-brief instance))
|
| 1316 | 1437 |
(pr-goal (ptree-node-goal context))
|
| 1317 | 1438 |
;;
|
| 1318 | |
(add-rule-to-method instance (term-method (rule-lhs instance)) (module-opinfo-table *current-module*))
|
|
1439 |
(set-operator-rewrite-rule *current-module* instance)
|
| 1319 | 1440 |
(adjoin-axiom-to-module *current-module* instance)
|
| 1320 | 1441 |
;; (!setup-reduction *current-module*)
|
| 1321 | 1442 |
)))))
|
|
| 1537 | 1658 |
(setf (rule-lhs cps) lhs
|
| 1538 | 1659 |
(rule-rhs cps) rhs)))
|
| 1539 | 1660 |
(compute-rule-method cps)
|
| 1540 | |
(add-rule-to-method cps (term-method (rule-lhs cps)) (module-opinfo-table *current-module*))
|
|
1661 |
(set-operator-rewrite-rule *current-module* cps)
|
| 1541 | 1662 |
(adjoin-axiom-to-module *current-module* cps)
|
| 1542 | 1663 |
(setq applied (nconc applied (list cps))))
|
| 1543 | 1664 |
(when applied
|
|
| 1564 | 1685 |
;;; returns the list of generated goal nodes.
|
| 1565 | 1686 |
;;; -----------------------------------------------------
|
| 1566 | 1687 |
|
| 1567 | |
(defun apply-tactic (ptree-node tactic)
|
|
1688 |
(defun apply-tactic (ptree-node tactic &optional (verbose t))
|
| 1568 | 1689 |
(declare (type ptree-node ptree-node)
|
| 1569 | 1690 |
(type tactic tactic))
|
| 1570 | 1691 |
(let ((*chaos-quiet* t))
|
|
| 1582 | 1703 |
(type list next-goals))
|
| 1583 | 1704 |
(unless applied (return-from apply-tactic nil))
|
| 1584 | 1705 |
(unless next-goals
|
| 1585 | |
#||
|
| 1586 | |
;; this means this goal is successfully proved
|
| 1587 | |
(if (null (discharge-node ptree-node))
|
| 1588 | |
;; all over
|
| 1589 | |
(return-from apply-tactic :done)
|
| 1590 | |
(return-from apply-tactic nil))
|
| 1591 | |
||#
|
|
1706 |
;; reset the current ptree-node status,
|
|
1707 |
;; i.e., cancel side effents
|
|
1708 |
(initialize-ptree-node ptree-node)
|
| 1592 | 1709 |
(return-from apply-tactic nil))
|
| 1593 | 1710 |
(format t "~%>> Generated ~d goal~p" (length next-goals) (length next-goals))
|
| 1594 | |
(dolist (goal next-goals)
|
| 1595 | |
(pr-goal goal)
|
| 1596 | |
(add-ptree-child ptree-node goal))
|
|
1711 |
(add-ptree-children ptree-node next-goals)
|
|
1712 |
(when verbose
|
|
1713 |
(dolist (gn (ptree-node-subnodes ptree-node))
|
|
1714 |
(pr-goal (ptree-node-goal gn))))
|
| 1597 | 1715 |
(ptree-node-subnodes ptree-node))))
|
| 1598 | 1716 |
|
| 1599 | 1717 |
;;;
|
| 1600 | 1718 |
;;; apply-tactics-to-node
|
| 1601 | 1719 |
;;;
|
| 1602 | 1720 |
(defun apply-tactics-to-node (target-node tactics)
|
|
1721 |
(unless tactics (return-from apply-tactics-to-node nil))
|
| 1603 | 1722 |
(let ((subs (apply-tactic target-node (car tactics))))
|
| 1604 | |
(dolist (tactic (cdr tactics))
|
| 1605 | |
(dolist (target subs)
|
| 1606 | |
(apply-tactic target tactic)))))
|
|
1723 |
(if subs
|
|
1724 |
(dolist (target subs)
|
|
1725 |
(apply-tactics-to-node target (cdr tactics)))
|
|
1726 |
(apply-tactics-to-node target-node (cdr tactics)))))
|
| 1607 | 1727 |
|
| 1608 | 1728 |
;;;
|
| 1609 | 1729 |
;;; apply-tactics
|
| 1610 | 1730 |
;;;
|
| 1611 | 1731 |
(defun apply-tactics (ptree tactics)
|
| 1612 | |
(if (next-proof-target-is-specified?)
|
| 1613 | |
(apply-tactics-to-node (get-next-proof-context ptree) tactics)
|
| 1614 | |
(dolist (tactic tactics)
|
| 1615 | |
(let ((next-targets (get-unproved-nodes ptree)))
|
| 1616 | |
(unless next-targets
|
| 1617 | |
(format t "~%>> All goals have been discharged!")
|
| 1618 | |
(setq *next-default-proof-node* nil)
|
| 1619 | |
(return-from apply-tactics nil))
|
| 1620 | |
(dolist (target next-targets)
|
| 1621 | |
(apply-tactic target tactic)))))
|
|
1732 |
(declare (type ptree ptree)
|
|
1733 |
(type list tactics))
|
|
1734 |
(let ((target (get-next-proof-context ptree)))
|
|
1735 |
(unless target
|
|
1736 |
(format t "~%>> All goals have been discharged!")
|
|
1737 |
(return-from apply-tactics nil))
|
|
1738 |
(apply-tactics-to-node target tactics))
|
| 1622 | 1739 |
(check-success ptree))
|
| 1623 | 1740 |
|
| 1624 | 1741 |
;;;
|