Deleted obsolate codes.
tswd
8 years ago
| 971 | 971 | (let ((term-nu nil) |
| 972 | 972 | (normal-form (get-hashed-term term *term-memo-table*))) |
| 973 | 973 | (unless normal-form |
| 974 | (let ((rule-count (number-rewritings))) | |
| 975 | (setq term-nu (simple-copy-term term)) | |
| 976 | ;; compute the normal form of "term" | |
| 977 | (reduce-term term strategy) | |
| 978 | (setq normal-form term) | |
| 979 | #| | |
| 980 | (unless (= rule-count (number-rewritings)) | |
| 981 | (when *memo-debug* | |
| 982 | (when (term-equational-equal term-nu normal-form) | |
| 983 | (with-output-chaos-warning () | |
| 984 | (format t "E-E term is about to be hashed!") | |
| 985 | (format t "~%(~d) old = " rule-count (number-rewritings)) | |
| 986 | (term-print-with-sort term-nu) | |
| 987 | (format t "~%(~d) new = " (number-rewritings)) | |
| 988 | (term-print-with-sort normal-form)))) | |
| 989 | ;; store the normal form | |
| 990 | (set-hashed-term term-nu *term-memo-table* normal-form)) | |
| 991 | |# | |
| 992 | (set-hashed-term term-nu *term-memo-table* normal-form))) | |
| 974 | (setq term-nu (simple-copy-term term)) | |
| 975 | ;; compute the normal form of "term" | |
| 976 | (reduce-term term strategy) | |
| 977 | (setq normal-form term) | |
| 978 | (set-hashed-term term-nu *term-memo-table* normal-form)) | |
| 993 | 979 | normal-form)) |
| 994 | 980 | |
| 995 | 981 | (defmacro check-closed-world-assumption (?term) |