		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex->lhs-range

Signature
(svex->lhs-range rsh w x) → lhs
Arguments: rsh — Guard (natp rsh).; w — Guard (natp w).; x — Guard (svex-p x).
Returns: lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: svex->lhs-range

(defun svex->lhs-range (rsh w x)
 (declare (xargs :guard (and (natp rsh) (natp w) (svex-p x))))
 (declare (xargs :guard (lhssvex-range-p rsh w x)))
 (let ((__function__ 'svex->lhs-range))
  (declare (ignorable __function__))
  (if (zp w)
      nil
    (svex-case
         x :var
         (list (lhrange w (lhatom-var x.name rsh)))
         :quote (list (lhrange w (lhatom-z)))
         :call
         (case x.fn
           (concat (b* (((unless (mbt (eql (len x.args) 3)))
                         nil)
                        ((list x.w x.lo x.hi) x.args)
                        (x.wval (2vec->val (svex-quote->val x.w)))
                        ((when (<= x.wval (lnfix rsh)))
                         (svex->lhs-range (- (lnfix rsh) x.wval)
                                          w x.hi))
                        ((when (<= (+ (lnfix rsh) w) x.wval))
                         (svex->lhs-range rsh w x.lo))
                        (lo-width (- x.wval (lnfix rsh))))
                     (lhs-concat lo-width
                                 (svex->lhs-range rsh lo-width x.lo)
                                 (svex->lhs-range 0 (- w lo-width)
                                                  x.hi))))
           (rsh (b* (((unless (mbt (eql (len x.args) 2)))
                      nil)
                     ((list x.sh x.sub) x.args)
                     (x.shval (2vec->val (svex-quote->val x.sh))))
                  (svex->lhs-range (+ x.shval (lnfix rsh))
                                   w x.sub))))))))

Theorem: lhs-p-of-svex->lhs-range

(defthm lhs-p-of-svex->lhs-range
  (b* ((lhs (svex->lhs-range rsh w x)))
    (lhs-p lhs))
  :rule-classes :rewrite)

Theorem: vars-of-svex->lhs-range

(defthm vars-of-svex->lhs-range
  (b* ((?lhs (svex->lhs-range rsh w x)))
    (implies (not (member v (svex-vars x)))
             (not (member v (lhs-vars lhs))))))

Theorem: svex->lhs-range-of-nfix-rsh

(defthm svex->lhs-range-of-nfix-rsh
  (equal (svex->lhs-range (nfix rsh) w x)
         (svex->lhs-range rsh w x)))

Theorem: svex->lhs-range-nat-equiv-congruence-on-rsh

(defthm svex->lhs-range-nat-equiv-congruence-on-rsh
  (implies (nat-equiv rsh rsh-equiv)
           (equal (svex->lhs-range rsh w x)
                  (svex->lhs-range rsh-equiv w x)))
  :rule-classes :congruence)

Theorem: svex->lhs-range-of-nfix-w

(defthm svex->lhs-range-of-nfix-w
  (equal (svex->lhs-range rsh (nfix w) x)
         (svex->lhs-range rsh w x)))

Theorem: svex->lhs-range-nat-equiv-congruence-on-w

(defthm svex->lhs-range-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (svex->lhs-range rsh w x)
                  (svex->lhs-range rsh w-equiv x)))
  :rule-classes :congruence)

Theorem: svex->lhs-range-of-svex-fix-x

(defthm svex->lhs-range-of-svex-fix-x
  (equal (svex->lhs-range rsh w (svex-fix x))
         (svex->lhs-range rsh w x)))

Theorem: svex->lhs-range-svex-equiv-congruence-on-x

(defthm svex->lhs-range-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex->lhs-range rsh w x)
                  (svex->lhs-range rsh w x-equiv)))
  :rule-classes :congruence)

Theorem: svex->lhs-range-correct

(defthm svex->lhs-range-correct
  (b* ((?lhs (svex->lhs-range rsh w x)))
    (implies (lhssvex-range-p rsh w x)
             (equal (lhs-eval lhs env)
                    (4vec-concat (2vec (nfix w))
                                 (4vec-rsh (2vec (nfix rsh))
                                           (svex-eval x env))
                                 (4vec-z))))))