		Search-engine friendly clone of the ACL2 documentation.

Support

Extract-keywords

Extract legal keyword/value pairs from an argument list.

If a keyword occurs as a singleton list in legal-kwds, it may have mulitple occurrences in the args, and the result stored in the kwd-alist will be a list of the arguments to the occurrences. For example:

(extract-keywords 'foo '((:bar)) '(:bar x :bar y) nil)

produces ((:bar y x)) as its keyword alist result.

Definitions and Theorems

Function: extract-keywords

(defun extract-keywords (ctx legal-kwds args kwd-alist)
  "Returns (mv kwd-alist other-args)"
  (declare (xargs :guard (and (legal-kwds-p legal-kwds)
                              (alistp kwd-alist))))
  (b*
    ((__function__ 'extract-keywords)
     ((when (atom args)) (mv kwd-alist args))
     (arg1 (first args))
     ((unless (keywordp arg1))
      (b* (((mv kwd-alist other-args)
            (extract-keywords ctx legal-kwds (cdr args)
                              kwd-alist)))
        (mv kwd-alist (cons arg1 other-args))))
     (legality (keyword-legality arg1 legal-kwds))
     ((unless legality)
      (raise (concatenate 'string
                          "~x0: invalid keyword ~x1."
                          (if legal-kwds "  Valid keywords: ~&2."
                            "  No keywords are valid here."))
             ctx arg1 legal-kwds)
      (mv nil nil))
     ((when (atom (rest args)))
      (raise "~x0: keyword ~x1 has no argument."
             ctx arg1)
      (mv nil nil))
     ((when (and (not (eq legality :multiple))
                 (assoc arg1 kwd-alist)))
      (raise "~x0: multiple occurrences of keyword ~x1."
             ctx arg1)
      (mv nil nil))
     (value (second args))
     (kwd-alist (if (eq legality :multiple)
                    (acons arg1
                           (cons value (cdr (assoc arg1 kwd-alist)))
                           (remove1-assoc arg1 kwd-alist))
                  (acons arg1 value kwd-alist))))
    (extract-keywords ctx legal-kwds (cddr args)
                      kwd-alist)))