		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Keyword-value-list-to-alist

Turn a true list of even length with keywords at its even-numbered positions (counting from 0), into the corresponding alist.

Signature
(keyword-value-list-to-alist kvlist) → alist
Arguments: kvlist — Guard (keyword-value-listp kvlist).
Returns: alist — Type (alistp alist).

The alist associates each of the keywords at the even positions with the immediately following element in the list. The keywords in the alist are in the same order as in the original list.

Definitions and Theorems

Function: keyword-value-list-to-alist-aux

(defun keyword-value-list-to-alist-aux (kvlist rev-alist)
  (declare (xargs :guard (and (keyword-value-listp kvlist)
                              (alistp rev-alist))))
  (let ((__function__ 'keyword-value-list-to-alist-aux))
    (declare (ignorable __function__))
    (if (endp kvlist)
        (rev rev-alist)
      (keyword-value-list-to-alist-aux
           (cddr kvlist)
           (cons (cons (car kvlist) (cadr kvlist))
                 rev-alist)))))

Function: keyword-value-list-to-alist

(defun keyword-value-list-to-alist (kvlist)
  (declare (xargs :guard (keyword-value-listp kvlist)))
  (let ((__function__ 'keyword-value-list-to-alist))
    (declare (ignorable __function__))
    (mbe :logic
         (if (endp kvlist)
             nil
           (cons (cons (car kvlist) (cadr kvlist))
                 (keyword-value-list-to-alist (cddr kvlist))))
         :exec (keyword-value-list-to-alist-aux kvlist nil))))

Theorem: alistp-of-keyword-value-list-to-alist

(defthm alistp-of-keyword-value-list-to-alist
  (b* ((alist (keyword-value-list-to-alist kvlist)))
    (alistp alist))
  :rule-classes :rewrite)

Theorem: symbol-alistp-of-keyword-value-list-to-alist

(defthm symbol-alistp-of-keyword-value-list-to-alist
  (implies (keyword-value-listp kvlist)
           (b* ((alist (keyword-value-list-to-alist kvlist)))
             (symbol-alistp alist)))
  :rule-classes :rewrite)