{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Data.Array.Nested.Permutation where
import Data.Coerce (coerce)
import Data.Functor.Const
import Data.List (sort)
import Data.Maybe (fromMaybe)
import Data.Proxy
import Data.Type.Bool
import Data.Type.Equality
import Data.Type.Ord
import GHC.Exts (withDict)
import GHC.TypeError
import GHC.TypeLits
import GHC.TypeNats qualified as TN
import Data.Array.Nested.Mixed.Shape
import Data.Array.Nested.Types
data Perm list where
PNil :: Perm '[]
PCons :: SNat a -> Perm l -> Perm (a : l)
infixr 5 `PCons`
deriving instance Show (Perm list)
deriving instance Eq (Perm list)
instance TestEquality Perm where
testEquality :: forall (a :: [Nat]) (b :: [Nat]).
Perm a -> Perm b -> Maybe (a :~: b)
testEquality Perm a
PNil Perm b
PNil = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
testEquality (SNat a
x `PCons` Perm l
xs) (SNat a
y `PCons` Perm l
ys)
| Just a :~: a
Refl <- SNat a -> SNat a -> Maybe (a :~: a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat a
x SNat a
y
, Just l :~: l
Refl <- Perm l -> Perm l -> Maybe (l :~: l)
forall (a :: [Nat]) (b :: [Nat]).
Perm a -> Perm b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Perm l
xs Perm l
ys = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
testEquality Perm a
_ Perm b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
permRank :: Perm list -> SNat (Rank list)
permRank :: forall (list :: [Nat]). Perm list -> SNat (Rank list)
permRank Perm list
PNil = SNat 0
SNat (Rank list)
forall (n :: Nat). KnownNat n => SNat n
SNat
permRank (SNat a
_ `PCons` Perm l
l) | SNat (Rank l)
SNat <- Perm l -> SNat (Rank l)
forall (list :: [Nat]). Perm list -> SNat (Rank list)
permRank Perm l
l = SNat (Rank l + 1)
SNat (Rank list)
forall (n :: Nat). KnownNat n => SNat n
SNat
permFromList :: [Int] -> (forall list. Perm list -> r) -> r
permFromList :: forall r. [Int] -> (forall (list :: [Nat]). Perm list -> r) -> r
permFromList [] forall (list :: [Nat]). Perm list -> r
k = Perm '[] -> r
forall (list :: [Nat]). Perm list -> r
k Perm '[]
PNil
permFromList (Int
x : [Int]
xs) forall (list :: [Nat]). Perm list -> r
k = Integer -> (forall {n :: Nat}. Maybe (SNat n) -> r) -> r
forall r. Integer -> (forall (n :: Nat). Maybe (SNat n) -> r) -> r
withSomeSNat (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x) ((forall {n :: Nat}. Maybe (SNat n) -> r) -> r)
-> (forall {n :: Nat}. Maybe (SNat n) -> r) -> r
forall a b. (a -> b) -> a -> b
$ \case
Just SNat n
sn -> [Int] -> (forall (list :: [Nat]). Perm list -> r) -> r
forall r. [Int] -> (forall (list :: [Nat]). Perm list -> r) -> r
permFromList [Int]
xs ((forall (list :: [Nat]). Perm list -> r) -> r)
-> (forall (list :: [Nat]). Perm list -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Perm list
list -> Perm (n : list) -> r
forall (list :: [Nat]). Perm list -> r
k (SNat n
sn SNat n -> Perm list -> Perm (n : list)
forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a : l)
`PCons` Perm list
list)
Maybe (SNat n)
Nothing -> String -> r
forall a. HasCallStack => String -> a
error (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$ String
"Data.Array.Mixed.permFromList: negative number in list: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x
permToList :: Perm list -> [Natural]
permToList :: forall (list :: [Nat]). Perm list -> [Nat]
permToList Perm list
PNil = [Nat]
forall a. Monoid a => a
mempty
permToList (SNat a
x `PCons` Perm l
l) = SNat a -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat SNat a
x Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: Perm l -> [Nat]
forall (list :: [Nat]). Perm list -> [Nat]
permToList Perm l
l
permToList' :: Perm list -> [Int]
permToList' :: forall (list :: [Nat]). Perm list -> [Int]
permToList' = (Nat -> Int) -> [Nat] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Nat] -> [Int]) -> (Perm list -> [Nat]) -> Perm list -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Perm list -> [Nat]
forall (list :: [Nat]). Perm list -> [Nat]
permToList
permCheckPermutation :: forall r list. Perm list -> (IsPermutation list => r) -> Maybe r
permCheckPermutation :: forall r (list :: [Nat]).
Perm list -> (IsPermutation list => r) -> Maybe r
permCheckPermutation = \Perm list
p IsPermutation list => r
k ->
let n :: SNat (Rank list)
n = Perm list -> SNat (Rank list)
forall (list :: [Nat]). Perm list -> SNat (Rank list)
permRank Perm list
p
in case (Proxy list
-> SNat (Rank list)
-> Perm list
-> Maybe (AllElem' list (Count 0 (Rank list)) :~: 'True)
forall {a} (isTop :: [a]) (is' :: [Nat]).
Proxy isTop
-> SNat (Rank isTop)
-> Perm is'
-> Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: 'True)
provePerm1 (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @list) SNat (Rank list)
n Perm list
p, SNat 0
-> SNat (Rank list)
-> Perm list
-> Maybe (AllElem' (Count 0 (Rank list)) list :~: 'True)
forall (i :: Nat) (n :: Nat) (is' :: [Nat]).
SNat i
-> SNat n -> Perm is' -> Maybe (AllElem' (Count i n) is' :~: 'True)
provePerm2 (forall (n :: Nat). KnownNat n => SNat n
SNat @0) SNat (Rank list)
n Perm list
p) of
(Just AllElem' list (Count 0 (Rank list)) :~: 'True
Refl, Just AllElem' (Count 0 (Rank list)) list :~: 'True
Refl) -> r -> Maybe r
forall a. a -> Maybe a
Just r
IsPermutation list => r
k
(Maybe (AllElem' list (Count 0 (Rank list)) :~: 'True),
Maybe (AllElem' (Count 0 (Rank list)) list :~: 'True))
_ -> Maybe r
forall a. Maybe a
Nothing
where
lemElemCount :: (0 <= n, Compare n m ~ LT)
=> proxy n -> proxy m -> Elem n (Count 0 m) :~: True
lemElemCount :: forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
(0 <= n, Compare n m ~ 'LT) =>
proxy n -> proxy m -> Elem n (Count 0 m) :~: 'True
lemElemCount proxy n
_ proxy m
_ = Elem n (Count 0 m) :~: 'True
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl
lemCount :: (OrdCond (Compare i n) True False True ~ True)
=> proxy i -> proxy n -> Count i n :~: i : Count (i + 1) n
lemCount :: forall (i :: Nat) (n :: Nat) (proxy :: Nat -> *).
(OrdCond (Compare i n) 'True 'False 'True ~ 'True) =>
proxy i -> proxy n -> Count i n :~: (i : Count (i + 1) n)
lemCount proxy i
_ proxy n
_ = Count i n :~: (i : Count (i + 1) n)
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl
lemElem :: Elem x ys ~ True => proxy x -> proxy' (y : ys) -> Elem x (y : ys) :~: True
lemElem :: forall {a} (x :: a) (ys :: [a]) (proxy :: a -> *)
(proxy' :: [a] -> *) (y :: a).
(Elem x ys ~ 'True) =>
proxy x -> proxy' (y : ys) -> Elem x (y : ys) :~: 'True
lemElem proxy x
_ proxy' (y : ys)
_ = Elem x (y : ys) :~: 'True
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl
provePerm1 :: Proxy isTop -> SNat (Rank isTop) -> Perm is'
-> Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: True)
provePerm1 :: forall {a} (isTop :: [a]) (is' :: [Nat]).
Proxy isTop
-> SNat (Rank isTop)
-> Perm is'
-> Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: 'True)
provePerm1 Proxy isTop
_ SNat (Rank isTop)
_ Perm is'
PNil = ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
provePerm1 Proxy isTop
p rtop :: SNat (Rank isTop)
rtop@SNat (Rank isTop)
SNat (PCons sn :: SNat a
sn@SNat a
SNat Perm l
perm)
| Just AllElem' l (Count 0 (Rank isTop)) :~: 'True
Refl <- Proxy isTop
-> SNat (Rank isTop)
-> Perm l
-> Maybe (AllElem' l (Count 0 (Rank isTop)) :~: 'True)
forall {a} (isTop :: [a]) (is' :: [Nat]).
Proxy isTop
-> SNat (Rank isTop)
-> Perm is'
-> Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: 'True)
provePerm1 Proxy isTop
p SNat (Rank isTop)
rtop Perm l
perm
= case (SNat 0 -> SNat a -> OrderingI 0 a
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (n :: Nat). KnownNat n => SNat n
SNat @0) SNat a
sn, SNat a -> SNat (Rank isTop) -> OrderingI a (Rank isTop)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
sn SNat (Rank isTop)
rtop) of
(OrderingI 0 a
LTI, OrderingI a (Rank isTop)
LTI) | Elem a (Count 0 (Rank isTop)) :~: 'True
Refl <- SNat a
-> SNat (Rank isTop) -> Elem a (Count 0 (Rank isTop)) :~: 'True
forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
(0 <= n, Compare n m ~ 'LT) =>
proxy n -> proxy m -> Elem n (Count 0 m) :~: 'True
lemElemCount SNat a
sn SNat (Rank isTop)
rtop -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
(OrderingI 0 a
EQI, OrderingI a (Rank isTop)
LTI) | Elem a (Count 0 (Rank isTop)) :~: 'True
Refl <- SNat a
-> SNat (Rank isTop) -> Elem a (Count 0 (Rank isTop)) :~: 'True
forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
(0 <= n, Compare n m ~ 'LT) =>
proxy n -> proxy m -> Elem n (Count 0 m) :~: 'True
lemElemCount SNat a
sn SNat (Rank isTop)
rtop -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
(OrderingI 0 a, OrderingI a (Rank isTop))
_ -> Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: 'True)
Maybe (Elem a (Count 0 (Rank isTop)) :~: 'True)
forall a. Maybe a
Nothing
| Bool
otherwise
= Maybe
((Elem a (Count 0 (Rank isTop))
&& AllElem' l (Count 0 (Rank isTop)))
:~: 'True)
Maybe (AllElem' is' (Count 0 (Rank isTop)) :~: 'True)
forall a. Maybe a
Nothing
provePerm2 :: SNat i -> SNat n -> Perm is'
-> Maybe (AllElem' (Count i n) is' :~: True)
provePerm2 :: forall (i :: Nat) (n :: Nat) (is' :: [Nat]).
SNat i
-> SNat n -> Perm is' -> Maybe (AllElem' (Count i n) is' :~: 'True)
provePerm2 = \i :: SNat i
i@(SNat i
SNat :: SNat i) n :: SNat n
n@SNat n
SNat Perm is'
perm ->
case SNat i -> SNat n -> OrderingI i n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat i
i SNat n
n of
OrderingI i n
EQI -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
OrderingI i n
LTI | Count i n :~: (i : Count (i + 1) n)
Refl <- SNat i -> SNat n -> Count i n :~: (i : Count (i + 1) n)
forall (i :: Nat) (n :: Nat) (proxy :: Nat -> *).
(OrdCond (Compare i n) 'True 'False 'True ~ 'True) =>
proxy i -> proxy n -> Count i n :~: (i : Count (i + 1) n)
lemCount SNat i
i SNat n
n
, Just AllElem' (Count (i + 1) n) is' :~: 'True
Refl <- SNat (i + 1)
-> SNat n
-> Perm is'
-> Maybe (AllElem' (Count (i + 1) n) is' :~: 'True)
forall (i :: Nat) (n :: Nat) (is' :: [Nat]).
SNat i
-> SNat n -> Perm is' -> Maybe (AllElem' (Count i n) is' :~: 'True)
provePerm2 (forall (n :: Nat). KnownNat n => SNat n
SNat @(i + 1)) SNat n
n Perm is'
perm
-> SNat i -> Perm is' -> Maybe (Elem i is' :~: 'True)
forall (i :: Nat) (is' :: [Nat]).
SNat i -> Perm is' -> Maybe (Elem i is' :~: 'True)
checkElem SNat i
i Perm is'
perm
| Bool
otherwise -> Maybe (AllElem' (Count i n) is' :~: 'True)
forall a. Maybe a
Nothing
OrderingI i n
GTI -> String -> Maybe (AllElem' (Count i n) is' :~: 'True)
forall a. HasCallStack => String -> a
error String
"unreachable"
where
checkElem :: SNat i -> Perm is' -> Maybe (Elem i is' :~: True)
checkElem :: forall (i :: Nat) (is' :: [Nat]).
SNat i -> Perm is' -> Maybe (Elem i is' :~: 'True)
checkElem SNat i
_ Perm is'
PNil = Maybe ('False :~: 'True)
Maybe (Elem i is' :~: 'True)
forall a. Maybe a
Nothing
checkElem i :: SNat i
i@SNat i
SNat (PCons k :: SNat a
k@SNat a
SNat Perm l
perm :: Perm is') =
case SNat i -> SNat a -> Maybe (i :~: a)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat SNat i
i SNat a
k of
Just i :~: a
Refl -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
Maybe (i :~: a)
Nothing | Just Elem i l :~: 'True
Refl <- SNat i -> Perm l -> Maybe (Elem i l :~: 'True)
forall (i :: Nat) (is' :: [Nat]).
SNat i -> Perm is' -> Maybe (Elem i is' :~: 'True)
checkElem SNat i
i Perm l
perm, Elem i (a : l) :~: 'True
Refl <- SNat i -> Proxy (a : l) -> Elem i (a : l) :~: 'True
forall {a} (x :: a) (ys :: [a]) (proxy :: a -> *)
(proxy' :: [a] -> *) (y :: a).
(Elem x ys ~ 'True) =>
proxy x -> proxy' (y : ys) -> Elem x (y : ys) :~: 'True
lemElem SNat i
i (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @is') -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
| Bool
otherwise -> Maybe (Elem i is' :~: 'True)
Maybe (Elem i (a : l) :~: 'True)
forall a. Maybe a
Nothing
class KnownPerm l where makePerm :: Perm l
instance KnownPerm '[] where makePerm :: Perm '[]
makePerm = Perm '[]
PNil
instance (KnownNat n, KnownPerm l) => KnownPerm (n : l) where makePerm :: Perm (n : l)
makePerm = SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing SNat n -> Perm l -> Perm (n : l)
forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a : l)
`PCons` Perm l
forall (l :: [Nat]). KnownPerm l => Perm l
makePerm
withKnownPerm :: forall l r. Perm l -> (KnownPerm l => r) -> r
withKnownPerm :: forall (l :: [Nat]) r. Perm l -> (KnownPerm l => r) -> r
withKnownPerm = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownPerm l)
type PermR = [Int]
type family Elem x l where
Elem x '[] = 'False
Elem x (x : _) = 'True
Elem x (_ : ys) = Elem x ys
type family AllElem' as bs where
AllElem' '[] bs = 'True
AllElem' (a : as) bs = Elem a bs && AllElem' as bs
type AllElem as bs = Assert (AllElem' as bs)
(TypeError (Text "The elements of " :<>: ShowType as :<>: Text " are not all in " :<>: ShowType bs))
type family Count i n where
Count n n = '[]
Count i n = i : Count (i + 1) n
type IsPermutation as = (AllElem as (Count 0 (Rank as)), AllElem (Count 0 (Rank as)) as)
type family Index i sh where
Index 0 (n : sh) = n
Index i (_ : sh) = Index (i - 1) sh
type family Permute is sh where
Permute '[] sh = '[]
Permute (i : is) sh = Index i sh : Permute is sh
type PermutePrefix is sh = Permute is (TakeLen is sh) ++ DropLen is sh
type family TakeLen ref l where
TakeLen '[] l = '[]
TakeLen (_ : ref) (x : xs) = x : TakeLen ref xs
type family DropLen ref l where
DropLen '[] l = l
DropLen (_ : ref) (_ : xs) = DropLen ref xs
listxTakeLen :: forall f is sh. Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxTakeLen :: forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxTakeLen Perm is
PNil ListX sh f
_ = ListX '[] f
ListX (TakeLen is sh) f
forall (f :: Maybe Nat -> *). ListX '[] f
ZX
listxTakeLen (SNat a
_ `PCons` Perm l
is) (f n
n ::% ListX sh1 f
sh) = f n
n f n -> ListX (TakeLen l sh1) f -> ListX (n : TakeLen l sh1) f
forall (f :: Maybe Nat -> *) (n :: Maybe Nat) (sh1 :: [Maybe Nat]).
f n -> ListX sh1 f -> ListX (n : sh1) f
::% Perm l -> ListX sh1 f -> ListX (TakeLen l sh1) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxTakeLen Perm l
is ListX sh1 f
sh
listxTakeLen (SNat a
_ `PCons` Perm l
_) ListX sh f
ZX = String -> ListX (TakeLen (a : l) '[]) f
forall a. HasCallStack => String -> a
error String
"Permutation longer than shape"
listxDropLen :: forall f is sh. Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxDropLen :: forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxDropLen Perm is
PNil ListX sh f
sh = ListX sh f
ListX (DropLen is sh) f
sh
listxDropLen (SNat a
_ `PCons` Perm l
is) (f n
_ ::% ListX sh1 f
sh) = Perm l -> ListX sh1 f -> ListX (DropLen l sh1) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxDropLen Perm l
is ListX sh1 f
sh
listxDropLen (SNat a
_ `PCons` Perm l
_) ListX sh f
ZX = String -> ListX (DropLen (a : l) '[]) f
forall a. HasCallStack => String -> a
error String
"Permutation longer than shape"
listxPermute :: forall f is sh. Perm is -> ListX sh f -> ListX (Permute is sh) f
listxPermute :: forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (Permute is sh) f
listxPermute Perm is
PNil ListX sh f
_ = ListX '[] f
ListX (Permute is sh) f
forall (f :: Maybe Nat -> *). ListX '[] f
ZX
listxPermute (SNat a
i `PCons` (Perm l
is :: Perm is')) (ListX sh f
sh :: ListX sh f) =
Proxy l -> Proxy sh -> SNat a -> ListX sh f -> f (Index a sh)
forall {k} {k} (f :: Maybe Nat -> *) (is :: k) (shT :: k)
(i :: Nat) (sh :: [Maybe Nat]).
Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxIndex (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @is') (forall (t :: [Maybe Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sh) SNat a
i ListX sh f
sh f (Index a sh)
-> ListX (Permute l sh) f -> ListX (Index a sh : Permute l sh) f
forall (f :: Maybe Nat -> *) (n :: Maybe Nat) (sh1 :: [Maybe Nat]).
f n -> ListX sh1 f -> ListX (n : sh1) f
::% Perm l -> ListX sh f -> ListX (Permute l sh) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (Permute is sh) f
listxPermute Perm l
is ListX sh f
sh
listxIndex :: forall f is shT i sh. Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxIndex :: forall {k} {k} (f :: Maybe Nat -> *) (is :: k) (shT :: k)
(i :: Nat) (sh :: [Maybe Nat]).
Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxIndex Proxy is
_ Proxy shT
_ SNat i
SZ (f n
n ::% ListX sh1 f
_) = f n
f (Index i sh)
n
listxIndex Proxy is
p Proxy shT
pT (SS (SNat n
i :: SNat i')) ((f n
_ :: f n) ::% (ListX sh1 f
sh :: ListX sh' f))
| Index (n + 1) (n : sh1) :~: Index n sh1
Refl <- Proxy n
-> Proxy n -> Proxy sh1 -> Index (n + 1) (n : sh1) :~: Index n sh1
forall {k} (i :: Nat) (a :: k) (l :: [k]).
Proxy i
-> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @i') (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: [Maybe Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sh')
= Proxy is -> Proxy shT -> SNat n -> ListX sh1 f -> f (Index n sh1)
forall {k} {k} (f :: Maybe Nat -> *) (is :: k) (shT :: k)
(i :: Nat) (sh :: [Maybe Nat]).
Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxIndex Proxy is
p Proxy shT
pT SNat n
i ListX sh1 f
sh
listxIndex Proxy is
_ Proxy shT
_ SNat i
_ ListX sh f
ZX = String -> f (Index i '[])
forall a. HasCallStack => String -> a
error String
"Index into empty shape"
listxPermutePrefix :: forall f is sh. Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
listxPermutePrefix :: forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
listxPermutePrefix Perm is
perm ListX sh f
sh = ListX (Permute is (TakeLen is sh)) f
-> ListX (DropLen is sh) f
-> ListX (Permute is (TakeLen is sh) ++ DropLen is sh) f
forall (sh :: [Maybe Nat]) (f :: Maybe Nat -> *)
(sh' :: [Maybe Nat]).
ListX sh f -> ListX sh' f -> ListX (sh ++ sh') f
listxAppend (Perm is
-> ListX (TakeLen is sh) f -> ListX (Permute is (TakeLen is sh)) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (Permute is sh) f
listxPermute Perm is
perm (Perm is -> ListX sh f -> ListX (TakeLen is sh) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxTakeLen Perm is
perm ListX sh f
sh)) (Perm is -> ListX sh f -> ListX (DropLen is sh) f
forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxDropLen Perm is
perm ListX sh f
sh)
ixxPermutePrefix :: forall i is sh. Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i
ixxPermutePrefix :: forall i (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i
ixxPermutePrefix = (Perm is
-> ListX sh (Const i)
-> ListX (Permute is (TakeLen is sh) ++ DropLen is sh) (Const i))
-> Perm is
-> IxX sh i
-> IxX (Permute is (TakeLen is sh) ++ DropLen is sh) i
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
listxPermutePrefix @(Const i))
ssxTakeLen :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
ssxTakeLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
ssxTakeLen = (Perm is
-> ListX sh (SMayNat () SNat)
-> ListX (TakeLen is sh) (SMayNat () SNat))
-> Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxTakeLen @(SMayNat () SNat))
ssxDropLen :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
ssxDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
ssxDropLen = (Perm is
-> ListX sh (SMayNat () SNat)
-> ListX (DropLen is sh) (SMayNat () SNat))
-> Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxDropLen @(SMayNat () SNat))
ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxPermute :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxPermute = (Perm is
-> ListX sh (SMayNat () SNat)
-> ListX (Permute is sh) (SMayNat () SNat))
-> Perm is -> StaticShX sh -> StaticShX (Permute is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (Permute is sh) f
listxPermute @(SMayNat () SNat))
ssxIndex :: Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () SNat (Index i sh)
ssxIndex :: forall {k} {k} (is :: k) (shT :: k) (i :: Nat) (sh :: [Maybe Nat]).
Proxy is
-> Proxy shT
-> SNat i
-> StaticShX sh
-> SMayNat () SNat (Index i sh)
ssxIndex Proxy is
p1 Proxy shT
p2 = (SNat i
-> ListX sh (SMayNat () SNat) -> SMayNat () SNat (Index i sh))
-> SNat i -> StaticShX sh -> SMayNat () SNat (Index i sh)
forall a b. Coercible a b => a -> b
coerce (forall {k} {k} (f :: Maybe Nat -> *) (is :: k) (shT :: k)
(i :: Nat) (sh :: [Maybe Nat]).
Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
forall (f :: Maybe Nat -> *) (is :: k) (shT :: k) (i :: Nat)
(sh :: [Maybe Nat]).
Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxIndex @(SMayNat () SNat) Proxy is
p1 Proxy shT
p2)
ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
ssxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
ssxPermutePrefix = (Perm is
-> ListX sh (SMayNat () SNat)
-> ListX
(Permute is (TakeLen is sh) ++ DropLen is sh) (SMayNat () SNat))
-> Perm is
-> StaticShX sh
-> StaticShX (Permute is (TakeLen is sh) ++ DropLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
listxPermutePrefix @(SMayNat () SNat))
shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
shxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> IShX sh -> IShX (PermutePrefix is sh)
shxPermutePrefix = (Perm is
-> ListX sh (SMayNat Int SNat)
-> ListX
(Permute is (TakeLen is sh) ++ DropLen is sh) (SMayNat Int SNat))
-> Perm is
-> IShX sh
-> IShX (Permute is (TakeLen is sh) ++ DropLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Maybe Nat -> *) (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
listxPermutePrefix @(SMayNat Int SNat))
permInverse :: Perm is
-> (forall is'.
IsPermutation is'
=> Perm is'
-> (forall sh. Rank sh ~ Rank is => StaticShX sh -> Permute is' (Permute is sh) :~: sh)
-> r)
-> r
permInverse :: forall (is :: [Nat]) r.
Perm is
-> (forall (is' :: [Nat]).
IsPermutation is' =>
Perm is'
-> (forall (sh :: [Maybe Nat]).
(Rank sh ~ Rank is) =>
StaticShX sh -> Permute is' (Permute is sh) :~: sh)
-> r)
-> r
permInverse = \Perm is
perm forall (is' :: [Nat]).
IsPermutation is' =>
Perm is'
-> (forall (sh :: [Maybe Nat]).
(Rank sh ~ Rank is) =>
StaticShX sh -> Permute is' (Permute is sh) :~: sh)
-> r
k ->
Perm is -> (forall {is' :: [Nat]}. Perm is' -> r) -> r
forall (is :: [Nat]) r.
Perm is -> (forall (is' :: [Nat]). Perm is' -> r) -> r
genPerm Perm is
perm ((forall {is' :: [Nat]}. Perm is' -> r) -> r)
-> (forall {is' :: [Nat]}. Perm is' -> r) -> r
forall a b. (a -> b) -> a -> b
$ \(Perm is'
invperm :: Perm is') ->
r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe
(String -> r
forall a. HasCallStack => String -> a
error (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$ String
"permInverse: did not generate permutation? perm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Perm is -> String
forall a. Show a => a -> String
show Perm is
perm
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ; invperm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Perm is' -> String
forall a. Show a => a -> String
show Perm is'
invperm)
(Perm is' -> (IsPermutation is' => r) -> Maybe r
forall r (list :: [Nat]).
Perm list -> (IsPermutation list => r) -> Maybe r
permCheckPermutation Perm is'
invperm
(Perm is'
-> (forall (sh :: [Maybe Nat]).
(Rank sh ~ Rank is) =>
StaticShX sh -> Permute is' (Permute is sh) :~: sh)
-> r
forall (is' :: [Nat]).
IsPermutation is' =>
Perm is'
-> (forall (sh :: [Maybe Nat]).
(Rank sh ~ Rank is) =>
StaticShX sh -> Permute is' (Permute is sh) :~: sh)
-> r
k Perm is'
invperm
(\StaticShX sh
ssh -> case Perm is
-> Perm is'
-> StaticShX sh
-> Maybe (Permute is' (Permute is sh) :~: sh)
forall (is :: [Nat]) (is' :: [Nat]) (sh :: [Maybe Nat]).
Perm is
-> Perm is'
-> StaticShX sh
-> Maybe (Permute is' (Permute is sh) :~: sh)
permCheckInverse Perm is
perm Perm is'
invperm StaticShX sh
ssh of
Just Permute is' (Permute is sh) :~: sh
eq -> Permute is' (Permute is sh) :~: sh
eq
Maybe (Permute is' (Permute is sh) :~: sh)
Nothing -> String -> Permute is' (Permute is sh) :~: sh
forall a. HasCallStack => String -> a
error (String -> Permute is' (Permute is sh) :~: sh)
-> String -> Permute is' (Permute is sh) :~: sh
forall a b. (a -> b) -> a -> b
$ String
"permInverse: did not generate inverse? perm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Perm is -> String
forall a. Show a => a -> String
show Perm is
perm
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ; invperm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Perm is' -> String
forall a. Show a => a -> String
show Perm is'
invperm)))
where
genPerm :: Perm is -> (forall is'. Perm is' -> r) -> r
genPerm :: forall (is :: [Nat]) r.
Perm is -> (forall (is' :: [Nat]). Perm is' -> r) -> r
genPerm Perm is
perm =
let permList :: [Int]
permList = Perm is -> [Int]
forall (list :: [Nat]). Perm list -> [Int]
permToList' Perm is
perm
in [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
forall r. [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
toHList ([Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r)
-> [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
forall a b. (a -> b) -> a -> b
$ ((Int, Nat) -> Nat) -> [(Int, Nat)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Nat) -> Nat
forall a b. (a, b) -> b
snd ([(Int, Nat)] -> [(Int, Nat)]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Nat] -> [(Int, Nat)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
permList [Nat
0..]))
where
toHList :: [Natural] -> (forall is'. Perm is' -> r) -> r
toHList :: forall r. [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
toHList [] forall (is' :: [Nat]). Perm is' -> r
k = Perm '[] -> r
forall (is' :: [Nat]). Perm is' -> r
k Perm '[]
PNil
toHList (Nat
n : [Nat]
ns) forall (is' :: [Nat]). Perm is' -> r
k = [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
forall r. [Nat] -> (forall (is' :: [Nat]). Perm is' -> r) -> r
toHList [Nat]
ns ((forall (is' :: [Nat]). Perm is' -> r) -> r)
-> (forall (is' :: [Nat]). Perm is' -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Perm is'
l -> Nat -> (forall {n :: Nat}. SNat n -> r) -> r
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat Nat
n ((forall {n :: Nat}. SNat n -> r) -> r)
-> (forall {n :: Nat}. SNat n -> r) -> r
forall a b. (a -> b) -> a -> b
$ \SNat n
sn -> Perm (n : is') -> r
forall (is' :: [Nat]). Perm is' -> r
k (SNat n -> Perm is' -> Perm (n : is')
forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a : l)
PCons SNat n
sn Perm is'
l)
permCheckInverse :: Perm is -> Perm is' -> StaticShX sh
-> Maybe (Permute is' (Permute is sh) :~: sh)
permCheckInverse :: forall (is :: [Nat]) (is' :: [Nat]) (sh :: [Maybe Nat]).
Perm is
-> Perm is'
-> StaticShX sh
-> Maybe (Permute is' (Permute is sh) :~: sh)
permCheckInverse Perm is
perm Perm is'
perminv StaticShX sh
ssh =
StaticShX (Permute is' (Permute is sh))
-> StaticShX sh -> Maybe (Permute is' (Permute is sh) :~: sh)
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh -> StaticShX sh' -> Maybe (sh :~: sh')
ssxEqType (Perm is'
-> StaticShX (Permute is sh)
-> StaticShX (Permute is' (Permute is sh))
forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxPermute Perm is'
perminv (Perm is -> StaticShX sh -> StaticShX (Permute is sh)
forall (is :: [Nat]) (sh :: [Maybe Nat]).
Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxPermute Perm is
perm StaticShX sh
ssh)) StaticShX sh
ssh
type family MapSucc is where
MapSucc '[] = '[]
MapSucc (i : is) = i + 1 : MapSucc is
permShift1 :: Perm l -> Perm (0 : MapSucc l)
permShift1 :: forall (l :: [Nat]). Perm l -> Perm (0 : MapSucc l)
permShift1 = (forall (n :: Nat). KnownNat n => SNat n
SNat @0 SNat 0 -> Perm (MapSucc l) -> Perm (0 : MapSucc l)
forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a : l)
`PCons`) (Perm (MapSucc l) -> Perm (0 : MapSucc l))
-> (Perm l -> Perm (MapSucc l)) -> Perm l -> Perm (0 : MapSucc l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Perm l -> Perm (MapSucc l)
forall (l :: [Nat]). Perm l -> Perm (MapSucc l)
permMapSucc
where
permMapSucc :: Perm l -> Perm (MapSucc l)
permMapSucc :: forall (l :: [Nat]). Perm l -> Perm (MapSucc l)
permMapSucc Perm l
PNil = Perm '[]
Perm (MapSucc l)
PNil
permMapSucc ((SNat a
SNat :: SNat i) `PCons` Perm l
ns) = forall (n :: Nat). KnownNat n => SNat n
SNat @(i + 1) SNat (a + 1) -> Perm (MapSucc l) -> Perm ((a + 1) : MapSucc l)
forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a : l)
`PCons` Perm l -> Perm (MapSucc l)
forall (l :: [Nat]). Perm l -> Perm (MapSucc l)
permMapSucc Perm l
ns
lemRankPermute :: Proxy sh -> Perm is -> Rank (Permute is sh) :~: Rank is
lemRankPermute :: forall {a} (sh :: [a]) (is :: [Nat]).
Proxy sh -> Perm is -> Rank (Permute is sh) :~: Rank is
lemRankPermute Proxy sh
_ Perm is
PNil = 0 :~: 0
Rank (Permute is sh) :~: Rank is
forall {k} (a :: k). a :~: a
Refl
lemRankPermute Proxy sh
p (SNat a
_ `PCons` Perm l
is) | Rank (Permute l sh) :~: Rank l
Refl <- Proxy sh -> Perm l -> Rank (Permute l sh) :~: Rank l
forall {a} (sh :: [a]) (is :: [Nat]).
Proxy sh -> Perm is -> Rank (Permute is sh) :~: Rank is
lemRankPermute Proxy sh
p Perm l
is = (Rank l + 1) :~: (Rank l + 1)
Rank (Permute is sh) :~: Rank is
forall {k} (a :: k). a :~: a
Refl
lemRankDropLen :: forall is sh. (Rank is <= Rank sh)
=> StaticShX sh -> Perm is -> Rank (DropLen is sh) :~: Rank sh - Rank is
lemRankDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]).
(Rank is <= Rank sh) =>
StaticShX sh
-> Perm is -> Rank (DropLen is sh) :~: (Rank sh - Rank is)
lemRankDropLen StaticShX sh
ZKX Perm is
PNil = 0 :~: 0
Rank (DropLen is sh) :~: (Rank sh - Rank is)
forall {k} (a :: k). a :~: a
Refl
lemRankDropLen (SMayNat () SNat n
_ :!% StaticShX sh
sh) (SNat a
_ `PCons` Perm l
is) | Rank (DropLen l sh) :~: (Rank sh - Rank l)
Refl <- StaticShX sh
-> Perm l -> Rank (DropLen l sh) :~: (Rank sh - Rank l)
forall (is :: [Nat]) (sh :: [Maybe Nat]).
(Rank is <= Rank sh) =>
StaticShX sh
-> Perm is -> Rank (DropLen is sh) :~: (Rank sh - Rank is)
lemRankDropLen StaticShX sh
sh Perm l
is = (Rank sh - Rank l) :~: (Rank sh - Rank l)
Rank (DropLen is sh) :~: (Rank sh - Rank is)
forall {k} (a :: k). a :~: a
Refl
lemRankDropLen (SMayNat () SNat n
_ :!% StaticShX sh
_) Perm is
PNil = (Rank sh + 1) :~: (Rank sh + 1)
Rank (DropLen is sh) :~: (Rank sh - Rank is)
forall {k} (a :: k). a :~: a
Refl
lemRankDropLen StaticShX sh
ZKX (SNat a
_ `PCons` Perm l
_) = String -> Rank (DropLen (a : l) '[]) :~: (0 - (Rank l + 1))
forall a. HasCallStack => String -> a
error String
"1 <= 0"
lemIndexSucc :: Proxy i -> Proxy a -> Proxy l
-> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc :: forall {k} (i :: Nat) (a :: k) (l :: [k]).
Proxy i
-> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc Proxy i
_ Proxy a
_ Proxy l
_ = Index (i + 1) (a : l) :~: Index i l
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl