Profile the number of applications of rewrite rules.
(svex-rewrite-trace-profile rule mask args localp rhs subst) → *
This is incredibly primitive; you can surely do better if you spend any time to improve it.
(defattach svex-rewrite-trace svex-rewrite-trace-profile) ;; do rewriting (sneaky-alist state) ;; see results (sneaky-clear) ;; clear data (defattach svex-rewrite-trace svex-rewrite-trace-default) ;; stop profiling
Function:
(defun svex-rewrite-trace-profile (rule mask args localp rhs subst) (declare (xargs :guard t)) (let ((__function__ 'svex-rewrite-trace-profile)) (declare (ignorable __function__)) (acl2::sneaky-mutate 'svex-sneaky-prof-mutator (list rule) (cons rule localp))))
A ACL2::sneaky mutator for profiling.