{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}

module LAoP.Utils.Internal
  (
    -- * 'Natural' data type
    Natural(..),
    nat,

    -- * Coerce auxiliar functions to help promote 'Int' typed functions to
    -- 'Natural' typed functions.
    coerceNat,
    coerceNat2,
    coerceNat3,

    -- * 'List' data type
    List (..),

    -- * Category type class
    Category(..)
  )
where

import Data.Coerce
import Data.Proxy
import Data.List
import Data.Maybe
import GHC.TypeLits
import Control.DeepSeq
import GHC.Generics
import Data.Kind
import Prelude hiding (id, (.))
import qualified Prelude

-- | Wrapper around 'Int's that have a restrictive semantic associated.
-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
-- @i@ that's @n <= i <= m@.
newtype Natural (start :: Nat) (end :: Nat) = Nat Int
  deriving (Int -> Natural start end -> ShowS
[Natural start end] -> ShowS
Natural start end -> String
(Int -> Natural start end -> ShowS)
-> (Natural start end -> String)
-> ([Natural start end] -> ShowS)
-> Show (Natural start end)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (start :: Nat) (end :: Nat).
Int -> Natural start end -> ShowS
forall (start :: Nat) (end :: Nat). [Natural start end] -> ShowS
forall (start :: Nat) (end :: Nat). Natural start end -> String
showList :: [Natural start end] -> ShowS
$cshowList :: forall (start :: Nat) (end :: Nat). [Natural start end] -> ShowS
show :: Natural start end -> String
$cshow :: forall (start :: Nat) (end :: Nat). Natural start end -> String
showsPrec :: Int -> Natural start end -> ShowS
$cshowsPrec :: forall (start :: Nat) (end :: Nat).
Int -> Natural start end -> ShowS
Show, ReadPrec [Natural start end]
ReadPrec (Natural start end)
Int -> ReadS (Natural start end)
ReadS [Natural start end]
(Int -> ReadS (Natural start end))
-> ReadS [Natural start end]
-> ReadPrec (Natural start end)
-> ReadPrec [Natural start end]
-> Read (Natural start end)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (start :: Nat) (end :: Nat). ReadPrec [Natural start end]
forall (start :: Nat) (end :: Nat). ReadPrec (Natural start end)
forall (start :: Nat) (end :: Nat).
Int -> ReadS (Natural start end)
forall (start :: Nat) (end :: Nat). ReadS [Natural start end]
readListPrec :: ReadPrec [Natural start end]
$creadListPrec :: forall (start :: Nat) (end :: Nat). ReadPrec [Natural start end]
readPrec :: ReadPrec (Natural start end)
$creadPrec :: forall (start :: Nat) (end :: Nat). ReadPrec (Natural start end)
readList :: ReadS [Natural start end]
$creadList :: forall (start :: Nat) (end :: Nat). ReadS [Natural start end]
readsPrec :: Int -> ReadS (Natural start end)
$creadsPrec :: forall (start :: Nat) (end :: Nat).
Int -> ReadS (Natural start end)
Read, Natural start end -> Natural start end -> Bool
(Natural start end -> Natural start end -> Bool)
-> (Natural start end -> Natural start end -> Bool)
-> Eq (Natural start end)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
/= :: Natural start end -> Natural start end -> Bool
$c/= :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
== :: Natural start end -> Natural start end -> Bool
$c== :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
Eq, Eq (Natural start end)
Eq (Natural start end)
-> (Natural start end -> Natural start end -> Ordering)
-> (Natural start end -> Natural start end -> Bool)
-> (Natural start end -> Natural start end -> Bool)
-> (Natural start end -> Natural start end -> Bool)
-> (Natural start end -> Natural start end -> Bool)
-> (Natural start end -> Natural start end -> Natural start end)
-> (Natural start end -> Natural start end -> Natural start end)
-> Ord (Natural start end)
Natural start end -> Natural start end -> Bool
Natural start end -> Natural start end -> Ordering
Natural start end -> Natural start end -> Natural start end
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
forall (start :: Nat) (end :: Nat). Eq (Natural start end)
forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Ordering
forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Natural start end
min :: Natural start end -> Natural start end -> Natural start end
$cmin :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Natural start end
max :: Natural start end -> Natural start end -> Natural start end
$cmax :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Natural start end
>= :: Natural start end -> Natural start end -> Bool
$c>= :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
> :: Natural start end -> Natural start end -> Bool
$c> :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
<= :: Natural start end -> Natural start end -> Bool
$c<= :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
< :: Natural start end -> Natural start end -> Bool
$c< :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Bool
compare :: Natural start end -> Natural start end -> Ordering
$ccompare :: forall (start :: Nat) (end :: Nat).
Natural start end -> Natural start end -> Ordering
$cp1Ord :: forall (start :: Nat) (end :: Nat). Eq (Natural start end)
Ord, Natural start end -> ()
(Natural start end -> ()) -> NFData (Natural start end)
forall a. (a -> ()) -> NFData a
forall (start :: Nat) (end :: Nat). Natural start end -> ()
rnf :: Natural start end -> ()
$crnf :: forall (start :: Nat) (end :: Nat). Natural start end -> ()
NFData, (forall x. Natural start end -> Rep (Natural start end) x)
-> (forall x. Rep (Natural start end) x -> Natural start end)
-> Generic (Natural start end)
forall x. Rep (Natural start end) x -> Natural start end
forall x. Natural start end -> Rep (Natural start end) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (start :: Nat) (end :: Nat) x.
Rep (Natural start end) x -> Natural start end
forall (start :: Nat) (end :: Nat) x.
Natural start end -> Rep (Natural start end) x
$cto :: forall (start :: Nat) (end :: Nat) x.
Rep (Natural start end) x -> Natural start end
$cfrom :: forall (start :: Nat) (end :: Nat) x.
Natural start end -> Rep (Natural start end) x
Generic)

