diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,10 @@ +## 0.2.0 (2022-05-31) +Initial Hackage release (dependency issues prevented uploading). + + * fix field indexing in generic errors + * add unsafe strengthening + * add property and error tests + ## 0.1.0 (2022-05-16) Initial release. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,24 +1,97 @@ +[lib-refined-hackage]: https://hackage.haskell.org/package/refined + # strongweak -Definitions for transforming between types. +Convert between pairs of "weak" and "strong"/"validated" types, with good +errors and generic derivers. - * `strong -> weak` drops invariants (e.g. going from a bounded to an unbounded - numeric type) - * `weak -> Maybe strong` introduces invariants +## Definition of strong and weak types +Take a pair of types `(strong, weak)`. We state the following: -This is not a `Convertible` library that enumerates transformations between -types into a dictionary. + * You may safely convert ("weaken") any `strong` value to a `weak` value. + * You can try to convert ("strengthen") any `weak` value to a `strong` value, + but it may fail. - * A "strong" type has exactly one "weak" representation. - * Weakening a type is safe. - * Strengthening a type may fail. +As a rule, a weak type should be *easier to use* than its related strong type. +That is, it should have fewer invariants to consider or maintain. You could +weaken an `a` to a `Maybe a`, but since a `Maybe a` is harder to use, it's not a +candidate for this library. +As an arbitrary limitation for ease of use, a strong type has only one +associated weak type. The same weak type may be used for multiple strong types. + +### Examples +The [refined][lib-refined-hackage] library defines a `newtype Refined p a = +Refined a`. To get a `Refined`, you must test its associated predicate. You may +recover the unrefined value by removing the newtype wrapper. Thus, you may +strengthen `a`s into `Refined p a`s, and weaken vice versa. + +The `WordX` family are like bounded `Natural`s. We can consider `Natural` as a +weak type, which can be strengthened into e.g. `Word8` by asserting +well-boundedness. + +## Cool points +### Validates as much as possible +This is primarily a validation library. Thus, we don't fail on the first error +-- we attempt to validate every part of a data type, and collate the errors into +a big list. (`ApplicativeDo` plus `Validation` is magical.) + +### One definition, strong + weak views +Using a type-level `Strength` switch and the `SW` type family, you can write a +single datatype definition and receive both a strong and a weak representation, +which the generic derivers can work with. See the `Strongweak.SW` module for +details. + +### Generic strengthening is extremely powerful There are generic derivers for generating `Strengthen` and `Weaken` instances -for arbitrary data types. The `Strengthen` instances annotate errors +between arbitrary data types. The `Strengthen` instances annotate errors extensively, telling you the datatype & record for which strengthening failed - -recursively, for nested types. +recursively, for nested types! -This is a validation library. We don't fail on the first error -- we attempt to -validate every part of a data type, and collate the errors into a list. This -happens magically in the generic deriver, but if you're writing your own -instances, you may want `ApplicativeDo` so you can use do notation. So it'll -monadic, but actually everything will get checked. +Note that the generic derivers work with any pair of matching data types. But +they must match very closely: both types are traversed in tandem, so every pair +of fields must be compatible. If you need to do calculation to move between your +strong and weak types, consider splitting it into calculation -> strengthening +and using the generic derivers. Or write your own instances. + +### Backdoors included +Sometimes you have can guarantee that a weak value can be safely strengthened, +but the compiler doesn't know - a common problem in parsing. In such cases, you +may use efficient unsafe strengthenings, which don't perform invariant checks. + +## What this library isn't +### Not a convertible +This is not a `Convertible` library that enumerates transformations between +types into a dictionary. A strong type has exactly one weak representation, and +strengthening may fail while weakening cannot. For safe conversion enumeration +via typeclasses, consider Taylor Fausak's +[witch](https://hackage.haskell.org/package/witch) library. + +### Not particularly speedy +The emphasis is on safety, possibly at the detriment of performance. However, my +expectation is that you only strengthen & weaken at the "edges" of your program, +and most of the time will be spent transforming weak representations. This may +improve performance if it means invariants don't have to be continually asserted +inline, but it also may slow things down e.g. `Natural`s are slower than +`Word`s. + +## Generic derivation algorithm +As far as I understand, `Strengthen` and `Weaken` generic derivations are safe, +in that they will either fail with a type error, or give you a correct instance. +Both work in a similar manner: + + * Both datatypes are traversed in tandem. + * When both datatypes are at a field: + * If both types are identical, the value is rewrapped with no changes. + * Else, if the input type can be transformed into the output type, it is. + (Strengthening will wrap any errors at this stage with metadata collected + from the datatype's generic representation. + * Else, the pair of fields are not compatible, and the derivation fails. + +Note this may fail for types with a manually-derived `Generic` instance: + + * The types' SOP tree structures must match. + * I don't think GHC itself guarantees this, so if you receive surprising + derivation errors, the types might have differing generic representation + structure (even if the "flat" representation may be identical). + * Strengthening requires that metadata is present for all parts of the + representation (datatype, constructor, selector). diff --git a/src/Strongweak.hs b/src/Strongweak.hs --- a/src/Strongweak.hs +++ b/src/Strongweak.hs @@ -1,9 +1,25 @@ module Strongweak ( module Strongweak.Weaken - , module Strongweak.Strengthen + , module Strongweak.Strengthen, restrengthen , module Strongweak.SW ) where import Strongweak.Weaken import Strongweak.Strengthen import Strongweak.SW + +import Data.Either.Validation +import Data.List.NonEmpty + +-- | Weaken and re-strengthen a strong value. +-- +-- In correct operation, @restrengthen === Right@. If your value was +-- strengthened incorrectly, or perhaps you cheated via @UnsafeStrengthen@, this +-- may not be the case. For example: +-- +-- >>> restrengthen $ unsafeStrengthen' @(Vector 2 Natural) [0] +-- Failure ... +restrengthen + :: forall w s. (Weaken s w, Strengthen w s) + => s -> Validation (NonEmpty StrengthenError) s +restrengthen = strengthen . weaken diff --git a/src/Strongweak/Generic/Strengthen.hs b/src/Strongweak/Generic/Strengthen.hs --- a/src/Strongweak/Generic/Strengthen.hs +++ b/src/Strongweak/Generic/Strengthen.hs @@ -1,22 +1,24 @@ -{- | -The generic derivation is split into 3 classes, dealing with different layers of -a Haskell data type: datatype, constructor and selector. At each point, we -gather up information about the type and push on. Strengthening occurs at -selectors. If a strengthening fails, the gathered information is pushed into an -error that wraps the original error. +{- | Strengthening for generic data types. + +The generic derivation is split into 3 classes, each dealing with a different +layer of a generic Haskell data type: datatype (D), constructor (C) and selector +(S). At each point, we gather up information about the type and push on. +Strengthening occurs at selectors. If a strengthening fails, the gathered +information is pushed into an error that wraps the original error. -} {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ApplicativeDo #-} module Strongweak.Generic.Strengthen where import Strongweak.Strengthen -import Data.Validation +import Data.Either.Validation import Data.List.NonEmpty - import GHC.Generics +import Numeric.Natural +import Control.Applicative ( liftA2 ) + strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s @@ -36,7 +38,7 @@ gstrengthenC _ _ = Success instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where - gstrengthenC dw ds = fmap M1 . gstrengthenS dw ds (conName' @cw) (conName' @cs) . unM1 + gstrengthenC dw ds = fmap M1 . snd . gstrengthenS dw ds (conName' @cw) (conName' @cs) 0 . unM1 -- | Strengthen sum types by strengthening left or right. instance (GStrengthenC lw ls, GStrengthenC rw rs) => GStrengthenC (lw :+: rw) (ls :+: rs) where @@ -44,29 +46,49 @@ R1 r -> R1 <$> gstrengthenC dw ds r class GStrengthenS w s where - gstrengthenS :: String -> String -> String -> String -> w p -> Validation (NonEmpty StrengthenError) (s p) + gstrengthenS :: String -> String -> String -> String -> Natural -> w p -> (Natural, Validation (NonEmpty StrengthenError) (s p)) -- | Nothing to do for empty constructors. instance GStrengthenS U1 U1 where - gstrengthenS _ _ _ _ = Success + gstrengthenS _ _ _ _ n x = (n, Success x) -- | Special case: if source and target types are equal, copy the value through. instance GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 w)) where - gstrengthenS _ _ _ _ = Success . M1 . unM1 + gstrengthenS _ _ _ _ n x = (n, Success (M1 (unM1 x))) -- | Strengthen a field using the existing 'Strengthen' instance. +-- +-- On strengthen failure, the errors are annotated with all the datatype +-- information we've hoarded. The upshot is that if you strengthen a type with +-- lots of types inside it, all with generically-derived 'Strengthen' instances, +-- you'll get a precise zoom-in of exactly where each error occurred. instance {-# OVERLAPS #-} (Strengthen w s, Selector mw, Selector ms) => GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 s)) where - gstrengthenS dw ds cw cs (M1 (K1 w)) = + gstrengthenS dw ds cw cs n (M1 (K1 w)) = case strengthen w of - Failure (e :| es) -> Failure $ StrengthenErrorField dw ds cw cs (selName' @mw) (selName' @ms) e :| es - Success s -> Success $ M1 $ K1 s + Failure es -> + let fw = selName'' @mw + fs = selName'' @ms + e = StrengthenErrorField dw ds cw cs n fw n fs es + in (n, Failure $ e :| []) + Success s -> (n, Success $ M1 $ K1 s) --- | Strengthen product types by strengthening left, then right. +-- | Get the record name for a selector if present. +-- +-- On the type level, a 'Maybe Symbol' is stored for record names. But the +-- reification is done using @fromMaybe ""@. So we have to inspect the resulting +-- string to determine whether the field uses record syntax or not. (Silly.) +selName'' :: forall s. Selector s => Maybe String +selName'' = case selName' @s of "" -> Nothing + s -> Just s + +-- | Strengthen product types by strengthening left and right. +-- +-- This is ordered (left then right), but only to pass the index along. instance (GStrengthenS lw ls, GStrengthenS rw rs) => GStrengthenS (lw :*: rw) (ls :*: rs) where - gstrengthenS dw ds cw cs (l :*: r) = do - l' <- gstrengthenS dw ds cw cs l - r' <- gstrengthenS dw ds cw cs r - return $ l' :*: r' + gstrengthenS dw ds cw cs n (l :*: r) = (n'', liftA2 (:*:) l' r') + where + (n', l') = gstrengthenS dw ds cw cs n l + (n'', r') = gstrengthenS dw ds cw cs (n'+1) r -------------------------------------------------------------------------------- @@ -80,7 +102,7 @@ datatypeName' :: forall d. Datatype d => String datatypeName' = datatypeName @d undefined --- | 'datatypeName' without the value (only used as a proxy). Lets us push our +-- | 'selName' without the value (only used as a proxy). Lets us push our -- 'undefined's into one place. selName' :: forall s. Selector s => String selName' = selName @s undefined diff --git a/src/Strongweak/Generic/Weaken.hs b/src/Strongweak/Generic/Weaken.hs --- a/src/Strongweak/Generic/Weaken.hs +++ b/src/Strongweak/Generic/Weaken.hs @@ -1,3 +1,5 @@ +-- | Weakening for generic data types. + module Strongweak.Generic.Weaken where import Strongweak.Weaken diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE CPP #-} module Strongweak.Strengthen where @@ -14,7 +15,7 @@ import Prettyprinter import Prettyprinter.Render.String -import Data.Validation +import Data.Either.Validation import Data.List.NonEmpty ( NonEmpty( (:|) ) ) import Data.Foldable qualified as Foldable @@ -28,37 +29,61 @@ -} class Strengthen w s | s -> w where strengthen :: w -> Validation (NonEmpty StrengthenError) s +-- | 'strengthen' with reordered type variables for more convenient visible type +-- application. +strengthen' :: forall s w. Strengthen w s => w -> Validation (NonEmpty StrengthenError) s +strengthen' = strengthen + +-- | Strengthen error data type. Don't use these constructors directly, use +-- the existing helper functions. +-- +-- Field indices are from 0 in the respective constructor. Field names are +-- provided if present. data StrengthenError - = StrengthenErrorBase String String String String - -- ^ weak type, strong type, weak value, msg - | StrengthenErrorField String String String String String String StrengthenError - -- ^ weak datatype name, strong datatype name, - -- weak constructor name, strong constructor name, - -- weak field name, strong field name, - -- error + = StrengthenErrorBase + String -- ^ weak type + String -- ^ strong type + String -- ^ weak value + String -- ^ msg + | StrengthenErrorField + String -- ^ weak datatype name + String -- ^ strong datatype name + String -- ^ weak constructor name + String -- ^ strong constructor name + Natural -- ^ weak field index + (Maybe String) -- ^ weak field name (if present) + Natural -- ^ strong field index + (Maybe String) -- ^ strong field name (if present) + (NonEmpty StrengthenError) -- ^ errors + deriving stock Eq + instance Show StrengthenError where showsPrec _ = renderShowS . layoutPretty defaultLayoutOptions . pretty +-- TODO shorten value if over e.g. 50 chars. e.g. @[0,1,2,...,255] -> FAIL@ instance Pretty StrengthenError where pretty = \case StrengthenErrorBase wt st wv msg -> vsep [ pretty wt<+>"->"<+>pretty st , pretty wv<+>"->"<+>"FAIL" , pretty msg ] - StrengthenErrorField dw _ds cw _cs sw _ss err -> - nest 1 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>pretty err + StrengthenErrorField dw _ds cw _cs iw fw _is _fs es -> + let sw = maybe (show iw) id fw + in nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>strengthenErrorPretty es +-- mutually recursive with its 'Pretty' instance. safe, but a bit confusing - +-- clean up +strengthenErrorPretty :: NonEmpty StrengthenError -> Doc a +strengthenErrorPretty = vsep . map go . Foldable.toList + where go e = "-"<+>indent 0 (pretty e) + strengthenErrorBase :: forall s w. (Typeable w, Show w, Typeable s) => w -> String -> Validation (NonEmpty StrengthenError) s strengthenErrorBase w msg = Failure (e :| []) where e = StrengthenErrorBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg -strengthenErrorPretty :: NonEmpty StrengthenError -> Doc a -strengthenErrorPretty = vsep . map go . Foldable.toList - where go e = "-"<+>indent 0 (pretty e) - -- | Strengthen each element of a list. instance Strengthen w s => Strengthen [w] [s] where strengthen = traverse strengthen @@ -71,7 +96,11 @@ Just s -> Success s -- | Obtain a refined type by applying its associated refinement. -instance (Predicate p a, Typeable a, Show a) => Strengthen a (Refined p a) where +#ifdef REFINED_POLYKIND +instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen a (Refined p a) where +#else +instance (Predicate p a, Typeable p, Typeable a, Show a) => Strengthen a (Refined p a) where +#endif strengthen a = case refine a of Left err -> strengthenErrorBase a (show err) diff --git a/src/Strongweak/Strengthen/Unsafe.hs b/src/Strongweak/Strengthen/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Strongweak/Strengthen/Unsafe.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE FunctionalDependencies #-} + +module Strongweak.Strengthen.Unsafe where + +import Numeric.Natural +import Data.Word +import Data.Int +import Refined ( Refined ) +import Refined.Unsafe ( reallyUnsafeRefine ) +import Data.Vector.Sized ( Vector ) +import Data.Vector.Generic.Sized.Internal qualified +import Data.Vector qualified + +{- | Any 'w' can be unsafely "strengthened" into an 's' by pretending that we've + asserted some properties. + +For example, you may unsafely strengthen some 'Natural' @n@ into a 'Word8' by +unsafely coercing the value, ignoring the possibility that @n >= 255@. + +Currently, this class is more of a thought experiment than something to use. +That is to say, do not use this. + +This typeclass should probably follow its big sis 'Strengthen'. Only provide +'UnsafeStrengthen' instances for types that have similar 'Strengthen' instances. +-} +class UnsafeStrengthen w s | s -> w where unsafeStrengthen :: w -> s + +-- | 'unsafeStrengthen' with reordered type variables for more convenient +-- visible type application. +unsafeStrengthen' :: forall s w. UnsafeStrengthen w s => w -> s +unsafeStrengthen' = unsafeStrengthen + +-- | Unsafely strengthen each element of a list. +instance UnsafeStrengthen w s => UnsafeStrengthen [w] [s] where + unsafeStrengthen = map unsafeStrengthen + +-- | Obtain a sized vector by unsafely assuming the size of a plain list. +-- Extremely unsafe. +instance UnsafeStrengthen [a] (Vector n a) where + unsafeStrengthen = Data.Vector.Generic.Sized.Internal.Vector . Data.Vector.fromList + +-- | Obtain a refined type by ignoring the predicate. +instance UnsafeStrengthen a (Refined p a) where + unsafeStrengthen = reallyUnsafeRefine + +-- Coerce 'Natural's into Haskell's bounded unsigned numeric types. Poorly-sized +-- values will safely overflow according to the type's behaviour. +instance UnsafeStrengthen Natural Word8 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Natural Word16 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Natural Word32 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Natural Word64 where unsafeStrengthen = fromIntegral + +-- Coerce 'Integer's into Haskell's bounded signed numeric types. Poorly-sized +-- values will safely overflow according to the type's behaviour. +instance UnsafeStrengthen Integer Int8 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Integer Int16 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Integer Int32 where unsafeStrengthen = fromIntegral +instance UnsafeStrengthen Integer Int64 where unsafeStrengthen = fromIntegral diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs --- a/src/Strongweak/Weaken.hs +++ b/src/Strongweak/Weaken.hs @@ -18,7 +18,7 @@ -} class Weaken s w | s -> w where weaken :: s -> w --- | Weaken each element of a list. +-- | Weaken each element of a list instance Weaken s w => Weaken [s] [w] where weaken = map weaken -- | Weaken sized vectors into plain lists. diff --git a/strongweak.cabal b/strongweak.cabal --- a/strongweak.cabal +++ b/strongweak.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: strongweak -version: 0.1.0 +version: 0.2.0 synopsis: Convert between strong and weak representations of types description: Please see README.md. category: Data @@ -26,6 +26,11 @@ type: git location: https://github.com/raehik/strongweak +flag refined-polykind + description: assume predicate p in Refined p a is polykinded + manual: True + default: False + library exposed-modules: Strongweak @@ -34,6 +39,7 @@ Strongweak.Generic.Strengthen Strongweak.Generic.Weaken Strongweak.Strengthen + Strongweak.Strengthen.Unsafe Strongweak.SW Strongweak.Weaken other-modules: @@ -75,8 +81,71 @@ ghc-options: -Wall build-depends: base >=4.14 && <5 + , either >=5.0.1.1 && <5.1 , prettyprinter >=1.7.1 && <1.8 , refined >=0.6.3 && <0.7 - , validation >=1.1.2 && <1.2 + , vector >=0.12.3.1 && <0.13 , vector-sized >=1.5.0 && <1.6 + if flag(refined-polykind) + cpp-options: -DREFINED_POLYKIND + default-language: Haskell2010 + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Common + Strongweak.LawsSpec + Strongweak.StrengthenSpec + Paths_strongweak + hs-source-dirs: + test + default-extensions: + EmptyCase + FlexibleContexts + FlexibleInstances + InstanceSigs + MultiParamTypeClasses + PolyKinds + LambdaCase + DerivingStrategies + StandaloneDeriving + DeriveAnyClass + DeriveGeneric + DeriveDataTypeable + DeriveFunctor + DeriveFoldable + DeriveTraversable + DeriveLift + ImportQualifiedPost + StandaloneKindSignatures + DerivingVia + RoleAnnotations + TypeApplications + DataKinds + TypeFamilies + TypeOperators + BangPatterns + GADTs + DefaultSignatures + RankNTypes + UndecidableInstances + MagicHash + ScopedTypeVariables + build-tool-depends: + hspec-discover:hspec-discover >=2.7 && <2.10 + build-depends: + QuickCheck >=2.14.2 && <2.15 + , base >=4.14 && <5 + , either >=5.0.1.1 && <5.1 + , generic-random >=1.5.0.1 && <1.6 + , hspec >=2.7 && <2.10 + , prettyprinter >=1.7.1 && <1.8 + , quickcheck-instances >=0.3.26 && <0.4 + , refined >=0.6.3 && <0.7 + , strongweak + , vector >=0.12.3.1 && <0.13 + , vector-sized >=1.5.0 && <1.6 + if flag(refined-polykind) + cpp-options: -DREFINED_POLYKIND default-language: Haskell2010 diff --git a/test/Common.hs b/test/Common.hs new file mode 100644 --- /dev/null +++ b/test/Common.hs @@ -0,0 +1,46 @@ +module Common where + +import Strongweak +import Strongweak.Generic +import Refined hiding ( Weaken, weaken, strengthen, NonEmpty ) +import GHC.Generics ( Generic ) +import Generic.Random +import Test.QuickCheck ( Arbitrary ) +import Numeric.Natural ( Natural ) +import Data.Word +import Test.QuickCheck.Instances.Natural() + +data DS (s :: Strength) + = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8) + | DS1 (SW s (Refined (LessThan 100) Natural)) + deriving stock (Generic) + +deriving stock instance Eq (DS 'Strong) +deriving stock instance Show (DS 'Strong) +deriving via (GenericArbitraryU `AndShrinking` (DS 'Strong)) instance Arbitrary (DS 'Strong) + +deriving stock instance Eq (DS 'Weak) +deriving stock instance Show (DS 'Weak) +deriving via (GenericArbitraryU `AndShrinking` (DS 'Weak)) instance Arbitrary (DS 'Weak) + +instance Weaken (DS 'Strong) (DS 'Weak) where weaken = weakenGeneric +instance Strengthen (DS 'Weak) (DS 'Strong) where strengthen = strengthenGeneric + +data DP (s :: Strength) = DP + { dp1f0 :: SW s Word32 + , dp1f1 :: SW s (Refined (GreaterThan 42) Natural) + , dp1f2 :: SW s Word8 + , dp1f3 :: Word8 + , dp1f4 :: SW s Word8 + } deriving stock (Generic) + +deriving stock instance Eq (DP 'Strong) +deriving stock instance Show (DP 'Strong) +deriving via (GenericArbitraryU `AndShrinking` (DP 'Strong)) instance Arbitrary (DP 'Strong) + +deriving stock instance Eq (DP 'Weak) +deriving stock instance Show (DP 'Weak) +deriving via (GenericArbitraryU `AndShrinking` (DP 'Weak)) instance Arbitrary (DP 'Weak) + +instance Weaken (DP 'Strong) (DP 'Weak) where weaken = weakenGeneric +instance Strengthen (DP 'Weak) (DP 'Strong) where strengthen = strengthenGeneric diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-} diff --git a/test/Strongweak/LawsSpec.hs b/test/Strongweak/LawsSpec.hs new file mode 100644 --- /dev/null +++ b/test/Strongweak/LawsSpec.hs @@ -0,0 +1,18 @@ +module Strongweak.LawsSpec ( spec ) where + +import Strongweak +import Common +import Data.Either.Validation +import Test.Hspec +import Test.Hspec.QuickCheck + +spec :: Spec +spec = modifyMaxSize (+1000) $ do + prop "weaken-strengthen roundtrip isomorphism (generic)" $ do + \(d :: DS 'Strong) -> strengthen @(DS 'Weak) (weaken d) `shouldBe` Success d + prop "strengthen-weaken-strengthen roundtrip partial isomorphism (generic)" $ do + \(dw :: DS 'Weak) -> + case strengthen dw of + Failure _ -> pure () + Success (ds :: DS 'Strong) -> + strengthen @(DS 'Weak) (weaken ds) `shouldBe` Success ds diff --git a/test/Strongweak/StrengthenSpec.hs b/test/Strongweak/StrengthenSpec.hs new file mode 100644 --- /dev/null +++ b/test/Strongweak/StrengthenSpec.hs @@ -0,0 +1,63 @@ +module Strongweak.StrengthenSpec ( spec ) where + +import Strongweak +import Common +import Data.Either.Validation +import Test.Hspec + +import Numeric.Natural ( Natural ) +import Data.Word +import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.Foldable qualified as Foldable + +spec :: Spec +spec = do + it "returns a precise error for failed generic strengthening (named field)" $ do + let w = fromIntegral (maxBound @Word32) + 1 + d = DP w 43 1 2 3 :: DP 'Weak + e = seGeneric1 + "DP" "DP" "DP" "DP" 0 (Just "dp1f0") 0 (Just "dp1f0") + "Natural" "Word32" w + strengthen @_ @(DP 'Strong) d `shouldSatisfy` svEqError e + it "returns a precise error for failed generic strengthening (unnamed field)" $ do + let w = fromIntegral (maxBound @Word8) + 1 + d = DS0 0 1 2 3 w :: DS 'Weak + e = seGeneric1 + "DS" "DS" "DS0" "DS0" 4 Nothing 4 Nothing + "Natural" "Word8" w + strengthen @_ @(DS 'Strong) d `shouldSatisfy` svEqError e + +seGeneric1 + :: Show w + => String -> String -> String -> String + -> Natural -> Maybe String -> Natural -> Maybe String + -> String -> String -> w + -> StrengthenError +seGeneric1 dw ds cw cs iw fw is fs tw ts w = + StrengthenErrorField dw ds cw cs iw fw is fs (e :| []) + where e = StrengthenErrorBase tw ts (show w) (error "TODO ignoring msg") + +seEqIgnoreMsg :: StrengthenError -> StrengthenError -> Bool +seEqIgnoreMsg s1 s2 = case s1 of + StrengthenErrorField dw ds cw cs iw fw is fs es -> case s2 of + StrengthenErrorField dw' ds' cw' cs' iw' fw' is' fs' es' -> + dw == dw' + && ds == ds' + && cw == cw' + && cs == cs' + && iw == iw' + && fw == fw' + && is == is' + && fs == fs' + && and (zipWith seEqIgnoreMsg (Foldable.toList es) (Foldable.toList es')) + _ -> False + StrengthenErrorBase wt st wv _ -> case s2 of + StrengthenErrorBase wt' st' wv' _ -> + wt == wt' + && st == st' + && wv == wv' + _ -> False + +svEqError :: StrengthenError -> Validation (NonEmpty StrengthenError) s -> Bool +svEqError e = \case Failure (e' :| []) -> seEqIgnoreMsg e e' + _ -> False