From 4a0b2ef27a6e31250c56faef0efc0abf611a0cda Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 18 Jun 2024 21:04:23 +0200
Subject: Init on ListX

---
 src/Data/Array/Mixed/Lemmas.hs |  3 +++
 src/Data/Array/Mixed/Shape.hs  | 10 ++++++++++
 src/Data/Array/Mixed/Types.hs  |  5 +++++
 3 files changed, 18 insertions(+)

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
-- 
cgit v1.2.3-70-g09d2