diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -4,6 +4,21 @@ The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/) and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## [0.6] - TBD +### Changed +- `strengthen` no longer returns an `Either`, since the proof + that it should always succeed is in its constraints. +- `validate` now takes a `Proxy` as its first argument. +- All uses of prettyprinter are now just `Text` + +### Removed +- Refined.These module +- Dependency on `prettyprinter` + +### Fixed +- bug in `sized` internal helper that caused formatting issues + in sized predicate errors + ## [0.5.1] - 2020-07-14 ### Changed - `refineTH_` is now implemented in terms of `refineTH` diff --git a/refined.cabal b/refined.cabal --- a/refined.cabal +++ b/refined.cabal @@ -3,7 +3,7 @@ name: refined version: - 0.5.1 + 0.6 synopsis: Refinement types with static and runtime checking description: @@ -65,7 +65,6 @@ src exposed-modules: Refined - Refined.These Refined.Unsafe Refined.Unsafe.Type default-language: @@ -76,7 +75,6 @@ , deepseq >= 1.4 && < 1.5 , exceptions >= 0.8 && < 0.11 , mtl >= 2.2.2 && < 2.3 - , prettyprinter >= 1.1.0.1 && < 1.7 , template-haskell >= 2.9 && < 2.17 , text >= 1.2 && < 1.3 , these-skinny >= 0.7.4 && < 0.8 diff --git a/src/Refined.hs b/src/Refined.hs --- a/src/Refined.hs +++ b/src/Refined.hs @@ -41,6 +41,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PackageImports #-} @@ -153,9 +154,6 @@ , throwRefineOtherException , throwRefineSomeException , success - - -- * Re-Exports - , PP.pretty ) where -------------------------------------------------------------------------------- @@ -164,14 +162,15 @@ import Data.Coerce (coerce) import Data.Either (isRight) import Data.Foldable (foldl') -import Data.Function (fix) import Data.Proxy (Proxy(Proxy)) import Data.Text (Text) import qualified Data.Text as Text +import qualified Data.Text.Lazy as TextLazy +import qualified Data.Text.Lazy.Builder as TextBuilder +import qualified Data.Text.Lazy.Builder.Int as TextBuilder import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as BL -import Data.Typeable (TypeRep, Typeable, typeOf) -import Data.Void (Void) +import Data.Typeable (TypeRep, Typeable, typeRep) import Control.Monad.Catch (MonadThrow, SomeException) import qualified Control.Monad.Catch as MonadThrow @@ -182,12 +181,12 @@ import Prelude hiding (fail) #endif +import GHC.Exts (Proxy#, proxy#) import GHC.Generics (Generic, Generic1) -import GHC.TypeLits (type (<=), KnownNat, Nat, natVal) +import GHC.TypeLits (type (<=), KnownNat, Nat, natVal') import Refined.Unsafe.Type (Refined(Refined)) -import qualified Data.Text.Prettyprint.Doc as PP import qualified Language.Haskell.TH.Syntax as TH #if HAVE_AESON @@ -198,7 +197,7 @@ #if HAVE_QUICKCHECK import Test.QuickCheck (Arbitrary, Gen) import qualified Test.QuickCheck as QC -import Data.Typeable (showsTypeRep, typeRep) +import Data.Typeable (showsTypeRep) #endif import "these-skinny" Data.These (These(This,That,These)) @@ -330,13 +329,8 @@ -- Checks the input value at runtime. -- -- @since 0.1.0.0 -refine :: (Predicate p x) => x -> Either RefineException (Refined p x) -refine x = do - let predicateByResult :: Either RefineException (Refined p x) -> p - predicateByResult = const undefined - fix $ \result -> do - maybe (Right (Refined x)) Left - (validate (predicateByResult result) x) +refine :: forall p x. (Predicate p x) => x -> Either RefineException (Refined p x) +refine x = maybe (Right (Refined x)) Left (validate (Proxy @p) x) {-# INLINABLE refine #-} -- | Like 'refine', but discards the refinement. @@ -405,18 +399,14 @@ -- . -- -- @since 0.1.0.0 -refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x)) +refineTH :: forall p x. (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x)) refineTH = - let refineByResult :: (Predicate p x) - => TH.Q (TH.TExp (Refined p x)) - -> x - -> Either RefineException (Refined p x) - refineByResult = const refine - showException = refineExceptionToTree .> showTree True - in fix $ \loop -> refineByResult (loop undefined) - .> either (showException .> show .> fail) TH.lift - .> fmap TH.TExp - + let showException = refineExceptionToTree + .> showTree True + .> fail + in refine @p @x + .> either showException TH.lift + .> fmap TH.TExp -- | Like 'refineTH', but immediately unrefines the value. -- This is useful when some value need only be refined -- at compile-time. @@ -458,15 +448,7 @@ -- such, the 'Maybe' here should be interpreted to mean -- the presence or absence of a 'RefineException', and -- nothing else. - -- - -- /Note/: An implementation of 'validate' should not - -- case on its first argument, @p@. This is due to an - -- implementation detail of the 'refine' function. See - -- - -- for more details. - -- - -- @since 0.1.0.0 - validate :: p -> x -> Maybe RefineException + validate :: Proxy p -> x -> Maybe RefineException -------------------------------------------------------------------------------- @@ -522,7 +504,7 @@ -- | @since 0.1.0.0 instance (Predicate p x, Typeable p) => Predicate (Not p) x where validate p x = do - maybe (Just (RefineNotException (typeOf p))) + maybe (Just (RefineNotException (typeRep p))) (const Nothing) (validate @p undefined x) @@ -556,7 +538,7 @@ validate p x = do let a = validate @l undefined x let b = validate @r undefined x - let throw err = Just (RefineAndException (typeOf p) err) + let throw err = Just (RefineAndException (typeRep p) err) case (a, b) of (Just e, Just e1) -> throw (These e e1) (Just e, _) -> throw (This e) @@ -597,7 +579,7 @@ let left = validate @l undefined x let right = validate @r undefined x case (left, right) of - (Just l, Just r) -> Just (RefineOrException (typeOf p) l r) + (Just l, Just r) -> Just (RefineOrException (typeRep p) l r) _ -> Nothing -------------------------------------------------------------------------------- @@ -634,8 +616,8 @@ let left = validate @l undefined x let right = validate @r undefined x case (left, right) of - (Nothing, Nothing) -> Just (RefineXorException (typeOf p) Nothing) - (Just l, Just r) -> Just (RefineXorException (typeOf p) (Just (l, r))) + (Nothing, Nothing) -> Just (RefineXorException (typeRep p) Nothing) + (Just l, Just r) -> Just (RefineXorException (typeRep p) (Just (l, r))) _ -> Nothing -------------------------------------------------------------------------------- @@ -781,7 +763,7 @@ if increasing x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Foldable is not in ascending order." -------------------------------------------------------------------------------- @@ -808,7 +790,7 @@ if decreasing x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Foldable is not in descending order." -------------------------------------------------------------------------------- @@ -832,12 +814,13 @@ -- | @since 0.1.0.0 instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x < x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value is not less than " <> PP.pretty (natVal p)) + (typeRep p) + ("Value is not less than " <> i2text n) -------------------------------------------------------------------------------- @@ -860,12 +843,13 @@ -- | @since 0.1.0.0 instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x > x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value is not greater than " <> PP.pretty (natVal p)) + (typeRep p) + ("Value is not greater than " <> i2text n) -------------------------------------------------------------------------------- @@ -891,12 +875,13 @@ -- | @since 0.1.2 instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x >= x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value is less than " <> PP.pretty (natVal p)) + (typeRep p) + ("Value is less than " <> i2text n) -------------------------------------------------------------------------------- @@ -919,12 +904,13 @@ -- | @since 0.1.2 instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x <= x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value is greater than " <> PP.pretty (natVal p)) + (typeRep p) + ("Value is greater than " <> i2text n) -------------------------------------------------------------------------------- @@ -953,18 +939,18 @@ instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx ) => Predicate (FromTo mn mx) x where validate p x = do - let mn' = natVal (Proxy @mn) - let mx' = natVal (Proxy @mx) + let mn' = nv @mn + let mx' = nv @mx if x >= fromIntegral mn' && x <= fromIntegral mx' then Nothing else let msg = [ "Value is out of range (minimum: " - , PP.pretty mn' + , i2text mn' , ", maximum: " - , PP.pretty mx' + , i2text mx' , ")" ] |> mconcat - in throwRefineOtherException (typeOf p) msg + in throwRefineOtherException (typeRep p) msg -------------------------------------------------------------------------------- @@ -987,12 +973,13 @@ -- | @since 0.1.0.0 instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x == x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value does not equal " <> PP.pretty (natVal p)) + (typeRep p) + ("Value does not equal " <> i2text n) -------------------------------------------------------------------------------- @@ -1015,12 +1002,13 @@ -- | @since 0.2.0.0 instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x /= x' then Nothing else throwRefineOtherException - (typeOf p) - ("Value does equal " <> PP.pretty (natVal p)) + (typeRep p) + ("Value does equal " <> i2text n) -------------------------------------------------------------------------------- @@ -1044,18 +1032,18 @@ -- | @since 0.4 instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where validate p x = do - let n' = natVal (Proxy @n) - let m' = natVal (Proxy @m) + let n' = nv @n + let m' = nv @m if x >= fromIntegral (negate n') && x <= fromIntegral m' then Nothing else let msg = [ "Value is out of range (minimum: " - , PP.pretty (negate n') + , i2text (negate n') , ", maximum: " - , PP.pretty m' + , i2text m' , ")" ] |> mconcat - in throwRefineOtherException (typeOf p) msg + in throwRefineOtherException (typeRep p) msg -------------------------------------------------------------------------------- @@ -1077,12 +1065,13 @@ -- | @since 0.4.2 instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where validate p x = do - let x' = fromIntegral (natVal p) + let n = nv @n + let x' = fromIntegral n if x `mod` x' == 0 then Nothing else throwRefineOtherException - (typeOf p) - ("Value is not divisible by " <> PP.pretty (natVal p)) + (typeRep p) + ("Value is not divisible by " <> i2text n) -------------------------------------------------------------------------------- @@ -1107,7 +1096,7 @@ if odd x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Value is not odd." -------------------------------------------------------------------------------- @@ -1133,7 +1122,7 @@ if isNaN x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Value is not IEEE \"not-a-number\" (NaN)." -------------------------------------------------------------------------------- @@ -1162,7 +1151,7 @@ if isInfinite x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Value is not IEEE infinity or negative infinity." -------------------------------------------------------------------------------- @@ -1188,7 +1177,7 @@ if even x then Nothing else throwRefineOtherException - (typeOf p) + (typeRep p) "Value is not even." -------------------------------------------------------------------------------- @@ -1325,8 +1314,8 @@ -- @since 0.4.2.2 strengthen :: forall p p' x. (Predicate p x, Predicate p' x) => Refined p x - -> Either RefineException (Refined (p && p') x) -strengthen r = refine @(p && p') (unrefine r) + -> Refined (p && p') x +strengthen = coerce {-# inlineable strengthen #-} -------------------------------------------------------------------------------- @@ -1379,15 +1368,6 @@ , _RefineException_children :: !(Maybe (RefineException, RefineException)) } - | -- | A 'RefineException' for failures involving all other predicates. - -- - -- @since 0.2.0.0 - RefineOtherException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the predicate that failed. - , _RefineException_message :: !(PP.Doc Void) - -- ^ A custom message to display. - } | -- | A 'RefineException' for failures involving all other predicates with custom exception. -- -- @since 0.5 @@ -1397,6 +1377,16 @@ , _RefineException_Exception :: !SomeException -- ^ A custom exception. } + + | -- | A 'RefineException' for failures involving all other predicates. + -- + -- @since 0.2.0.0 + RefineOtherException + { _RefineException_typeRep :: !TypeRep + -- ^ The 'TypeRep' of the predicate that failed. + , _RefineException_message :: !Text + -- ^ A custom message to display. + } deriving ( Generic -- ^ @since 0.3.0.0 ) @@ -1405,14 +1395,14 @@ -- -- @since 0.2.0.0 instance Show RefineException where - show = PP.pretty .> show + show = displayRefineException -- | A Tree which is a bit easier to pretty-print -- TODO: get rid of this data ExceptionTree a = NodeNone | NodeSome !TypeRep SomeException - | NodeOther !TypeRep !(PP.Doc Void) + | NodeOther !TypeRep !Text | NodeNot !TypeRep | NodeOr !TypeRep [ExceptionTree a] | NodeAnd !TypeRep [ExceptionTree a] @@ -1422,13 +1412,12 @@ -- work differently whether or not you are "inGhc", i.e. -- inside of refineTH/refineTH_ (because GHC messes with -- the indentation) -showTree :: Bool -> ExceptionTree RefineException -> PP.Doc ann +showTree :: Bool -> ExceptionTree RefineException -> String showTree inGhc | inGhc = showOne "" "" "" .> mapOnTail (indent 6) .> unlines - .> PP.pretty - | otherwise = showOne " " "" "" .> unlines .> PP.pretty + | otherwise = showOne " " "" "" .> unlines where mapOnTail :: (a -> a) -> [a] -> [a] mapOnTail f = \case @@ -1459,7 +1448,7 @@ <> "The predicate (" <> show tr <> ") failed with the message: " - <> show p + <> Text.unpack p ] NodeNot tr -> [ leader @@ -1511,7 +1500,7 @@ RefineXorException tr Nothing -> NodeXor tr [] RefineXorException tr (Just (l, r)) -> NodeXor tr [go l, go r] --- | Display a 'RefineException' as a @'PP.Doc' ann@ +-- | Display a 'RefineException' as @'String'@ -- -- This function can be extremely useful for debugging -- @'RefineException's@, especially deeply nested ones. @@ -1549,17 +1538,9 @@ -- /Note/: Equivalent to @'show' \@'RefineException'@ -- -- @since 0.2.0.0 -displayRefineException :: RefineException -> PP.Doc ann +displayRefineException :: RefineException -> String displayRefineException = refineExceptionToTree .> showTree False --- | Pretty-print a 'RefineException'. --- --- /Note/: Equivalent to 'displayRefineException'. --- --- @since 0.2.0.0 -instance PP.Pretty RefineException where - pretty = displayRefineException - -- | Encode a 'RefineException' for use with \Control.Exception\. -- -- /Note/: Equivalent to @'displayRefineException'@. @@ -1575,11 +1556,15 @@ -- 'throwRefineOtherException' is useful for defining what -- behaviour 'validate' should have in the event of a predicate failure. -- +-- Typically the first argument passed to this function +-- will be the result of applying 'typeRep' to the first +-- argument of 'validate'. +-- -- @since 0.2.0.0 throwRefineOtherException :: TypeRep - -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'. - -> PP.Doc Void + -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'. + -> Text -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed. -> Maybe RefineException throwRefineOtherException rep @@ -1594,7 +1579,7 @@ -- @since 0.5 throwRefineSomeException :: TypeRep - -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'. + -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'. -> SomeException -- ^ A custom exception. -> Maybe RefineException @@ -1624,27 +1609,42 @@ -------------------------------------------------------------------------------- -- | Helper function for sized predicates. -sized :: (Typeable (p n), KnownNat n) - => p n +sized :: forall p n a. (Typeable (p n), KnownNat n) + => Proxy (p n) -- ^ predicate - -> (a, PP.Doc Void) + -> (a, Text) -- ^ (value, type) -> (a -> Int) -- ^ length of value - -> (Int -> Int -> Bool, PP.Doc Void) + -> (Int -> Int -> Bool, Text) -- ^ (compare :: Length -> KnownNat -> Bool, comparison string) -> Maybe RefineException sized p (x, typ) lenF (cmp, cmpDesc) = do - let x' = fromIntegral (natVal p) + let x' = fromIntegral (nv @n) let sz = lenF x if cmp sz x' then Nothing else let msg = - [ "Size of ", typ, " is not ", cmpDesc - , PP.pretty x' - , "\n " + [ "Size of ", typ, " is not ", cmpDesc, " " + , i2text x' + , ". " , "Size is: " - , PP.pretty sz + , i2text sz ] |> mconcat - in throwRefineOtherException (typeOf p) msg + in throwRefineOtherException (typeRep p) msg + +-- helper function to make sure natVal calls are +-- zero runtime overhead +nv :: forall n. KnownNat n => Integer +nv = natVal' (proxy# :: Proxy# n) + +-- convert an Integral number to Text +-- +-- todo: use toLazyTextWith, providing a tiny buffer size +i2text :: Integral a => a -> Text +i2text = TextBuilder.decimal + .> TextBuilder.toLazyText + .> TextLazy.toStrict +{-# SPECIALISE i2text :: Int -> Text #-} +{-# SPECIALISE i2text :: Integer -> Text #-} diff --git a/src/Refined/These.hs b/src/Refined/These.hs deleted file mode 100644 --- a/src/Refined/These.hs +++ /dev/null @@ -1,46 +0,0 @@ --------------------------------------------------------------------------------- - --- Copyright © 2015 Nikita Volkov --- Copyright © 2018 Remy Goldschmidt --- Copyright © 2020 chessai --- --- Permission is hereby granted, free of charge, to any person --- obtaining a copy of this software and associated documentation --- files (the "Software"), to deal in the Software without --- restriction, including without limitation the rights to use, --- copy, modify, merge, publish, distribute, sublicense, and/or sell --- copies of the Software, and to permit persons to whom the --- Software is furnished to do so, subject to the following --- conditions: --- --- The above copyright notice and this permission notice shall be --- included in all copies or substantial portions of the Software. --- --- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, --- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES --- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND --- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT --- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, --- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING --- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR --- OTHER DEALINGS IN THE SOFTWARE. - --------------------------------------------------------------------------------- - -{-# LANGUAGE PackageImports #-} - --------------------------------------------------------------------------------- - -{-# OPTIONS_GHC -Wall #-} - --------------------------------------------------------------------------------- - --- | This module is deprecated. It will be removed in a future --- release. Use the 'Data.These' module from the these-skinny --- package instead. -module Refined.These - {-# DEPRECATED "This module will be removed in the next majour release. Use Data.These from the these-skinny package instead." #-} - ( module Data.These - ) where - -import "these-skinny" Data.These diff --git a/test/Compiles.hs b/test/Compiles.hs --- a/test/Compiles.hs +++ b/test/Compiles.hs @@ -17,6 +17,19 @@ even_ = $$(refineTH_ @(Not Even) @Int 3) odd_ = $$(refineTH_ @Odd @Int 3) +--fails = +-- $$(refineTH +-- @( And +-- NonEmpty +-- ( Empty +-- ) +-- ) +-- @[Int] +-- +-- [1,2,3] +-- ) + + --foo = $$(refineTH -- @( And -- Even diff --git a/test/Doctests.hs b/test/Doctests.hs --- a/test/Doctests.hs +++ b/test/Doctests.hs @@ -8,7 +8,6 @@ srcFiles :: [String] srcFiles = [ "src/Refined.hs" - , "src/Refined/These.hs" , "src/Refined/Unsafe/Type.hs" , "src/Refined/Unsafe.hs" ]