diff options
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 93c46ed..2e0c1ca 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -174,23 +174,31 @@ type family DropLen ref l where listhTakeLen :: forall i is sh. Perm is -> ListH sh i -> ListH (TakeLen is sh) i listhTakeLen PNil _ = ZH -listhTakeLen (_ `PCons` is) (n ::# sh) = n ::# listhTakeLen is sh +listhTakeLen (_ `PCons` is) (n `ConsUnknown` sh) = n `ConsUnknown` listhTakeLen is sh +listhTakeLen (_ `PCons` is) (n `ConsKnown` sh) = n `ConsKnown` listhTakeLen is sh listhTakeLen (_ `PCons` _) ZH = error "Permutation longer than shape" listhDropLen :: forall i is sh. Perm is -> ListH sh i -> ListH (DropLen is sh) i listhDropLen PNil sh = sh -listhDropLen (_ `PCons` is) (_ ::# sh) = listhDropLen is sh +listhDropLen (_ `PCons` is) (_ `ConsUnknown` sh) = listhDropLen is sh +listhDropLen (_ `PCons` is) (_ `ConsKnown` sh) = listhDropLen is sh listhDropLen (_ `PCons` _) ZH = error "Permutation longer than shape" listhPermute :: forall i is sh. Perm is -> ListH sh i -> ListH (Permute is sh) i listhPermute PNil _ = ZH listhPermute (i `PCons` (is :: Perm is')) (sh :: ListH sh i) = - listhIndex i sh ::# listhPermute is sh + case listhIndex i sh of + SUnknown x -> x `ConsUnknown` listhPermute is sh + SKnown x -> x `ConsKnown` listhPermute is sh listhIndex :: forall i k sh. SNat k -> ListH sh i -> SMayNat i (Index k sh) -listhIndex SZ (n ::# _) = n -listhIndex (SS (i :: SNat k')) ((_ :: SMayNat i n) ::# (sh :: ListH sh' i)) - | Refl <- lemIndexSucc (Proxy @k') (Proxy @n) (Proxy @sh') +listhIndex SZ (n `ConsUnknown` _) = SUnknown n +listhIndex SZ (n `ConsKnown` _) = SKnown n +listhIndex (SS (i :: SNat k')) ((_ :: i) `ConsUnknown` (sh :: ListH sh' i)) + | Refl <- lemIndexSucc (Proxy @k') (Proxy @Nothing) (Proxy @sh') + = listhIndex i sh +listhIndex (SS (i :: SNat k')) ((_ :: SNat n) `ConsKnown` (sh :: ListH sh' i)) + | Refl <- lemIndexSucc (Proxy @k') (Proxy @(Just n)) (Proxy @sh') = listhIndex i sh listhIndex _ ZH = error "Index into empty shape" |