From fc2a1370d67f12b50e3e5750d17aefd33bc3d8a3 Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski Date: Mon, 16 Mar 2026 14:36:36 +0100 Subject: Fill and clean up *TakeIx and *DropIx functions --- src/Data/Array/Nested/Ranked/Shape.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Data/Array/Nested/Ranked/Shape.hs') diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index e44ab64..c5cdf6b 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -422,6 +422,16 @@ shrTail | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n) = coerce (shxTail @_ @_ @i) +{-# INLINEABLE shrTakeIx #-} +shrTakeIx :: forall n n' i j. Proxy n' -> IxR n j -> ShR (n + n') i -> ShR n i +shrTakeIx _ ZIR _ = ZSR +shrTakeIx p (_ :.: idx) sh = case sh of n :$: sh' -> n :$: shrTakeIx p idx sh' + +{-# INLINEABLE shrDropIx #-} +shrDropIx :: forall n n' i j. IxR n j -> ShR (n + n') i -> ShR n' i +shrDropIx ZIR long = long +shrDropIx (_ :.: short) long = case long of _ :$: long' -> shrDropIx short long' + shrInit :: forall n i. ShR (n + 1) i -> ShR n i shrInit | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n) -- cgit v1.2.3-70-g09d2