		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-compile-phases-lazy

Signature
(svtv-compile-phases-lazy phase nphases outs updates data state-machine) → (mv outalist final-state)
Arguments: phase — Guard (natp phase).; nphases — Guard (posp nphases).; outs — Guard (svtv-lines-p outs).; updates — Guard (svex-alist-p updates).; data — Guard (svtv-composedata-p data).
Returns: outalist — Type (svex-alist-p outalist).; final-state — Type (svex-alist-p final-state).

Definitions and Theorems

Function: svtv-compile-phases-lazy

(defun svtv-compile-phases-lazy
       (phase nphases outs updates data state-machine)
 (declare (xargs :guard (and (natp phase)
                             (posp nphases)
                             (svtv-lines-p outs)
                             (svex-alist-p updates)
                             (svtv-composedata-p data))))
 (declare (xargs :guard (<= phase nphases)))
 (let ((__function__ 'svtv-compile-phases-lazy))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (pos-fix nphases) (nfix phase)))
                :exec (eql nphases phase)))
     (mv nil
         (and state-machine
              (svex-alist-compose-svtv-phases
                   (nth phase
                        (svtv-composedata->nextstates data))
                   (1- (lposfix nphases))
                   data))))
    (phase-outalist
         (svex-alist-compose (svtv-outputs->outalist outs phase)
                             updates))
    (composed-outalist
         (svex-alist-compose-svtv-phases phase-outalist phase data))
    ((mv rest-outs final-state)
     (svtv-compile-phases-lazy (1+ (lnfix phase))
                               nphases
                               outs updates data state-machine)))
   (mv (append composed-outalist rest-outs)
       final-state))))

Theorem: svex-alist-p-of-svtv-compile-phases-lazy.outalist

(defthm svex-alist-p-of-svtv-compile-phases-lazy.outalist
  (b* (((mv ?outalist ?final-state)
        (svtv-compile-phases-lazy phase nphases
                                  outs updates data state-machine)))
    (svex-alist-p outalist))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svtv-compile-phases-lazy.final-state

(defthm svex-alist-p-of-svtv-compile-phases-lazy.final-state
  (b* (((mv ?outalist ?final-state)
        (svtv-compile-phases-lazy phase nphases
                                  outs updates data state-machine)))
    (svex-alist-p final-state))
  :rule-classes :rewrite)

Theorem: svtv-compile-phases-lazy-of-nfix-phase

(defthm svtv-compile-phases-lazy-of-nfix-phase
 (equal
  (svtv-compile-phases-lazy (nfix phase)
                            nphases outs updates data state-machine)
  (svtv-compile-phases-lazy phase nphases
                            outs updates data state-machine)))

Theorem: svtv-compile-phases-lazy-nat-equiv-congruence-on-phase

(defthm svtv-compile-phases-lazy-nat-equiv-congruence-on-phase
 (implies
   (nat-equiv phase phase-equiv)
   (equal
        (svtv-compile-phases-lazy
             phase
             nphases outs updates data state-machine)
        (svtv-compile-phases-lazy phase-equiv nphases
                                  outs updates data state-machine)))
 :rule-classes :congruence)

Theorem: svtv-compile-phases-lazy-of-pos-fix-nphases

(defthm svtv-compile-phases-lazy-of-pos-fix-nphases
 (equal (svtv-compile-phases-lazy phase (pos-fix nphases)
                                  outs updates data state-machine)
        (svtv-compile-phases-lazy phase nphases
                                  outs updates data state-machine)))

Theorem: svtv-compile-phases-lazy-pos-equiv-congruence-on-nphases

(defthm svtv-compile-phases-lazy-pos-equiv-congruence-on-nphases
 (implies
   (pos-equiv nphases nphases-equiv)
   (equal
        (svtv-compile-phases-lazy
             phase
             nphases outs updates data state-machine)
        (svtv-compile-phases-lazy phase nphases-equiv
                                  outs updates data state-machine)))
 :rule-classes :congruence)

Theorem: svtv-compile-phases-lazy-of-svtv-lines-fix-outs

(defthm svtv-compile-phases-lazy-of-svtv-lines-fix-outs
  (equal
       (svtv-compile-phases-lazy phase nphases (svtv-lines-fix outs)
                                 updates data state-machine)
       (svtv-compile-phases-lazy phase nphases
                                 outs updates data state-machine)))

Theorem: svtv-compile-phases-lazy-svtv-lines-equiv-congruence-on-outs

(defthm svtv-compile-phases-lazy-svtv-lines-equiv-congruence-on-outs
  (implies (svtv-lines-equiv outs outs-equiv)
           (equal (svtv-compile-phases-lazy
                       phase
                       nphases outs updates data state-machine)
                  (svtv-compile-phases-lazy
                       phase nphases
                       outs-equiv updates data state-machine)))
  :rule-classes :congruence)

Theorem: svtv-compile-phases-lazy-of-svex-alist-fix-updates

(defthm svtv-compile-phases-lazy-of-svex-alist-fix-updates
 (equal
     (svtv-compile-phases-lazy phase
                               nphases outs (svex-alist-fix updates)
                               data state-machine)
     (svtv-compile-phases-lazy phase nphases
                               outs updates data state-machine)))

Theorem: svtv-compile-phases-lazy-svex-alist-equiv-congruence-on-updates

(defthm
    svtv-compile-phases-lazy-svex-alist-equiv-congruence-on-updates
  (implies (svex-alist-equiv updates updates-equiv)
           (equal (svtv-compile-phases-lazy
                       phase
                       nphases outs updates data state-machine)
                  (svtv-compile-phases-lazy
                       phase nphases
                       outs updates-equiv data state-machine)))
  :rule-classes :congruence)

Theorem: svtv-compile-phases-lazy-of-svtv-composedata-fix-data

(defthm svtv-compile-phases-lazy-of-svtv-composedata-fix-data
 (equal
  (svtv-compile-phases-lazy phase nphases
                            outs updates (svtv-composedata-fix data)
                            state-machine)
  (svtv-compile-phases-lazy phase nphases
                            outs updates data state-machine)))

Theorem: svtv-compile-phases-lazy-svtv-composedata-equiv-congruence-on-data

(defthm
 svtv-compile-phases-lazy-svtv-composedata-equiv-congruence-on-data
 (implies (svtv-composedata-equiv data data-equiv)
          (equal (svtv-compile-phases-lazy
                      phase
                      nphases outs updates data state-machine)
                 (svtv-compile-phases-lazy
                      phase nphases
                      outs updates data-equiv state-machine)))
 :rule-classes :congruence)