refined-extras-0.1.0.0: Increased functionality for refined types.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Refined.Extras.Utils

Description

Utilities for Refined.

Since: 0.1.0.0

Synopsis

Pattern Synonym

pattern MkRefined :: a -> Refined p a Source #

Unidirectional pattern synonym for Refined. This allows us to pattern match on a refined term without exposing the unsafe internal details.

Examples

Expand
>>> :{
let safeDiv :: Implies p NonZero => Int -> Refined p Int -> Int
    safeDiv n (MkRefined d) = n `div` d
    two = $$(refineTH @NonZero @Int 2)
 in safeDiv 10 two
:}
5

Since: 0.1.0.0

Exception Functions

showRefineException :: RefineException -> String Source #

Displays a RefineException without formatting. Intended for situations where RefineException's default formatting is undesirable (e.g. doctests, logging).

Examples

Expand
>>> first showRefineException $ refine @(And NonZero NonNegative) 0
Left "RefineAndException (And * * (NotEqualTo 0) (From 0)) (This (RefineOtherException (NotEqualTo 0) \"Value does equal 0\"))"

>>> let ex = refine @(Xor (And NonZero NonNegative) NonZero) 0
>>> first showRefineException ex
Left "RefineXorException (Xor * * (And * * (NotEqualTo 0) (From 0)) (NotEqualTo 0)) (RefineAndException (And * * (NotEqualTo 0) (From 0)) (This (RefineOtherException (NotEqualTo 0) \"Value does equal 0\"))) (RefineOtherException (NotEqualTo 0) \"Value does equal 0\")"

Since: 0.1.0.0

showtRefineException :: RefineException -> Text Source #

Variant of showRefineException for Text.

Since: 0.1.0.0

refineExceptionToType :: RefineException -> TypeRep Source #

Retrieves the TypeRep corresponding to a RefineException.

Examples

Expand
>>> first refineExceptionToType $ refine @(And NonZero NonNegative) 0
Left (And * * (NotEqualTo 0) (From 0))

Since: 0.1.0.0