    {-# OPTIONS_GHC -Wunused-imports #-}

    -- |  Possibly infinite sets of integers (but with finitely many consecutive
    --    segments). Used for checking guard coverage in int/nat cases in the
    --    treeless compiler.

    module Agda.Utils.IntSet.Infinite
      ( IntSet
      , empty, full, below, above, singleton
      , difference, member, toFiniteList
      , invariant )
      where

    import Data.Set (Set)
    import qualified Data.Set as Set

    -- | Represents a set of integers.
    --   Invariants:
    --     - All cannot be the argument to `Below` or `Above`
    --     - at most one 'IntsBelow'
    --     - at most one 'IntsAbove'
    --     - if `Below lo` and `Below hi`, then `lo < hi`
    --     - if `Below lo .. (Some xs)` then `all (> lo) xs`
    --     - if `Above hi .. (Some xs)` then `all (< hi - 1) xs`
    data IntSet = All
                  | Some (Set Integer)
                  | Below Integer IntSet  -- exclusive
                  | Above Integer IntSet  -- inclusive
      deriving (Int -> IntSet -> ShowS
    [IntSet] -> ShowS
    IntSet -> String
    (Int -> IntSet -> ShowS)
    -> (IntSet -> String) -> ([IntSet] -> ShowS) -> Show IntSet
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IntSet -> ShowS
    showsPrec :: Int -> IntSet -> ShowS
    $cshow :: IntSet -> String
    show :: IntSet -> String
    $cshowList :: [IntSet] -> ShowS
    showList :: [IntSet] -> ShowS
    Show)

    instance Eq IntSet where
      IntSet
    r == :: IntSet -> IntSet -> Bool
    == IntSet
    r' = IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    norm IntSet
    r Maybe (Maybe Integer, Maybe Integer, Set Integer)
    -> Maybe (Maybe Integer, Maybe Integer, Set Integer) -> Bool
    forall a. Eq a => a -> a -> Bool
    == IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    norm IntSet
    r'
        where
          norm :: IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    norm IntSet
    All          = Maybe (Maybe Integer, Maybe Integer, Set Integer)
    forall a. Maybe a
    Nothing
          norm (Some Set Integer
    xs)    = (Maybe Integer, Maybe Integer, Set Integer)
    -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    forall a. a -> Maybe a
    Just (Maybe Integer
    forall a. Maybe a
    Nothing, Maybe Integer
    forall a. Maybe a
    Nothing, Set Integer
    xs)
          norm (Below Integer
    lo IntSet
    r) = do (_, hi, xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    norm IntSet
    r; return (Just lo, hi, xs)
          norm (Above Integer
    hi IntSet
    r) = do (lo, _, xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
    norm IntSet
    r; return (lo, Just hi, xs)

    below' :: Integer -> IntSet -> IntSet
    below' :: Integer -> IntSet -> IntSet
    below' Integer
    _  IntSet
    All = IntSet
    All
    below' Integer
    lo r :: IntSet
    r@(Some Set Integer
    xs)
      | Integer
    lo Integer -> Set Integer -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Integer
    xs = Integer -> IntSet -> IntSet
    below' (Integer
    lo Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) IntSet
    r
      | Bool
    otherwise  = Integer -> IntSet -> IntSet
    Below Integer
    lo (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Set Integer -> IntSet
    Some (Set Integer -> IntSet) -> Set Integer -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    lo) Set Integer
    xs
    below' Integer
    lo r0 :: IntSet
    r0@(Below Integer
    lo' IntSet
    r)
      | Integer
    lo' Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    lo = IntSet
    r0
      | Bool
    otherwise = Integer -> IntSet -> IntSet
    below' Integer
    lo IntSet
    r
    below' Integer
    lo (Above Integer
    hi IntSet
    r)
      | Integer
    hi Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lo  = IntSet
    All
      | Bool
    otherwise = Integer -> IntSet -> IntSet
    Above Integer
    hi (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Integer -> IntSet -> IntSet
    below' Integer
    lo IntSet
    r

    above' :: Integer -> IntSet -> IntSet
    above' :: Integer -> IntSet -> IntSet
    above' Integer
    _  IntSet
    All = IntSet
    All
    above' Integer
    hi r :: IntSet
    r@(Some Set Integer
    xs)
      | (Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Integer -> Set Integer -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Integer
    xs = Integer -> IntSet -> IntSet
    above' (Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) IntSet
    r
      | Bool
    otherwise        = Integer -> IntSet -> IntSet
    Above Integer
    hi (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Set Integer -> IntSet
    Some (Set Integer -> IntSet) -> Set Integer -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi) Set Integer
    xs
    above' Integer
    hi r0 :: IntSet
    r0@(Above Integer
    hi' IntSet
    r)
      | Integer
    hi' Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    hi = IntSet
    r0
      | Bool
    otherwise = Integer -> IntSet -> IntSet
    above' Integer
    hi IntSet
    r
    above' Integer
    hi (Below Integer
    lo IntSet
    r)
      | Integer
    hi Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lo  = IntSet
    All
      | Bool
    otherwise = Integer -> IntSet -> IntSet
    Below Integer
    lo (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Integer -> IntSet -> IntSet
    above' Integer
    hi IntSet
    r

    some' :: Set Integer -> IntSet -> IntSet
    some' :: Set Integer -> IntSet -> IntSet
    some' Set Integer
    xs IntSet
    r | Set Integer -> Bool
    forall a. Set a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set Integer
    xs = IntSet
    r
    some' Set Integer
    xs (Some Set Integer
    ys) = Set Integer -> IntSet
    Some (Set Integer -> Set Integer -> Set Integer
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set Integer
    xs Set Integer
    ys)
    some' Set Integer
    _  IntSet
    All = IntSet
    All
    some' Set Integer
    xs (Below Integer
    lo IntSet
    r)
      | Integer
    lo Integer -> Set Integer -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Integer
    xs = Set Integer -> IntSet -> IntSet
    some' Set Integer
    xs (Integer -> IntSet -> IntSet
    Below (Integer
    lo Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) IntSet
    r)
      | Bool
    otherwise  = Integer -> IntSet -> IntSet
    below' Integer
    lo (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Set Integer -> IntSet -> IntSet
    some' ((Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    lo) Set Integer
    xs) IntSet
    r
    some' Set Integer
    xs (Above Integer
    hi IntSet
    r)
      | (Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Integer -> Set Integer -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Integer
    xs = Set Integer -> IntSet -> IntSet
    some' Set Integer
    xs (Integer -> IntSet -> IntSet
    Above (Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) IntSet
    r)
      | Bool
    otherwise        = Integer -> IntSet -> IntSet
    above' Integer
    hi (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Set Integer -> IntSet -> IntSet
    some' ((Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi) Set Integer
    xs) IntSet
    r

    difference :: IntSet -> IntSet -> IntSet
    difference :: IntSet -> IntSet -> IntSet
    difference IntSet
    r IntSet
    All           = IntSet
    empty
    difference IntSet
    r (Some Set Integer
    xs)     = IntSet -> Set Integer -> IntSet
    subtractSome IntSet
    r Set Integer
    xs
    difference IntSet
    r (Below Integer
    lo IntSet
    r') = IntSet -> IntSet -> IntSet
    difference (IntSet -> Integer -> IntSet
    subtractBelow IntSet
    r Integer
    lo) IntSet
    r'
    difference IntSet
    r (Above Integer
    hi IntSet
    r') = IntSet -> IntSet -> IntSet
    difference (IntSet -> Integer -> IntSet
    subtractAbove IntSet
    r Integer
    hi) IntSet
    r'

    subtractSome :: IntSet -> Set Integer -> IntSet
    subtractSome :: IntSet -> Set Integer -> IntSet
    subtractSome IntSet
    r Set Integer
    xs | Set Integer -> Bool
    forall a. Set a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set Integer
    xs = IntSet
    r
    subtractSome IntSet
    All Set Integer
    xs = Integer -> IntSet
    below Integer
    lo IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> Integer -> IntSet
    above Integer
    hi IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> Set Integer -> IntSet
    Some ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer
    lo..Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1] Set Integer -> Set Integer -> Set Integer
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set Integer
    xs)
      where lo :: Integer
    lo = Set Integer -> Integer
    forall a. Ord a => Set a -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum Set Integer
    xs
            hi :: Integer
    hi = Set Integer -> Integer
    forall a. Ord a => Set a -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum Set Integer
    xs Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
    subtractSome (Some Set Integer
    ys) Set Integer
    xs = Set Integer -> IntSet
    Some (Set Integer -> Set Integer -> Set Integer
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference Set Integer
    ys Set Integer
    xs)
    subtractSome (Below Integer
    lo IntSet
    r) Set Integer
    xs = Integer -> IntSet -> IntSet
    Below (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    lo Integer
    lo') (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ IntSet -> Set Integer -> IntSet
    subtractSome (Set Integer -> IntSet
    Some ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer
    lo'..Integer
    lo Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1]) IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> IntSet
    r) Set Integer
    xs
      where lo' :: Integer
    lo' = Set Integer -> Integer
    forall a. Ord a => Set a -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum Set Integer
    xs
    subtractSome (Above Integer
    hi IntSet
    r) Set Integer
    xs = Integer -> IntSet -> IntSet
    Above (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    hi Integer
    hi') (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ IntSet -> Set Integer -> IntSet
    subtractSome (Set Integer -> IntSet
    Some ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer
    hi..Integer
    hi' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1]) IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> IntSet
    r) Set Integer
    xs
      where hi' :: Integer
    hi' = Set Integer -> Integer
    forall a. Ord a => Set a -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum Set Integer
    xs Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1

    subtractBelow :: IntSet -> Integer -> IntSet
    subtractBelow :: IntSet -> Integer -> IntSet
    subtractBelow IntSet
    All           Integer
    lo = Integer -> IntSet
    above Integer
    lo
    subtractBelow (Below Integer
    lo' IntSet
    r) Integer
    lo = Set Integer -> IntSet -> IntSet
    some' ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer
    lo..Integer
    lo' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1]) (IntSet -> Integer -> IntSet
    subtractBelow IntSet
    r Integer
    lo)
    subtractBelow (Above Integer
    hi IntSet
    r)  Integer
    lo = Integer -> IntSet -> IntSet
    Above (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    hi Integer
    lo) (IntSet -> Integer -> IntSet
    subtractBelow IntSet
    r Integer
    lo)
    subtractBelow (Some Set Integer
    xs)     Integer
    lo = Set Integer -> IntSet
    Some (Set Integer -> IntSet) -> Set Integer -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    lo) Set Integer
    xs

    subtractAbove :: IntSet -> Integer -> IntSet
    subtractAbove :: IntSet -> Integer -> IntSet
    subtractAbove IntSet
    All           Integer
    hi = Integer -> IntSet
    below Integer
    hi
    subtractAbove (Above Integer
    hi' IntSet
    r) Integer
    hi = Set Integer -> IntSet -> IntSet
    some' ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer
    hi'..Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1]) (IntSet -> Integer -> IntSet
    subtractAbove IntSet
    r Integer
    hi)
    subtractAbove (Below Integer
    lo IntSet
    r)  Integer
    hi = Integer -> IntSet -> IntSet
    Below (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    lo Integer
    hi) (IntSet -> Integer -> IntSet
    subtractAbove IntSet
    r Integer
    hi)
    subtractAbove (Some Set Integer
    xs)     Integer
    hi = Set Integer -> IntSet
    Some (Set Integer -> IntSet) -> Set Integer -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Bool) -> Set Integer -> Set Integer
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi) Set Integer
    xs

    instance Semigroup IntSet where
      Below Integer
    lo IntSet
    r <> :: IntSet -> IntSet -> IntSet
    <> IntSet
    r' = Integer -> IntSet -> IntSet
    below' Integer
    lo (IntSet
    r IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> IntSet
    r')
      Above Integer
    hi IntSet
    r <> IntSet
    r' = Integer -> IntSet -> IntSet
    above' Integer
    hi (IntSet
    r IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> IntSet
    r')
      Some Set Integer
    xs    <> IntSet
    r' = Set Integer -> IntSet -> IntSet
    some' Set Integer
    xs IntSet
    r'
      IntSet
    All        <> IntSet
    _  = IntSet
    All

    instance Monoid IntSet where
      mempty :: IntSet
    mempty  = IntSet
    empty
      mappend :: IntSet -> IntSet -> IntSet
    mappend = IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Membership
    member :: Integer -> IntSet -> Bool
    member :: Integer -> IntSet -> Bool
    member Integer
    _ IntSet
    All          = Bool
    True
    member Integer
    x (Some Set Integer
    xs)    = Integer -> Set Integer -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Integer
    x Set Integer
    xs
    member Integer
    x (Below Integer
    lo IntSet
    s) = Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    lo  Bool -> Bool -> Bool
    || Integer -> IntSet -> Bool
    member Integer
    x IntSet
    s
    member Integer
    x (Above Integer
    hi IntSet
    s) = Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    hi Bool -> Bool -> Bool
    || Integer -> IntSet -> Bool
    member Integer
    x IntSet
    s

    -- | All integers `< n`
    below :: Integer -> IntSet
    below :: Integer -> IntSet
    below Integer
    lo = Integer -> IntSet -> IntSet
    Below Integer
    lo IntSet
    empty

    -- | All integers `>= n`
    above :: Integer -> IntSet
    above :: Integer -> IntSet
    above Integer
    hi = Integer -> IntSet -> IntSet
    Above Integer
    hi IntSet
    empty

    -- | A single integer.
    singleton :: Integer -> IntSet
    singleton :: Integer -> IntSet
    singleton Integer
    x = [Integer] -> IntSet
    fromList [Integer
    x]

    -- | From a list of integers.
    fromList :: [Integer] -> IntSet
    fromList :: [Integer] -> IntSet
    fromList [Integer]
    xs = Set Integer -> IntSet
    Some ([Integer] -> Set Integer
    forall a. Ord a => [a] -> Set a
    Set.fromList [Integer]
    xs)

    -- | No integers.
    empty :: IntSet
    empty :: IntSet
    empty = Set Integer -> IntSet
    Some Set Integer
    forall a. Set a
    Set.empty

    -- | All integers.
    full :: IntSet
    full :: IntSet
    full = IntSet
    All

    -- | If finite, return the list of elements.
    toFiniteList :: IntSet -> Maybe [Integer]
    toFiniteList :: IntSet -> Maybe [Integer]
    toFiniteList (Some Set Integer
    xs) = [Integer] -> Maybe [Integer]
    forall a. a -> Maybe a
    Just ([Integer] -> Maybe [Integer]) -> [Integer] -> Maybe [Integer]
    forall a b. (a -> b) -> a -> b
    $ Set Integer -> [Integer]
    forall a. Set a -> [a]
    Set.toList Set Integer
    xs
    toFiniteList IntSet
    All       = Maybe [Integer]
    forall a. Maybe a
    Nothing
    toFiniteList Above{}   = Maybe [Integer]
    forall a. Maybe a
    Nothing
    toFiniteList Below{}   = Maybe [Integer]
    forall a. Maybe a
    Nothing

    -- | Invariant.
    invariant :: IntSet -> Bool
    invariant :: IntSet -> Bool
    invariant IntSet
    xs =
      case IntSet
    xs of
        IntSet
    All         -> Bool
    True
        Some{}      -> Bool
    True
        Below Integer
    lo IntSet
    ys -> IntSet -> Bool
    invariant IntSet
    ys Bool -> Bool -> Bool
    && Integer -> IntSet -> Bool
    invBelow Integer
    lo IntSet
    ys
        Above Integer
    hi IntSet
    ys -> IntSet -> Bool
    invariant IntSet
    ys Bool -> Bool -> Bool
    && Integer -> IntSet -> Bool
    invAbove Integer
    hi IntSet
    ys
      where
        invBelow :: Integer -> IntSet -> Bool
    invBelow Integer
    lo IntSet
    All          = Bool
    False
        invBelow Integer
    lo (Some Set Integer
    xs)    = (Integer -> Bool) -> Set Integer -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    lo) Set Integer
    xs
        invBelow Integer
    lo Below{}      = Bool
    False
        invBelow Integer
    lo (Above Integer
    hi IntSet
    r) = Integer
    lo Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi Bool -> Bool -> Bool
    && Integer -> IntSet -> Bool
    invBelow Integer
    lo IntSet
    r

        invAbove :: Integer -> IntSet -> Bool
    invAbove Integer
    hi IntSet
    All          = Bool
    False
        invAbove Integer
    hi (Some Set Integer
    xs)    = (Integer -> Bool) -> Set Integer -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Set Integer
    xs
        invAbove Integer
    hi Above{}      = Bool
    False
        invAbove Integer
    hi (Below Integer
    lo IntSet
    r) = Integer
    lo Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    hi Bool -> Bool -> Bool
    && Integer -> IntSet -> Bool
    invAbove Integer
    hi IntSet
    r