module ASCII.CaseRefinement
  (
    {- * ASCII'case type constructor -} ASCII'case, lift, asciiCaseUnsafe, forgetCase,
    {- ** Aliases -} {- $aliases -} ASCII'upper, ASCII'lower,
    {- * Character functions -} validateChar, fromCaselessChar,
          toCaselessChar, substituteChar, asCaselessChar, refineCharToCase,
    {- * String functions -} validateString, fromCaselessCharList,
          toCaselessCharList, substituteString, mapChars, refineStringToCase,
    {- * KnownCase -} KnownCase (..),
  )
  where

import ASCII.Case (Case (..))
import ASCII.Caseless (CaselessChar)
import {-# source #-} ASCII.Refinement.Internal (ASCII)
import ASCII.Superset (CharSuperset, StringSuperset)

import qualified ASCII.Case as Case
import qualified ASCII.Caseless as Caseless
import qualified ASCII.Char as ASCII
import qualified ASCII.Superset as S
import {-# source #-} qualified ASCII.Refinement.Internal as Refinement

import Control.Monad (guard)
import Data.Data (Data, Typeable)
import Data.Eq (Eq)
import Data.Foldable (any)
import Data.Function (($), (.))
import Data.Hashable (Hashable)
import Data.Maybe (Maybe (..))
import Data.Monoid (Monoid)
import Data.Ord (Ord, (>))
import Data.Semigroup (Semigroup)
import GHC.Generics (Generic)
import Prelude (succ)
import Text.Show (Show, showList, showParen, showString, showsPrec)

import qualified Data.Bool as Bool
import qualified Data.List as List

{-| Indicates that a value from some ASCII superset is valid ASCII, and also
    that any letters belong to a particular 'Case' indicated by the @letterCase@
    type parameter

The @superset@ type parameter is the ASCII superset, which should be a type with
an instance of either 'CharSuperset' or 'StringSuperset'.

For example, whereas a 'Data.Text.Text' value may contain a combination of ASCII
and non-ASCII characters, a value of type @'ASCII'case' ''ASCII.Case.UpperCase'
'Data.Text.Text'@ may contain only uppercase ASCII letters and ASCII
non-letters. -}
newtype ASCII'case (letterCase :: Case) superset = ASCII'case_Unsafe
  { forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift :: superset
      {- ^ Discard the evidence that the value is known to consist
           entirely of ASCII characters in a particular case -}
  }

deriving stock instance Eq superset =>
    Eq (ASCII'case letterCase superset)

deriving stock instance Ord superset =>
    Ord (ASCII'case letterCase superset)

deriving newtype instance Hashable superset =>
    Hashable (ASCII'case letterCase superset)

deriving newtype instance Semigroup superset =>
    Semigroup (ASCII'case letterCase superset)

deriving newtype instance Monoid superset =>
    Monoid (ASCII'case letterCase superset)

deriving stock instance (Data superset, Typeable letterCase) =>
    Data (ASCII'case letterCase superset)

deriving stock instance Generic (ASCII'case letterCase superset)

instance Show superset => Show (ASCII'case letterCase superset) where
    showsPrec :: Int -> ASCII'case letterCase superset -> ShowS
showsPrec Int
d ASCII'case letterCase superset
x = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
app_prec) forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"asciiCaseUnsafe " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec (forall a. Enum a => a -> a
succ Int
app_prec) (forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift ASCII'case letterCase superset
x)
      where app_prec :: Int
app_prec = Int
10

    showList :: [ASCII'case letterCase superset] -> ShowS
showList [ASCII'case letterCase superset]
x = String -> ShowS
showString String
"asciiCaseUnsafe " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => [a] -> ShowS
showList (forall a b. (a -> b) -> [a] -> [b]
List.map forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift [ASCII'case letterCase superset]
x)

instance S.ToCaselessChar char => S.ToCaselessChar (ASCII'case letterCase char) where
    isAsciiCaselessChar :: ASCII'case letterCase char -> Bool
isAsciiCaselessChar ASCII'case letterCase char
_ = Bool
Bool.True
    toCaselessCharUnsafe :: ASCII'case letterCase char -> CaselessChar
toCaselessCharUnsafe = forall char. ToCaselessChar char => char -> CaselessChar
S.toCaselessCharUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

instance S.CharSuperset char => S.ToChar (ASCII'case letterCase char) where
    isAsciiChar :: ASCII'case letterCase char -> Bool
isAsciiChar ASCII'case letterCase char
_ = Bool
Bool.True
    toCharUnsafe :: ASCII'case letterCase char -> Char
toCharUnsafe = forall char. ToChar char => char -> Char
S.toCharUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

instance S.ToCaselessString string => S.ToCaselessString (ASCII'case letterCase string) where
    isAsciiCaselessString :: ASCII'case letterCase string -> Bool
isAsciiCaselessString ASCII'case letterCase string
_ = Bool
Bool.True
    toCaselessCharListUnsafe :: ASCII'case letterCase string -> [CaselessChar]
toCaselessCharListUnsafe = forall string. ToCaselessString string => string -> [CaselessChar]
S.toCaselessCharListUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift
    toCaselessCharListSub :: ASCII'case letterCase string -> [CaselessChar]
toCaselessCharListSub = forall string. ToCaselessString string => string -> [CaselessChar]
S.toCaselessCharListSub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

instance S.ToString string => S.ToString (ASCII'case letterCase string) where
    isAsciiString :: ASCII'case letterCase string -> Bool
isAsciiString ASCII'case letterCase string
_ = Bool
Bool.True
    toCharListUnsafe :: ASCII'case letterCase string -> [Char]
toCharListUnsafe = forall string. ToString string => string -> [Char]
S.toCharListUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift
    toCharListSub :: ASCII'case letterCase string -> [Char]
toCharListSub = forall string. ToString string => string -> [Char]
S.toCharListUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

instance (S.FromChar superset, KnownCase letterCase) => S.ToCasefulChar letterCase (ASCII'case letterCase superset) where
    toCasefulChar :: CaselessChar -> ASCII'case letterCase superset
toCasefulChar = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall char. FromChar char => Char -> char
S.fromChar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)

instance (S.FromString superset, KnownCase letterCase) => S.ToCasefulString letterCase (ASCII'case letterCase superset) where
    toCasefulString :: [CaselessChar] -> ASCII'case letterCase superset
toCasefulString = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. FromString string => [Char] -> string
S.fromCharList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
List.map (Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase))

{-| Change the type of an ASCII superset value that is known to be valid ASCII where
    letters are restricted to the 'Case' designated by the @letterCase@ type variable

This is "unsafe" because this assertion is unchecked, so this function is capable
of producing an invalid 'ASCII'case' value. -}
asciiCaseUnsafe :: superset -> ASCII'case letterCase superset
asciiCaseUnsafe :: forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe = forall (letterCase :: Case) superset.
superset -> ASCII'case letterCase superset
ASCII'case_Unsafe

forgetCase :: ASCII'case letterCase superset -> ASCII superset
forgetCase :: forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> ASCII superset
forgetCase = forall superset. superset -> ASCII superset
Refinement.asciiUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

---

{- $aliases

The 'ASCII'upper' and 'ASCII'lower' type aliases exist primarily so that you can
use 'ASCII'case' without the DataKinds language extension. -}
type ASCII'upper superset = ASCII'case 'UpperCase superset

type ASCII'lower superset = ASCII'case 'LowerCase superset

---

class KnownCase (letterCase :: Case) where theCase :: Case
instance KnownCase 'UpperCase where theCase :: Case
theCase = Case
UpperCase
instance KnownCase 'LowerCase where theCase :: Case
theCase = Case
LowerCase

---

{-| Return 'Just' an 'ASCII'case' character if the input is an ASCII character
    in the proper case, or 'Nothing' otherwise -}
validateChar :: forall letterCase superset. KnownCase letterCase => CharSuperset superset =>
    superset {- ^ Character which may or may not be in the ASCII character set;
                  if a letter, may be in any case -}
    -> Maybe (ASCII'case letterCase superset)
validateChar :: forall (letterCase :: Case) superset.
(KnownCase letterCase, CharSuperset superset) =>
superset -> Maybe (ASCII'case letterCase superset)
validateChar superset
x = do
    Char
c <- forall char. ToChar char => char -> Maybe Char
S.toCharMaybe superset
x
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
Bool.not (Case -> Char -> Bool
Case.isCase (Case -> Case
Case.opposite (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)) Char
c))
    forall a. a -> Maybe a
Just (forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe superset
x)

{-| Return an 'ASCII'case' character if the input is an ASCII character in the
    proper case, or 'ASCII.Substitute' otherwise -}
substituteChar :: forall letterCase superset. KnownCase letterCase => CharSuperset superset =>
    superset
    -> ASCII'case letterCase superset
substituteChar :: forall (letterCase :: Case) superset.
(KnownCase letterCase, CharSuperset superset) =>
superset -> ASCII'case letterCase superset
substituteChar superset
x = case forall (letterCase :: Case) superset.
(KnownCase letterCase, CharSuperset superset) =>
superset -> Maybe (ASCII'case letterCase superset)
validateChar superset
x of
    Maybe (ASCII'case letterCase superset)
Nothing -> forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe (forall char. FromChar char => Char -> char
S.fromChar Char
ASCII.Substitute)
    Just ASCII'case letterCase superset
c -> ASCII'case letterCase superset
c

{-| Lift a 'CaselessChar' into a superset type, wrapped in the 'ASCII'case'
    refinement to save the evidence that it is ASCII in a particular case -}
fromCaselessChar :: forall letterCase superset. KnownCase letterCase => CharSuperset superset =>
    CaselessChar -- ^ Character which, if it is a letter, does not have a specified case
    -> ASCII'case letterCase superset
fromCaselessChar :: forall (letterCase :: Case) superset.
(KnownCase letterCase, CharSuperset superset) =>
CaselessChar -> ASCII'case letterCase superset
fromCaselessChar = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall char. FromChar char => Char -> char
S.fromChar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)

{-| Given a character from some type that is known to represent an ASCII
    character in a particular case, obtain the caseless ASCII character
    it represents -}
toCaselessChar :: CharSuperset superset =>
    ASCII'case letterCase superset {- ^ Character that is known to be ASCII, and
                                        in the particular case if it is a letter -}
    -> CaselessChar
toCaselessChar :: forall superset (letterCase :: Case).
CharSuperset superset =>
ASCII'case letterCase superset -> CaselessChar
toCaselessChar = Char -> CaselessChar
Caseless.disregardCase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall char. ToChar char => char -> Char
S.toCharUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

{-| Given a character from a larger set that is known to represent an ASCII
    character, manipulate it as if it were an ASCII character -}
asCaselessChar :: forall letterCase superset. KnownCase letterCase => CharSuperset superset =>
    (CaselessChar -> CaselessChar) -- ^ Case-insensitive function over ASCII characters
    -> ASCII'case letterCase superset {- ^ Character that is known to be ASCII, and
                                           in the particular case if it is a letter -}
    -> ASCII'case letterCase superset
asCaselessChar :: forall (letterCase :: Case) superset.
(KnownCase letterCase, CharSuperset superset) =>
(CaselessChar -> CaselessChar)
-> ASCII'case letterCase superset -> ASCII'case letterCase superset
asCaselessChar CaselessChar -> CaselessChar
f = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall char. CharSuperset char => (Char -> Char) -> char -> char
S.asCharUnsafe Char -> Char
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift
  where
    g :: Char -> Char
g = Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaselessChar -> CaselessChar
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> Char -> CaselessChar
Caseless.assumeCaseUnsafe (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)

{-| Given an ASCII superset character that is known to be valid ASCII,
    refine it further by converting it to a particular letter case -}
refineCharToCase :: forall letterCase char. KnownCase letterCase => CharSuperset char =>
    ASCII char -> ASCII'case letterCase char
refineCharToCase :: forall (letterCase :: Case) char.
(KnownCase letterCase, CharSuperset char) =>
ASCII char -> ASCII'case letterCase char
refineCharToCase = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall char. CharSuperset char => Case -> char -> char
S.toCaseChar (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall superset. ASCII superset -> superset
Refinement.lift

---

{-| Return 'Just' an 'ASCII'case' string if the input consists entirely of ASCII
    characters in the proper case, or 'Nothing' otherwise -}
validateString :: forall letterCase superset. KnownCase letterCase => StringSuperset superset =>
    superset -- ^ String which may or may not be valid ASCII, where letters may be in any case
    -> Maybe (ASCII'case letterCase superset)
validateString :: forall (letterCase :: Case) superset.
(KnownCase letterCase, StringSuperset superset) =>
superset -> Maybe (ASCII'case letterCase superset)
validateString superset
x = do
    [Char]
s <- forall string. ToString string => string -> Maybe [Char]
S.toCharListMaybe superset
x
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
Bool.not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Case -> Char -> Bool
Case.isCase (Case -> Case
Case.opposite (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase))) [Char]
s))
    forall a. a -> Maybe a
Just (forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe superset
x)

{-| Lift a list of 'CaselessChar' into a superset string type, wrapped in the
    'ASCII'case' refinement to save the evidence that all of the characters in
    the string are ASCII in a particular case -}
fromCaselessCharList :: forall letterCase superset. KnownCase letterCase => StringSuperset superset =>
    [CaselessChar] -- ^ Case-insensitive ASCII string represented as a list of caseless characters
    -> ASCII'case letterCase superset
fromCaselessCharList :: forall (letterCase :: Case) superset.
(KnownCase letterCase, StringSuperset superset) =>
[CaselessChar] -> ASCII'case letterCase superset
fromCaselessCharList = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. FromString string => [Char] -> string
S.fromCharList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
List.map (Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase))

{-| Given a string from some type that is known to represent only ASCII characters
    in a particular case, obtain the caseless characters it represents -}
toCaselessCharList :: forall letterCase superset. KnownCase letterCase => StringSuperset superset =>
    ASCII'case letterCase superset -- ^ String that is known to be valid ASCII in a particular case
    -> [CaselessChar]
toCaselessCharList :: forall (letterCase :: Case) superset.
(KnownCase letterCase, StringSuperset superset) =>
ASCII'case letterCase superset -> [CaselessChar]
toCaselessCharList = forall a b. (a -> b) -> [a] -> [b]
List.map (Case -> Char -> CaselessChar
Caseless.assumeCaseUnsafe (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. ToString string => string -> [Char]
S.toCharListUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift

{-| Forces a string from a larger character set into cased ASCII by using the
    'ASCII.Substitute' character in place of any unacceptable characters -}
substituteString :: forall letterCase superset. KnownCase letterCase => StringSuperset superset =>
    superset -- ^ String which may or may not be valid ASCII, where letters may be in any case
    -> ASCII'case letterCase superset
substituteString :: forall (letterCase :: Case) superset.
(KnownCase letterCase, StringSuperset superset) =>
superset -> ASCII'case letterCase superset
substituteString = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. FromString string => [Char] -> string
S.fromCharList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
List.map Char -> Char
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. ToString string => string -> [Char]
S.toCharListSub
  where
    f :: Char -> Char
f Char
x = if Case -> Char -> Bool
Case.isCase (Case -> Case
Case.opposite (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)) Char
x
          then Char
ASCII.Substitute
          else Char
x

{-| Given a string from a larger set that is known to consist entirely of ASCII
    characters in a particular case, map over the characters in the string as if
    they were caseless ASCII characters -}
mapChars :: forall letterCase superset. KnownCase letterCase => StringSuperset superset =>
    (CaselessChar -> CaselessChar) -- ^ Case-insensitive function over ASCII characters
    -> ASCII'case letterCase superset -- ^ String that is known to be valid ASCII in a particular case
    -> ASCII'case letterCase superset
mapChars :: forall (letterCase :: Case) superset.
(KnownCase letterCase, StringSuperset superset) =>
(CaselessChar -> CaselessChar)
-> ASCII'case letterCase superset -> ASCII'case letterCase superset
mapChars CaselessChar -> CaselessChar
f = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string.
StringSuperset string =>
(Char -> Char) -> string -> string
S.mapCharsUnsafe Char -> Char
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift
  where
    g :: Char -> Char
g = Case -> CaselessChar -> Char
Caseless.toCase (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaselessChar -> CaselessChar
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> Char -> CaselessChar
Caseless.assumeCaseUnsafe (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase)

{-| Given an ASCII superset string that is known to be valid ASCII,
refine it further by converting it to a particular letter case -}
refineStringToCase :: forall letterCase char. KnownCase letterCase => StringSuperset char =>
    ASCII char -> ASCII'case letterCase char
refineStringToCase :: forall (letterCase :: Case) char.
(KnownCase letterCase, StringSuperset char) =>
ASCII char -> ASCII'case letterCase char
refineStringToCase = forall superset (letterCase :: Case).
superset -> ASCII'case letterCase superset
asciiCaseUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall string. StringSuperset string => Case -> string -> string
S.toCaseString (forall (letterCase :: Case). KnownCase letterCase => Case
theCase @letterCase) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall superset. ASCII superset -> superset
Refinement.lift