-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Refinement types with static and runtime checking
--   
--   For an extensive introduction to the library please follow to <a>this
--   blog-post</a>.
@package refined
@version 0.1.2

module Refined

-- | A refinement type, which wraps a value of type <tt>x</tt>, ensuring
--   that it satisfies a type-level predicate <tt>p</tt>.
data Refined p x

-- | A smart constructor of a <a>Refined</a> value. Checks the input value
--   at runtime.
refine :: Predicate p x => x -> Either String (Refined p x)

-- | Constructs a <a>Refined</a> value with checking at compile-time using
--   Template Haskell. E.g.,
--   
--   <pre>
--   &gt;&gt;&gt; $$(refineTH 23) :: Refined Positive Int
--   Refined 23
--   </pre>
--   
--   Here's an example of an invalid value:
--   
--   <pre>
--   &gt;&gt;&gt; $$(refineTH 0) :: Refined Positive Int
--   &lt;interactive&gt;:6:4:
--       Value is not greater than 0
--       In the Template Haskell splice $$(refineTH 0)
--       In the expression: $$(refineTH 0) :: Refined Positive Int
--       In an equation for ‘it’:
--           it = $$(refineTH 0) :: Refined Positive Int
--   </pre>
--   
--   If it's not evident, the example above indicates a compile-time
--   failure, which means that the checking was done at compile-time, thus
--   introducing a zero runtime overhead compared to a plain value
--   construction.
refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))

-- | Extracts the refined value.
unrefine :: Refined p x -> x

-- | A class which defines a runtime interpretation of a type-level
--   predicate <tt>p</tt> for type <tt>x</tt>.
class Predicate p x

-- | Check the value <tt>x</tt> according to the predicate <tt>p</tt>,
--   producing an error string if the value does not satisfy.
validate :: Predicate p x => p -> x -> Maybe String

-- | A logical negation of a predicate.
data Not r

-- | A logical conjunction predicate, composed of two other predicates.
data And l r

-- | A logical disjunction predicate, composed of two other predicates.
data Or l r

-- | A predicate, which ensures that a value is less than the specified
--   type-level number.
data LessThan (n :: Nat)

-- | A predicate, which ensures that a value is greater than the specified
--   type-level number.
data GreaterThan (n :: Nat)

-- | A predicate, which ensures that a value is greater than or equal to
--   the specified type-level number.
data From (n :: Nat)

-- | A predicate, which ensures that a value is less than or equal to the
--   specified type-level number.
data To (n :: Nat)

-- | A predicate, which ensures that a value is between or equal to either
--   of the specified type-level numbers.
data FromTo (mn :: Nat) (mx :: Nat)

-- | A predicate, which ensures that a value equals to the specified
--   type-level number.
data EqualTo (n :: Nat)

-- | A predicate, which ensures that the value is greater than zero.
type Positive = GreaterThan 0

-- | A predicate, which ensures that the value is less than or equal to
--   zero.
type NonPositive = To 0

-- | A predicate, which ensures that the value is less than zero.
type Negative = LessThan 0

-- | A predicate, which ensures that the value is greater than or equal to
--   zero.
type NonNegative = From 0

-- | A range of values from zero to one, including both.
type ZeroToOne = FromTo 0 1
instance GHC.Generics.Constructor Refined.C1_0Refined
instance GHC.Generics.Datatype Refined.D1Refined
instance GHC.Generics.Generic (Refined.Refined p x)
instance (Data.Data.Data p, Data.Data.Data x) => Data.Data.Data (Refined.Refined p x)
instance GHC.Classes.Ord x => GHC.Classes.Ord (Refined.Refined p x)
instance GHC.Classes.Eq x => GHC.Classes.Eq (Refined.Refined p x)
instance GHC.Show.Show x => GHC.Show.Show (Refined.Refined p x)
instance (GHC.Read.Read x, Refined.Predicate p x) => GHC.Read.Read (Refined.Refined p x)
instance Language.Haskell.TH.Syntax.Lift x => Language.Haskell.TH.Syntax.Lift (Refined.Refined p x)
instance Refined.Predicate r x => Refined.Predicate (Refined.Not r) x
instance (Refined.Predicate l x, Refined.Predicate r x) => Refined.Predicate (Refined.And l r) x
instance (Refined.Predicate l x, Refined.Predicate r x) => Refined.Predicate (Refined.Or l r) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat n) => Refined.Predicate (Refined.LessThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat n) => Refined.Predicate (Refined.GreaterThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat n) => Refined.Predicate (Refined.From n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat n) => Refined.Predicate (Refined.To n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat mn, GHC.TypeLits.KnownNat mx, mn GHC.TypeLits.<= mx) => Refined.Predicate (Refined.FromTo mn mx) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeLits.KnownNat n) => Refined.Predicate (Refined.EqualTo n) x