		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-compare-int-width

Signature
(sparseint$-compare-int-width width offset x y) → sign
Arguments: width — Guard (posp width).; 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-width

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

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

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

Theorem: sparseint$-compare-int-width-correct

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

Theorem: sparseint$-compare-int-width-of-pos-fix-width

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

Theorem: sparseint$-compare-int-width-pos-equiv-congruence-on-width

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

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

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

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

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

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

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

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

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

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

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

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

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