Fixed the problem with reduction immediately after adding an axiom in opening module.
tswd
8 years ago
| 248 | 248 |
;; (reset-rewrite-counters)-(begin-rewrite)-(end-rewrite)
|
| 249 | 249 |
(defun reducer-no-stat (term context-module rewrite-mode)
|
| 250 | 250 |
(with-in-module ((prepare-reduction-env term context-module rewrite-mode nil))
|
|
251 |
;; be ready for rewriting
|
|
252 |
(!setup-reduction *current-module*)
|
| 251 | 253 |
(catch 'rewrite-abort
|
| 252 | 254 |
(if *rewrite-exec-mode*
|
| 253 | 255 |
(rewrite-exec $$target-term *current-module* rewrite-mode)
|
| 148 | 148 |
;; print out prelude message
|
| 149 | 149 |
(unless *chaos-quiet*
|
| 150 | 150 |
(with-in-module (mod)
|
| 151 | |
(format t "~%-- ~a in " (if (eq mode :exec)
|
|
151 |
(format t "~&-- ~a in " (if (eq mode :exec)
|
| 152 | 152 |
"execute"
|
| 153 | 153 |
(if (eq mode :exec+)
|
| 154 | 154 |
"execute!"
|
|
| 162 | 162 |
(term-print-with-sort term))
|
| 163 | 163 |
(flush-all)))
|
| 164 | 164 |
;; do the rewriting
|
|
165 |
(let ((*chaos-quiet* t))
|
|
166 |
(compile-module mod))
|
| 165 | 167 |
(setq result (reducer term mod mode))
|
| 166 | 168 |
;; print out the resultant term
|
| 167 | 169 |
(with-in-module (mod)
|
|
| 263 | 265 |
(target-term nil))
|
| 264 | 266 |
(when (modexp-is-error mod)
|
| 265 | 267 |
(with-output-chaos-error ('no-such-module)
|
| 266 | |
(princ "incorrect module expression, not such module: ")
|
|
268 |
(princ "incorrect module expression, no such module: ")
|
| 267 | 269 |
(print-chaos-object modexp)))
|
| 268 | 270 |
;;
|
| 269 | 271 |
(context-push-and-move (get-context-module t) mod)
|
|
| 455 | 457 |
(setf mod (eval-modexp modexp))
|
| 456 | 458 |
(when (modexp-is-error mod)
|
| 457 | 459 |
(with-output-chaos-error ('no-such-module)
|
| 458 | |
(format t "incorrect module expression, unknown module?")
|
|
460 |
(format t "incorrect module expression, or unknown module: ")
|
| 459 | 461 |
(print-modexp modexp)))
|
| 460 | 462 |
(describe-module mod)))
|
| 461 | 463 |
|
|
| 472 | 474 |
(eval-modexp modexp)))
|
| 473 | 475 |
(when (modexp-is-error mod)
|
| 474 | 476 |
(with-output-chaos-error ('no-such-module)
|
| 475 | |
(princ "incorrect module expression or uknown module")
|
|
477 |
(princ "incorrect module expression or uknown module ")
|
| 476 | 478 |
(print-modexp modexp)))
|
| 477 | 479 |
;;
|
| 478 | 480 |
(unless mod
|