-- | Throws a runtime error if any of the operations overflows or
-- underflows.
instance (KnownNat n, KnownNat m) => Num (Natural n m) where
    (Nat Int
a) + :: Natural n m -> Natural n m -> Natural n m
+ (Nat Int
b) = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)
    (Nat Int
a) - :: Natural n m -> Natural n m -> Natural n m
- (Nat Int
b) = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b)
    (Nat Int
a) * :: Natural n m -> Natural n m -> Natural n m
* (Nat Int
b) = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
b)
    abs :: Natural n m -> Natural n m
abs (Nat Int
a) = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Int -> Int
forall a. Num a => a -> a
abs Int
a)
    signum :: Natural n m -> Natural n m
signum (Nat Int
a) = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Int -> Int
forall a. Num a => a -> a
signum Int
a)
    fromInteger :: Integer -> Natural n m
fromInteger Integer
i = Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat @n @m (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)

-- | Natural constructor function. Throws a runtime error if the 'Int'
-- value is greater than the corresponding @m@ or lower than @n@ in the @'Natural' n m@ type.
nat :: forall n m . (KnownNat n, KnownNat m) => Int -> Natural n m
nat :: Int -> Natural n m
nat Int
i =
  let start :: Int
start = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))
      end :: Int
end   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))
   in if Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end
        then Int -> Natural n m
forall (start :: Nat) (end :: Nat). Int -> Natural start end
Nat Int
i
        else String -> Natural n m
forall a. HasCallStack => String -> a
error String
"Off limits"

-- | Auxiliary function that promotes binary 'Int' functions to 'Natural'
-- binary functions.
coerceNat :: (Int -> Int -> Int) -> (Natural a a' -> Natural b b' -> Natural c c')
coerceNat :: (Int -> Int -> Int) -> Natural a a' -> Natural b b' -> Natural c c'
coerceNat = (Int -> Int -> Int) -> Natural a a' -> Natural b b' -> Natural c c'
coerce

-- | Auxiliary function that promotes ternary (binary) 'Int' functions to 'Natural'
-- functions.
coerceNat2 :: ((Int, Int) -> Int -> Int) -> ((Natural a a', Natural b b') -> Natural c c' -> Natural d d')
coerceNat2 :: ((Int, Int) -> Int -> Int)
-> (Natural a a', Natural b b') -> Natural c c' -> Natural d d'
coerceNat2 = ((Int, Int) -> Int -> Int)
-> (Natural a a', Natural b b') -> Natural c c' -> Natural d d'
coerce

-- | Auxiliary function that promotes ternary (binary) 'Int' functions to 'Natural'
-- functions.
coerceNat3 :: (Int -> Int -> a) -> (Natural b b' -> Natural c c' -> a) 
coerceNat3 :: (Int -> Int -> a) -> Natural b b' -> Natural c c' -> a
coerceNat3 = (Int -> Int -> a) -> Natural b b' -> Natural c c' -> a
coerce

instance (KnownNat n, KnownNat m) => Bounded (Natural n m) where
  minBound :: Natural n m
minBound = Int -> Natural n m
forall (start :: Nat) (end :: Nat). Int -> Natural start end
Nat (Int -> Natural n m) -> Int -> Natural n m
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))
  maxBound :: Natural n m
