closed-0.2.0.3: Integers bounded by a closed interval
Safe HaskellNone
LanguageHaskell2010

Closed

Synopsis

Documentation

data Endpoint Source #

Describe whether the endpoint of a Bounds includes or excludes its argument

Constructors

Inclusive Nat

Endpoint includes its argument

Exclusive Nat

Endpoint excludes its argument

data Closed (n :: Nat) (m :: Nat) Source #

Instances

Instances details
(n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

arbitrary :: Gen (Closed n m) #

shrink :: Closed n m -> [Closed n m] #

(n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

parseJSON :: Value -> Parser (Closed n m) #

parseJSONList :: Value -> Parser [Closed n m] #

omittedField :: Maybe (Closed n m) #

ToJSON (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

toJSON :: Closed n m -> Value #

toEncoding :: Closed n m -> Encoding #

toJSONList :: [Closed n m] -> Value #

toEncodingList :: [Closed n m] -> Encoding #

omitField :: Closed n m -> Bool #

(n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) Source #

Generate the lowest and highest inhabitant of a given Closed type

Instance details

Defined in Closed.Internal

Methods

minBound :: Closed n m #

maxBound :: Closed n m #

(n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) Source #

Enumerate values in the range of a given Closed type

Instance details

Defined in Closed.Internal

Methods

succ :: Closed n m -> Closed n m #

pred :: Closed n m -> Closed n m #

toEnum :: Int -> Closed n m #

fromEnum :: Closed n m -> Int #

enumFrom :: Closed n m -> [Closed n m] #

enumFromThen :: Closed n m -> Closed n m -> [Closed n m] #

enumFromTo :: Closed n m -> Closed n m -> [Closed n m] #

enumFromThenTo :: Closed n m -> Closed n m -> Closed n m -> [Closed n m] #

Generic (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Associated Types

type Rep (Closed n m) 
Instance details

Defined in Closed.Internal

type Rep (Closed n m) = D1 ('MetaData "Closed" "Closed.Internal" "closed-0.2.0.3-Iw0RZsZMMp99q2nd3YJgcD" 'True) (C1 ('MetaCons "Closed" 'PrefixI 'True) (S1 ('MetaSel ('Just "getClosed") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

Methods

from :: Closed n m -> Rep (Closed n m) x #

to :: Rep (Closed n m) x -> Closed n m #

(n <= m, KnownNat n, KnownNat m) => Num (Closed n m) Source #

Bounded arithmetic, e.g. maxBound + 1 == maxBound

Instance details

Defined in Closed.Internal

Methods

(+) :: Closed n m -> Closed n m -> Closed n m #

(-) :: Closed n m -> Closed n m -> Closed n m #

(*) :: Closed n m -> Closed n m -> Closed n m #

negate :: Closed n m -> Closed n m #

abs :: Closed n m -> Closed n m #

signum :: Closed n m -> Closed n m #

fromInteger :: Integer -> Closed n m #

(n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

quot :: Closed n m -> Closed n m -> Closed n m #

rem :: Closed n m -> Closed n m -> Closed n m #

div :: Closed n m -> Closed n m -> Closed n m #

mod :: Closed n m -> Closed n m -> Closed n m #

quotRem :: Closed n m -> Closed n m -> (Closed n m, Closed n m) #

divMod :: Closed n m -> Closed n m -> (Closed n m, Closed n m) #

toInteger :: Closed n m -> Integer #

(n <= m, KnownNat n, KnownNat m) => Real (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

toRational :: Closed n m -> Rational #

Show (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

showsPrec :: Int -> Closed n m -> ShowS #

show :: Closed n m -> String #

showList :: [Closed n m] -> ShowS #

(n <= m, KnownNat n, KnownNat m) => FromField (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

parseField :: Field -> Parser (Closed n m) #

ToField (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

toField :: Closed n m -> Field #

NFData (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

rnf :: Closed n m -> () #

Eq (Closed n m) Source #

Test equality on Closed values in the same range

Instance details

Defined in Closed.Internal

Methods

(==) :: Closed n m -> Closed n m -> Bool #

(/=) :: Closed n m -> Closed n m -> Bool #

Ord (Closed n m) Source #

Compare Closed values in the same range

Instance details

Defined in Closed.Internal

Methods

compare :: Closed n m -> Closed n m -> Ordering #

(<) :: Closed n m -> Closed n m -> Bool #

(<=) :: Closed n m -> Closed n m -> Bool #

(>) :: Closed n m -> Closed n m -> Bool #

(>=) :: Closed n m -> Closed n m -> Bool #

max :: Closed n m -> Closed n m -> Closed n m #

min :: Closed n m -> Closed n m -> Closed n m #

Hashable (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

hashWithSalt :: Int -> Closed n m -> Int #

hash :: Closed n m -> Int #

(n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

toPersistValue :: Closed n m -> PersistValue #

fromPersistValue :: PersistValue -> Either Text (Closed n m) #

(n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) Source # 
Instance details

Defined in Closed.Internal

Methods

sqlType :: Proxy (Closed n m) -> SqlType #

type Rep (Closed n m) Source # 
Instance details

Defined in Closed.Internal

type Rep (Closed n m) = D1 ('MetaData "Closed" "Closed.Internal" "closed-0.2.0.3-Iw0RZsZMMp99q2nd3YJgcD" 'True) (C1 ('MetaCons "Closed" 'PrefixI 'True) (S1 ('MetaSel ('Just "getClosed") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) where ... Source #

Syntactic sugar to express open and half-open intervals using the Closed type

Equations

Bounds ('Inclusive n) ('Inclusive m) = Closed n m 
Bounds ('Inclusive n) ('Exclusive m) = Closed n (m - 1) 
Bounds ('Exclusive n) ('Inclusive m) = Closed (n + 1) m 
Bounds ('Exclusive n) ('Exclusive m) = Closed (n + 1) (m - 1) 

type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n) Source #

Syntactic sugar to express a value that has only one non-bottom inhabitant using the Closed type

type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs Source #

Syntactic sugar to express a value whose lower bound is zero

closed :: forall (n :: Nat) (m :: Nat). (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m) Source #

Safely create a Closed value using the specified argument

unsafeClosed :: forall (n :: Nat) (m :: Nat). (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m Source #

Create a Closed value throwing an error if the argument is not in range

clamp :: forall (n :: Nat) (m :: Nat) a. (KnownNat n, KnownNat m, n <= m, Integral a) => a -> Closed n m Source #

Clamp an Integral in the range constrained by a Closed interval

getClosed :: Closed n m -> Integer Source #

lowerBound :: forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n Source #

Proxy for the lower bound of a Closed value

upperBound :: forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m Source #

Proxy for the upper bound of a Closed value

equals :: forall (n :: Nat) (m :: Nat) (o :: Nat) (p :: Nat). Closed n m -> Closed o p -> Bool infix 4 Source #

Test two different types of Closed values for equality.

cmp :: forall (n :: Nat) (m :: Nat) (o :: Nat) (p :: Nat). Closed n m -> Closed o p -> Ordering Source #

Compare two different types of Closed values

natToClosed :: forall (n :: Nat) (m :: Nat) (x :: Nat) proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m Source #

Convert a type-level literal into a Closed value

weakenUpper :: forall (k :: Nat) (n :: Nat) (m :: Nat). (n <= m, m <= k) => Closed n m -> Closed n k Source #

Add inhabitants at the end

weakenLower :: forall (k :: Nat) (n :: Nat) (m :: Nat). (n <= m, k <= n) => Closed n m -> Closed k m Source #

Add inhabitants at the beginning

strengthenUpper :: forall (k :: Nat) (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k) Source #

Remove inhabitants from the end. Returns Nothing if the input was removed

strengthenLower :: forall (k :: Nat) (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m) Source #

Remove inhabitants from the beginning. Returns Nothing if the input was removed

add :: forall (n :: Nat) (m :: Nat) (o :: Nat) (p :: Nat). Closed n m -> Closed o p -> Closed (n + o) (m + p) Source #

Add two different types of Closed values

sub :: forall (n :: Nat) (m :: Nat) (o :: Nat) (p :: Nat). Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p)) Source #

Subtract two different types of Closed values Returns Left for negative results, and Right for positive results.

multiply :: forall (n :: Nat) (m :: Nat) (o :: Nat) (p :: Nat). Closed n m -> Closed o p -> Closed (n * o) (m * p) Source #

Multiply two different types of Closed values

isValidClosed :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) => Closed n m -> Bool Source #

Verifies that a given Closed value is valid. Should always return True unles you bring the Closed.Internal.Closed constructor into scope, or use unsafeCoerce or other nasty hacks