|
|
|---|
|
|
|
|---|
Turn the keyword arguments of a macro into terms.
This complements partition-macro-args, which extracts a list of regular arguments and an alist of keyword arguments. This alist has keys that are keywords but values that, in general, are terms that need to be evaluated to obtain the actual values of the keyword arguments; the terms are the ones supplied by the caller of the macro. This function turns that alist into a list of terms that, when put inside a list, construct the alist with evaluated values: each term, when evaluated, returns a cons pair.
Function:
(defun keyword-macro-args-to-terms (alist) (declare (xargs :guard (alistp alist))) (cond ((endp alist) nil) (t (cons (cons 'cons (cons (caar alist) (cons (cdar alist) 'nil))) (keyword-macro-args-to-terms (cdr alist))))))
Theorem:
(defthm true-listp-of-keyword-macro-args-to-terms (true-listp (keyword-macro-args-to-terms alist)))