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))))))Last modified: Fri Jan 18 16:42:35 EST 2008