CS U290 Logic and Computation
Spring 2008

[Syllabus] [Lectures] [Assignments]

The defunt macro

Defunt is a macro that allows us to extend the functionality of defun by formalizing the contract and data definitions of the design recipe. It does this by allowing us to write, formally in ACL2, what the type of the function we are defining is, modulo type assumptions about the input. Defunt then generates a defthm and asks ACL2 to prove it. If ACL2 is successful, then we have proven that the function satisfies its data definition. So, you can think of this as using the theorem prover to prove type correctness.

Here is an example of how it is used. Notice that it is just like defun, except that after providing the name and arguments to app, we also formalize the data definitions.

(defunt app (x y)
  (implies (true-listp y)
           (true-listp (app x y)))
  (if (endp x)
      y
    (cons (car x)
          (app (cdr x) y))))

The above gives rise to both the definition of app we would get if we just used defun:

(defun app (x y)
  (if (endp x)
      y
    (cons (car x) (app (cdr x) y))))

and also gives rise to a defthm about its type.

(defthm app-type
  (implies (true-listp y)
           (true-listp (app x y)))))

Here is the definition of the macro (and two helper functions).

(defun make-sym (s suf)
  ; Returns the symbol s-suf.
  (declare (xargs :guard (and (symbolp s) (symbolp suf))))
  (intern-in-package-of-symbol
   (concatenate 'string
                (symbol-name s)
                "-"
                (symbol-name suf))
   s))

(defun make-code-list (l)
  (if (or (null l)
          (and (consp l)
               (consp (car l))
               (not (eq 'lambda (caar l)))))
      l
    (list l)))

(defmacro defunt (&rest def)

  ; This macro extends a subset of the functionality of defun.
  ; See the example above. One thing to note is that after the
  ; name of the function and the argument list, there is an
  ; optional documentation string. Also, the type theorem can be
  ; either of the form (thm) or of the form ((thm) commands)
  ; where commands can be anything that you would give to a
  ; defthm (look at defthm documentation), specifically it is:
  ; :rule-classes rule-classes :instructions instructions :hints
  ; hints :otf-flg otf-flg :doc doc-string. BTW, the if test
  ; below checks for documentation strings.

  (list 'progn
        (cons 'defun (append (list (first def)
                                   (second def))
                             (if (stringp (third def))
                                 (list (third def)
                                       (fifth def))
                               (list (fourth def)))))
        (append (list 'defthm (make-sym (car def) 'type))
                (if (stringp (third def))
                    (make-code-list (fourth def))
                  (make-code-list (third def))))))