aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2024-06-18 21:04:23 +0200
committerTom Smeding <tom@tomsmeding.com>2024-06-18 21:04:23 +0200
commit4a0b2ef27a6e31250c56faef0efc0abf611a0cda (patch)
tree45b3e259d0c811824d15cd0e08e47c0efee1f8c9
parent5dbabda5ef848e8b4b58b8dee55e5a22de7ee7d6 (diff)
Init on ListX
-rw-r--r--src/Data/Array/Mixed/Lemmas.hs3
-rw-r--r--src/Data/Array/Mixed/Shape.hs10
-rw-r--r--src/Data/Array/Mixed/Types.hs5
3 files changed, 18 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index ff2e45c..633c9c2 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -105,6 +105,9 @@ lemTakeLenApp :: Rank l1 <= Rank l2
-> TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest)
lemTakeLenApp _ _ _ = unsafeCoerceRefl
+lemInitApp :: Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
+lemInitApp _ _ = unsafeCoerceRefl
+
-- ** KnownNat
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs
index 95cd4ef..a15e0a2 100644
--- a/src/Data/Array/Mixed/Shape.hs
+++ b/src/Data/Array/Mixed/Shape.hs
@@ -117,6 +117,10 @@ listxDrop :: forall f g sh sh'. ListX (sh ++ sh') f -> ListX sh g -> ListX sh' f
listxDrop long ZX = long
listxDrop long (_ ::% short) = case long of _ ::% long' -> listxDrop long' short
+listxInit :: forall f n sh. ListX (n : sh) f -> ListX (Init (n : sh)) f
+listxInit (i ::% sh@(_ ::% _)) = i ::% listxInit sh
+listxInit (_ ::% ZX) = ZX
+
-- * Mixed indices
@@ -172,6 +176,9 @@ ixxAppend = coerce (listxAppend @_ @(Const i))
ixxDrop :: forall sh sh' i. IxX (sh ++ sh') i -> IxX sh i -> IxX sh' i
ixxDrop = coerce (listxDrop @(Const i) @(Const i))
+ixxInit :: forall n sh i. IxX (n : sh) i -> IxX (Init (n : sh)) i
+ixxInit = coerce (listxInit @(Const i))
+
ixxFromLinear :: IShX sh -> Int -> IIxX sh
ixxFromLinear = \sh i -> case go sh i of
(idx, 0) -> idx
@@ -320,6 +327,9 @@ shxDropIx = coerce (listxDrop @(SMayNat i SNat) @(Const j))
shxDropSh :: forall sh sh' i. ShX (sh ++ sh') i -> ShX sh i -> ShX sh' i
shxDropSh = coerce (listxDrop @(SMayNat i SNat) @(SMayNat i SNat))
+shxInit :: forall n sh i. ShX (n : sh) i -> ShX (Init (n : sh)) i
+shxInit = coerce (listxInit @(SMayNat i SNat))
+
shxTakeSSX :: forall sh sh' i. Proxy sh' -> ShX (sh ++ sh') i -> StaticShX sh -> ShX sh i
shxTakeSSX _ = flip go
where
diff --git a/src/Data/Array/Mixed/Types.hs b/src/Data/Array/Mixed/Types.hs
index b8f0824..22d06e5 100644
--- a/src/Data/Array/Mixed/Types.hs
+++ b/src/Data/Array/Mixed/Types.hs
@@ -28,6 +28,7 @@ module Data.Array.Mixed.Types (
lemReplicateSucc,
MapJust,
Tail,
+ Init,
-- * Unsafe
unsafeCoerceRefl,
@@ -100,6 +101,10 @@ type family MapJust l where
type family Tail l where
Tail (_ : xs) = xs
+type family Init l where
+ Init (x : y : xs) = x : Init (y : xs)
+ Init '[x] = '[]
+
-- | This is just @'Unsafe.Coerce.unsafeCoerce' 'Refl'@, but specialised to
-- only typecheck for actual type equalities. One cannot, e.g. accidentally