other
(in-package "ACL2")
other
(program)
*macfun-&words*constant
(defconst *macfun-&words* '(&whole &optional &rest &body &key &allow-other-keys &auto))
macfun-find-next-&word-indexfunction
(defun macfun-find-next-&word-index (formals) (if (atom formals) nil (if (member-eq (car formals) *macfun-&words*) 0 (let ((idx (macfun-find-next-&word-index (cdr formals)))) (and idx (1+ idx))))))
macfun-split-formals-at-next-&wordfunction
(defun macfun-split-formals-at-next-&word (formals) (let ((idx (macfun-find-next-&word-index formals))) (if idx (mv (take idx formals) (nthcdr idx formals)) (mv formals nil))))
macfun-formals-to-macro-formalsfunction
(defun macfun-formals-to-macro-formals (formals) (let* ((mem (member-eq '&auto formals))) (if mem (let* ((len (len formals)) (lenrest (len mem)) (prefix (take (- len lenrest) formals)) (suffix-idx (macfun-find-next-&word-index (cdr mem))) (suffix (and suffix-idx (nthcdr suffix-idx (cdr mem))))) (append prefix suffix)) formals)))
macfun-key/opt/autos-to-function-formalsfunction
(defun macfun-key/opt/autos-to-function-formals (formals) (if (atom formals) nil (let ((rest (macfun-key/opt/autos-to-function-formals (cdr formals)))) (case (len (car formals)) (0 (cons (car formals) rest)) (1 (cons (caar formals) rest)) (2 (cons (caar formals) rest)) (3 (list* (caar formals) (caddar formals) rest)) (otherwise rest)))))
macfun-formals-to-function-formals1function
(defun macfun-formals-to-function-formals1 (formals) (case (car formals) ((&whole &rest &body) (if (consp (cdr formals)) (mv (list (cadr formals)) (cddr formals)) (mv nil nil))) ((&optional &key &auto) (mv-let (key/opt/autos formals) (macfun-split-formals-at-next-&word (cdr formals)) (mv (macfun-key/opt/autos-to-function-formals key/opt/autos) formals))) (&allow-other-keys (mv nil (cdr formals))) (otherwise (mv-let (reqs rest) (macfun-split-formals-at-next-&word formals) (mv reqs rest)))))
macfun-formals-to-function-formalsfunction
(defun macfun-formals-to-function-formals (formals) (if (atom formals) nil (mv-let (fn-formals rest) (macfun-formals-to-function-formals1 formals) (append fn-formals (macfun-formals-to-function-formals rest)))))
macfun-autos-to-function-actualsfunction
(defun macfun-autos-to-function-actuals (autos) (if (atom autos) nil (cons (list 'quote (case (len (car autos)) (0 (car autos)) (1 (caar autos)) (2 (cadar autos)) (otherwise (er hard? 'defmacfun "An &auto binding should either be just a variable or a form (variable term), which ~x0 isn't.~%" (car autos))))) (macfun-autos-to-function-actuals (cdr autos)))))
macfun-formals-to-function-actuals1function
(defun macfun-formals-to-function-actuals1 (formals) (case (car formals) ((&whole &rest &body) (if (consp (cdr formals)) (mv (list (list 'list ''quote (cadr formals))) (cddr formals)) (mv nil nil))) (&auto (mv-let (autos formals) (macfun-split-formals-at-next-&word (cdr formals)) (mv (macfun-autos-to-function-actuals autos) formals))) ((&optional &key) (mv-let (key/opts formals) (macfun-split-formals-at-next-&word (cdr formals)) (mv (macfun-key/opt/autos-to-function-formals key/opts) formals))) (&allow-other-keys (mv nil (cdr formals))) (otherwise (mv-let (reqs rest) (macfun-split-formals-at-next-&word formals) (mv reqs rest)))))
macfun-formals-to-function-actualsfunction
(defun macfun-formals-to-function-actuals (formals) (if (atom formals) nil (mv-let (actuals rest) (macfun-formals-to-function-actuals1 formals) (append actuals (macfun-formals-to-function-actuals rest)))))
macfun-get-nonstringsfunction
(defun macfun-get-nonstrings (x) (if (atom x) nil (if (stringp (car x)) (macfun-get-nonstrings (cdr x)) (cons (car x) (macfun-get-nonstrings (cdr x))))))
macfun-get-stringsfunction
(defun macfun-get-strings (x) (if (atom x) nil (if (stringp (car x)) (cons (car x) (macfun-get-strings (cdr x))) (macfun-get-strings (cdr x)))))
defmacfun-fnfunction
(defun defmacfun-fn (name formals doc-decl-body type) (let* ((bodylst (last doc-decl-body)) (doc-decl (butlast doc-decl-body 1)) (docs (macfun-get-strings doc-decl)) (decls (macfun-get-nonstrings doc-decl)) (fnname (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-FN") name)) (fn-formals (macfun-formals-to-function-formals formals)) (fn-actuals (macfun-formals-to-function-actuals formals)) (mac-formals (macfun-formals-to-macro-formals formals))) `(progn (defun ,FNNAME ,FN-FORMALS ,@DECLS . ,BODYLST) (defmacro ,NAME ,MAC-FORMALS ,@DOCS ,(CASE TYPE (FUNCTION `(LIST ',FNNAME . ,FN-ACTUALS)) (MACRO `(,FNNAME . ,FN-ACTUALS)))))))
defmacfunmacro
(defmacro defmacfun (name formals &rest doc-decl-body) (defmacfun-fn name formals doc-decl-body 'function))
deffunmacmacro
(defmacro deffunmac (name formals &rest doc-decl-body) (defmacfun-fn name formals doc-decl-body 'macro))