Safe Haskell	None
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 Source #

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

Instances details

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

empty :: IntSet Source #

No integers.

full :: IntSet Source #

All integers.

below :: Integer -> IntSet Source #

All integers `< n`

above :: Integer -> IntSet Source #

All integers `>= n`

singleton :: Integer -> IntSet Source #

A single integer.

difference :: IntSet -> IntSet -> IntSet Source #

member :: Integer -> IntSet -> Bool Source #

Membership

toFiniteList :: IntSet -> Maybe [Integer] Source #

If finite, return the list of elements.

invariant :: IntSet -> Bool Source #

Invariant.