		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex-lhsrewrite-aux

Signature
(svex-lhsrewrite-aux x shift w) → xx
Arguments: x — Guard (svex-p x).; shift — Guard (natp shift).; w — Guard (natp w).
Returns: xx — Type (svex-p xx).

Definitions and Theorems

Function: svex-lhsrewrite-aux

(defun svex-lhsrewrite-aux (x shift w)
 (declare (xargs :guard (and (svex-p x) (natp shift) (natp w))))
 (let ((__function__ 'svex-lhsrewrite-aux))
  (declare (ignorable __function__))
  (svex-case
   x :var (svex-fix x)
   :quote (svex-fix x)
   :call
   (b* ((shift (lnfix shift)) (w (lnfix w)))
    (case x.fn
     (concat
      (b*
       (((unless
              (and (eql (len x.args) 3)
                   (eq (svex-kind (first x.args)) :quote)
                   (4vec-index-p (svex-quote->val (first x.args)))))
         (svex-fix x))
        (xw (2vec->val (svex-quote->val (first x.args))))
        ((when (<= xw shift))
         (svex-concat xw (svex-quote (4vec-z))
                      (svex-lhsrewrite-aux (third x.args)
                                           (- shift xw)
                                           w)))
        ((when (<= (+ shift w) xw))
         (svex-lhsrewrite-aux (second x.args)
                              shift w))
        (low (svex-lhsrewrite-aux (second x.args)
                                  shift (- xw shift)))
        (high (svex-lhsrewrite-aux (third x.args)
                                   0 (- (+ shift w) xw))))
       (svex-concat xw low high)))
     (signx
      (b*
       (((unless
              (and (eql (len x.args) 2)
                   (eq (svex-kind (first x.args)) :quote)
                   (4vec-index-p (svex-quote->val (first x.args)))))
         (svex-fix x))
        (xw (2vec->val (svex-quote->val (first x.args))))
        ((when (<= xw shift)) (svex-fix x))
        ((when (<= (+ shift w) xw))
         (svex-lhsrewrite-aux (second x.args)
                              shift w)))
       (svex-fix x)))
     (rsh
      (b*
       (((unless
              (and (eql (len x.args) 2)
                   (eq (svex-kind (first x.args)) :quote)
                   (4vec-index-p (svex-quote->val (first x.args)))))
         (svex-fix x))
        (xsh (2vec->val (svex-quote->val (first x.args)))))
       (svex-rsh xsh
                 (svex-lhsrewrite-aux (second x.args)
                                      (+ shift xsh)
                                      w))))
     (otherwise (svex-fix x)))))))

Theorem: svex-p-of-svex-lhsrewrite-aux

(defthm svex-p-of-svex-lhsrewrite-aux
  (b* ((xx (svex-lhsrewrite-aux x shift w)))
    (svex-p xx))
  :rule-classes :rewrite)

Theorem: svex-lhsrewrite-aux-of-svex-fix-x

(defthm svex-lhsrewrite-aux-of-svex-fix-x
  (equal (svex-lhsrewrite-aux (svex-fix x)
                              shift w)
         (svex-lhsrewrite-aux x shift w)))

Theorem: svex-lhsrewrite-aux-svex-equiv-congruence-on-x

(defthm svex-lhsrewrite-aux-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-lhsrewrite-aux x shift w)
                  (svex-lhsrewrite-aux x-equiv shift w)))
  :rule-classes :congruence)

Theorem: svex-lhsrewrite-aux-of-nfix-shift

(defthm svex-lhsrewrite-aux-of-nfix-shift
  (equal (svex-lhsrewrite-aux x (nfix shift) w)
         (svex-lhsrewrite-aux x shift w)))

Theorem: svex-lhsrewrite-aux-nat-equiv-congruence-on-shift

(defthm svex-lhsrewrite-aux-nat-equiv-congruence-on-shift
  (implies (nat-equiv shift shift-equiv)
           (equal (svex-lhsrewrite-aux x shift w)
                  (svex-lhsrewrite-aux x shift-equiv w)))
  :rule-classes :congruence)

Theorem: svex-lhsrewrite-aux-of-nfix-w

(defthm svex-lhsrewrite-aux-of-nfix-w
  (equal (svex-lhsrewrite-aux x shift (nfix w))
         (svex-lhsrewrite-aux x shift w)))

Theorem: svex-lhsrewrite-aux-nat-equiv-congruence-on-w

(defthm svex-lhsrewrite-aux-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (svex-lhsrewrite-aux x shift w)
                  (svex-lhsrewrite-aux x shift w-equiv)))
  :rule-classes :congruence)

Theorem: svex-lhsrewrite-aux-correct-lemma

(defthm svex-lhsrewrite-aux-correct-lemma
 (equal
   (4vec-concat (2vec (nfix w))
                (4vec-rsh (2vec (nfix shift))
                          (svex-eval (svex-lhsrewrite-aux x shift w)
                                     env))
                (4vec-z))
   (4vec-concat (2vec (nfix w))
                (4vec-rsh (2vec (nfix shift))
                          (svex-eval x env))
                (4vec-z))))

Theorem: svex-lhsrewrite-aux-vars

(defthm svex-lhsrewrite-aux-vars
  (implies (not (member v (svex-vars x)))
           (not (member v
                        (svex-vars (svex-lhsrewrite-aux x sh w))))))