A ACL2::sneaky mutator for profiling.
Function:
(defun svex-sneaky-prof-mutator (val name-localp) (declare (xargs :guard (and (consp val) (consp name-localp)))) (let ((__function__ 'svex-sneaky-prof-mutator)) (declare (ignorable __function__)) (b* ((val (car val)) ((mv nonloc loc) (if (consp val) (mv (car val) (cdr val)) (mv nil nil)))) (list (cons (car name-localp) (if (cdr name-localp) (cons nonloc (+ 1 (fix loc))) (cons (+ 1 (fix nonloc)) loc)))))))