Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.IntSet.Infinite

Description

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

Synopsis

data IntSet
empty :: IntSet
full :: IntSet
below :: Integer -> IntSet
above :: Integer -> IntSet
singleton :: Integer -> IntSet
difference :: IntSet -> IntSet -> IntSet
member :: Integer -> IntSet -> Bool
toFiniteList :: IntSet -> Maybe [Integer]
invariant :: IntSet -> Bool

Documentation

data IntSet #

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`

Instances

Eq IntSet #
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (==) :: IntSet -> IntSet -> Bool # (/=) :: IntSet -> IntSet -> Bool #
Show IntSet #
Instance details Defined in Agda.Utils.IntSet.Infinite Methods showsPrec :: Int -> IntSet -> ShowS # show :: IntSet -> String # showList :: [IntSet] -> ShowS #
Semigroup IntSet #
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (<>) :: IntSet -> IntSet -> IntSet # sconcat :: NonEmpty IntSet -> IntSet # stimes :: Integral b => b -> IntSet -> IntSet #
Monoid IntSet #
Instance details Defined in Agda.Utils.IntSet.Infinite Methods mempty :: IntSet # mappend :: IntSet -> IntSet -> IntSet # mconcat :: [IntSet] -> IntSet #

empty :: IntSet #

No integers.

full :: IntSet #

All integers.

below :: Integer -> IntSet #

All integers `< n`

above :: Integer -> IntSet #

All integers `>= n`

singleton :: Integer -> IntSet #

A single integer.

difference :: IntSet -> IntSet -> IntSet #

member :: Integer -> IntSet -> Bool #

Membership

toFiniteList :: IntSet -> Maybe [Integer] #

If finite, return the list of elements.

invariant :: IntSet -> Bool #

Invariant.