Apply one-hot rewriting to a sexpr-alist.
Logically this just walks over the alist and applies 4v-onehot-rw-sexpr to each value. But we actually use mbe to provide a more efficient implementation; see 4v-onehot-sexpr-list-prime for the basic idea and motivation.
This is only an
Function:
(defun 4v-onehot-rw-sexpr-alist-fast (vars sexpr-alist) (declare (xargs :guard (and (atom-listp vars) (not (member-equal nil vars))))) (let* ((names (alist-keys sexpr-alist)) (sexprs (alist-vals sexpr-alist)) (new-sexprs (4vs-ite*-list-dumb (4vs-onehot vars) (4v-onehot-sexpr-list-prime vars sexprs) (replicate (len sexprs) (4vs-x))))) (pairlis$ names new-sexprs)))
Function:
(defun 4v-onehot-rw-sexpr-alist-aux (vars sexpr-alist) (declare (xargs :guard (and (atom-listp vars) (not (member-equal nil vars))))) (mbe :logic (cond ((atom sexpr-alist) nil) ((atom (car sexpr-alist)) (4v-onehot-rw-sexpr-alist-aux vars (cdr sexpr-alist))) (t (cons (cons (caar sexpr-alist) (4v-onehot-rw-sexpr vars (cdar sexpr-alist))) (4v-onehot-rw-sexpr-alist-aux vars (cdr sexpr-alist))))) :exec (4v-onehot-rw-sexpr-alist-fast vars sexpr-alist)))
Theorem:
(defthm 4v-onehot-rw-sexpr-alist-fast-removal (equal (4v-onehot-rw-sexpr-alist-fast vars sexpr-alist) (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist)))
Theorem:
(defthm hons-assoc-equal-of-4v-onehot-rw-sexpr-alist-aux (equal (hons-assoc-equal name (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist)) (if (hons-assoc-equal name sexpr-alist) (cons name (4v-onehot-rw-sexpr vars (cdr (hons-assoc-equal name sexpr-alist)))) nil)))
Theorem:
(defthm 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist-aux (implies (and (atom-listp vars) (not (member-equal nil vars))) (4v-sexpr-alist-<= (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist) sexpr-alist)))
Theorem:
(defthm 4v-sexpr-vars-list-of-4v-onehot-rw-sexpr-alist-aux (implies (atom-listp vars) (subsetp-equal (4v-sexpr-vars-list (alist-vals (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist))) (append vars (4v-sexpr-vars-list (alist-vals sexpr-alist))))))