Case
Conditional based on if-then-else using eql
Example Form:
(case typ
((:character foo)
(open file-name :direction :output))
(bar (open-for-bar file-name))
(otherwise
(my-error "Illegal.")))
is the same as
(cond ((member typ '(:character foo))
(open file-name :direction :output))
((eql typ 'bar)
(open-for-bar file-name))
(t (my-error "Illegal.")))
which in turn is the same as
(if (member typ '(:character foo))
(open file-name :direction :output)
(if (eql typ 'bar)
(open-for-bar file-name)
(my-error "Illegal.")))
Notice the quotations that appear in the example above: '(:character
foo) and 'bar. Indeed, a case expression expands to a cond expression in which each tested form is quoted, and eql is used
to test equality, as described below..
General Forms:
(case expr
(x1 val-1)
...
(xk val-k)
(otherwise val-k+1))
(case expr
(x1 val-1)
...
(xk val-k)
(t val-k+1))
(case expr
(x1 val-1)
...
(xk val-k))
where each xi is either eqlablep or a true list of eqlablep objects. The final otherwise or t case is optional; if
neither is present, then an equivalent expression results from adding the
final case (t nil).
As suggested above, each case (xi val-i) generates an if-then-else
expression as follows. If xi is a non-nil atom (i.e., xi is not
nil or a cons pair), then that case generates the expression (if (eql
expr (quote xi)) vali ...) where `...' denotes the expression
generated by the rest of the cases. If however xi is a list, then
instead the generated expression is (if (member expr (quote xi)) vali
...). The final case (t val-k+1) or (otherwise val-k+1) generates
val-k+1. Note that t and otherwise here must be in the
"ACL2" package. Also note that to compare expr with nil, you
should write the case as ((nil) val-i) rather than (nil val-i)
— and similarly for t or otherwise — that is, put the
symbol in a list.
Case is defined in Common Lisp. See any Common Lisp documentation for
more information.
Subtopics
- Safe-case
- Error-checking alternative to case.
