{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Taiwan.ID
  (
  -- * Type
    ID (..)

  -- * Construction
  , fromSymbol
  , fromText
  , FromTextError (..)

  -- * Conversion
  , toText

  -- * Validity
  , checksum

  -- * Generation
  , generate

  -- * Inspection
  , getGender
  , getIssuer
  , getRegion

  -- * Modification
  , setGender
  , setIssuer
  , setRegion
  )
  where

import Control.Monad.Random.Class
  ( 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 Taiwan.ID.CharIndex
  ( CharIndex (..) )
import Taiwan.ID.CharSet
  ( CharSet (..) )
import Taiwan.ID.Digit
  ( Digit (..) )
import Taiwan.ID.Digit1289
  ( Digit1289 (..) )
import Taiwan.ID.Gender
  ( Gender (..) )
import Taiwan.ID.Issuer
  ( Issuer (..) )
import Taiwan.ID.Letter
  ( Letter (..) )
import Taiwan.ID.Region
  ( Region )
import Taiwan.ID.Unchecked
  ( UncheckedID (UncheckedID), ValidID )
import Taiwan.ID.Utilities
  ( guard, randomFinitary )
import Text.Read
  ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens, prec )

import qualified Data.Text as T
import qualified Taiwan.ID.Region as Region
import qualified Taiwan.ID.Unchecked as U

-- |
-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeApplications
-- >>> import Taiwan.ID
-- >>> import qualified Taiwan.ID as ID

--------------------------------------------------------------------------------
-- Type
--------------------------------------------------------------------------------

-- | Represents a __valid__ 10-digit uniform identification number of the form
-- __@A123456789@__.
--
-- By construction, invalid identification numbers are __not representable__ by
-- this data type.
--
-- 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 'checksum'.
--
data ID = ID
  { ID -> Letter
c0 :: !Letter
  , ID -> Digit1289
c1 :: !Digit1289
  , ID -> Digit
c2 :: !Digit
  , ID -> Digit
c3 :: !Digit
  , ID -> Digit
c4 :: !Digit
  , ID -> Digit
c5 :: !Digit
  , ID -> Digit
c6 :: !Digit
  , ID -> Digit
c7 :: !Digit
  , ID -> Digit
c8 :: !Digit
  }
  deriving stock (ID -> ID -> Bool
(ID -> ID -> Bool) -> (ID -> ID -> Bool) -> Eq ID
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ID -> ID -> Bool
== :: ID -> ID -> Bool
$c/= :: ID -> ID -> Bool
/= :: ID -> ID -> Bool
Eq, Eq ID
Eq ID =>
(ID -> ID -> Ordering)
-> (ID -> ID -> Bool)
-> (ID -> ID -> Bool)
-> (ID -> ID -> Bool)
-> (ID -> ID -> Bool)
-> (ID -> ID -> ID)
-> (ID -> ID -> ID)
-> Ord ID
ID -> ID -> Bool
ID -> ID -> Ordering
ID -> ID -> ID
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ID -> ID -> Ordering
compare :: ID -> ID -> Ordering
$c< :: ID -> ID -> Bool
< :: ID -> ID -> Bool
$c<= :: ID -> ID -> Bool
<= :: ID -> ID -> Bool
$c> :: ID -> ID -> Bool
> :: ID -> ID -> Bool
$c>= :: ID -> ID -> Bool
>= :: ID -> ID -> Bool
$cmax :: ID -> ID -> ID
max :: ID -> ID -> ID
$cmin :: ID -> ID -> ID
min :: ID -> ID -> ID
Ord, (forall x. ID -> Rep ID x)
-> (forall x. Rep ID x -> ID) -> Generic ID
forall x. Rep ID x -> ID
forall x. ID -> Rep ID x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ID -> Rep ID x
from :: forall x. ID -> Rep ID x
$cto :: forall x. Rep ID x -> ID
to :: forall x. Rep ID x -> ID
Generic)
  deriving anyclass Eq ID
KnownNat (Cardinality ID)
(Eq ID, KnownNat (Cardinality ID)) =>
(Finite (Cardinality ID) -> ID)
-> (ID -> Finite (Cardinality ID))
-> ((1 <= Cardinality ID) => ID)
-> ((1 <= Cardinality ID) => ID)
-> (ID -> Maybe ID)
-> (ID -> Maybe ID)
-> Finitary ID
(1 <= Cardinality ID) => ID
Finite (Cardinality ID) -> ID
ID -> Maybe ID
ID -> Finite (Cardinality ID)
forall a.
(Eq a, KnownNat (Cardinality a)) =>
(Finite (Cardinality a) -> a)
-> (a -> Finite (Cardinality a))
-> ((1 <= Cardinality a) => a)
-> ((1 <= Cardinality a) => a)
-> (a -> Maybe a)
-> (a -> Maybe a)
-> Finitary a
$cfromFinite :: Finite (Cardinality ID) -> ID
fromFinite :: Finite (Cardinality ID) -> ID
$ctoFinite :: ID -> Finite (Cardinality ID)
toFinite :: ID -> Finite (Cardinality ID)
$cstart :: (1 <= Cardinality ID) => ID
start :: (1 <= Cardinality ID) => ID
$cend :: (1 <= Cardinality ID) => ID
end :: (1 <= Cardinality ID) => ID
$cprevious :: ID -> Maybe ID
previous :: ID -> Maybe ID
$cnext :: ID -> Maybe ID
next :: ID -> Maybe ID
Finitary

instance Read ID where
  readPrec :: ReadPrec ID
readPrec = ReadPrec ID -> ReadPrec ID
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec ID -> ReadPrec ID) -> ReadPrec ID -> ReadPrec ID
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec ID -> ReadPrec ID
forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
10 (ReadPrec ID -> ReadPrec ID) -> ReadPrec ID -> ReadPrec ID
forall a b. (a -> b) -> a -> b
$ do
    Ident  "ID"         <- ReadPrec Lexeme
