refined 0.1.1.0 → 0.1.2

raw patch · 2 files changed

+72/−9 lines, 2 filesdep ~base-prelude

Dependency ranges changed: base-prelude

Files

• library/Refined.hs +70/−7
• refined.cabal +2/−2

@@ -14,9 +14,14 @@   -- ** Numeric   LessThan,   GreaterThan,+  From,+  To,+  FromTo,   EqualTo,   Positive,+  NonPositive,   Negative,+  NonNegative,   ZeroToOne, ) where@@ -51,10 +56,16 @@ -- A smart constructor of a 'Refined' value. -- Checks the input value at runtime. {-# INLINABLE refine #-}-refine :: forall p x. Predicate p x => x -> Either String (Refined p x)+refine :: Predicate p x => x -> Either String (Refined p x) refine x =-  maybe (Right (Refined x)) Left $-  validate (undefined :: p) x+  fix $ \result ->+    maybe (Right (Refined x)) Left $+    validate (predicateByResult result) x+  where+    -- A work-around for the type-inference.+    predicateByResult :: Either String (Refined p x) -> p+    predicateByResult =+      const undefined  -- | -- Constructs a 'Refined' value with checking at compile-time using Template Haskell.@@ -76,9 +87,15 @@ -- 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 :: forall p x. (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))+refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x)) refineTH =-  fmap TH.TExp . either fail TH.lift . (refine :: x -> Either String (Refined p x))+  fix $ \loop ->+    fmap TH.TExp . either fail TH.lift . refineByResult (loop undefined)+  where+    -- A work-around for the type-inference.+    refineByResult :: Predicate p x => TH.Q (TH.TExp (Refined p x)) -> x -> Either String (Refined p x)+    refineByResult =+      const refine  -- | -- Extracts the refined value.@@ -170,6 +187,43 @@       x' = natVal p  -- |+-- A predicate, which ensures that a value is greater than or equal to the specified type-level number.+data From (n :: Nat)++instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where+  validate p x =+    if x >= fromIntegral x'+      then Nothing+      else Just ("Value is less than " <> show x')+    where+      x' = natVal p++-- |+-- A predicate, which ensures that a value is less than or equal to the specified type-level number.+data To (n :: Nat)++instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where+  validate p x =+    if x <= fromIntegral x'+      then Nothing+      else Just ("Value is greater than " <> show x')+    where+      x' = natVal p++-- |+-- 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)++instance (Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx) x where+  validate p x =+    if x >= fromIntegral mn' && x <= fromIntegral mx'+      then Nothing+      else Just ("Value is out of range (minimum: " <> show mn' <> ", maximum: " <> show mx' <> ")")+    where+      mn' = natVal (Proxy :: Proxy mn)+      mx' = natVal (Proxy :: Proxy mx)++-- | -- A predicate, which ensures that a value equals to the specified type-level number. data EqualTo (n :: Nat) @@ -187,12 +241,21 @@   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 =-  And (Not (LessThan 0)) (Not (GreaterThan 1))-+  FromTo 0 1

@@ -1,7 +1,7 @@ name:   refined version:-  0.1.1.0+  0.1.2 synopsis:   Refinement types with static and runtime checking description:@@ -50,5 +50,5 @@     Haskell2010   build-depends:     template-haskell >= 2.9 && < 3,-    base-prelude >= 0.1.19 && < 0.2,+    base-prelude >= 0.1.19 && < 2,     base >= 4.7 && < 5