		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm

Svtv-to-fsm-final-thm-var-bindings

Signature
(svtv-to-fsm-final-thm-var-bindings vars bindings overridetype envs-var x) → (mv bindings equation-alist)
Arguments: vars — Guard (symbol-listp vars).; bindings — Guard (lhprobe-map-p bindings).; overridetype — Guard (svar-overridetype-p overridetype).; envs-var — Guard (symbolp envs-var).; x — Guard (svtv-to-fsm-thm-p x).
Returns: equation-alist — Type (alistp equation-alist).

Definitions and Theorems

Function: svtv-to-fsm-final-thm-var-bindings

(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: alistp-of-svtv-to-fsm-final-thm-var-bindings.equation-alist

(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)