maxBound = Int -> Natural n m
forall (start :: Nat) (end :: Nat). Int -> Natural start end
Nat (Int -> Natural n m) -> Int -> Natural n m
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))

instance (KnownNat n, KnownNat m) => Enum (Natural n m) where
  toEnum :: Int -> Natural n m
toEnum Int
i = 
      let start :: Int
start = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))
       in Int -> Natural n m
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)
  -- | Throws a runtime error if the value is off limits
  fromEnum :: Natural n m -> Int
fromEnum (Nat Int
nat) =
    let start :: Int
start = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))
        end :: Int
end   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))
     in if Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
nat Bool -> Bool -> Bool
&& Int
nat Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end
          then Int
nat Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
start
          else String -> Int
forall a. HasCallStack => String -> a
error String
"Off limits"

-- | Optimized 'Enum' instance for tuples that comply with the given
-- constraints.
instance
  ( Enum a,
    Enum b,
    Bounded b
  ) =>
  Enum (a, b)
  where

  toEnum :: Int -> (a, b)
toEnum Int
i =
    let ([b]
listB :: [b]) = [b
forall a. Bounded a => a
minBound .. b
forall a. Bounded a => a
maxBound]
        lengthB :: Int
lengthB = [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
listB
        fstI :: Int
fstI = Int -> Int -> Int
forall a. Integral a => a -> a -> a
div Int
i Int
lengthB
        sndI :: Int
sndI = Int -> Int -> Int
forall a. Integral a => a -> a -> a
mod Int
i Int
lengthB
     in (Int -> a
forall a. Enum a => Int -> a
toEnum Int
fstI, Int -> b
forall a. Enum a => Int -> a
toEnum Int
sndI)

  fromEnum :: (a, b) -> Int
fromEnum (a
a, b
b) =
    let ([b]
listB :: [b]) = [b
forall a. Bounded a => a
minBound .. b
forall a. Bounded a => a
maxBound]
        lengthB :: Int
lengthB = [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
listB
        fstI :: Int
fstI = a -> Int
forall a. Enum a => a -> Int
fromEnum a
a
        sndI :: Int
sndI = b -> Int
forall a. Enum a => a -> Int
fromEnum b
b
     in Int
fstI Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
lengthB Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sndI

instance
  ( Bounded a,
    Bounded b
  ) => Bounded (Either a b)
  where
  minBound :: Either a b
minBound = a -> Either a b
forall a b. a -> Either a b
Left (a
forall a. Bounded a => a
minBound :: a)
  maxBound :: Either a b
maxBound = b -> Either a b
forall a b. b -> Either a b
Right (b
forall a. Bounded a => a
maxBound :: b)

instance
  ( Enum a,
    Bounded a,
    Enum b,
    Bounded b
  ) => Enum (Either a b)
  where
  toEnum :: Int -> Either a b
toEnum Int
i =
      let la :: [Either a b]
la = (a -> Either a b) -> [a] -> [Either a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left ([a
forall a. Bounded a => a
minBound..a
forall a. Bounded a => a
maxBound] :: [a])
          lb :: [Either a b]
lb = (b -> Either a b) -> [b] -> [Either a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either a b
forall a b. b -> Either a b
Right ([b
forall a. Bounded a => a
minBound..b
forall a. Bounded a => a
maxBound] :: [b])
       in ([Either a b]
la [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
++ [Either a b]
lb) [Either a b] -> Int -> Either a b
forall a. [a] -> Int -> a
!! Int
i

  fromEnum :: Either a b -> Int
fromEnum (Left a
a) = a -> Int
forall a. Enum a => a -> Int
fromEnum a
a
  fromEnum (Right b
b) = a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
maxBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ b -> Int
forall a. Enum a => a -> Int
fromEnum b
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

-- | Powerset data type.
--
-- This data type is a newtype wrapper around '[]'. This exists in order to
-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.
newtype List a = L [a]
  deriving (List a -> List a -> Bool
(List a -> List a -> Bool)
-> (List a -> List a -> Bool) -> Eq (List a)
forall a. Eq a => List a -> List a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: List a -> List a -> Bool
$c/= :: forall a. Eq a => List a -> List a -> Bool
== :: List a -> List a -> Bool
$c== :: forall a. Eq a => List a -> List a -> Bool
Eq, Int -> List a -> ShowS
[List a] -> ShowS
List a -> String
(Int -> List a -> ShowS)
-> (List a -> String) -> ([List a] -> ShowS) -> Show (List a)
forall a. Show a => Int -> List a -> ShowS
forall a. Show a => [List a] -> ShowS
forall a. Show a => List a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [List a] -> ShowS
$cshowList :: forall a. Show a => [List a] -> ShowS
show :: List a -> String
$cshow :: forall a. Show a => List a -> String
showsPrec :: Int -> List a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> List a -> ShowS
Show, ReadPrec [List a]
ReadPrec (List a)
Int -> ReadS (List a)
ReadS [List a]
(Int -> ReadS (List a))
-> ReadS [List a]
-> ReadPrec (List a)
-> ReadPrec [List a]
-> Read (List a)
forall a. Read a => ReadPrec [List a]
forall a. Read a => ReadPrec (List a)
forall a. Read a => Int -> ReadS (List a)
forall a. Read a => ReadS [List a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [List a]
$creadListPrec :: forall a. Read a => ReadPrec [List a]
readPrec :: ReadPrec (List a)
$creadPrec :: forall a. Read a => ReadPrec (List a)
readList :: ReadS [List a]
$creadList :: forall a. Read a => ReadS [List a]
readsPrec :: Int -> ReadS (List a)
$creadsPrec :: forall a. Read a => Int -> ReadS (List a)
Read)

powerset :: [a] -> [[a]]
powerset :: [a] -> [[a]]
powerset [] = [[]]
powerset (a
x:[a]
xs) = [a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
xs [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ps | [a]
ps <- [a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
xs]

instance
  ( Enum a,
    Bounded a
  ) => Bounded (List a)
  where
  minBound :: List a
minBound = [a] -> List a
forall a. [a] -> List a
L [] 
  maxBound :: List a
maxBound = [a] -> List a
forall a. [a] -> List a
L [a
forall a. Bounded a => a
minBound .. a
forall a. Bounded a => a
maxBound]

instance
  ( Bounded a,
    Enum a,
    Eq a
  ) => Enum (List a)
  where
  toEnum :: Int -> List a
toEnum Int
i =
    let as :: [a]
as = [a
forall a. Bounded a => a
minBound .. a
forall a. Bounded a => a
maxBound]
        in [a] -> List a
forall a. [a] -> List a
L ([a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
as [[a]] -> Int -> [a]
forall a. [a] -> Int -> a
!! Int
i)

  fromEnum :: List a -> Int
fromEnum (L []) = Int
0
  fromEnum (L [a]
x) = 
    let as :: [a]
as = [a
forall a. Bounded a => a
minBound .. a
forall a. Bounded a => a
maxBound]
        in Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
"Does not exist") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ [a] -> [[a]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [a]
x ([a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
as)

-- | Constrained category instance
class Category k where
  type Object k o :: Constraint
  type Object k o = ()
  id :: Object k a => k a a
  (.) :: k b c -> k a b -> k a c

{-# RULES
"identity/left" forall p .
                id . p = p
"identity/right"        forall p .
                p . id = p
"association"   forall p q r .
                (p . q) . r = p . (q . r)
 #-}

instance Category (->) where
  id :: a -> a
id = a -> a
forall a. a -> a
Prelude.id
  . :: (b -> c) -> (a -> b) -> a -> c
(.) = (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(Prelude..)