diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,15 @@ +# 0.4.0.0 + +- Revised the `Show` instance of `ID` to produce a valid Haskell expression + when applied to nested values of `ID`. +- Revised the `ID.fromSymbol` function so that users are presented with a + helpful error if they forget to apply the function to a concrete type. +- Simplified the error handling for `ID.fromText` by merging the `TextTooShort` + and `TextTooLong` errors into a unified `InvalidLength` error. +- Renamed `ID.checksumDigit` to `ID.checksum`. +- Made `ID` an instance of the `Finitary` type class. +- Made `ID` an instance of the `Generic` type class. + # 0.3.0.0 - Added support for ARC (Alien Residence Certificate) numbers. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright Jonathan Knowles (c) 2018–2025 +Copyright Jonathan Knowles (c) 2018–2026 All rights reserved. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,5 +1,11 @@ # `roc-id` - + +[![Latest Release]( + https://img.shields.io/hackage/v/roc-id?label=Latest%20Release&color=227755 +)](https://hackage.haskell.org/package/roc-id) +[![Development Branch]( + https://img.shields.io/badge/Development%20Branch-API%20Documentation-225577 +)](https://jonathanknowles.github.io/roc-id/) This package provides a [Haskell](https://www.haskell.org/) implementation of the ROC (Taiwan) Uniform Identification Number (中華民國統一證號) format. diff --git a/components/roc-id-test/Spec.hs b/components/roc-id-test/Spec.hs --- a/components/roc-id-test/Spec.hs +++ b/components/roc-id-test/Spec.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -17,6 +18,10 @@ ( NonEmpty ((:|)) ) import Data.Text ( Text ) +import Lens.Micro + ( Lens', lens, set ) +import Lens.Micro.Extras + ( view ) import ROC.ID ( ID (..) ) import ROC.ID.CharIndex @@ -36,10 +41,11 @@ import ROC.ID.Nationality ( Nationality (..) ) import Test.Hspec - ( describe, hspec, it, shouldBe, shouldSatisfy ) + ( Spec, describe, hspec, it, shouldBe, shouldSatisfy ) import Test.QuickCheck ( Arbitrary (..) , NonEmptyList (..) + , Property , arbitraryBoundedEnum , choose , elements @@ -47,12 +53,14 @@ , property , shrinkBoundedEnum , shrinkMap + , (===) ) import Test.QuickCheck.Classes ( boundedEnumLaws, eqLaws, numLaws, ordLaws, showLaws, showReadLaws ) import Test.QuickCheck.Classes.Hspec ( testLawsMany ) +import qualified Data.Finitary as Finitary import qualified Data.Set.NonEmpty as NESet import qualified Data.Text as T import qualified ROC.ID as ID @@ -130,6 +138,48 @@ , showReadLaws ] + describe "Finitary instances" $ do + + describe "ID" $ do + + let start = Finitary.start @ID + end = Finitary.end @ID + previous = Finitary.previous @ID + next = Finitary.next @ID + + it "previous start" $ + previous start + `shouldBe` Nothing + + it "start" $ + start + `shouldBe` ID.fromSymbol @"A100000001" + + it "next start" $ + next start + `shouldBe` Just (ID.fromSymbol @"A100000010") + + it "previous end" $ + previous end + `shouldBe` Just (ID.fromSymbol @"Z999999987") + + it "end" $ + end + `shouldBe` ID.fromSymbol @"Z999999996" + + it "next end" $ + next end + `shouldBe` Nothing + + describe "ID attribute getters and setters" $ do + + describe "Gender" $ + checkLensLaws gender + describe "Location" $ + checkLensLaws location + describe "Nationality" $ + checkLensLaws nationality + describe "ID.fromText" $ do it "successfully parses known-valid identification numbers" $ @@ -144,12 +194,12 @@ property $ \(i :: ID) n -> do let newLength = n `mod` 10 let invalidID = T.take newLength $ ID.toText i - ID.fromText invalidID `shouldBe` Left ID.TextTooShort + ID.fromText invalidID `shouldBe` Left ID.InvalidLength it "does not parse identification numbers that are too long" $ property $ \(i :: ID) (NonEmpty s) -> do let invalidID = ID.toText i <> T.pack s - ID.fromText invalidID `shouldBe` Left ID.TextTooLong + ID.fromText invalidID `shouldBe` Left ID.InvalidLength it "does not parse identification numbers with invalid location codes" $ property $ \(i :: ID) (c :: Int) -> do @@ -170,7 +220,7 @@ it "does not parse identification numbers with invalid checksums" $ property $ \(i :: ID) (c :: Int) -> do let invalidChecksumDigit = intToDigit $ - ((c `mod` 9) + fromEnum (ID.checksumDigit i) + 1) `mod` 10 + ((c `mod` 9) + fromEnum (ID.checksum i) + 1) `mod` 10 let invalidID = T.take 9 (ID.toText i) <> T.pack [invalidChecksumDigit] ID.fromText invalidID `shouldBe` Left ID.InvalidChecksum @@ -193,7 +243,48 @@ replaceCharAt invalidCharIndex 'x' (ID.toText i) <> T.pack trailingExcess - ID.fromText textInvalid `shouldBe` Left ID.TextTooLong + ID.fromText textInvalid `shouldBe` Left ID.InvalidLength + +checkLensLaws + :: forall i v. (Arbitrary i, Arbitrary v, Eq i, Eq v, Show i, Show v) + => Lens' i v + -> Spec +checkLensLaws l = + do + it "Finality" + $ property lensLawFinality + it "Idempotence" + $ property lensLawIdempotence + it "Invertibility" + $ property lensLawInvertibility + it "Reversibility" + $ property lensLawReversibility + it "Stability" + $ property lensLawStability + where + lensLawFinality :: i -> v -> v -> Property + lensLawFinality i v1 v2 = set l v2 (set l v1 i) === set l v2 i + + lensLawIdempotence :: i -> v -> Property + lensLawIdempotence i v = set l v (set l v i) === set l v i + + lensLawInvertibility :: i -> v -> Property + lensLawInvertibility i v = view l (set l v i) === v + + lensLawReversibility :: i -> v -> Property + lensLawReversibility i v = set l (view l i) (set l v i) === i + + lensLawStability :: i -> Property + lensLawStability i = set l (view l i) i === i + +gender :: Lens' ID Gender +gender = lens ID.getGender (flip ID.setGender) + +location :: Lens' ID Location +location = lens ID.getLocation (flip ID.setLocation) + +nationality :: Lens' ID Nationality +nationality = lens ID.getNationality (flip ID.setNationality) -- | Replaces a character at a specific position. -- diff --git a/components/roc-id/ROC/ID.hs b/components/roc-id/ROC/ID.hs --- a/components/roc-id/ROC/ID.hs +++ b/components/roc-id/ROC/ID.hs @@ -1,5 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -20,7 +23,7 @@ , toText -- * Validity - , checksumDigit + , checksum -- * Generation , generate @@ -41,10 +44,14 @@ ( MonadRandom ) import Data.Bifunctor ( Bifunctor (first) ) +import Data.Finitary + ( Finitary ) import Data.Proxy ( Proxy (Proxy) ) import Data.Text ( Text ) +import GHC.Generics + ( Generic ) import GHC.TypeLits ( Symbol, symbolVal ) import ROC.ID.CharIndex @@ -64,24 +71,20 @@ import ROC.ID.Nationality ( Nationality (..) ) import ROC.ID.Unchecked - ( UncheckedID (UncheckedID) - , ValidID - ) + ( UncheckedID (UncheckedID), ValidID ) import ROC.ID.Utilities - ( guard ) + ( guard, randomFinitary ) import Text.Read - ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens ) + ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens, prec ) import qualified Data.Text as T -import qualified ROC.ID.Digit as Digit -import qualified ROC.ID.Digit1289 as Digit1289 -import qualified ROC.ID.Letter as Letter import qualified ROC.ID.Location as Location import qualified ROC.ID.Unchecked as U -- | -- $setup -- >>> :set -XDataKinds +-- >>> :set -XOverloadedStrings -- >>> :set -XTypeApplications -- >>> import ROC.ID -- >>> import qualified ROC.ID as ID @@ -99,7 +102,7 @@ -- To guarantee correctness, an 'ID' value does __not__ store the terminal -- checksum digit of the identification number it represents. -- --- To compute the checksum digit, use 'checksumDigit'. +-- To compute the checksum digit, use 'checksum'. -- data ID = ID { c0 :: !Letter @@ -112,10 +115,11 @@ , c7 :: !Digit , c8 :: !Digit } - deriving (Eq, Ord) + deriving stock (Eq, Ord, Generic) + deriving anyclass Finitary instance Read ID where - readPrec = parens $ do + readPrec = parens $ prec 10 $ do Ident "ID" <- lexP Symbol "." <- lexP Ident "fromSymbol" <- lexP @@ -123,8 +127,9 @@ unsafeFromText <$> readPrec instance Show ID where - showsPrec _ s = - showString "ID.fromSymbol @" . shows (toText s) + showsPrec d s = + showParen (d > 10) $ + showString "ID.fromSymbol @" . shows (toText s) -------------------------------------------------------------------------------- -- Construction @@ -187,14 +192,29 @@ -- Character at this position must be a digit in the range [0 .. 9]. -- ... -- +-- === Missing or empty symbols +-- +-- >>> ID.fromSymbol +-- ... +-- ... Expected a type-level symbol of the form "A123456789". +-- ... +-- +-- >>> ID.fromSymbol @"" +-- ... +-- ... Expected a type-level symbol of the form "A123456789". +-- ... +-- fromSymbol :: forall (s :: Symbol). ValidID s => ID fromSymbol = unsafeFromText $ T.pack $ symbolVal $ Proxy @s -- | Attempts to construct an 'ID' from 'Text'. -- -- The input must be exactly 10 characters in length and of the form --- __@A123456789@__. +-- __@A123456789@__: -- +-- >>> ID.fromText "A123456789" +-- Right (ID.fromSymbol @"A123456789") +-- -- More precisely, the input must match the regular expression -- __@^[A-Z][1289][0-9]{8}$@__, and the resultant ID must have a valid -- checksum. @@ -212,12 +232,10 @@ where fromUncheckedError :: U.FromTextError -> FromTextError fromUncheckedError = \case - U.TextTooShort -> - TextTooShort - U.TextTooLong -> - TextTooLong U.InvalidChar i r -> InvalidChar i r + U.InvalidLength -> + InvalidLength unsafeFromText :: Text -> ID unsafeFromText t = @@ -229,23 +247,20 @@ -- data FromTextError - = TextTooShort - -- ^ Indicates that the input text is too short. - - | TextTooLong - -- ^ Indicates that the input text is too long. - - | InvalidChar CharIndex CharSet + = InvalidChar CharIndex CharSet -- ^ Indicates that the input text contains a character that is not allowed. -- - -- - `CharIndex` specifies the position of the offending character. + -- - `CharIndex` specifies the position of the invalid character. -- - `CharSet` specifies the set of characters allowed at that position. | InvalidChecksum -- ^ Indicates that the parsed identification number has an invalid checksum. - deriving (Eq, Ord, Show) + | InvalidLength + -- ^ Indicates that the input text has an invalid length. + deriving stock (Eq, Ord, Show) + -------------------------------------------------------------------------------- -- Conversion -------------------------------------------------------------------------------- @@ -269,8 +284,8 @@ -- | Computes the terminal checksum digit of an 'ID'. -- -checksumDigit :: ID -> Digit -checksumDigit (ID u0 u1 u2 u3 u4 u5 u6 u7 u8) = +checksum :: ID -> Digit +checksum (ID u0 u1 u2 u3 u4 u5 u6 u7 u8) = negate $ U.checksum (UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 0) -------------------------------------------------------------------------------- @@ -280,17 +295,7 @@ -- | Generates a random 'ID'. -- generate :: MonadRandom m => m ID -generate = - ID - <$> Letter.generate - <*> Digit1289.generate - <*> Digit.generate - <*> Digit.generate - <*> Digit.generate - <*> Digit.generate - <*> Digit.generate - <*> Digit.generate - <*> Digit.generate +generate = randomFinitary -------------------------------------------------------------------------------- -- Inspection @@ -358,4 +363,4 @@ toUnchecked :: ID -> UncheckedID toUnchecked i@(ID u0 u1 u2 u3 u4 u5 u6 u7 u8) = - UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 (checksumDigit i) + UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 (checksum i) diff --git a/components/roc-id/ROC/ID/Digit.hs b/components/roc-id/ROC/ID/Digit.hs --- a/components/roc-id/ROC/ID/Digit.hs +++ b/components/roc-id/ROC/ID/Digit.hs @@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -16,12 +18,14 @@ import Control.Monad.Random ( MonadRandom ) +import Data.Finitary + ( Finitary ) import GHC.Generics ( Generic ) import GHC.TypeNats ( Nat ) import ROC.ID.Utilities - ( maybeBoundedEnum, randomBoundedEnum ) + ( maybeFinitary, randomFinitary ) import Text.Read ( Read (readPrec), readMaybe ) @@ -34,7 +38,8 @@ -- data Digit = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 - deriving (Bounded, Enum, Eq, Generic, Ord) + deriving stock (Bounded, Enum, Eq, Generic, Ord) + deriving anyclass Finitary -- | Arithmetic modulo 10. -- @@ -56,7 +61,7 @@ -- The 'Char' must be a decimal digit in the range @0@ to @9@. -- fromChar :: Char -> Maybe Digit -fromChar c = readMaybe [c] >>= maybeBoundedEnum +fromChar c = readMaybe [c] >>= maybeFinitary -- | Converts a 'Digit' to a decimal digit character. -- @@ -73,7 +78,7 @@ -- | Generates a random digit. -- generate :: MonadRandom m => m Digit -generate = randomBoundedEnum +generate = randomFinitary type family FromChar (c :: Char) :: Maybe Digit where FromChar '0' = Just D0 diff --git a/components/roc-id/ROC/ID/Digit1289.hs b/components/roc-id/ROC/ID/Digit1289.hs --- a/components/roc-id/ROC/ID/Digit1289.hs +++ b/components/roc-id/ROC/ID/Digit1289.hs @@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} @@ -18,6 +20,8 @@ import Control.Monad.Random ( MonadRandom ) +import Data.Finitary + ( Finitary ) import GHC.Generics ( Generic ) import GHC.TypeNats @@ -25,16 +29,14 @@ import ROC.ID.Digit ( Digit (..) ) import ROC.ID.Utilities - ( randomBoundedEnum ) + ( randomFinitary ) -- | Represents a single decimal digit from the set {@1@, @2@, @8@, @9@}. -- data Digit1289 = D1289_1 | D1289_2 | D1289_8 | D1289_9 - deriving (Bounded, Enum, Eq, Generic, Ord) - -instance Show Digit1289 where - show = (: []) . toChar + deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show) + deriving anyclass Finitary -- | Attempts to parse a 'Digit1289' from a character. -- @@ -69,7 +71,7 @@ -- | Generates a random 'Digit1289'. -- generate :: MonadRandom m => m Digit1289 -generate = randomBoundedEnum +generate = randomFinitary type family FromChar (c :: Char) :: Maybe Digit1289 where FromChar '1' = Just D1289_1 diff --git a/components/roc-id/ROC/ID/Gender.hs b/components/roc-id/ROC/ID/Gender.hs --- a/components/roc-id/ROC/ID/Gender.hs +++ b/components/roc-id/ROC/ID/Gender.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} @@ -10,6 +12,8 @@ import Control.Monad.Random.Class ( MonadRandom (..) ) +import Data.Finitary + ( Finitary ) import Data.Text ( Text ) import GHC.Generics @@ -17,12 +21,13 @@ import ROC.ID.Language ( Language (..) ) import ROC.ID.Utilities - ( randomBoundedEnum ) + ( randomFinitary ) -- | A person's gender, encodable within an ROC identification number. -- data Gender = Male | Female - deriving (Bounded, Enum, Eq, Generic, Ord, Read, Show) + deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show) + deriving anyclass Finitary -- | Prints the specified 'Gender'. -- @@ -44,4 +49,4 @@ -- | Generates a random 'Gender'. -- generate :: MonadRandom m => m Gender -generate = randomBoundedEnum +generate = randomFinitary diff --git a/components/roc-id/ROC/ID/Letter.hs b/components/roc-id/ROC/ID/Letter.hs --- a/components/roc-id/ROC/ID/Letter.hs +++ b/components/roc-id/ROC/ID/Letter.hs @@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -13,10 +15,12 @@ import Control.Monad.Random.Class ( MonadRandom (..) ) +import Data.Finitary + ( Finitary ) import GHC.Generics ( Generic ) import ROC.ID.Utilities - ( randomBoundedEnum ) + ( randomFinitary ) import Text.Read ( readMaybe ) @@ -25,7 +29,8 @@ data Letter = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z - deriving (Bounded, Enum, Eq, Generic, Ord, Read, Show) + deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show) + deriving anyclass Finitary -- | Attempts to parse a 'Letter' from a character. -- @@ -45,7 +50,7 @@ -- | Generates a random 'Letter'. -- generate :: MonadRandom m => m Letter -generate = randomBoundedEnum +generate = randomFinitary type family FromChar (c :: Char) :: Maybe Letter where FromChar 'A' = Just A; FromChar 'N' = Just N diff --git a/components/roc-id/ROC/ID/Location.hs b/components/roc-id/ROC/ID/Location.hs --- a/components/roc-id/ROC/ID/Location.hs +++ b/components/roc-id/ROC/ID/Location.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} @@ -14,6 +15,8 @@ import Control.Monad.Random.Class ( MonadRandom (..) ) +import Data.Finitary + ( Finitary ) import Data.Text ( Text ) import GHC.Generics @@ -22,11 +25,11 @@ ( Language (..) ) import ROC.ID.Letter ( Letter (..) ) +import ROC.ID.Utilities + ( randomFinitary ) import Text.Read ( Lexeme (Ident, Symbol), Read (readPrec), lexP, parens ) -import qualified ROC.ID.Letter as Letter - -- | Represents a location, encodable within an ROC identification number. -- -- == Location codes @@ -102,6 +105,7 @@ newtype Location = Location Letter deriving stock (Eq, Generic, Ord) deriving newtype (Bounded, Enum) + deriving anyclass Finitary instance Read Location where readPrec = parens $ do @@ -191,4 +195,4 @@ -- | Generates a random 'Location'. -- generate :: MonadRandom m => m Location -generate = Location <$> Letter.generate +generate = randomFinitary diff --git a/components/roc-id/ROC/ID/Nationality.hs b/components/roc-id/ROC/ID/Nationality.hs --- a/components/roc-id/ROC/ID/Nationality.hs +++ b/components/roc-id/ROC/ID/Nationality.hs @@ -1,3 +1,7 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} + module ROC.ID.Nationality ( Nationality (..) , generate @@ -6,15 +10,20 @@ import Control.Monad.Random.Class ( MonadRandom (..) ) +import Data.Finitary + ( Finitary ) +import GHC.Generics + ( Generic ) import ROC.ID.Utilities - ( randomBoundedEnum ) + ( randomFinitary ) -- | Specifies a person's nationality. -- data Nationality = National | NonNational - deriving (Bounded, Enum, Eq, Ord, Read, Show) + deriving stock (Bounded, Enum, Eq, Ord, Generic, Read, Show) + deriving anyclass Finitary -- | Generates a random 'Nationality'. -- generate :: MonadRandom m => m Nationality -generate = randomBoundedEnum +generate = randomFinitary diff --git a/components/roc-id/ROC/ID/Unchecked.hs b/components/roc-id/ROC/ID/Unchecked.hs --- a/components/roc-id/ROC/ID/Unchecked.hs +++ b/components/roc-id/ROC/ID/Unchecked.hs @@ -31,6 +31,8 @@ ( NonEmpty ((:|)) ) import Data.Text ( Text ) +import Data.Type.Bool + ( If ) import Data.Type.Equality ( type (==) ) import GHC.TypeError @@ -38,7 +40,7 @@ import GHC.TypeLits ( AppendSymbol, KnownSymbol, Symbol ) import GHC.TypeNats - ( Mod, Nat, type (+) ) + ( CmpNat, Mod, Nat, type (+) ) import ROC.ID.CharIndex ( CharIndex (..) ) import ROC.ID.CharSet @@ -50,7 +52,7 @@ import ROC.ID.Letter ( Letter (..) ) import ROC.ID.Utilities - ( FromJust, Fst, ReplicateChar, Snd, SymbolToCharList, guard ) + ( FromJust, Fst, ReplicateChar, Snd, SymbolLength, SymbolToCharList, guard ) import qualified Data.Set.NonEmpty as NESet import qualified Data.Text as T @@ -88,16 +90,15 @@ ) data FromTextError - = TextTooShort - | TextTooLong - | InvalidChar CharIndex CharSet + = InvalidChar CharIndex CharSet + | InvalidLength deriving stock (Eq, Ord, Read, Show) type Parser a = Text -> Either FromTextError (Text, a) fromText :: Text -> Either FromTextError UncheckedID fromText text0 = do - when (T.length text0 > 10) $ Left TextTooLong + when (T.length text0 > 10) $ Left InvalidLength (text1, c0 ) <- parseLetter text0 (text2, c1 ) <- parseDigit1289 text1 (_____, (c2, c3, c4, c5, c6, c7, c8, c9)) <- parseDigits text2 @@ -105,13 +106,13 @@ where parseLetter :: Parser Letter parseLetter text = do - (char, remainder) <- guard TextTooShort $ T.uncons text + (char, remainder) <- guard InvalidLength $ T.uncons text letter <- guard (InvalidChar 0 (CharRange 'A' 'Z')) (Letter.fromChar char) pure (remainder, letter) parseDigit1289 :: Parser Digit1289 parseDigit1289 text = do - (char, remainder) <- guard TextTooShort $ T.uncons text + (char, remainder) <- guard InvalidLength $ T.uncons text digit1289 <- guard (InvalidChar 1 (CharSet $ NESet.fromList $ '1' :| ['2', '8', '9'])) (Digit1289.fromChar char) @@ -121,7 +122,7 @@ parseDigits text = do let (chars, remainder) = T.splitAt 8 text digitList <- traverse parseIndexedDigit (zip [2 ..] $ T.unpack chars) - digitTuple <- guard TextTooShort (listToTuple8 digitList) + digitTuple <- guard InvalidLength (listToTuple8 digitList) pure (remainder, digitTuple) where parseIndexedDigit (i, c) = @@ -162,7 +163,7 @@ data ChecksumValidity = ChecksumValid | ChecksumInvalid - deriving (Eq, Show) + deriving stock (Eq, Show) checksumValidity :: UncheckedID -> ChecksumValidity checksumValidity u = @@ -297,5 +298,18 @@ type ValidID s = ( KnownSymbol s - , ChecksumValid (SymbolToId s) + , ChecksumValid (SymbolToId (ConcreteSymbol s)) ) :: Constraint + +-- | Ensures the existence of a concrete symbol, or else raises a type error. +-- +type family ConcreteSymbol (s :: Symbol) :: Symbol where + -- If we can compute the symbol's length, then we have a concrete symbol. + ConcreteSymbol s = + If + (CmpNat (SymbolLength s) 0 == GT) + s + (TypeError (TypeError.Text ConcreteSymbolError)) + +type ConcreteSymbolError = + "Expected a type-level symbol of the form \"A123456789\"." diff --git a/components/roc-id/ROC/ID/Utilities.hs b/components/roc-id/ROC/ID/Utilities.hs --- a/components/roc-id/ROC/ID/Utilities.hs +++ b/components/roc-id/ROC/ID/Utilities.hs @@ -1,6 +1,8 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} @@ -9,24 +11,45 @@ import Control.Monad.Random.Class ( MonadRandom (..) ) +import Data.Finitary + ( Finitary (fromFinite), Cardinality ) +import Data.Finite + ( packFinite ) +import Data.Maybe + ( fromMaybe ) +import Data.Proxy + ( Proxy (Proxy) ) import GHC.TypeLits - ( Symbol, UnconsSymbol, ConsSymbol ) + ( Symbol, UnconsSymbol, ConsSymbol, type (<=), type (+) ) import GHC.TypeNats - ( Nat, type (-) ) + ( Nat, type (-), natVal ) +import Numeric.Natural + ( Natural ) +cardinality :: forall a. Finitary a => Natural +cardinality = natVal $ Proxy @(Cardinality a) + guard :: x -> Maybe y -> Either x y guard x = maybe (Left x) Right -maybeBoundedEnum :: forall a. (Bounded a, Enum a) => Int -> Maybe a -maybeBoundedEnum i - | i < fromEnum (minBound :: a) = Nothing - | i > fromEnum (maxBound :: a) = Nothing - | otherwise = pure $ toEnum i +maybeFinitary :: forall a. Finitary a => Natural -> Maybe a +maybeFinitary = fmap fromFinite . packFinite . fromIntegral @Natural @Integer -randomBoundedEnum :: forall m a. (MonadRandom m, Bounded a, Enum a) => m a -randomBoundedEnum = - toEnum <$> getRandomR (fromEnum (minBound :: a), fromEnum (maxBound :: a)) +randomFinitary + :: forall m a. (MonadRandom m, Finitary a, 1 <= Cardinality a) => m a +randomFinitary = + fromMaybe failure . maybeFinitary <$> randomNatural (0, cardinality @a - 1) + where + failure = error "randomFinitary: unexpected out-of-bounds value" +randomNatural :: MonadRandom m => (Natural, Natural) -> m Natural +randomNatural (lo, hi) = + fromIntegral @Integer @Natural <$> + getRandomR + ( fromIntegral @Natural @Integer lo + , fromIntegral @Natural @Integer hi + ) + type family FromJust (m :: Maybe a) e where FromJust Nothing e = e FromJust (Just a) _ = a @@ -36,6 +59,16 @@ type family Snd (t :: (a, a)) :: a where Snd '(_, y) = y + +type family ListLength (as :: [a]) :: Nat where + ListLength as = ListLengthInner 0 as + +type family ListLengthInner (n :: Nat) (as :: [a]) :: Nat where + ListLengthInner n '[] = n + ListLengthInner n (a : as) = ListLengthInner (n + 1) as + +type family SymbolLength (s :: Symbol) :: Nat where + SymbolLength s = ListLength (SymbolToCharList s) type family SymbolToCharList (s :: Symbol) :: [Char] diff --git a/roc-id.cabal b/roc-id.cabal --- a/roc-id.cabal +++ b/roc-id.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: roc-id -version: 0.3.0.0 +version: 0.4.0.0 synopsis: Implementation of the ROC (Taiwan) Uniform ID Number format. category: Identification homepage: https://github.com/jonathanknowles/roc-id#readme @@ -43,8 +43,14 @@ build-depends:base >= 4.17.2.1 && < 4.22 common dependency-doctest build-depends:doctest >= 0.24.2 && < 0.25 +common dependency-finitary + build-depends:finitary >= 2.2.0.0 && < 2.3 +common dependency-finite-typelits + build-depends:finite-typelits >= 0.2.1.0 && < 0.3 common dependency-hspec build-depends:hspec >= 2.5.5 && < 2.12 +common dependency-microlens + build-depends:microlens >= 0.5.0.0 && < 0.6 common dependency-MonadRandom build-depends:MonadRandom >= 0.5.1.1 && < 0.7 common dependency-nonempty-containers @@ -68,6 +74,8 @@ library import: , dependency-base + , dependency-finitary + , dependency-finite-typelits , dependency-MonadRandom , dependency-nonempty-containers , dependency-text @@ -93,8 +101,10 @@ test-suite roc-id-test import: , dependency-base + , dependency-finitary , dependency-hspec , dependency-MonadRandom + , dependency-microlens , dependency-nonempty-containers , dependency-QuickCheck , dependency-quickcheck-classes