Debugging Computed Hints
We have found that it is sometimes helpful to define hints so that they print out messages to the terminal when they fire, so you can see what hint was generated and which of your computed hints did it.
To that end we have defined a macro we sometimes use. Suppose you have a
:hints (computed-hint-fn (hint-expr id))
If you defmacro the macro below you could then write instead:
:hints ((show-hint computed-hint-fn 1) (show-hint (hint-expr id) 2))
with the effect that whenever either hint is fired (i.e., returns
non-
(defmacro show-hint (hint &optional marker) (cond ((and (consp hint) (stringp (car hint))) hint) (t `(let ((marker ,marker) (ans ,(if (symbolp hint) `(,hint id clause world stable-under-simplificationp) hint))) (if ans (prog2$ (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%" (if (null marker) 0 1) marker (cons (string-for-tilde-@-clause-id-phrase id) ans)) ans) nil)))))
Note that when
:hints ((show-hints (computed-hint-fn id clause world) 1) (show-hint (hint-expr id) 2)).
If you only use computed hints of arity 3, you might eliminate the
occurrence of
Putting a