		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-compare-int

Signature
(sparseint$-compare-int offset x y) → sign
Arguments: offset — Guard (natp offset).; x — Guard (sparseint$-p x).; y — Guard (integerp y).
Returns: sign — Type (integerp sign).

Definitions and Theorems

Function: sparseint$-compare-int

(defun sparseint$-compare-int (offset x y)
 (declare (xargs :guard (and (natp offset)
                             (sparseint$-p x)
                             (integerp y))))
 (let ((__function__ 'sparseint$-compare-int))
  (declare (ignorable __function__))
  (b* ((y (lifix y)) (offset (lnfix offset)))
   (sparseint$-case
     x :leaf
     (b* ((x (logtail offset x.val)))
       (compare x y))
     :concat
     (b* (((when (<= x.width offset))
           (sparseint$-compare-int (- offset x.width)
                                   x.msbs y))
          (width1 (- x.width offset))
          (msbs-compare
               (sparseint$-compare-int 0 x.msbs (logtail width1 y)))
          ((unless (eql 0 msbs-compare))
           msbs-compare))
       (sparseint$-compare-int-width
            width1 offset
            x.lsbs (bignum-loghead width1 y)))))))

Theorem: integerp-of-sparseint$-compare-int

(defthm integerp-of-sparseint$-compare-int
  (b* ((sign (sparseint$-compare-int offset x y)))
    (integerp sign))
  :rule-classes :type-prescription)

Theorem: sparseint$-compare-int-correct

(defthm sparseint$-compare-int-correct
  (b* ((?sign (sparseint$-compare-int offset x y)))
    (b* ((xval (logtail offset (sparseint$-val x))))
      (equal sign (compare xval y)))))

Theorem: sparseint$-compare-int-of-nfix-offset

(defthm sparseint$-compare-int-of-nfix-offset
  (equal (sparseint$-compare-int (nfix offset)
                                 x y)
         (sparseint$-compare-int offset x y)))

Theorem: sparseint$-compare-int-nat-equiv-congruence-on-offset

(defthm sparseint$-compare-int-nat-equiv-congruence-on-offset
  (implies (nat-equiv offset offset-equiv)
           (equal (sparseint$-compare-int offset x y)
                  (sparseint$-compare-int offset-equiv x y)))
  :rule-classes :congruence)

Theorem: sparseint$-compare-int-of-sparseint$-fix-x

(defthm sparseint$-compare-int-of-sparseint$-fix-x
  (equal (sparseint$-compare-int offset (sparseint$-fix x)
                                 y)
         (sparseint$-compare-int offset x y)))

Theorem: sparseint$-compare-int-sparseint$-equiv-congruence-on-x

(defthm sparseint$-compare-int-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-compare-int offset x y)
                  (sparseint$-compare-int offset x-equiv y)))
  :rule-classes :congruence)

Theorem: sparseint$-compare-int-of-ifix-y

(defthm sparseint$-compare-int-of-ifix-y
  (equal (sparseint$-compare-int offset x (ifix y))
         (sparseint$-compare-int offset x y)))

Theorem: sparseint$-compare-int-int-equiv-congruence-on-y

(defthm sparseint$-compare-int-int-equiv-congruence-on-y
  (implies (int-equiv y y-equiv)
           (equal (sparseint$-compare-int offset x y)
                  (sparseint$-compare-int offset x y-equiv)))
  :rule-classes :congruence)