diff options
Diffstat (limited to 'src/Data')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 20 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 19 |
2 files changed, 19 insertions, 20 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 8b46d81..e458806 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -185,14 +185,14 @@ listxDropLen (_ `PCons` _) ZX = error "Permutation longer than shape" listxPermute :: forall f is sh. Perm is -> ListX sh f -> ListX (Permute is sh) f listxPermute PNil _ = ZX listxPermute (i `PCons` (is :: Perm is')) (sh :: ListX sh f) = - listxIndex (Proxy @is') (Proxy @sh) i sh ::% listxPermute is sh + listxIndex i sh ::% listxPermute is sh -listxIndex :: forall f is shT i sh. Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh) -listxIndex _ _ SZ (n ::% _) = n -listxIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f)) +listxIndex :: forall f i sh. SNat i -> ListX sh f -> f (Index i sh) +listxIndex SZ (n ::% _) = n +listxIndex (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f)) | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh') - = listxIndex p pT i sh -listxIndex _ _ _ ZX = error "Index into empty shape" + = listxIndex i sh +listxIndex _ ZX = error "Index into empty shape" listxPermutePrefix :: forall f is sh. Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f listxPermutePrefix perm sh = listxAppend (listxPermute perm (listxTakeLen perm sh)) (listxDropLen perm sh) @@ -209,8 +209,8 @@ ssxDropLen = coerce (listxDropLen @(SMayNat ())) ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh) ssxPermute = coerce (listxPermute @(SMayNat ())) -ssxIndex :: Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () (Index i sh) -ssxIndex p1 p2 i = coerce (listxIndex @(SMayNat ()) p1 p2 i) +ssxIndex :: SNat i -> StaticShX sh -> SMayNat () (Index i sh) +ssxIndex i = coerce (listxIndex @(SMayNat ()) i) ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh) ssxPermutePrefix = coerce (listxPermutePrefix @(SMayNat ())) @@ -224,8 +224,8 @@ shxDropLen = coerce (listxDropLen @(SMayNat Int)) shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh) shxPermute = coerce (listxPermute @(SMayNat Int)) -shxIndex :: Proxy is -> Proxy shT -> SNat i -> IShX sh -> SMayNat Int (Index i sh) -shxIndex p1 p2 i = coerce (listxIndex @(SMayNat Int) p1 p2 i) +shxIndex :: SNat i -> IShX sh -> SMayNat Int (Index i sh) +shxIndex i = coerce (listxIndex @(SMayNat Int) i) shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh) shxPermutePrefix = coerce (listxPermutePrefix @(SMayNat Int)) diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index d815adf..030a065 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -196,16 +196,16 @@ listsDropLenPerm (_ `PCons` _) ZS = error "Permutation longer than shape" listsPermute :: forall f is sh. Perm is -> ListS sh f -> ListS (Permute is sh) f listsPermute PNil _ = ZS listsPermute (i `PCons` (is :: Perm is')) (sh :: ListS sh f) = - case listsIndex (Proxy @is') (Proxy @sh) i sh of + case listsIndex i sh of item -> item ::$ listsPermute is sh -- TODO: try to remove this SNat now that the KnownNat constraint in ListS is removed -listsIndex :: forall f i is sh shT. Proxy is -> Proxy shT -> SNat i -> ListS sh f -> f (Index i sh) -listsIndex _ _ SZ (n ::$ _) = n -listsIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::$ (sh :: ListS sh' f)) +listsIndex :: forall f i sh. SNat i -> ListS sh f -> f (Index i sh) +listsIndex SZ (n ::$ _) = n +listsIndex (SS (i :: SNat i')) ((_ :: f n) ::$ (sh :: ListS sh' f)) | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh') - = listsIndex p pT i sh -listsIndex _ _ _ ZS = error "Index into empty shape" + = listsIndex i sh +listsIndex _ ZS = error "Index into empty shape" listsPermutePrefix :: forall f is sh. Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f listsPermutePrefix perm sh = listsAppend (listsPermute perm (listsTakeLenPerm perm sh)) (listsDropLenPerm perm sh) @@ -460,12 +460,11 @@ shsPermute = :: Permute is (MapJust sh) :~: MapJust (Permute is sh)) $ coerce shxPermute -shsIndex :: forall is shT i sh. - Proxy is -> Proxy shT -> SNat i -> ShS sh -> SNat (Index i sh) -shsIndex pis pshT i sh = +shsIndex :: forall i sh. SNat i -> ShS sh -> SNat (Index i sh) +shsIndex i sh = gcastWith (unsafeCoerceRefl :: Index i (MapJust sh) :~: Just (Index i sh)) $ - case shxIndex pis pshT i (coerce sh) of + case shxIndex i (coerce sh) of SKnown SNat -> SNat shsPermutePrefix :: forall is sh. Perm is -> ShS sh -> ShS (PermutePrefix is sh) |