Filtering...

defmacfun

books/tools/defmacfun
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))