{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Taiwan.ID.Utilities where

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, type (<=), type (+) )
import GHC.TypeNats
  ( Nat, type (-), natVal )
import Numeric.Natural
  ( Natural )

cardinality :: forall a. Finitary a => Natural
cardinality :: forall a. Finitary a => Natural
cardinality = Proxy (Cardinality a) -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy (Cardinality a) -> Natural)
-> Proxy (Cardinality a) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Cardinality a)

guard :: x -> Maybe y -> Either x y
guard :: forall x y. x -> Maybe y -> Either x y
guard x
x = Either x y -> (y -> Either x y) -> Maybe y -> Either x y
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (x -> Either x y
forall a b. a -> Either a b
Left x
x) y -> Either x y
forall a b. b -> Either a b
Right

maybeFinitary :: forall a. Finitary a => Natural -> Maybe a
maybeFinitary :: forall a. Finitary a => Natural -> Maybe a
maybeFinitary = (Finite (Cardinality a) -> a)
-> Maybe (Finite (Cardinality a)) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Maybe (Finite (Cardinality a)) -> Maybe a)
-> (Natural -> Maybe (Finite (Cardinality a)))
-> Natural
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Maybe (Finite (Cardinality a))
forall (n :: Natural). KnownNat n => Integer -> Maybe (Finite n)
packFinite (Integer -> Maybe (Finite (Cardinality a)))
-> (Natural -> Integer)
-> Natural
-> Maybe (Finite (Cardinality a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @Natural @Integer

randomFinitary
  :: forall m a. (MonadRandom m, Finitary a, 1 <= Cardinality a) => m a
randomFinitary :: forall (m :: * -> *) a.
(MonadRandom m, Finitary a, 1 <= Cardinality a) =>
m a
randomFinitary =
    a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
forall {a}. a
failure (Maybe a -> a) -> (Natural -> Maybe a) -> Natural -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Maybe a
forall a. Finitary a => Natural -> Maybe a
maybeFinitary (Natural -> a) -> m Natural -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Natural, Natural) -> m Natural
forall (m :: * -> *).
MonadRandom m =>
(Natural, Natural) -> m Natural
randomNatural (Natural
0, forall a. Finitary a => Natural
cardinality @a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
  where
    failure :: a
failure = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"randomFinitary: unexpected out-of-bounds value"

randomNatural :: MonadRandom m => (Natural, Natural) -> m Natural
randomNatural :: forall (m :: * -> *).
MonadRandom m =>
(Natural, Natural) -> m Natural
randomNatural (Natural
lo, Natural
hi) =
  forall a b. (Integral a, Num b) => a -> b
fromIntegral @Integer @Natural (Integer -> Natural) -> m Integer -> m Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (Integer, Integer) -> m Integer
forall a. Random a => (a, a) -> m a
forall (m :: * -> *) a. (MonadRandom m, Random a) => (a, a) -> m a
getRandomR
      ( forall a b. (Integral a, Num b) => a -> b
fromIntegral @Natural @Integer Natural
lo
      , forall a b. (Integral a, Num b) => a -> b
fromIntegral @Natural @Integer Natural
hi
      )

type family FromJust (m :: Maybe a) e where
  FromJust Nothing e = e
  FromJust (Just a) _ = a

type family Fst (t :: (a, a)) :: a where
  Fst '(x, _) = x

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]
  where
    SymbolToCharList s = MaybeCharSymbolToCharList (UnconsSymbol s)

type family
  MaybeCharSymbolToCharList
    (m :: Maybe (Char, Symbol)) :: [Char]
  where
    MaybeCharSymbolToCharList ('Just '(c, rest)) = c ': SymbolToCharList rest
    MaybeCharSymbolToCharList 'Nothing = '[]

type family ReplicateChar (n :: Nat) (c :: Char) :: Symbol where
  ReplicateChar n c = ReplicateChar' "" n c

type family ReplicateChar' (s :: Symbol) (n :: Nat) (c :: Char) :: Symbol where
  ReplicateChar' s 0 _ = s
  ReplicateChar' s n c = ReplicateChar' (ConsSymbol c s) (n - 1) c