lexP
    Symbol "."          <- lexP
    Ident  "fromSymbol" <- lexP
    Punc   "@"          <- lexP
    unsafeFromText <$> readPrec

instance Show ID where
  showsPrec :: Int -> ID -> ShowS
showsPrec Int
d ID
s =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"ID.fromSymbol @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ShowS
forall a. Show a => a -> ShowS
shows (ID -> Text
toText ID
s)

--------------------------------------------------------------------------------
-- Construction
--------------------------------------------------------------------------------

-- | Constructs an 'ID' from a type-level textual symbol.
--
-- The symbol must be exactly 10 characters in length and of the form
-- __@A123456789@__:
--
-- >>> ID.fromSymbol @"A123456789"
-- ID.fromSymbol @"A123456789"
--
-- More precisely:
--
--  - the symbol must match the regular expression __@^[A-Z][1289][0-9]{8}$@__
--  - the resultant ID must have a valid checksum.
--
-- Failure to satisfy these constraints will result in one of the following
-- __type errors__:
--
-- === Invalid lengths
--
-- >>> ID.fromSymbol @"A12345678"
-- ...
-- ... An ID must have exactly 10 characters.
-- ...
--
-- === Invalid checksums
--
-- >>> ID.fromSymbol @"A123456780"
-- ...
-- ... ID has invalid checksum.
-- ...
--
-- === Invalid characters
--
-- On detection of an invalid character, the resulting type error reports
-- both the position of the character and the set of characters permitted
-- at that position.
--
-- >>> ID.fromSymbol @"_123456789"
-- ...
--     • "_123456789"
--        ^
--       Character at this position must be an uppercase letter.
-- ...
--
-- >>> ID.fromSymbol @"A_23456789"
-- ...
--     • "A_23456789"
--         ^
--       Character at this position must be a digit from the set {1, 2, 8, 9}.
-- ...
--
-- >>> ID.fromSymbol @"A1_3456789"
-- ...
--     • "A1_3456789"
--          ^
--       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 :: forall (s :: Symbol). ValidID s => ID
fromSymbol = Text -> ID
unsafeFromText (Text -> ID) -> Text -> ID
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s -> String) -> Proxy s -> String
forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @s

-- | Attempts to construct an 'ID' from 'Text'.
--
-- The input must be exactly 10 characters in length and of the form
-- __@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.
--
-- This function satisfies the following law:
--
-- @
-- 'fromText' ('toText' i) '==' 'Right' i
-- @
--
fromText :: Text -> Either FromTextError ID
fromText :: Text -> Either FromTextError ID
fromText Text
text = do
    unchecked <- (FromTextError -> FromTextError)
-> Either FromTextError UncheckedID
-> Either FromTextError UncheckedID
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first FromTextError -> FromTextError
fromUncheckedError (Either FromTextError UncheckedID
 -> Either FromTextError UncheckedID)
-> Either FromTextError UncheckedID
-> Either FromTextError UncheckedID
forall a b. (a -> b) -> a -> b
$ Text -> Either FromTextError UncheckedID
U.fromText Text
text
    guard InvalidChecksum $ fromUnchecked unchecked
  where
    fromUncheckedError :: U.FromTextError -> FromTextError
    fromUncheckedError :: FromTextError -> FromTextError
