-- 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.2.2.0


-- | In type theory, a refinement type is a type endowed with a predicate
--   which is assumed to hold for any element of the refined type.
--   
--   This library allows one to capture the idea of a refinement type using
--   the <a>Refined</a> type. A <a>Refined</a> <tt>p</tt> <tt>x</tt> wraps
--   a value of type <tt>x</tt>, ensuring that it satisfies a type-level
--   predicate <tt>p</tt>.
--   
--   A simple introduction to this library can be found here:
--   <a>http://nikita-volkov.github.io/refined/</a>
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>.
--   
--   The only ways that this library provides to construct a value of type
--   <a>Refined</a> are with the 'refine-' family of functions, because the
--   use of the newtype constructor gets around the checking of the
--   predicate. This restriction on the user makes <a>unrefine</a> safe.
--   
--   If you would <i>really</i> like to construct a <a>Refined</a> value
--   without checking the predicate, use <a>unsafeCoerce</a>.
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 RefineException (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>throwM</a>
--   if the value does not satisfy the predicate.
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>fail</a> if
--   the value does not satisfy the predicate.
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling
--   <a>throwError</a> if the value does not satisfy the predicate.
refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>error</a> if
--   the value does not satisfy the predicate.
--   
--   WARNING: this function is not total!
unsafeRefine :: (Predicate p x) => x -> Refined p x

-- | Constructs a <a>Refined</a> value at compile-time using
--   <tt>-XTemplateHaskell</tt>.
--   
--   For example:
--   
--   <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 typeclass which defines a runtime interpretation of a type-level
--   predicate <tt>p</tt> for type <tt>x</tt>.
class (Typeable p) => 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, (Monad m)) => p -> x -> RefineT m ()

-- | The negation of a predicate.
data Not p

-- | The conjunction of two predicates.
data And l r

-- | The conjunction of two predicates.
type && = And

-- | The disjunction of two predicates.
data Or l r

-- | The disjunction of two predicates.
type || = Or

-- | A <a>Predicate</a> ensuring that the value is less than the specified
--   type-level number.
data LessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than the
--   specified type-level number.
data GreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   the specified type-level number.
data From (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   the specified type-level number.
data To (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is within an inclusive
--   range.
data FromTo (mn :: Nat) (mx :: Nat)

-- | A <a>Predicate</a> ensuring that the value is equal to the specified
--   type-level number <tt>n</tt>.
data EqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is not equal to the
--   specified type-level number <tt>n</tt>.
data NotEqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than zero.
type Positive = GreaterThan 0

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   zero.
type NonPositive = To 0

-- | A <a>Predicate</a> ensuring that the value is less than zero.
type Negative = LessThan 0

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   zero.
type NonNegative = From 0

-- | An inclusive range of values from zero to one.
type ZeroToOne = FromTo 0 1

-- | A <a>Predicate</a> ensuring that the value is not equal to zero.
type NonZero = NotEqualTo 0

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is less than the specified type-level number.
data SizeLessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is greater than the specified type-level number.
data SizeGreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is equal to the specified type-level number.
data SizeEqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> is non-empty.
type NonEmpty = SizeGreaterThan 0

-- | A <a>Predicate</a> ensuring that the <a>IsList</a> contains elements
--   in a strictly ascending order.
data Ascending

-- | A <a>Predicate</a> ensuring that the <a>IsList</a> contains elements
--   in a strictly descending order.
data Descending

-- | A typeclass containing "safe" conversions between refined predicates
--   where the target is <i>weaker</i> than the source: that is, all values
--   that satisfy the first predicate will be guarunteed to satisy the
--   second.
--   
--   Take care: writing an instance declaration for your custom predicates
--   is the same as an assertion that <a>weaken</a> is safe to use:
--   
--   <pre>
--   instance <a>Weaken</a> Pred1 Pred2
--   </pre>
--   
--   For most of the instances, explicit type annotations for the result
--   value's type might be required.
class Weaken from to
weaken :: Weaken from to => Refined from x -> Refined to x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) l
--   </pre>
andLeft :: Refined (And l r) x -> Refined l x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) r
--   </pre>
andRight :: Refined (And l r) x -> Refined r x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken l (Or l r)
--   </pre>
leftOr :: Refined l x -> Refined (Or l r) x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken r (Or l r)
--   </pre>
rightOr :: Refined r x -> Refined (Or l r) x

-- | An exception encoding the way in which a <a>Predicate</a> failed.
data RefineException

-- | A <a>RefineException</a> for failures involving the <a>Not</a>
--   predicate.
RefineNotException :: !TypeRep -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>And</a>
--   predicate.
RefineAndException :: !TypeRep -> !(These RefineException RefineException) -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>Or</a>
--   predicate.
RefineOrException :: !TypeRep -> !RefineException -> !RefineException -> RefineException

-- | A <a>RefineException</a> for failures involving all other predicates.
RefineOtherException :: !TypeRep -> !(Doc Void) -> RefineException

-- | Display a <a>RefineException</a> as a <tt><a>Doc</a> ann</tt>
displayRefineException :: RefineException -> Doc ann

-- | A monad transformer that adds <tt><a>RefineException</a></tt>s to
--   other monads.
--   
--   The <tt><a>pure</a></tt> and <tt><a>return</a></tt> functions yield
--   computations that produce the given value, while
--   <tt><tt>&gt;&gt;=</tt></tt> sequences two subcomputations, exiting on
--   the first <tt><a>RefineException</a></tt>.
data RefineT m a

-- | The inverse of <tt><a>RefineT</a></tt>.
runRefineT :: RefineT m a -> m (Either RefineException a)

