Impossible
Prove that some case is unreachable using guards.
Logically, (impossible) just returns nil, and
(impossible x) just returns x.
But impossible has a guard of nil, so whenever you use it in a
function, you will be obliged to prove that it cannot be executed when the
guard holds.
What good is this? One use is to make sure that every possible case in a
sum type has been covered. For instance, you can write:
(define f ((x whatever-p))
(case (type-of x)
(:foo (handle-foo ...))
(:bar (handle-bar ...))
(otherwise (impossible))))
This is a nice style in that, if we later extend x so that its type can
also be :baz, then the guard verification will fail and remind us that we
need to extend f to handle :baz types as well.
The optional argument to impossible can be used to design your code in
a more convenient way. Suppose that in the example of the function f
above, both handle-foo and handle-bar are functions that always
return integers. Then by changing (impossible) to, say, (impossible
0) in the definition of f, you can now prove that f always returns
an integer. With the original definition of f, you would require the
additional hypothesis (whatever-p x), and as part of the proof of the
theorem, ACL2 would have to re-prove that the otherwise case is
unreachable.
If somehow (impossible) is ever executed — e.g., due to program
mode code that is violating guards, or because guard-checking has been
set to nil or :none — it just causes a hard error.
Definitions and Theorems
Macro: impossible
(defmacro impossible (&optional retval)
(if retval (cons 'prog2$
(cons '(impossible-fn)
(cons retval 'nil)))
'(impossible-fn)))Function: impossible-fn
(defun impossible-fn nil
(declare (xargs :guard nil))
(er
hard 'impossible
"Reached code that is provably impossible to reach without violating ~
guards somewhere (see :DOC GUARD). This could have happened because ~
you are running code that is in program mode (see :DOC DEFUN-MODE), ~
or because you have guard checking set to NIL or :NONE (see :DOC ~
SET-GUARD-CHECKING)."))
