= (values min0 (min max0 max1) (max min0 min1) max1))
      ('>= (values (max min0 min1) max0 min1 (min max0 max1)))
      ('> (values (max min0 (1+ min1)) max0 min1 (min (1- max0) max1)))))
  (define (infer-real-ranges)
    (match op
      ((or '< '<=) (values min0 (min max0 max1) (max min0 min1) max1))
      ((or '> '>=) (values (max min0 min1) max0 min1 (min max0 max1)))))
  (if (= (logior type0 type1) &exact-integer)
      (infer-integer-ranges)
      (infer-real-ranges)))

(define-syntax-rule (true-comparison-restrictions op a b a-type b-type)
  (call-with-values
      (lambda ()
        (restricted-comparison-ranges op
                                      (&type a) (&min a) (&max a)
                                      (&type b) (&min b) (&max b)))
    (lambda (min0 max0 min1 max1)
      (restrict! a a-type min0 max0)
      (restrict! b b-type min1 max1))))

(define-syntax-rule (define-comparison-inferrer (op inverse))
  (define-predicate-inferrer (op a b true?)
    (when (zero? (logand (logior (&type a) (&type b)) (lognot &number)))
      (true-comparison-restrictions (if true? 'op 'inverse) a b &real &real))))

(define-simple-type-checker (< &real &real))
(define-comparison-inferrer (< >=))

(define-simple-type-checker (<= &real &real))
(define-comparison-inferrer (<= >))

(define-simple-type-checker (>= &real &real))
(define-comparison-inferrer (>= <))

(define-simple-type-checker (> &real &real))
(define-comparison-inferrer (> <=))

(define-simple-type-checker (u64-= &u64 &u64))
(define-predicate-inferrer (u64-= a b true?)
  (when true?
    (let ((min (max (&min/0 a) (&min/0 b)))
          (max (min (&max/u64 a) (&max/u64 b))))
      (restrict! a &u64 min max)
      (restrict! b &u64 min max))))

(define-simple-type-checker (u64-=-scm &u64 &real))
(define-predicate-inferrer (u64-=-scm a b true?)
  (when (and true? (zero? (logand (&type b) (lognot &real))))
    (let ((min (max (&min/0 a) (&min/0 b)))
          (max (min (&max/u64 a) (&max/u64 b))))
      (restrict! a &u64 min max)
      (restrict! b &real min max))))

(define-simple-type-checker (u64-<-scm &u64 &real))
(define-predicate-inferrer (u64-<-scm a b true?)
  (when (and true? (zero? (logand (&type b) (lognot &real))))
    (true-comparison-restrictions '< a b &u64 &real)))

(define-simple-type-checker (u64-<=-scm &u64 &real))
(define-predicate-inferrer (u64-<=-scm a b true?)
  (when (and true? (zero? (logand (&type b) (lognot &real))))
    (true-comparison-restrictions '<= a b &u64 &real)))

(define-simple-type-checker (u64->=-scm &u64 &real))
(define-predicate-inferrer (u64->=-scm a b true?)
  (when (and true? (zero? (logand (&type b) (lognot &real))))
    (true-comparison-restrictions '>= a b &u64 &real)))

(define-simple-type-checker (u64->-scm &u64 &real))
(define-predicate-inferrer (u64->-scm a b true?)
  (when (and true? (zero? (logand (&type b) (lognot &real))))
    (true-comparison-restrictions '> a b &u64 &real)))

(define (infer-u64-comparison-ranges op min0 max0 min1 max1)
  (match op
    ('< (values min0 (min max0 (1- max1)) (max (1+ min0) min1) max1))
    ('<= (values min0 (min max0 max1) (max min0 min1) max1))
    ('>= (values (max min0 min1) max0 min1 (min max0 max1)))
    ('> (values (max min0 (1+ min1)) max0 min1 (min (1- max0) max1)))))
(define-syntax-rule (define-u64-comparison-inferrer (u64-op op inverse))
  (define-predicate-inferrer (u64-op a b true?)
    (call-with-values
        (lambda ()
          (infer-u64-comparison-ranges (if true? 'op 'inverse)
                                       (&min/0 a) (&max/u64 a)
                                       (&min/0 b) (&max/u64 b)))
      (lambda (min0 max0 min1 max1)
        (restrict! a &u64 min0 max0)
        (restrict! b &u64 min1 max1)))))

(define-simple-type-checker (u64-< &u64 &u64))
(define-u64-comparison-inferrer (u64-< < >=))

(define-simple-type-checker (u64-<= &u64 &u64))
(define-u64-comparison-inferrer (u64-<= <= >))

(define-simple-type-checker (u64->= &u64 &u64))
(define-u64-comparison-inferrer (u64-<= >= <))

(define-simple-type-checker (u64-> &u64 &u64))
(define-u64-comparison-inferrer (u64-> > <=))

;; Arithmetic.
(define-syntax-rule (define-unary-result! a result min max)
  (let ((min* min)
        (max* max)
        (type (logand (&type a) &number)))
    (cond
     ((not (= type (&type a)))
      ;; Not a number.  Punt and do nothing.
      (define! result &all-types -inf.0 +inf.0))
     ;; Complex numbers don't have a range.
     ((eqv? type &complex)
      (define! result &complex -inf.0 +inf.0))
     (else
      (define! result type min* max*)))))

(define-syntax-rule (define-binary-result! a b result closed? min max)
  (let ((min* min)
        (max* max)
        (a-type (logand (&type a) &number))
        (b-type (logand (&type b) &number)))
    (cond
     ((or (not (= a-type (&type a))) (not (= b-type (&type b))))
      ;; One input not a number.  Perhaps we end up dispatching to
      ;; GOOPS.
      (define! result &all-types -inf.0 +inf.0))
     ;; Complex numbers are contagious.
     ((or (eqv? a-type &complex) (eqv? b-type &complex))
      (define! result &complex -inf.0 +inf.0))
     ((or (eqv? a-type &flonum) (eqv? b-type &flonum))
      ;; If one argument is a flonum, the result will be flonum or
      ;; possibly complex.
      (let ((result-type (logand (logior a-type b-type)
                                 (logior &complex &flonum))))
        (define! result result-type min* max*)))
     ;; Exact integers are closed under some operations.
     ((and closed? (eqv? a-type &exact-integer) (eqv? b-type &exact-integer))
      (define! result &exact-integer min* max*))
     (else
      (let* ((type (logior a-type b-type))
             ;; Fractions may become integers.
             (type (if (zero? (logand type &fraction))
                       type
                       (logior type &exact-integer)))
             ;; Integers may become fractions under division.
             (type (if (or closed?
                           (zero? (logand type (logior &exact-integer))))
                       type
                       (logior type &fraction))))
        (define! result type min* max*))))))

(define-simple-type-checker (add &number &number))
(define-type-aliases add add/immediate)
(define-type-checker (fadd a b) #t)
(define-type-checker (uadd a b) #t)
(define-type-inferrer (add a b result)
  (define-binary-result! a b result #t
                         (+ (&min a) (&min b))
                         (+ (&max a) (&max b))))
(define-type-inferrer (fadd a b result)
  (define! result &f64
    (+ (&min a) (&min b))
    (+ (&max a) (&max b))))
(define-type-inferrer (uadd a b result)
  ;; Handle wraparound.
  (let ((max (+ (&max/u64 a) (&max/u64 b))))
    (if (<= max &u64-max)
        (define! result &u64 (+ (&min/0 a) (&min/0 b)) max)
        (define! result &u64 0 &u64-max))))
(define-type-aliases uadd uadd/immediate)

(define-simple-type-checker (sub &number &number))
(define-type-aliases sub sub/immediate)
(define-type-checker (fsub a b) #t)
(define-type-checker (usub a b) #t)
(define-type-inferrer (sub a b result)
  (define-binary-result! a b result #t
                         (- (&min a) (&max b))
                         (- (&max a) (&min b))))
(define-type-inferrer (fsub a b result)
  (define! result &f64
    (- (&min a) (&max b))
    (- (&max a) (&min b))))
(define-type-inferrer (usub a b result)
  ;; Handle wraparound.
  (let ((min (- (&min/0 a) (&max/u64 b))))
    (if (< min 0)
        (define! result &u64 0 &u64-max)
        (define! result &u64 min (- (&max/u64 a) (&min/0 b))))))
(define-type-aliases usub usub/immediate)

(define-simple-type-checker (mul &number &number))
(define-type-checker (fmul a b) #t)
(define-type-checker (umul a b) #t)
(define (mul-result-range same? nan-impossible? min-a max-a min-b max-b)
  (define (nan* a b)
    (if (and (or (and (inf? a) (zero? b))
                 (and (zero? a) (inf? b)))
             nan-impossible?)
        0 
        (* a b)))
  (let ((-- (nan* min-a min-b))
        (-+ (nan* min-a max-b))
        (++ (nan* max-a max-b))
        (+- (nan* max-a min-b)))
    (let ((has-nan? (or (nan? --) (nan? -+) (nan? ++) (nan? +-))))
      (values (cond
               (same? 0)
               (has-nan? -inf.0)
               (else (min -- -+ ++ +-)))
              (if has-nan?
                  +inf.0
                  (max -- -+ ++ +-))))))
(define-type-inferrer (mul a b result)
  (let ((min-a (&min a)) (max-a (&max a))
        (min-b (&min b)) (max-b (&max b))
        ;; We only really get +inf.0 at runtime for flonums and
        ;; compnums.  If we have inferred that the arguments are not
        ;; flonums and not compnums, then the result of (* +inf.0 0) at
        ;; range inference time is 0 and not +nan.0.
        (nan-impossible? (not (logtest (logior (&type a) (&type b))
                                       (logior &flonum &complex)))))
    (call-with-values (lambda ()
                        (mul-result-range (eqv? a b) nan-impossible?
                                          min-a max-a min-b max-b))
      (lambda (min max)
        (define-binary-result! a b result #t min max)))))
(define-type-inferrer (fmul a b result)
  (let ((min-a (&min a)) (max-a (&max a))
        (min-b (&min b)) (max-b (&max b))
        (nan-impossible? #f))
    (call-with-values (lambda ()
                        (mul-result-range (eqv? a b) nan-impossible?
                                          min-a max-a min-b max-b))
      (lambda (min max)
        (define! result &f64 min max)))))
(define-type-inferrer (umul a b result)
  ;; Handle wraparound.
  (let ((max (* (&max/u64 a) (&max/u64 b))))
    (if (<= max &u64-max)
        (define! result &u64 (* (&min/0 a) (&min/0 b)) max)
        (define! result &u64 0 &u64-max))))
(define-type-aliases umul umul/immediate)

(define-type-checker (div a b)
  (and (check-type a &number -inf.0 +inf.0)
       (check-type b &number -inf.0 +inf.0)
       ;; We only know that there will not be an exception if b is not
       ;; zero.
       (not (<= (&min b) 0 (&max b)))))
(define-type-checker (fdiv a b) #t)
(define (div-result-range min-a max-a min-b max-b)
  (if (<= min-b 0 max-b)
      ;; If the range of the divisor crosses 0, the result spans
      ;; the whole range.
      (values -inf.0 +inf.0)
      ;; Otherwise min-b and max-b have the same sign, and cannot both
      ;; be infinity.
      (let ((--- (if (inf? min-b) 0 (floor/ min-a min-b)))
            (-+- (if (inf? max-b) 0 (floor/ min-a max-b)))
            (++- (if (inf? max-b) 0 (floor/ max-a max-b)))
            (+-- (if (inf? min-b) 0 (floor/ max-a min-b)))
            (--+ (if (inf? min-b) 0 (ceiling/ min-a min-b)))
            (-++ (if (inf? max-b) 0 (ceiling/ min-a max-b)))
            (+++ (if (inf? max-b) 0 (ceiling/ max-a max-b)))
            (+-+ (if (inf? min-b) 0 (ceiling/ max-a min-b))))
        (values (min (min --- -+- ++- +--)
                     (min --+ -++ +++ +-+))
                (max (max --- -+- ++- +--)
                     (max --+ -++ +++ +-+))))))
(define-type-inferrer (div a b result)
  (let ((min-a (&min a)) (max-a (&max a))
        (min-b (&min b)) (max-b (&max b)))
    (call-with-values (lambda ()
                        (div-result-range min-a max-a min-b max-b))
      (lambda (min max)
        (define-binary-result! a b result #f min max)))))
(define-type-inferrer (fdiv a b result)
  (let ((min-a (&min a)) (max-a (&max a))
        (min-b (&min b)) (max-b (&max b)))
    (call-with-values (lambda ()
                        (div-result-range min-a max-a min-b max-b))
      (lambda (min max)
        (define! result &f64 min max)))))

(define-type-checker (quo a b)
  (and (check-type a &exact-integer -inf.0 +inf.0)
       (check-type b &exact-integer -inf.0 +inf.0)
       ;; We only know that there will not be an exception if b is not
       ;; zero.
       (not (<= (&min b) 0 (&max b)))))
(define-type-inferrer (quo a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  (define! result &exact-integer -inf.0 +inf.0))

(define-type-checker-aliases quo rem)
(define-type-inferrer (rem a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  ;; Same sign as A.
  (let ((max-abs-rem (1- (max (abs (&min b)) (abs (&max b))))))
    (cond
     ((< (&min a) 0)
      (if (< 0 (&max a))
          (define! result &exact-integer (- max-abs-rem) max-abs-rem)
          (define! result &exact-integer (- max-abs-rem) 0)))
     (else
      (define! result &exact-integer 0 max-abs-rem)))))

(define-type-checker-aliases quo mod)
(define-type-inferrer (mod a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  ;; Same sign as B.
  (let ((max-abs-mod (1- (max (abs (&min b)) (abs (&max b))))))
    (cond
     ((< (&min b) 0)
      (if (< 0 (&max b))
          (define! result &exact-integer (- max-abs-mod) max-abs-mod)
          (define! result &exact-integer (- max-abs-mod) 0)))
     (else
      (define! result &exact-integer 0 max-abs-mod)))))

;; Predicates.
(define-syntax-rule (define-number-kind-predicate-inferrer name type)
  (define-type-inferrer (name val result)
    (cond
     ((zero? (logand (&type val) type))
      (define! result &false 0 0))
     ((zero? (logand (&type val) (lognot type)))
      (define! result &true 0 0))
     (else
      (define! result (logior &true &false) 0 0)))))
(define-number-kind-predicate-inferrer complex? &number)
(define-number-kind-predicate-inferrer real? &real)
(define-number-kind-predicate-inferrer rational?
  (logior &exact-integer &fraction))
(define-number-kind-predicate-inferrer integer?
  (logior &exact-integer &flonum))
(define-number-kind-predicate-inferrer exact-integer?
  &exact-integer)

(define-simple-type-checker (exact? &number))
(define-type-inferrer (exact? val result)
  (restrict! val &number -inf.0 +inf.0)
  (cond
   ((zero? (logand (&type val) (logior &exact-integer &fraction)))
    (define! result &false 0 0))
   ((zero? (logand (&type val) (lognot (logior &exact-integer &fraction))))
    (define! result &true 0 0))
   (else
    (define! result (logior &true &false) 0 0))))

(define-simple-type-checker (inexact? &number))
(define-type-inferrer (inexact? val result)
  (restrict! val &number -inf.0 +inf.0)
  (cond
   ((zero? (logand (&type val) (logior &flonum &complex)))
    (define! result &false 0 0))
   ((zero? (logand (&type val) (logand &number
                                       (lognot (logior &flonum &complex)))))
    (define! result &true 0 0))
   (else
    (define! result (logior &true &false) 0 0))))

(define-simple-type-checker (inf? &real))
(define-type-inferrer (inf? val result)
  (restrict! val &real -inf.0 +inf.0)
  (cond
   ((or (zero? (logand (&type val) (logior &flonum &complex)))
        (and (not (inf? (&min val))) (not (inf? (&max val)))))
    (define! result &false 0 0))
   (else
    (define! result (logior &true &false) 0 0))))

(define-type-aliases inf? nan?)

(define-simple-type (even? &exact-integer)
  ((logior &true &false) 0 0))
(define-type-aliases even? odd?)

;; Bit operations.
(define-simple-type-checker (ash &exact-integer &exact-integer))
(define-type-inferrer (ash val count result)
  (define (ash* val count)
    ;; As we only precisely represent a 64-bit range, don't bother inferring
    ;; shifts that might exceed that range.
    (cond
     ((inf? val) val) ; Preserves sign.
     ((< -64 count 64) (ash val count))
     ((zero? val) 0)
     ((positive? val) +inf.0)
     (else -inf.0)))
  (restrict! val &exact-integer -inf.0 +inf.0)
  (restrict! count &exact-integer -inf.0 +inf.0)
  (let ((-- (ash* (&min val) (&min count)))
        (-+ (ash* (&min val) (&max count)))
        (++ (ash* (&max val) (&max count)))
        (+- (ash* (&max val) (&min count))))
    (define! result &exact-integer
             (min -- -+ ++ +-)
             (max -- -+ ++ +-))))

(define-simple-type-checker (ursh &u64 &u64))
(define-type-inferrer (ursh a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (define! result &u64
    (ash (&min/0 a) (- (&max/u64 b)))
    (ash (&max/u64 a) (- (&min/0 b)))))
(define-type-aliases ursh ursh/immediate)

(define-simple-type-checker (ulsh &u64 &u64))
(define-type-inferrer (ulsh a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (if (and (< (&max/u64 b) 64)
           (<= (ash (&max/u64 a) (&max/u64 b)) &u64-max))
      ;; No overflow; we can be precise.
      (define! result &u64
        (ash (&min/0 a) (&min/0 b))
        (ash (&max/u64 a) (&max/u64 b)))
      ;; Otherwise assume the whole range.
      (define! result &u64 0 &u64-max)))
(define-type-aliases ulsh ulsh/immediate)

(define-inlinable (non-negative? n)
  "Return true if N is non-negative, otherwise return false."
  (not (negative? n)))

;; Like 'lognot', but handles infinities.
(define-inlinable (lognot* n)
  "Return the bitwise complement of N.  If N is infinite, return -N."
  (- -1 n))

(define saturate+
  (case-lambda
    "Let N be the least upper bound of the integer lengths of the
arguments.  Return the greatest integer whose integer length is N.
If any of the arguments are infinite, return positive infinity."
    ((a b)
     (if (or (inf? a) (inf? b))
         +inf.0
         (1- (ash 1 (max (integer-length a)
                         (integer-length b))))))
    ((a b c)
     (saturate+ (saturate+ a b) c))
    ((a b c d)
     (saturate+ (saturate+ a b) c d))))

(define saturate-
  (case-lambda
    "Let N be the least upper bound of the integer lengths of the
arguments.  Return the least integer whose integer length is N.
If any of the arguments are infinite, return negative infinity."
    ((a b)     (lognot* (saturate+ a b)))
    ((a b c)   (lognot* (saturate+ a b c)))
    ((a b c d) (lognot* (saturate+ a b c d)))))

(define (logand-bounds a0 a1 b0 b1)
  "Return two values: lower and upper bounds for (logand A B)
where (A0 <= A <= A1) and (B0 <= B <= B1)."
  ;; For each argument, we consider three cases: (1) the argument is
  ;; non-negative, (2) its sign is unknown, or (3) it is negative.
  ;; To handle both arguments, we must consider a total of 9 cases:
  ;;
  ;; -----------------------------------------------------------------------
  ;;    LOGAND      | non-negative B   | unknown-sign B | negative B
  ;; -----------------------------------------------------------------------
  ;; non-negative A | 0 .. (min A1 B1) | 0 .. A1        | 0 .. A1
  ;; -----------------------------------------------------------------------
  ;; unknown-sign A | 0 .. B1          | (sat- A0 B0)   | (sat- A0 B0)
  ;;                |                  |      ..        |    .. A1
  ;;                |                  | (sat+ A1 B1)   |
  ;; -----------------------------------------------------------------------
  ;;     negative A | 0 .. B1          | (sat- A0 B0)   | (sat- A0 B0)
  ;;                |                  |    .. B1       |    .. (min A1 B1)
  ;; -----------------------------------------------------------------------
  (values (if (or (non-negative? a0) (non-negative? b0))
              0
              (saturate- a0 b0))
          (cond ((or (and (non-negative? a0) (non-negative? b0))
                     (and (negative? a1) (negative? b1)))
                 (min a1 b1))
                ((or (non-negative? a0) (negative? b1))
                 a1)
                ((or (non-negative? b0) (negative? a1))
                 b1)
                (else
                 (saturate+ a1 b1)))))

(define-simple-type-checker (logand &exact-integer &exact-integer))
(define-type-inferrer (logand a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  (call-with-values (lambda ()
                      (logand-bounds (&min a) (&max a) (&min b) (&max b)))
    (lambda (min max)
      (define! result &exact-integer min max))))

(define-simple-type-checker (ulogand &u64 &u64))
(define-type-inferrer (ulogand a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (define! result &u64 0 (min (&max/u64 a) (&max/u64 b))))

(define (logsub-bounds a0 a1 b0 b1)
  "Return two values: lower and upper bounds for (logsub A B),
i.e. (logand A (lognot B)), where (A0 <= A <= A1) and (B0 <= B <= B1)."
  ;; Here we use 'logand-bounds' to compute the bounds, after
  ;; computing the bounds of (lognot B) from the bounds of B.
  ;; From (B0 <= B <= B1) it follows that (~B1 <= ~B <= ~B0),
  ;; where ~X means (lognot X).
  (logand-bounds a0 a1 (lognot* b1) (lognot* b0)))

(define-simple-type-checker (logsub &exact-integer &exact-integer))
(define-type-inferrer (logsub a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  (call-with-values (lambda ()
                      (logsub-bounds (&min a) (&max a) (&min b) (&max b)))
    (lambda (min max)
      (define! result &exact-integer min max))))

(define-simple-type-checker (ulogsub &u64 &u64))
(define-type-inferrer (ulogsub a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (define! result &u64 0 (&max/u64 a)))

(define (logior-bounds a0 a1 b0 b1)
  "Return two values: lower and upper bounds for (logior A B)
where (A0 <= A <= A1) and (B0 <= B <= B1)."
  ;; For each argument, we consider three cases: (1) the argument is
  ;; non-negative, (2) its sign is unknown, or (3) it is negative.
  ;; To handle both arguments, we must consider a total of 9 cases.
  ;;
  ;; ---------------------------------------------------------------------
  ;;    LOGIOR      | non-negative B | unknown-sign B | negative B
  ;; ---------------------------------------------------------------------
  ;; non-negative A | (max A0 B0)    | B0             | B0 .. -1
  ;;                |   ..           |   ..           |
  ;;                | (sat+ A1 B1)   | (sat+ A1 B1)   |
  ;; ---------------------------------------------------------------------
  ;; unknown-sign A | A0             | (sat- A0 B0)   | B0 .. -1
  ;;                |   ..           |        ..      |
  ;;                | (sat+ A1 B1)   | (sat+ A1 B1)   |
  ;; ---------------------------------------------------------------------
  ;;     negative A | A0 .. -1       | A0 .. -1       | (max A0 B0) .. -1
  ;; ---------------------------------------------------------------------
  (values (cond ((or (and (non-negative? a0) (non-negative? b0))
                     (and (negative? a1) (negative? b1)))
                 (max a0 b0))
                ((or (non-negative? a0) (negative? b1))
                 b0)
                ((or (non-negative? b0) (negative? a1))
                 a0)
                (else
                 (saturate- a0 b0)))
          (if (or (negative? a1) (negative? b1))
              -1
              (saturate+ a1 b1))))

(define-simple-type-checker (logior &exact-integer &exact-integer))
(define-type-inferrer (logior a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  (call-with-values (lambda ()
                      (logior-bounds (&min a) (&max a) (&min b) (&max b)))
    (lambda (min max)
      (define! result &exact-integer min max))))

(define-simple-type-checker (ulogior &u64 &u64))
(define-type-inferrer (ulogior a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (define! result &u64
    (max (&min/0 a) (&min/0 b))
    (saturate+ (&max/u64 a) (&max/u64 b))))

(define (logxor-bounds a0 a1 b0 b1)
  "Return two values: lower and upper bounds for (logxor A B)
where (A0 <= A <= A1) and (B0 <= B <= B1)."
  ;; For each argument, we consider three cases: (1) the argument is
  ;; non-negative, (2) its sign is unknown, or (3) it is negative.
  ;; To handle both arguments, we must consider a total of 9 cases.
  ;;
  ;; --------------------------------------------------------------------
  ;;    LOGXOR      | non-negative B | unknown-sign B     | negative B
  ;; --------------------------------------------------------------------
  ;; non-negative A | 0              |       (sat- A1 B0) | (sat- A1 B0)
  ;;                |   ..           |         ..         |   ..
  ;;                | (sat+ A1 B1)   | (sat+ A1 B1)       |     -1
  ;; --------------------------------------------------------------------
  ;; unknown-sign A | (sat- A0 B1)   | (sat- A0 B1 A1 B0) | (sat- A1 B0)
  ;;                |   ..           |   ..               |   ..
  ;;                | (sat+ A1 B1)   | (sat+ A1 B1 A0 B0) | (sat+ A0 B0)
  ;; --------------------------------------------------------------------
  ;;     negative A | (sat- A0 B1)   | (sat- A0 B1)       | 0
  ;;                |   ..           |    ..              |   ..
  ;;                |     -1         |       (sat+ A0 B0) | (sat+ A0 B0)
  ;; --------------------------------------------------------------------
  (values (cond ((or (and (non-negative? a0) (non-negative? b0))
                     (and (negative? a1) (negative? b1)))
                 0)
                ((or (non-negative? a0) (negative? b1))
                 (saturate- a1 b0))
                ((or (non-negative? b0) (negative? a1))
                 (saturate- a0 b1))
                (else
                 (saturate- a0 b1 a1 b0)))
          (cond ((or (and (non-negative? a0) (negative? b1))
                     (and (non-negative? b0) (negative? a1)))
                 -1)
                ((or (non-negative? a0) (non-negative? b0))
                 (saturate+ a1 b1))
                ((or (negative? a1) (negative? b1))
                 (saturate+ a0 b0))
                (else
                 (saturate+ a1 b1 a0 b0)))))

(define-simple-type-checker (logxor &exact-integer &exact-integer))
(define-type-inferrer (logxor a b result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0)
  (call-with-values (lambda ()
                      (logxor-bounds (&min a) (&max a) (&min b) (&max b)))
    (lambda (min max)
      (define! result &exact-integer min max))))

(define-simple-type-checker (ulogxor &u64 &u64))
(define-type-inferrer (ulogxor a b result)
  (restrict! a &u64 0 &u64-max)
  (restrict! b &u64 0 &u64-max)
  (define! result &u64 0 (saturate+ (&max/u64 a) (&max/u64 b))))

(define-simple-type-checker (lognot &exact-integer))
(define-type-inferrer (lognot a result)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (define! result &exact-integer
           (lognot* (&max a))
           (lognot* (&min a))))

(define-simple-type-checker (logtest &exact-integer &exact-integer))
(define-predicate-inferrer (logtest a b true?)
  (restrict! a &exact-integer -inf.0 +inf.0)
  (restrict! b &exact-integer -inf.0 +inf.0))

(define-simple-type-checker (logbit? (&exact-integer 0 +inf.0) &exact-integer))
(define-type-inferrer (logbit? a b result)
  (let ((a-min (&min a))
        (a-max (&max a))
        (b-min (&min b))
        (b-max (&max b)))
    (if (and (eqv? a-min a-max) (>= a-min 0) (not (inf? a-min))
             (eqv? b-min b-max) (>= b-min 0) (not (inf? b-min)))
        (let ((type (if (logbit? a-min b-min) &true &false)))
          (define! result type 0 0))
        (define! result (logior &true &false) 0 0))))

;; Flonums.
(define-simple-type-checker (sqrt &number))
(define-type-inferrer (sqrt x result)
  (let ((type (&type x)))
    (cond
     ((and (zero? (logand type &complex))
           (non-negative? (&min x)))
      (define! result
               (logior type &flonum)
               (exact-integer-sqrt (&min x))
               (if (inf? (&max x))
                   +inf.0
                   (call-with-values (lambda () (exact-integer-sqrt (&max x)))
                     (lambda (s r)
                       (if (zero? r) s (+ s 1)))))))
     (else
      (define! result (logior type &flonum &complex) -inf.0 +inf.0)))))

(define-simple-type-checker (abs &real))
(define-type-inferrer (abs x result)
  (let ((type (&type x)))
    (cond
     ((eqv? type (logand type &number))
      (restrict! x &real -inf.0 +inf.0)
      (define! result (logand type &real)
        (min (abs (&min x)) (abs (&max x)))
        (max (abs (&min x)) (abs (&max x)))))
     (else
      (define! result (logior (logand (&type x) (lognot &number))
                              (logand (&type x) &real))
        (&min/0 x)
        (max (abs (&min x)) (abs (&max x))))))))


