{-# 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)