module Morley.Util.Generic
( mkGenericTree
, mkGenericTreeVec
, GenericTypeName
, GRep
, NiceGeneric
) where
import Control.Exception (assert)
import Data.Vector qualified as V
import GHC.Generics qualified as G
import GHC.TypeLits (Symbol)
import Type.Errors (ErrorMessage(..), IfStuck, Pure, TypeError)
import Unsafe qualified (fromIntegral)
mkGenericTree :: (Natural -> a -> a -> a) -> NonEmpty a -> a
mkGenericTree :: forall a. (Natural -> a -> a -> a) -> NonEmpty a -> a
mkGenericTree Natural -> a -> a -> a
mkNode = (a -> a) -> (Natural -> a -> a -> a) -> Vector a -> a
forall a b.
HasCallStack =>
(a -> b) -> (Natural -> b -> b -> b) -> Vector a -> b
mkGenericTreeVec a -> a
forall a. a -> a
id Natural -> a -> a -> a
mkNode (Vector a -> a) -> (NonEmpty a -> Vector a) -> NonEmpty a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Vector a
forall a. [a] -> Vector a
V.fromList ([a] -> Vector a) -> (NonEmpty a -> [a]) -> NonEmpty a -> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> [a]
NonEmpty a -> [Element (NonEmpty a)]
forall t. Container t => t -> [Element t]
toList
mkGenericTreeVec
:: HasCallStack
=> (a -> b) -> (Natural -> b -> b -> b) -> V.Vector a -> b
mkGenericTreeVec :: forall a b.
HasCallStack =>
(a -> b) -> (Natural -> b -> b -> b) -> Vector a -> b
mkGenericTreeVec a -> b
mkLeaf Natural -> b -> b -> b
mkNode Vector a
vector
| Vector a -> Bool
forall a. Vector a -> Bool
V.null Vector a
vector = Text -> b
forall a. HasCallStack => Text -> a
error Text
"Empty vector"
| Bool
otherwise = Int -> Vector a -> b
mkTreeDo Int
0 Vector a
vector
where
mkTreeDo :: Int -> Vector a -> b
mkTreeDo Int
idxBase Vector a
es
| Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = a -> b
mkLeaf (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Vector a -> a
forall a. Vector a -> a
V.head Vector a
es
| Bool
otherwise = Bool -> b -> b
forall a. HasCallStack => Bool -> a -> a
assert (Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$
let mid :: Int
mid = Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
es Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
mid' :: Int
mid' = Int
idxBase Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
mid
(Vector a
h, Vector a
t) = Int -> Vector a -> (Vector a, Vector a)
forall a. Int -> Vector a -> (Vector a, Vector a)
V.splitAt Int
mid Vector a
es
in Natural -> b -> b -> b
mkNode (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Int @Natural Int
mid') (Int -> Vector a -> b
mkTreeDo Int
idxBase Vector a
h) (Int -> Vector a -> b
mkTreeDo Int
mid' Vector a
t)
type GenericTypeName a = GTypeName (GRep a)
type family GTypeName (x :: Type -> Type) :: Symbol where
GTypeName (G.D1 ('G.MetaData tyName _ _ _) _) = tyName
data ThisTypeShallNotBeExported
type family GRep t where
GRep ThisTypeShallNotBeExported = TypeError ('Text "impossible")
GRep t = IfStuck (G.Rep t) (TypeError (GRepErrorMsg t)) (Pure (G.Rep t))
type GRepErrorMsg t = 'ShowType (G.Rep t)
':$$: 'Text "is stuck. Likely"
':$$: 'ShowType (Generic t)
':$$: 'Text "instance is missing or out of scope."
type NiceGeneric t = (Generic t, GRep t ~ G.Rep t)