fromUncheckedError = \case
      U.InvalidChar CharIndex
i CharSet
r ->
        CharIndex -> CharSet -> FromTextError
InvalidChar CharIndex
i CharSet
r
      FromTextError
U.InvalidLength ->
        FromTextError
InvalidLength

unsafeFromText :: Text -> ID
unsafeFromText :: Text -> ID
unsafeFromText Text
t =
  case Text -> Either FromTextError ID
fromText Text
t of
    Left FromTextError
_ -> String -> ID
forall a. HasCallStack => String -> a
error String
"unsafeFromText"
    Right ID
i -> ID
i

-- | Indicates an error that occurred while constructing an 'ID' from 'Text'.
--
data FromTextError

  = InvalidChar CharIndex CharSet
  -- ^ Indicates that the input text contains a character that is not allowed.
  --
  --   - `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.

  | InvalidLength
  -- ^ Indicates that the input text has an invalid length.

  deriving stock (FromTextError -> FromTextError -> Bool
(FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool) -> Eq FromTextError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FromTextError -> FromTextError -> Bool
== :: FromTextError -> FromTextError -> Bool
$c/= :: FromTextError -> FromTextError -> Bool
/= :: FromTextError -> FromTextError -> Bool
Eq, Eq FromTextError
Eq FromTextError =>
(FromTextError -> FromTextError -> Ordering)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> Bool)
-> (FromTextError -> FromTextError -> FromTextError)
-> (FromTextError -> FromTextError -> FromTextError)
-> Ord FromTextError
FromTextError -> FromTextError -> Bool
FromTextError -> FromTextError -> Ordering
FromTextError -> FromTextError -> FromTextError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FromTextError -> FromTextError -> Ordering
compare :: FromTextError -> FromTextError -> Ordering
$c< :: FromTextError -> FromTextError -> Bool
< :: FromTextError -> FromTextError -> Bool
$c<= :: FromTextError -> FromTextError -> Bool
<= :: FromTextError -> FromTextError -> Bool
$c> :: FromTextError -> FromTextError -> Bool
> :: FromTextError -> FromTextError -> Bool
$c>= :: FromTextError -> FromTextError -> Bool
>= :: FromTextError -> FromTextError -> Bool
$cmax :: FromTextError -> FromTextError -> FromTextError
max :: FromTextError -> FromTextError -> FromTextError
$cmin :: FromTextError -> FromTextError -> FromTextError
min :: FromTextError -> FromTextError -> FromTextError
Ord, Int -> FromTextError -> ShowS
[FromTextError] -> ShowS
FromTextError -> String
(Int -> FromTextError -> ShowS)
-> (FromTextError -> String)
-> ([FromTextError] -> ShowS)
-> Show FromTextError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FromTextError -> ShowS
showsPrec :: Int -> FromTextError -> ShowS
$cshow :: FromTextError -> String
show :: FromTextError -> String
$cshowList :: [FromTextError] -> ShowS
showList :: [FromTextError] -> ShowS
Show)

--------------------------------------------------------------------------------
-- Conversion
--------------------------------------------------------------------------------

-- | Converts an 'ID' to 'Text'.
--
-- The output is of the form __@A123456789@__.
--
-- This function satisfies the following law:
--
-- @
-- 'fromText' ('toText' i) '==' 'Right' i
-- @
--
toText :: ID -> Text
toText :: ID -> Text
toText = UncheckedID -> Text
U.toText (UncheckedID -> Text) -> (ID -> UncheckedID) -> ID -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ID -> UncheckedID
toUnchecked

--------------------------------------------------------------------------------
-- Validity
--------------------------------------------------------------------------------

-- | Computes the terminal checksum digit of an 'ID'.
--
checksum :: ID -> Digit
checksum :: ID -> Digit
checksum (ID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8) =
  Digit -> Digit
forall a. Num a => a -> a
negate (Digit -> Digit) -> Digit -> Digit
forall a b. (a -> b) -> a -> b
$ UncheckedID -> Digit
U.checksum (Letter
-> Digit1289
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> UncheckedID
UncheckedID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8 Digit
0)

--------------------------------------------------------------------------------
-- Generation
--------------------------------------------------------------------------------

-- | Generates a random 'ID'.
--
generate :: MonadRandom m => m ID
generate :: forall (m :: * -> *). MonadRandom m => m ID
generate = m ID
forall (m :: * -> *) a.
(MonadRandom m, Finitary a, 1 <= Cardinality a) =>
m a
randomFinitary

--------------------------------------------------------------------------------
-- Inspection
--------------------------------------------------------------------------------

-- | Decodes the 'Gender' component of an 'ID'.
--
getGender :: ID -> Gender
getGender :: ID -> Gender
getGender ID {Digit1289
c1 :: ID -> Digit1289
c1 :: Digit1289
c1} = (Gender, Issuer) -> Gender
forall a b. (a, b) -> a
fst ((Gender, Issuer) -> Gender) -> (Gender, Issuer) -> Gender
forall a b. (a -> b) -> a -> b
$ Digit1289 -> (Gender, Issuer)
decodeC1 Digit1289
c1

-- | Decodes the 'Issuer' component of an 'ID'.
--
getIssuer :: ID -> Issuer
getIssuer :: ID -> Issuer
getIssuer ID {Digit1289
c1 :: ID -> Digit1289
c1 :: Digit1289
c1} = (Gender, Issuer) -> Issuer
forall a b. (a, b) -> b
snd ((Gender, Issuer) -> Issuer) -> (Gender, Issuer) -> Issuer
forall a b. (a -> b) -> a -> b
$ Digit1289 -> (Gender, Issuer)
decodeC1 Digit1289
c1

-- | Decodes the 'Region' component of an 'ID'.
--
getRegion :: ID -> Region
getRegion :: ID -> Region
getRegion ID {Letter
c0 :: ID -> Letter
c0 :: Letter
c0} = Letter -> Region
Region.fromLetter Letter
c0

--------------------------------------------------------------------------------
-- Modification
--------------------------------------------------------------------------------

-- | Updates the 'Gender' component of an 'ID'.
--
setGender :: Gender -> ID -> ID
setGender :: Gender -> ID -> ID
setGender Gender
gender ID
i = ID
i {c1 = encodeC1 (gender, getIssuer i)}

-- | Updates the 'Issuer' component of an 'ID'.
--
setIssuer :: Issuer -> ID -> ID
setIssuer :: Issuer -> ID -> ID
setIssuer Issuer
issuer ID
i = ID
i {c1 = encodeC1 (getGender i, issuer)}

-- | Updates the 'Region' component of an 'ID'.
--
setRegion :: Region -> ID -> ID
setRegion :: Region -> ID -> ID
setRegion Region
region ID
i = ID
i {c0 = Region.toLetter region}

--------------------------------------------------------------------------------
-- Internal
--------------------------------------------------------------------------------

decodeC1 :: Digit1289 -> (Gender, Issuer)
decodeC1 :: Digit1289 -> (Gender, Issuer)
decodeC1 = \case
  Digit1289
D1289_1 -> (  Gender
Male, Issuer
HouseholdRegistrationOffice)
  Digit1289
D1289_2 -> (Gender
Female, Issuer
HouseholdRegistrationOffice)
  Digit1289
D1289_8 -> (  Gender
Male,   Issuer
NationalImmigrationAgency)
  Digit1289
D1289_9 -> (Gender
Female,   Issuer
NationalImmigrationAgency)

encodeC1 :: (Gender, Issuer) -> Digit1289
encodeC1 :: (Gender, Issuer) -> Digit1289
encodeC1 = \case
  (  Gender
Male, Issuer
HouseholdRegistrationOffice) -> Digit1289
D1289_1
  (Gender
Female, Issuer
HouseholdRegistrationOffice) -> Digit1289
D1289_2
  (  Gender
Male,   Issuer
NationalImmigrationAgency) -> Digit1289
D1289_8
  (Gender
Female,   Issuer
NationalImmigrationAgency) -> Digit1289
D1289_9

fromUnchecked :: UncheckedID -> Maybe ID
fromUnchecked :: UncheckedID -> Maybe ID
fromUnchecked u :: UncheckedID
u@(UncheckedID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8 Digit
_) =
    case UncheckedID -> ChecksumValidity
U.checksumValidity UncheckedID
u of
      ChecksumValidity
U.ChecksumValid   -> ID -> Maybe ID
forall a. a -> Maybe a
Just ID
i
      ChecksumValidity
U.ChecksumInvalid -> Maybe ID
forall a. Maybe a
Nothing
  where
    i :: ID
i = Letter
-> Digit1289
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> ID
ID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8

toUnchecked :: ID -> UncheckedID
toUnchecked :: ID -> UncheckedID
toUnchecked i :: ID
i@(ID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8) =
  Letter
-> Digit1289
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> Digit
-> UncheckedID
UncheckedID Letter
u0 Digit1289
u1 Digit
u2 Digit
u3 Digit
u4 Digit
u5 Digit
u6 Digit
u7 Digit
u8 (ID -> Digit
checksum ID
i)