{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# LANGUAGE BangPatterns #-}
module Data.Functor.Pow (
  -- * Powers of a functor 
  Pow(..), Pow'(..),
  functionToPow, powToFunction,
  
  -- * Tag of powers of a polynomial functor
  TagPow(..), TagPow'(..),
  geqPow, geqPow', gcomparePow, gcomparePow'
) where

import GHC.TypeNats
import GHC.TypeNats.Extra ( SNat(Succ, Zero) )
import Data.Finite
import Data.Void
import Data.Type.Equality ( type (:~:)(..) )

import Data.GADT.HasFinitary
import Data.GADT.Show ( GShow(..) )
import Data.GADT.Compare
import Data.GADT.Compare.Extra ((>>?))
import Data.Some (Some(..))
import Unsafe.Coerce (unsafeCoerce)
import Data.Finite.Extra (combineSumS, separateSumS, absurdFinite)


-- | @Pow n f = f :*: f :*: ...(n)... :*: f@
data Pow n f x where
  Pow0 :: Pow 0 f x
  PowNZ :: Pow' n f x -> Pow n f x

deriving instance Functor f => Functor (Pow n f)
data Pow' n f x where
  Pow1 :: f x -> Pow' 1 f x
  PowEven :: (KnownNat n, n ~ m * 2) => Pow' m f x -> Pow' m f x -> Pow' n f x
  PowOdd  :: (KnownNat n, n ~ m * 2 + 1) => f x -> Pow' m f x -> Pow' m f x -> Pow' n f x

deriving instance Functor f => Functor (Pow' n f)

withKnownNatPow' :: Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k) r.
Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' Pow' n f x
fs KnownNat n => r
body = case Pow' n f x
fs of
  Pow1{} -> r
KnownNat n => r
body
  PowEven{} -> r
KnownNat n => r
body
  PowOdd{} -> r
KnownNat n => r
body

powEven :: Pow n f x -> Pow n f x -> Pow (n * 2) f x
powEven :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow n f x -> Pow n f x -> Pow (n * 2) f x
powEven Pow n f x
Pow0 Pow n f x
Pow0 = Pow 0 f x
Pow (n * 2) f x
forall {k} (f :: k -> Type) (x :: k). Pow 0 f x
Pow0
powEven (PowNZ Pow' n f x
l) (PowNZ Pow' n f x
r) = Pow' n f x -> (KnownNat n => Pow (n * 2) f x) -> Pow (n * 2) f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k) r.
Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' Pow' n f x
l ((KnownNat n => Pow (n * 2) f x) -> Pow (n * 2) f x)
-> (KnownNat n => Pow (n * 2) f x) -> Pow (n * 2) f x
forall a b. (a -> b) -> a -> b
$ Pow' (n * 2) f x -> Pow (n * 2) f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Pow n f x
PowNZ (Pow' n f x -> Pow' n f x -> Pow' (n * 2) f x
forall {k} (n :: Natural) (n :: Natural) (f :: k -> Type) (x :: k).
(KnownNat n, n ~ (n * 2)) =>
Pow' n f x -> Pow' n f x -> Pow' n f x
PowEven Pow' n f x
l Pow' n f x
r)
powEven !Pow n f x
_ !Pow n f x
_ = [Char] -> Pow (n * 2) f x
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"

powOdd :: f x -> Pow n f x -> Pow n f x -> Pow (n * 2 + 1) f x
powOdd :: forall {k} (f :: k -> Type) (x :: k) (n :: Natural).
f x -> Pow n f x -> Pow n f x -> Pow ((n * 2) + 1) f x
powOdd f x
f0 (PowNZ Pow' n f x
l) (PowNZ Pow' n f x
r) = Pow' n f x
-> (KnownNat n => Pow ((n * 2) + 1) f x) -> Pow ((n * 2) + 1) f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k) r.
Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' Pow' n f x
l ((KnownNat n => Pow ((n * 2) + 1) f x) -> Pow ((n * 2) + 1) f x)
-> (KnownNat n => Pow ((n * 2) + 1) f x) -> Pow ((n * 2) + 1) f x
forall a b. (a -> b) -> a -> b
$ Pow' ((n * 2) + 1) f x -> Pow ((n * 2) + 1) f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Pow n f x
PowNZ (f x -> Pow' n f x -> Pow' n f x -> Pow' ((n * 2) + 1) f x
forall {k} (n :: Natural) (n :: Natural) (f :: k -> Type) (x :: k).
(KnownNat n, n ~ ((n * 2) + 1)) =>
f x -> Pow' n f x -> Pow' n f x -> Pow' n f x
PowOdd f x
f0 Pow' n f x
l Pow' n f x
r)
powOdd f x
_ !Pow n f x
_ !Pow n f x
_ = [Char] -> Pow ((n * 2) + 1) f x
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"

functionToPow :: SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat n
sn Finite n -> f x
f = case SNat n -> BinView n
forall (n :: Natural). SNat n -> BinView n
binView SNat n
sn of
  BinView n
View0 -> Pow n f x
Pow 0 f x
forall {k} (f :: k -> Type) (x :: k). Pow 0 f x
Pow0
  ViewNZ BinView' n
View1 -> Pow' n f x -> Pow n f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Pow n f x
PowNZ (f x -> Pow' 1 f x
forall {k} (f :: k -> Type) (x :: k). f x -> Pow' 1 f x
Pow1 (Finite n -> f x
f Finite n
forall a. Bounded a => a
minBound))
  ViewNZ (ViewEven SNat n
sn') ->
    let f1 :: Finite n -> f x
f1 = Finite n -> f x
f (Finite n -> f x) -> (Finite n -> Finite n) -> Finite n -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat n -> Either (Finite n) (Finite n) -> Finite (n + n)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Either (Finite l) (Finite r) -> Finite (l + r)
combineSumS SNat n
sn' SNat n
sn' (Either (Finite n) (Finite n) -> Finite n)
-> (Finite n -> Either (Finite n) (Finite n))
-> Finite n
-> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Either (Finite n) (Finite n)
forall a b. a -> Either a b
Left
        f2 :: Finite n -> f x
f2 = Finite n -> f x
f (Finite n -> f x) -> (Finite n -> Finite n) -> Finite n -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat n -> Either (Finite n) (Finite n) -> Finite (n + n)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Either (Finite l) (Finite r) -> Finite (l + r)
combineSumS SNat n
sn' SNat n
sn' (Either (Finite n) (Finite n) -> Finite n)
-> (Finite n -> Either (Finite n) (Finite n))
-> Finite n
-> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Either (Finite n) (Finite n)
forall a b. b -> Either a b
Right
    in Pow n f x -> Pow n f x -> Pow (n * 2) f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow n f x -> Pow n f x -> Pow (n * 2) f x
powEven (SNat n -> (Finite n -> f x) -> Pow n f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat n
sn' Finite n -> f x
f1) (SNat n -> (Finite n -> f x) -> Pow n f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat n
sn' Finite n -> f x
f2)
  ViewNZ (ViewOdd SNat n
sn') ->
    let f0 :: f x
f0 = SNat n -> (KnownNat n => f x) -> f x
forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn (Finite n -> f x
f Finite n
forall a. Bounded a => a
minBound)
        f1 :: Finite n -> f x
f1 = Finite n -> f x
f (Finite n -> f x) -> (Finite n -> Finite n) -> Finite n -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (n * 2) -> Finite n
Finite (n * 2) -> Finite ((n * 2) + 1)
forall (n :: Natural). Finite n -> Finite (n + 1)
shift (Finite (n * 2) -> Finite n)
-> (Finite n -> Finite (n * 2)) -> Finite n -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat n -> Either (Finite n) (Finite n) -> Finite (n + n)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Either (Finite l) (Finite r) -> Finite (l + r)
combineSumS SNat n
sn' SNat n
sn' (Either (Finite n) (Finite n) -> Finite (n * 2))
-> (Finite n -> Either (Finite n) (Finite n))
-> Finite n
-> Finite (n * 2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Either (Finite n) (Finite n)
forall a b. a -> Either a b
Left
        f2 :: Finite n -> f x
f2 = Finite n -> f x
f (Finite n -> f x) -> (Finite n -> Finite n) -> Finite n -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (n * 2) -> Finite n
Finite (n * 2) -> Finite ((n * 2) + 1)
forall (n :: Natural). Finite n -> Finite (n + 1)
shift (Finite (n * 2) -> Finite n)
-> (Finite n -> Finite (n * 2)) -> Finite n -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat n -> Either (Finite n) (Finite n) -> Finite (n + n)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Either (Finite l) (Finite r) -> Finite (l + r)
combineSumS SNat n
sn' SNat n
sn' (Either (Finite n) (Finite n) -> Finite (n * 2))
-> (Finite n -> Either (Finite n) (Finite n))
-> Finite n
-> Finite (n * 2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Either (Finite n) (Finite n)
forall a b. b -> Either a b
Right
    in f x -> Pow n f x -> Pow n f x -> Pow ((n * 2) + 1) f x
forall {k} (f :: k -> Type) (x :: k) (n :: Natural).
f x -> Pow n f x -> Pow n f x -> Pow ((n * 2) + 1) f x
powOdd f x
f0 (SNat n -> (Finite n -> f x) -> Pow n f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat n
sn' Finite n -> f x
f1) (SNat n -> (Finite n -> f x) -> Pow n f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat n
sn' Finite n -> f x
f2)

powToFunction :: Pow n f x -> Finite n -> f x
powToFunction :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow n f x -> Finite n -> f x
powToFunction Pow n f x
Pow0 = Finite Integer n -> f x
Finite 0 -> f x
forall a. Finite 0 -> a
absurdFinite
powToFunction (PowNZ Pow' n f x
fs) = Pow' n f x -> Finite Integer n -> f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' Pow' n f x
fs

powToFunction' :: Pow' n f x -> Finite n -> f x
powToFunction' :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' (Pow1 f x
fx) Finite n
_ = f x
fx
powToFunction' (PowEven Pow' m f x
fs1 Pow' m f x
fs2) Finite n
k =
  case SNat m -> SNat m -> Finite (m + m) -> Either (Finite m) (Finite m)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Finite (l + r) -> Either (Finite l) (Finite r)
separateSumS SNat m
sn' SNat m
sn' Finite n
Finite (m + m)
k of
      Left Finite m
k1 -> Pow' m f x -> Finite m -> f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' Pow' m f x
fs1 Finite m
k1
      Right Finite m
k2 -> Pow' m f x -> Finite m -> f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' Pow' m f x
fs2 Finite m
k2
  where
    sn' :: SNat m
sn' = Pow' m f x -> (KnownNat m => SNat m) -> SNat m
forall {k} (n :: Natural) (f :: k -> Type) (x :: k) r.
Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' Pow' m f x
fs1 SNat m
KnownNat m => SNat m
forall (n :: Natural). KnownNat n => SNat n
SNat
powToFunction' (PowOdd f x
f0 Pow' m f x
fs1 Pow' m f x
fs2) Finite n
k =
  case Finite ((m * 2) + 1) -> Maybe (Finite (m * 2))
forall (n :: Natural). Finite (n + 1) -> Maybe (Finite n)
unshift Finite n
Finite ((m * 2) + 1)
k of
    Maybe (Finite (m * 2))
Nothing -> f x
f0
    Just Finite (m * 2)
k' -> case SNat m -> SNat m -> Finite (m + m) -> Either (Finite m) (Finite m)
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Finite (l + r) -> Either (Finite l) (Finite r)
separateSumS SNat m
sn' SNat m
sn' Finite (m + m)
Finite (m * 2)
k' of
      Left Finite m
k1 -> Pow' m f x -> Finite m -> f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' Pow' m f x
fs1 Finite m
k1
      Right Finite m
k2 -> Pow' m f x -> Finite m -> f x
forall {k} (n :: Natural) (f :: k -> Type) (x :: k).
Pow' n f x -> Finite n -> f x
powToFunction' Pow' m f x
fs2 Finite m
k2
  where
    sn' :: SNat m
sn' = Pow' m f x -> (KnownNat m => SNat m) -> SNat m
forall {k} (n :: Natural) (f :: k -> Type) (x :: k) r.
Pow' n f x -> (KnownNat n => r) -> r
withKnownNatPow' Pow' m f x
fs1 SNat m
KnownNat m => SNat m
forall (n :: Natural). KnownNat n => SNat n
SNat

-- * Tag for Pow of polynomial functors

-- | When @t@ represents @(U,α :: U -> Type)@,
--   @TagPow n t xs@ represents @α^n@ below:
--
--   > α^n :: U^n -> Type
--   > α^n(u1, u2, ..., u_n) = α u1 + α u2 + ... + α u_n
--
--   This is the tag of @'Pow' n f@ when @t@ is the tag of @f@.
data TagPow n t xs where
  TagPow0 :: TagPow 0 t Void
  TagPowNZ :: TagPow' n t xs -> TagPow n t xs

deriving instance (forall n. Show (t n)) => Show (TagPow m t xs)

instance (forall n. Show (t n)) => GShow (TagPow m t) where
  gshowsPrec :: forall a. Int -> TagPow m t a -> ShowS
gshowsPrec = Int -> TagPow m t a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance (HasFinitary t) => HasFinitary (TagPow n t) where
  withFinitary :: forall n r. TagPow n t n -> (Finitary n => r) -> r
withFinitary TagPow n t n
TagPow0 Finitary n => r
body = r
Finitary n => r
body
  withFinitary (TagPowNZ TagPow' n t n
ts) Finitary n => r
body = TagPow' n t n -> (Finitary n => r) -> r
forall n r. TagPow' n t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow' n t n
ts r
Finitary n => r
body

instance GEq t => GEq (TagPow n t) where
  geq :: forall a b. TagPow n t a -> TagPow n t b -> Maybe (a :~: b)
geq TagPow n t a
t TagPow n t b
t' = ((n :~: n, a :~: b) -> a :~: b)
-> Maybe (n :~: n, a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (n :~: n, a :~: b) -> a :~: b
forall a b. (a, b) -> b
snd (TagPow n t a -> TagPow n t b -> Maybe (n :~: n, a :~: b)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow n t xs -> TagPow n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow TagPow n t a
t TagPow n t b
t')

instance GEq t => Eq (TagPow n t xs) where
  == :: TagPow n t xs -> TagPow n t xs -> Bool
(==) = TagPow n t xs -> TagPow n t xs -> Bool
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance GCompare t => GCompare (TagPow n t) where
  gcompare :: forall a b. TagPow n t a -> TagPow n t b -> GOrdering a b
gcompare TagPow n t a
t TagPow n t b
t' = TagPow n t a -> TagPow n t b -> GOrdering '(n, a) '(n, b)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GCompare t =>
TagPow n t xs -> TagPow n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow TagPow n t a
t TagPow n t b
t' GOrdering '(n, a) '(n, b)
-> (('(n, a) ~ '(n, b)) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering a a
GOrdering a b
('(n, a) ~ '(n, b)) => GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

instance GCompare t => Ord (TagPow n t xs) where
  compare :: TagPow n t xs -> TagPow n t xs -> Ordering
compare = TagPow n t xs -> TagPow n t xs -> Ordering
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

data TagPow' n t xs where
  TagPow1 :: t x -> TagPow' 1 t x
  TagPowEven :: (KnownNat n, n ~ m * 2) => TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either xs1 xs2)
  TagPowOdd :: (KnownNat n, n ~ m * 2 + 1) => t x -> TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either x (Either xs1 xs2))

instance HasFinitary t => HasFinitary (TagPow' n t) where
  withFinitary :: forall n r. TagPow' n t n -> (Finitary n => r) -> r
withFinitary TagPow' n t n
ts Finitary n => r
body = case TagPow' n t n
ts of
    TagPow1 t n
t -> t n -> (Finitary n => r) -> r
forall n r. t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t n
t r
Finitary n => r
body
    TagPowEven TagPow' m t xs1
ts1 TagPow' m t xs2
ts2 -> TagPow' m t xs1 -> (Finitary xs1 => r) -> r
forall n r. TagPow' m t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow' m t xs1
ts1 ((Finitary xs1 => r) -> r) -> (Finitary xs1 => r) -> r
forall a b. (a -> b) -> a -> b
$ TagPow' m t xs2 -> (Finitary xs2 => r) -> r
forall n r. TagPow' m t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow' m t xs2
ts2 r
Finitary n => r
Finitary xs2 => r
body
    TagPowOdd t x
t0 TagPow' m t xs1
ts1 TagPow' m t xs2
ts2 -> t x -> (Finitary x => r) -> r
forall n r. t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t x
t0 ((Finitary x => r) -> r) -> (Finitary x => r) -> r
forall a b. (a -> b) -> a -> b
$ TagPow' m t xs1 -> (Finitary xs1 => r) -> r
forall n r. TagPow' m t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow' m t xs1
ts1 ((Finitary xs1 => r) -> r) -> (Finitary xs1 => r) -> r
forall a b. (a -> b) -> a -> b
$ TagPow' m t xs2 -> (Finitary xs2 => r) -> r
forall n r. TagPow' m t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow' m t xs2
ts2 r
Finitary n => r
Finitary xs2 => r
body

deriving instance (forall m. Show (t m)) => Show (TagPow' n t xs)

instance (forall m. Show (t m)) => GShow (TagPow' n t) where
  gshowsPrec :: forall a. Int -> TagPow' n t a -> ShowS
gshowsPrec = Int -> TagPow' n t a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance GEq t => GEq (TagPow' n t) where
  geq :: forall a b. TagPow' n t a -> TagPow' n t b -> Maybe (a :~: b)
geq TagPow' n t a
t TagPow' n t b
t' = ((n :~: n, a :~: b) -> a :~: b)
-> Maybe (n :~: n, a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (n :~: n, a :~: b) -> a :~: b
forall a b. (a, b) -> b
snd (TagPow' n t a -> TagPow' n t b -> Maybe (n :~: n, a :~: b)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' n t a
t TagPow' n t b
t')

instance GEq t => Eq (TagPow' n t xs) where
  == :: TagPow' n t xs -> TagPow' n t xs -> Bool
(==) = TagPow' n t xs -> TagPow' n t xs -> Bool
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance GCompare t => GCompare (TagPow' n t) where
  gcompare :: forall a b. TagPow' n t a -> TagPow' n t b -> GOrdering a b
gcompare TagPow' n t a
t TagPow' n t b
t' = TagPow' n t a -> TagPow' n t b -> GOrdering '(n, a) '(n, b)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow' TagPow' n t a
t TagPow' n t b
t' GOrdering '(n, a) '(n, b)
-> (('(n, a) ~ '(n, b)) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering a a
GOrdering a b
('(n, a) ~ '(n, b)) => GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

instance GCompare t => Ord (TagPow' n t xs) where
  compare :: TagPow' n t xs -> TagPow' n t xs -> Ordering
compare = TagPow' n t xs -> TagPow' n t xs -> Ordering
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

-- *

geqPow :: GEq t => TagPow n t xs -> TagPow n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow n t xs -> TagPow n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow TagPow n t xs
TagPow0 TagPow n' t xs'
TagPow0 = (n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs')
forall a. a -> Maybe a
Just (n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl, xs :~: xs
xs :~: xs'
forall {k} (a :: k). a :~: a
Refl)
geqPow (TagPowNZ TagPow' n t xs
ts1) (TagPowNZ TagPow' n' t xs'
ts2) = TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' n t xs
ts1 TagPow' n' t xs'
ts2 Maybe (n :~: n', xs :~: xs')
-> ((n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs'))
-> Maybe (n :~: n', xs :~: xs')
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(n :~: n'
Refl, xs :~: xs'
Refl) -> (n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs')
forall a. a -> Maybe a
Just (n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl, xs :~: xs
xs :~: xs'
forall {k} (a :: k). a :~: a
Refl)
geqPow TagPow n t xs
_ TagPow n' t xs'
_ = Maybe (n :~: n', xs :~: xs')
forall a. Maybe a
Nothing

geqPow' :: GEq t => TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' (TagPow1 t xs
t) (TagPow1 t xs'
t') = t xs -> t xs' -> Maybe (xs :~: xs')
forall a b. t a -> t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t xs
t t xs'
t' Maybe (xs :~: xs')
-> ((xs :~: xs') -> Maybe (n :~: n', xs :~: xs'))
-> Maybe (n :~: n', xs :~: xs')
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \xs :~: xs'
eq -> (n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs')
forall a. a -> Maybe a
Just (n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl, xs :~: xs'
eq)
geqPow' (TagPowEven TagPow' m t xs1
t1 TagPow' m t xs2
t2) (TagPowEven TagPow' m t xs1
t1' TagPow' m t xs2
t2') = do
  (m :~: m
Refl, xs1 :~: xs1
Refl) <- TagPow' m t xs1 -> TagPow' m t xs1 -> Maybe (m :~: m, xs1 :~: xs1)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' m t xs1
t1 TagPow' m t xs1
t1'
  (m :~: m
Refl, xs2 :~: xs2
Refl) <- TagPow' m t xs2 -> TagPow' m t xs2 -> Maybe (m :~: m, xs2 :~: xs2)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' m t xs2
t2 TagPow' m t xs2
t2'
  (n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs')
forall a. a -> Maybe a
Just (n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl, xs :~: xs
xs :~: xs'
forall {k} (a :: k). a :~: a
Refl)
geqPow' (TagPowOdd t x
t0 TagPow' m t xs1
t1 TagPow' m t xs2
t2) (TagPowOdd t x
t0' TagPow' m t xs1
t1' TagPow' m t xs2
t2') = do
  x :~: x
Refl <- t x -> t x -> Maybe (x :~: x)
forall a b. t a -> t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t x
t0 t x
t0'
  (m :~: m
Refl, xs1 :~: xs1
Refl) <- TagPow' m t xs1 -> TagPow' m t xs1 -> Maybe (m :~: m, xs1 :~: xs1)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' m t xs1
t1 TagPow' m t xs1
t1'
  (m :~: m
Refl, xs2 :~: xs2
Refl) <- TagPow' m t xs2 -> TagPow' m t xs2 -> Maybe (m :~: m, xs2 :~: xs2)
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GEq t =>
TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' TagPow' m t xs2
t2 TagPow' m t xs2
t2'
  (n :~: n', xs :~: xs') -> Maybe (n :~: n', xs :~: xs')
forall a. a -> Maybe a
Just (n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl, xs :~: xs
xs :~: xs'
forall {k} (a :: k). a :~: a
Refl)
geqPow' TagPow' n t xs
_ TagPow' n' t xs'
_ = Maybe (n :~: n', xs :~: xs')
forall a. Maybe a
Nothing

gcomparePow :: GCompare t => TagPow n t xs -> TagPow n' t xs' -> GOrdering '(n,xs) '(n',xs')
gcomparePow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GCompare t =>
TagPow n t xs -> TagPow n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow TagPow n t xs
TagPow0 TagPow n' t xs'
TagPow0 = GOrdering '(n, xs) '(n, xs)
GOrdering '(n, xs) '(n', xs')
forall {k} (a :: k). GOrdering a a
GEQ
gcomparePow TagPow n t xs
TagPow0 TagPowNZ{} = GOrdering '(n, xs) '(n', xs')
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcomparePow TagPowNZ{} TagPow n' t xs'
TagPow0 = GOrdering '(n, xs) '(n', xs')
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcomparePow (TagPowNZ TagPow' n t xs
ts) (TagPowNZ TagPow' n' t xs'
ts') = TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs')
forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow' TagPow' n t xs
ts TagPow' n' t xs'
ts' GOrdering '(n, xs) '(n', xs')
-> (('(n, xs) ~ '(n', xs')) => GOrdering '(n, xs) '(n', xs'))
-> GOrdering '(n, xs) '(n', xs')
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering '(n, xs) '(n, xs)
GOrdering '(n, xs) '(n', xs')
('(n, xs) ~ '(n', xs')) => GOrdering '(n, xs) '(n', xs')
forall {k} (a :: k). GOrdering a a
GEQ

gcomparePow' :: GCompare t => TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n,xs) '(n',xs')
gcomparePow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow' TagPow' n t xs
ts1 TagPow' n' t xs'
ts2 = SNat n -> SNat n' -> GOrdering n n'
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare SNat n
sn1 SNat n'
sn2 GOrdering n n'
-> ((n ~ n') => GOrdering '(n, xs) '(n', xs'))
-> GOrdering '(n, xs) '(n', xs')
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' TagPow' n t xs
ts1 TagPow' n t xs'
TagPow' n' t xs'
ts2 GOrdering xs xs'
-> ((xs ~ xs') => GOrdering '(n, xs) '(n', xs'))
-> GOrdering '(n, xs) '(n', xs')
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering '(n, xs) '(n, xs)
GOrdering '(n, xs) '(n', xs')
(xs ~ xs') => GOrdering '(n, xs) '(n', xs')
forall {k} (a :: k). GOrdering a a
GEQ
  where
    sn1 :: SNat n
sn1 = TagPow' n t xs -> SNat n
forall (n :: Natural) (t :: Type -> Type) xs.
TagPow' n t xs -> SNat n
toSNatTagPow' TagPow' n t xs
ts1
    sn2 :: SNat n'
sn2 = TagPow' n' t xs' -> SNat n'
forall (n :: Natural) (t :: Type -> Type) xs.
TagPow' n t xs -> SNat n
toSNatTagPow' TagPow' n' t xs'
ts2

gcomparePowN' :: GCompare t => TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' :: forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' (TagPow1 t xs
t) (TagPow1 t xs'
t') = t xs -> t xs' -> GOrdering xs xs'
forall a b. t a -> t b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t xs
t t xs'
t'
gcomparePowN' (TagPowEven TagPow' m t xs1
t1 TagPow' m t xs2
t2) (TagPowEven TagPow' m t xs1
t1' TagPow' m t xs2
t2') = TagPow' m t xs1 -> TagPow' m t xs1 -> GOrdering xs1 xs1
forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' TagPow' m t xs1
t1 TagPow' m t xs1
TagPow' m t xs1
t1' GOrdering xs1 xs1
-> ((xs1 ~ xs1) => GOrdering xs xs') -> GOrdering xs xs'
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? TagPow' m t xs2 -> TagPow' m t xs2 -> GOrdering xs2 xs2
forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' TagPow' m t xs2
t2 TagPow' m t xs2
TagPow' m t xs2
t2' GOrdering xs2 xs2
-> ((xs2 ~ xs2) => GOrdering xs xs') -> GOrdering xs xs'
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering xs xs
GOrdering xs xs'
(xs2 ~ xs2) => GOrdering xs xs'
forall {k} (a :: k). GOrdering a a
GEQ
gcomparePowN' (TagPowOdd t x
t TagPow' m t xs1
t1 TagPow' m t xs2
t2) (TagPowOdd t x
t' TagPow' m t xs1
t1' TagPow' m t xs2
t2') = t x -> t x -> GOrdering x x
forall a b. t a -> t b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t x
t t x
t' GOrdering x x -> ((x ~ x) => GOrdering xs xs') -> GOrdering xs xs'
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? TagPow' m t xs1 -> TagPow' m t xs1 -> GOrdering xs1 xs1
forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' TagPow' m t xs1
t1 TagPow' m t xs1
TagPow' m t xs1
t1' GOrdering xs1 xs1
-> ((xs1 ~ xs1) => GOrdering xs xs') -> GOrdering xs xs'
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? TagPow' m t xs2 -> TagPow' m t xs2 -> GOrdering xs2 xs2
forall (t :: Type -> Type) (n :: Natural) xs xs'.
GCompare t =>
TagPow' n t xs -> TagPow' n t xs' -> GOrdering xs xs'
gcomparePowN' TagPow' m t xs2
t2 TagPow' m t xs2
TagPow' m t xs2
t2' GOrdering xs2 xs2
-> ((xs2 ~ xs2) => GOrdering xs xs') -> GOrdering xs xs'
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering xs xs
GOrdering xs xs'
(xs2 ~ xs2) => GOrdering xs xs'
forall {k} (a :: k). GOrdering a a
GEQ
gcomparePowN' TagPow' n t xs
_ TagPow' n t xs'
_ = [Char] -> GOrdering xs xs'
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable!"

toSNatTagPow' :: TagPow' n t xs -> SNat n
toSNatTagPow' :: forall (n :: Natural) (t :: Type -> Type) xs.
TagPow' n t xs -> SNat n
toSNatTagPow' TagPow1{} = SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat
toSNatTagPow' TagPowEven{} = SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat
toSNatTagPow' TagPowOdd{} = SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat

-- *

-- | Binary representation of Nat
data BinView (n :: Nat) where
  View0 :: BinView 0
  ViewNZ :: BinView' n -> BinView n

data BinView' (n :: Nat) where
  View1 :: BinView' 1
  ViewEven :: SNat n -> BinView' (n * 2)
  ViewOdd :: SNat n -> BinView' (n * 2 + 1)

binView :: SNat n -> BinView n
binView :: forall (n :: Natural). SNat n -> BinView n
binView SNat n
Zero = BinView n
BinView 0
View0
binView sn :: SNat n
sn@(Succ SNat m
_) = BinView' n -> BinView n
forall (n :: Natural). BinView' n -> BinView n
ViewNZ (SNat (m + 1) -> BinView' (m + 1)
forall (n :: Natural). SNat (n + 1) -> BinView' (n + 1)
binView' SNat n
SNat (m + 1)
sn)

binView' :: SNat (n + 1) -> BinView' (n + 1)
binView' :: forall (n :: Natural). SNat (n + 1) -> BinView' (n + 1)
binView' SNat (n + 1)
sn = Some BinView' -> BinView' (n + 1)
forall {k} (f :: k -> Type) (any :: k). Some f -> f any
unsafeCoerceFromSome Some BinView'
res
  where
    n :: Natural
n = SNat (n + 1) -> Natural
forall (n :: Natural). SNat n -> Natural
fromSNat SNat (n + 1)
sn
    res :: Some BinView'
res = case Natural
n of
      Natural
0 -> [Char] -> Some BinView'
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable!"
      Natural
1 -> BinView' 1 -> Some BinView'
forall {k} (tag :: k -> Type) (a :: k). tag a -> Some tag
Some BinView' 1
View1
      Natural
_ | Natural -> Bool
forall a. Integral a => a -> Bool
even Natural
n    -> Natural
-> (forall {n :: Natural}. SNat n -> Some BinView')
-> Some BinView'
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
withSomeSNat (Natural
n Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
2) ((forall {n :: Natural}. SNat n -> Some BinView') -> Some BinView')
-> (forall {n :: Natural}. SNat n -> Some BinView')
-> Some BinView'
forall a b. (a -> b) -> a -> b
$ \SNat n
sn' -> BinView' (n * 2) -> Some BinView'
forall {k} (tag :: k -> Type) (a :: k). tag a -> Some tag
Some (SNat n -> BinView' (n * 2)
forall (n :: Natural). SNat n -> BinView' (n * 2)
ViewEven SNat n
sn')
        | Bool
otherwise -> Natural
-> (forall {n :: Natural}. SNat n -> Some BinView')
-> Some BinView'
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
withSomeSNat (Natural
n Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
2) ((forall {n :: Natural}. SNat n -> Some BinView') -> Some BinView')
-> (forall {n :: Natural}. SNat n -> Some BinView')
-> Some BinView'
forall a b. (a -> b) -> a -> b
$ \SNat n
sn' -> BinView' ((n * 2) + 1) -> Some BinView'
forall {k} (tag :: k -> Type) (a :: k). tag a -> Some tag
Some (SNat n -> BinView' ((n * 2) + 1)
forall (n :: Natural). SNat n -> BinView' ((n * 2) + 1)
ViewOdd SNat n
sn')

unsafeCoerceFromSome :: Some f -> f any
unsafeCoerceFromSome :: forall {k} (f :: k -> Type) (any :: k). Some f -> f any
unsafeCoerceFromSome (Some f a
fb) = f a -> f any
forall a b. a -> b
unsafeCoerce f a
fb