(map-alist-term-keys-to-val-terms x) → (mv err al)
Function:
(defun map-alist-term-keys-to-val-terms (x) (declare (xargs :guard (pseudo-termp x))) (let ((__function__ 'map-alist-term-keys-to-val-terms)) (declare (ignorable __function__)) (b* (((acl2::when-match x '(:? rest-al)) (if (svex-env-p rest-al) (mv nil (map-alist-const-keys-to-val-terms rest-al)) (mv (msg "Malformed environment: ~x0~%" rest-al) nil))) ((acl2::when-match x (cons (cons '(:? var) (:? val)) (:? rest))) (b* (((unless (svar-p var)) (mv (msg "Wrong type for variable: ~x0~%" var) nil)) ((mv err rest) (map-alist-term-keys-to-val-terms rest))) (mv err (cons (cons var val) rest)))) ((acl2::when-match x (cons '((:? var) :? val) (:? rest))) (b* (((unless (svar-p var)) (mv (msg "Wrong type for variable: ~x0~%" var) nil)) ((mv err rest) (map-alist-term-keys-to-val-terms rest))) (mv err (cons (cons var (list 'quote val)) rest)))) ((acl2::when-match x (binary-append (:? first) (:? rest))) (b* (((mv err first) (map-alist-term-keys-to-val-terms first)) ((when err) (mv err nil)) ((mv err rest) (map-alist-term-keys-to-val-terms rest)) ((when err) (mv err nil))) (mv nil (append first rest)))) ((acl2::when-match x (svex-alist-eval '(:? svalist) (:? env))) (b* (((unless (svex-alist-p svalist)) (mv (msg "Malformed svex alist: ~x0~%" svalist) nil))) (mv nil (svex-alist-evaluation-to-symenv svalist env))))) (mv (msg "Failed to parse ~x0 as an alist term~%" x) nil))))
Theorem:
(defthm return-type-of-map-alist-term-keys-to-val-terms.al (b* (((mv ?err ?al) (map-alist-term-keys-to-val-terms x))) (and (implies (pseudo-termp x) (svdecomp-symenv-p al)) (svar-alist-p al))) :rule-classes :rewrite)
Theorem:
(defthm lookup-exists-of-map-alist-term-keys-to-val-terms (b* (((mv err al) (map-alist-term-keys-to-val-terms x))) (implies (not err) (iff (svar-lookup k al) (svar-lookup k (svdecomp-ev x a))))))
Theorem:
(defthm lookup-exists-of-map-alist-term-keys-to-val-terms-1 (b* (((mv err al) (map-alist-term-keys-to-val-terms x))) (implies (and (not err) (svar-lookup k (svdecomp-ev x a))) (svar-lookup k al))))
Theorem:
(defthm lookup-exists-of-map-alist-term-keys-to-val-terms-2 (b* (((mv err al) (map-alist-term-keys-to-val-terms x))) (implies (and (not err) (not (svar-lookup k (svdecomp-ev x a)))) (not (svar-lookup k al)))))
Theorem:
(defthm eval-lookup-of-map-alist-term-keys-to-val-terms (b* (((mv err al) (map-alist-term-keys-to-val-terms x))) (implies (and (not err) (svar-lookup k (svdecomp-ev x env))) (equal (svdecomp-ev (cdr (svar-lookup k al)) env) (cdr (svar-lookup k (svdecomp-ev x env)))))))
Theorem:
(defthm svdecomp-ev-symenv-of-map-alist-term-keys-to-val-terms (b* (((mv err al) (map-alist-term-keys-to-val-terms x))) (implies (not err) (equal (svdecomp-ev-symenv al env) (svdecomp-ev x env)))))