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.Case qualified as Case
import ASCII.Caseless (CaselessChar)
import ASCII.Caseless qualified as Caseless
import ASCII.Char qualified as ASCII
import {-# SOURCE #-} ASCII.Refinement.Internal (ASCII)
import {-# SOURCE #-} ASCII.Refinement.Internal qualified as Refinement
import ASCII.Superset (CharSuperset, StringSuperset)
import ASCII.Superset qualified as S
import Control.Monad (guard)
import Data.Bool qualified as Bool
import Data.Data (Data, Typeable)
import Data.Eq (Eq)
import Data.Foldable (any)
import Data.Function (($), (.))
import Data.Hashable (Hashable)
import Data.Kind (Type)
import Data.List qualified as List
import Data.Maybe (Maybe (..))
import Data.Monoid (Monoid)
import Data.Ord (Ord, (>))
import Data.Semigroup (Semigroup)
import GHC.Generics (Generic)
import Text.Show (Show, showList, showParen, showString, showsPrec)
import Prelude (succ)

-- | 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 :: Type) = ASCII'case_Unsafe
  { -- | Discard the evidence that the value is known to consist
    --           entirely of ASCII characters in a particular case
    forall (letterCase :: Case) superset.
ASCII'case letterCase superset -> superset
lift :: superset
  }

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 =>
  -- | Character which may or may not be in the ASCII character set;
  --                  if a letter, may be in any case
  superset ->
  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 =>
  -- | Character which, if it is a letter, does not have a specified case
  CaselessChar ->
  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 =>
  -- | Character that is known to be ASCII, and
  --                                        in the particular case if it is a letter
  ASCII'case letterCase superset ->
  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 =>
  -- | Case-insensitive function over ASCII characters
  (CaselessChar -> CaselessChar) ->
  -- | Character that is known to be ASCII, and
  --                                           in the particular case if it is a letter
  ASCII'case letterCase superset ->
  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 =>
  -- | String which may or may not be valid ASCII, where letters may be in any case
  superset ->
  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 =>
  -- | Case-insensitive ASCII string represented as a list of caseless characters
  [CaselessChar] ->
  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 =>
  -- | String that is known to be valid ASCII in a particular case
  ASCII'case letterCase superset ->
  [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 =>
  -- | String which may or may not be valid ASCII, where letters may be in any case
  superset ->
  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 =>
  -- | Case-insensitive function over ASCII characters
  (CaselessChar -> CaselessChar) ->
  -- | String that is known to be valid ASCII in a particular case
  ASCII'case letterCase superset ->
  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