-- | Map the unwrapped computation using the given function.
--   
--   <pre>
--   <a>runRefineT</a> (<a>mapRefineT</a> f m) = f (<a>runRefineT</a> m)
--   </pre>
mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b

-- | <tt><a>RefineM</a> a</tt> is equivalent to <tt><a>RefineT</a>
--   <a>Identity</a> a</tt> for any type <tt>a</tt>.
type RefineM a = RefineT Identity a

-- | Constructs a computation in the <a>RefineM</a> monad. (The inverse of
--   <tt><a>runRefineM</a></tt>).
refineM :: Either RefineException a -> RefineM a

-- | Run a monadic action of type <tt><a>RefineM</a> a</tt>, yielding an
--   <tt><a>Either</a> <a>RefineException</a> a</tt>.
--   
--   This is just defined as <tt><a>runIdentity</a> <tt>.</tt>
--   <a>runRefineT</a></tt>.
runRefineM :: RefineM a -> Either RefineException a

-- | One can use <tt><a>throwRefine</a></tt> inside of a monadic context to
--   begin processing a <tt><a>RefineException</a></tt>.
throwRefine :: (Monad m) => RefineException -> RefineT m a

-- | A handler function to handle previous <tt><a>RefineException</a></tt>s
--   and return to normal execution. A common idiom is:
--   
--   <pre>
--   do { action1; action2; action3 } `<tt>catchRefine'</tt> handler
--   </pre>
--   
--   where the action functions can call <tt><a>throwRefine</a></tt>. Note
--   that handler and the do-block must have the same return type.
catchRefine :: (Monad m) => RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a

-- | A handler for a <tt><a>RefineException</a></tt>.
--   
--   <a>throwRefineOtherException</a> is useful for defining what behaviour
--   <a>validate</a> should have in the event of a predicate failure.
throwRefineOtherException :: (Monad m) => TypeRep -> Doc Void -> RefineT m a
instance GHC.Generics.Generic1 (Refined.RefineT m)
instance GHC.Generics.Generic (Refined.RefineT m a)
instance Control.Monad.Trans.Class.MonadTrans Refined.RefineT
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError Refined.RefineException (Refined.RefineT m)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Refined.RefineT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Refined.RefineT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Refined.RefineT m)
instance GHC.Base.Functor m => GHC.Base.Functor (Refined.RefineT m)
instance GHC.Generics.Generic Refined.RefineException
instance GHC.Show.Show x => GHC.Show.Show (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.Read.Read x, Refined.Predicate p x) => GHC.Read.Read (Refined.Refined p x)
instance (Refined.Predicate p x, Data.Typeable.Internal.Typeable p) => Refined.Predicate (Refined.Not p) x
instance (Refined.Predicate l x, Refined.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r) => Refined.Predicate (Refined.And l r) x
instance (Refined.Predicate l x, Refined.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r) => Refined.Predicate (Refined.Or l r) x
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeLessThan n) (t a)
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeGreaterThan n) (t a)
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeEqualTo n) (t a)
instance (GHC.Exts.IsList t, GHC.Classes.Ord (GHC.Exts.Item t)) => Refined.Predicate Refined.Ascending t
instance (GHC.Exts.IsList t, GHC.Classes.Ord (GHC.Exts.Item t)) => Refined.Predicate Refined.Descending t
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.LessThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.GreaterThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.From n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.To n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat mn, GHC.TypeNats.KnownNat mx, mn GHC.TypeNats.<= mx) => Refined.Predicate (Refined.FromTo mn mx) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.EqualTo n) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.NotEqualTo n) x
instance GHC.Show.Show Refined.RefineException
instance Data.Text.Prettyprint.Doc.Internal.Pretty Refined.RefineException
instance GHC.Exception.Exception Refined.RefineException
instance (n GHC.TypeNats.<= m) => Refined.Weaken (Refined.LessThan n) (Refined.LessThan m)
instance (n GHC.TypeNats.<= m) => Refined.Weaken (Refined.LessThan n) (Refined.To m)
instance (n GHC.TypeNats.<= m) => Refined.Weaken (Refined.To n) (Refined.To m)
instance (m GHC.TypeNats.<= n) => Refined.Weaken (Refined.GreaterThan n) (Refined.GreaterThan m)
instance (m GHC.TypeNats.<= n) => Refined.Weaken (Refined.GreaterThan n) (Refined.From m)
instance (m GHC.TypeNats.<= n) => Refined.Weaken (Refined.From n) (Refined.From m)
instance (p GHC.TypeNats.<= n, m GHC.TypeNats.<= q) => Refined.Weaken (Refined.FromTo n m) (Refined.FromTo p q)
instance (p GHC.TypeNats.<= n) => Refined.Weaken (Refined.FromTo n m) (Refined.From p)
instance (m GHC.TypeNats.<= q) => Refined.Weaken (Refined.FromTo n m) (Refined.To q)
instance Language.Haskell.TH.Syntax.Lift x => Language.Haskell.TH.Syntax.Lift (Refined.Refined p x)


-- | This module contains orphan <a>Lift</a> instances of types in common
--   libraries such as <tt>containers</tt>, for more available compile-time
--   checking of predicates.
module Refined.TH
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.IntMap.Internal.IntMap a)
instance (Language.Haskell.TH.Syntax.Lift k, Language.Haskell.TH.Syntax.Lift v) => Language.Haskell.TH.Syntax.Lift (Data.Map.Internal.Map k v)
instance Language.Haskell.TH.Syntax.Lift v => Language.Haskell.TH.Syntax.Lift (Data.Set.Internal.Set v)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.Elem a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.Node a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.Digit a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.FingerTree a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.Seq a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.ViewL a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Sequence.Internal.ViewR a)
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Tree.Tree a)