define-keyed-function

other

(in-package "ACL2")

parse-keyed-argumentsfunction

(defun parse-keyed-arguments
  (args)
  (cond ((atom args) (mv nil nil))
    ((equal (car args) '&key) (mv nil (cdr args)))
    (t (mv-let (non-keyed keyed)
        (parse-keyed-arguments (cdr args))
        (mv (cons (car args) non-keyed) keyed)))))

fix-args-order-and-remove-keysfunction

(defun fix-args-order-and-remove-keys
  (non-keyed-args keyed-args body)
  (declare (xargs :measure (+ (acl2-count non-keyed-args) (acl2-count keyed-args))))
  (cond ((consp non-keyed-args) (cons (car body)
        (fix-args-order-and-remove-keys (cdr non-keyed-args)
          keyed-args
          (cdr body))))
    ((consp keyed-args) (let* ((keyword (car keyed-args)) (keyword-value (cadr (member-equal (intern (symbol-name keyword) "KEYWORD") body))))
        (cons keyword-value
          (fix-args-order-and-remove-keys non-keyed-args
            (cdr keyed-args)
            body))))
    (t nil)))

fix-defkun-recursive-call-argsmutual-recursion

(mutual-recursion (defun fix-defkun-recursive-call-args
    (original-name fname non-keyed-args keyed-args body)
    (declare (xargs :mode :program))
    (if (atom body)
      body
      (cons (fix-defkun-recursive-call original-name
          fname
          non-keyed-args
          keyed-args
          (car body))
        (fix-defkun-recursive-call-args original-name
          fname
          non-keyed-args
          keyed-args
          (cdr body)))))
  (defun fix-defkun-recursive-call
    (original-name fname non-keyed-args keyed-args body)
    (declare (xargs :mode :program))
    (cond ((atom body) body)
      ((equal (car body) original-name) (let ((body (fix-args-order-and-remove-keys non-keyed-args
               keyed-args
               (cdr body))))
          (cons fname
            (fix-defkun-recursive-call-args original-name
              fname
              non-keyed-args
              keyed-args
              body))))
      (t (cons (car body)
          (fix-defkun-recursive-call-args original-name
            fname
            non-keyed-args
            keyed-args
            (cdr body)))))))

defkunmacro

(defmacro defkun
  (name args body)
  (mv-let (non-keyed-args keyed-args)
    (parse-keyed-arguments args)
    (let* ((fname (packn (list name "-fn"))) (args-list (append non-keyed-args keyed-args))
        (new-body (fix-defkun-recursive-call name
            fname
            non-keyed-args
            keyed-args
            body)))
      `(progn (defun ,FNAME ,(APPEND NON-KEYED-ARGS KEYED-ARGS) ,NEW-BODY)
        (defmacro ,NAME ,ARGS (list ',FNAME ,@ARGS-LIST))
        (add-macro-alias ,NAME ,FNAME)))))