Try to simplify an sv::svexlist structure with rp::RP-Rewriter using regular rewrite rules about 4vec functions.
(svex-alist-simplify x &key (state 'state) (rp-state 'rp-state) (context 'nil) (runes 'nil) (reload-rules 't) (linearize ':auto) (only-local '4) (vars-are-integer 't) (verbose 'nil) (svex-env-is-var 'nil)) → (mv res rp::rp-state-res)
Function:
(defun svex-alist-simplify-fn (x state rp-state context runes reload-rules linearize only-local vars-are-integer verbose svex-env-is-var) (declare (xargs :stobjs (state rp-state))) (declare (xargs :guard (and (sv::svex-alist-p x) (booleanp verbose)))) (declare (xargs :guard (and (or reload-rules (valid-rp-state-syntaxp rp-state)) (or (rp::context-syntaxp context) (cw "ATTENTION! Given context must satisfy rp::context-syntaxp. Make sure you are giving a translated term ~%"))) :stobjs (state rp-state))) (let ((acl2::__function__ 'svex-alist-simplify)) (declare (ignorable acl2::__function__)) (b* ((svexlist (strip-cdrs x)) ((mv res rp-state) (svexlist-simplify svexlist :context context :runes runes :reload-rules reload-rules :linearize linearize :only-local only-local :vars-are-integer vars-are-integer :verbose verbose :svex-env-is-var svex-env-is-var))) (mv (pairlis$ (strip-cars x) res) rp-state))))
Theorem:
(defthm valid-rp-state-syntaxp-of-svex-alist-simplify.rp-state-res (implies (if reload-rules (rp::rp-statep rp-state) (valid-rp-state-syntaxp rp-state)) (b* (((mv ?res rp::?rp-state-res) (svex-alist-simplify-fn x state rp-state context runes reload-rules linearize only-local vars-are-integer verbose svex-env-is-var))) (valid-rp-state-syntaxp rp::rp-state-res))) :rule-classes :rewrite)