[Table of Contents]

ecase.lisp

The exhaustive-case macro is somewhat analagous to the CLtL macro ecase, except that it generates a guard-conjecture asserting that the case clauses are an exhaustive enumeration of the possible values of the case selector expression.

This works by introducing the function forced-member, which takes arguments like member, but has a guard asserting that its first argument is a member of its second argument. The macro exhaustive-case expands into a call to the regular case macro and a call to forced-member. Here's an example:

(ecase (foo x) (:alpha (foo1 x)) (:bravo (foo2 x)))

expands into

(and (forced-member (foo x) '(:alpha bravo)) (case (foo x) (:alpha (foo1 x)) (:bravo (foo2 x))))


(in-package "ACL2")


(defun legal-ecase-clause-p (clause)
  (declare (xargs :guard t))
  (and (consp clause)
       (if (atom (car clause))
           (and (eqlablep (car clause))
                (not (member (car clause) '(t otherwise))))
         (and (eqlable-listp (car clause))
              (not (member 't         (car clause)))
              (not (member 'otherwise (car clause)))))
       (consp (cdr clause))
       (null (cdr (cdr clause)))))


(defun legal-ecase-clauses-p (clauses)
  (declare (xargs :guard t))
  (if (atom clauses)
      (eq clauses nil)
    (and (legal-ecase-clause-p  (car clauses))
         (legal-ecase-clauses-p (cdr clauses)))))
Note that the symbols T and OTHERWISE are not allowed keys in an ECASE clause. 

(defun strip-ecase (clause)
  (declare (xargs :guard (legal-ecase-clause-p clause)))
  (if (atom (car clause))
      (list (car clause))
    (car clause)))


#+IGNORE-IN-BOOK
(thm (implies (legal-ecase-clause-p clause)
              (eqlable-listp (strip-ecase clause))))


(defun strip-ecases (clauses)
  (declare (xargs :guard (legal-ecase-clauses-p clauses)))
  (if (atom clauses)
      nil
    (append (strip-ecase  (car clauses))
            (strip-ecases (cdr clauses)))))


#+IGNORE-IN-BOOK
(thm (implies (legal-ecase-clauses-p clauses)
              (eqlable-listp (strip-ecases clauses))))


(defun forced-member (elt list)
  (declare (xargs :guard (and (eqlable-listp list)
                              (member elt list))))
  t)


(defmacro  exhaustive-case (selector \&rest clauses)
  (declare (xargs :guard (legal-ecase-clauses-p clauses)))
  (let ((legal-keys (strip-ecases clauses)))
    `(and (eqlablep ,selector)
          (forced-member ,selector ',legal-keys)
          (case ,selector ,@clauses))))
Here's an example of a function whose guard proofs will succeed, and one whose guard proofs will fail.

(defun good-foo (arg) (declare (xargs :guard (member (f arg) '(:alpha :bravo)))) (exhaustive-case (f x) (:alpha 1) (:bravo 2)))

(defun bad-foo (arg) (declare (xargs :guard t)) (exhaustive-case (f arg) (:alpha 1) (:bravo 2)))

The guard conjecture generated by exhaustive-case above can be proven if

(member (f x) '(:alpha :bravo))

can be proven. Thus, if the function F is disabled, the lemma

(defthm f-enumeration-rule (member (f x) (f-enumeration)))

assuming the definition

(defun f-enumeration () '(:alpha :bravo))

would suffice for the guard proof to succeed automatically.

This page is URL http://www.computationallogic.com/software/djvm/html-0.5/ecase.html