diff options
Diffstat (limited to 'src/Data/Array/Nested/Ranked/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 690b7da..a352eb3 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -366,10 +366,10 @@ shrSize (ShR sh) = shxSize sh -- We don't report the size of the list in case of errors in order not to retain the list. {-# INLINEABLE shrFromList #-} shrFromList :: SNat n -> [Int] -> IShR n -shrFromList snat topl = ShR $ ShX $ go snat topl +shrFromList snat topl = ShR $ go snat topl where - go :: SNat n -> [Int] -> ListH (Replicate n Nothing) Int - go SZ [] = ZH + go :: SNat n -> [Int] -> ShX (Replicate n Nothing) Int + go SZ [] = ZSX go SZ _ = error $ "shrFromList: List too long (type says " ++ show (fromSNat' snat) ++ ")" go (SS sn :: SNat n1) (i : is) | Refl <- lemReplicateSucc2 (Proxy @n1) Refl = ConsUnknown i (go sn is) go _ _ = error $ "shrFromList: List too short (type says " ++ show (fromSNat' snat) ++ ")" @@ -377,9 +377,9 @@ shrFromList snat topl = ShR $ ShX $ go snat topl -- This is equivalent to but faster than @coerce shxToList@. {-# INLINEABLE shrToList #-} shrToList :: IShR n -> [Int] -shrToList (ShR (ShX l)) = build (\(cons :: i -> is -> is) (nil :: is) -> - let go :: ListH sh Int -> is - go ZH = nil +shrToList (ShR l) = build (\(cons :: i -> is -> is) (nil :: is) -> + let go :: ShX sh Int -> is + go ZSX = nil go (ConsUnknown i rest) = i `cons` go rest go ConsKnown{} = error "shrToList: impossible case" in go l) @@ -411,7 +411,7 @@ shrInit = -- TODO: change this and all other unsafeCoerceRefl to lemmas: gcastWith (unsafeCoerceRefl :: Init (Replicate (n + 1) (Nothing @Nat)) :~: Replicate n Nothing) $ - coerce (shxInit @_ @_ @i) + coerce (shxInit @i) shrLast :: forall n i. ShR (n + 1) i -> i shrLast (ShR sh) @@ -431,7 +431,7 @@ shrAppend = -- lemReplicatePlusApp requires an SNat gcastWith (unsafeCoerceRefl :: Replicate n (Nothing @Nat) ++ Replicate m Nothing :~: Replicate (n + m) Nothing) $ - coerce (shxAppend @_ @_ @i) + coerce (shxAppend @_ @i) {-# INLINE shrZipWith #-} shrZipWith :: (i -> j -> k) -> ShR n i -> ShR n j -> ShR n k @@ -447,7 +447,7 @@ shrSplitAt (SS m) (n :$: sh) = (\(pre, post) -> (n :$: pre, post)) (shrSplitAt m shrSplitAt SS{} ZSR = error "m' + 1 <= 0" shrIndex :: forall k sh i. SNat k -> ShR sh i -> i -shrIndex k (ShR sh) = case shxIndex @_ @_ @i k sh of +shrIndex k (ShR sh) = case shxIndex @i k sh of SUnknown i -> i SKnown{} -> error "shrIndex: impossible SKnown" |