(svtv-to-fsm-final-thm-var-bindings vars bindings overridetype envs-var x) → (mv bindings equation-alist)
Function:
(defun svtv-to-fsm-final-thm-var-bindings (vars bindings overridetype envs-var x) (declare (xargs :guard (and (symbol-listp vars) (lhprobe-map-p bindings) (svar-overridetype-p overridetype) (symbolp envs-var) (svtv-to-fsm-thm-p x)))) (declare (xargs :guard (b* (((svtv-to-fsm-thm x))) (and (symbolp x.base-cycle-var) (symbolp x.pkg-sym))))) (let ((__function__ 'svtv-to-fsm-final-thm-var-bindings)) (declare (ignorable __function__)) (b* (((when (atom vars)) (mv nil nil)) (in (car vars)) (look (hons-get in bindings)) ((unless look) (raise "SVTV input not found in bindings: ~x0~%" in) (svtv-to-fsm-final-thm-var-bindings (cdr vars) bindings overridetype envs-var x)) ((lhprobe probe) (cdr look)) ((mv rest-bindings rest-equations) (svtv-to-fsm-final-thm-var-bindings (cdr vars) bindings overridetype envs-var x)) ((svtv-to-fsm-thm x)) ((mv cycle-var equations) (case x.cycle-num-rewrite-strategy (:all-free (b* ((cycle-var (intern-in-package-of-symbol (concatenate 'string (symbol-name in) "-CYCLE-NUM") x.pkg-sym)) (eqn (if (eq in x.primary-output-var) (cons 'and (cons (cons 'integerp (cons cycle-var 'nil)) (cons (cons '<= (cons probe.stage (cons cycle-var 'nil))) (cons (cons 'equal (cons x.base-cycle-var (cons (cons '- (cons cycle-var (cons probe.stage 'nil))) 'nil))) 'nil)))) (cons 'equal (cons cycle-var (cons (cons '+ (cons probe.stage (cons x.base-cycle-var 'nil))) 'nil)))))) (mv cycle-var (cons (cons in eqn) rest-equations)))) (:by-cycle (b* (((when (eql probe.stage 0)) (mv x.base-cycle-var rest-equations)) (cycle-var (intern-in-package-of-symbol (concatenate 'string (symbol-name x.base-cycle-var) "+" (natstr probe.stage)) x.pkg-sym)) (eqn (if (eq in x.primary-output-var) (cons 'and (cons (cons 'integerp (cons cycle-var 'nil)) (cons (cons '<= (cons probe.stage (cons cycle-var 'nil))) (cons (cons 'equal (cons x.base-cycle-var (cons (cons '- (cons cycle-var (cons probe.stage 'nil))) 'nil))) 'nil)))) (cons 'equal (cons cycle-var (cons (cons '+ (cons probe.stage (cons x.base-cycle-var 'nil))) 'nil))))) (eqns (b* ((look (rassoc-equal eqn rest-equations)) ((unless look) (cons (cons in eqn) rest-equations)) ((when (eq in x.primary-output-var)) (cons (cons in eqn) (remove-equal look rest-equations)))) rest-equations))) (mv cycle-var eqns))) (t (mv (if (eql probe.stage 0) x.base-cycle-var (cons '+ (cons probe.stage (cons x.base-cycle-var 'nil)))) rest-equations))))) (mv (cons (cons in (cons (cons (if probe.signedp 'lhs-eval-signx 'lhs-eval-zx) (cons (cons 'quote (cons (lhs-change-override probe.lhs overridetype) 'nil)) (cons (cons 'nth (cons cycle-var (cons envs-var 'nil))) 'nil))) 'nil)) rest-bindings) equations))))
Theorem:
(defthm alistp-of-svtv-to-fsm-final-thm-var-bindings.equation-alist (b* (((mv ?bindings ?equation-alist) (svtv-to-fsm-final-thm-var-bindings vars bindings overridetype envs-var x))) (alistp equation-alist)) :rule-classes :rewrite)