    {-# LANGUAGE CPP #-}

    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Manage sets of natural numbers (de Bruijn indices).

    module Agda.Utils.VarSet
      ( VarSet
      , empty, insert, singleton, union, unions
      , fromList, toList, toAscList, toDescList
      , disjoint, isSubsetOf, member, IntSet.null
      , delete, difference, IntSet.filter, filterGE, intersection
      , mapMonotonic, Agda.Utils.VarSet.subtract
      )
      where

    import Data.IntSet as IntSet

    type VarSet = IntSet

    #if !MIN_VERSION_containers(0,6,3)
    mapMonotonic :: (Int -> Int) -> VarSet -> VarSet
    mapMonotonic f = fromDistinctAscList . fmap f . toAscList
    #endif

    -- | Subtract from each element.
    subtract :: Int -> VarSet -> VarSet
    subtract :: Key -> VarSet -> VarSet
    subtract Key
    n = (Key -> Key) -> VarSet -> VarSet
    mapMonotonic (Key -> Key -> Key
    forall a. Num a => a -> a -> a
    Prelude.subtract Key
    n)

    -- | Keep only elements greater or equal to the given pivot.
    filterGE :: Int -> VarSet -> VarSet
    filterGE :: Key -> VarSet -> VarSet
    filterGE Key
    n = (VarSet, VarSet) -> VarSet
    forall a b. (a, b) -> b
    snd ((VarSet, VarSet) -> VarSet)
    -> (VarSet -> (VarSet, VarSet)) -> VarSet -> VarSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Key -> VarSet -> (VarSet, VarSet)
    IntSet.split (Key
    n Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - Key
    1)