		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-overrides->assigns

Signature
(svtv-overrides->assigns x phase) → assigns
Arguments: x — Guard (svtv-overridelines-p x).; phase — Guard (natp phase).
Returns: assigns — Type (svex-alist-p assigns).

Definitions and Theorems

Function: svtv-overrides->assigns

(defun svtv-overrides->assigns (x phase)
  (declare (xargs :guard (and (svtv-overridelines-p x)
                              (natp phase))))
  (let ((__function__ 'svtv-overrides->assigns))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((svtv-overrideline xf) (car x))
         (ent (or (nth phase xf.entries) '_))
         ((when (svtv-dontcare-p ent))
          (cons (cons xf.test (svex-quote 0))
                (svtv-overrides->assigns (cdr x)
                                         phase)))
         ((mv val test)
          (if (svtv-condoverride-p ent)
              (b* (((svtv-condoverride ent)))
                (mv (svtv-baseentry-svex ent.value)
                    (svtv-baseentry-svex ent.test)))
            (mv (svtv-baseentry-svex ent)
                (svex-quote -1)))))
      (cons (cons xf.val val)
            (cons (cons xf.test test)
                  (svtv-overrides->assigns (cdr x)
                                           phase))))))

Theorem: svex-alist-p-of-svtv-overrides->assigns

(defthm svex-alist-p-of-svtv-overrides->assigns
  (b* ((assigns (svtv-overrides->assigns x phase)))
    (svex-alist-p assigns))
  :rule-classes :rewrite)

Theorem: svtv-overrides->assigns-of-svtv-overridelines-fix-x

(defthm svtv-overrides->assigns-of-svtv-overridelines-fix-x
  (equal (svtv-overrides->assigns (svtv-overridelines-fix x)
                                  phase)
         (svtv-overrides->assigns x phase)))

Theorem: svtv-overrides->assigns-svtv-overridelines-equiv-congruence-on-x

(defthm
   svtv-overrides->assigns-svtv-overridelines-equiv-congruence-on-x
  (implies (svtv-overridelines-equiv x x-equiv)
           (equal (svtv-overrides->assigns x phase)
                  (svtv-overrides->assigns x-equiv phase)))
  :rule-classes :congruence)

Theorem: svtv-overrides->assigns-of-nfix-phase

(defthm svtv-overrides->assigns-of-nfix-phase
  (equal (svtv-overrides->assigns x (nfix phase))
         (svtv-overrides->assigns x phase)))

Theorem: svtv-overrides->assigns-nat-equiv-congruence-on-phase

(defthm svtv-overrides->assigns-nat-equiv-congruence-on-phase
  (implies (nat-equiv phase phase-equiv)
           (equal (svtv-overrides->assigns x phase)
                  (svtv-overrides->assigns x phase-equiv)))
  :rule-classes :congruence)