From 4a0b2ef27a6e31250c56faef0efc0abf611a0cda Mon Sep 17 00:00:00 2001 From: Tom Smeding 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(+) (limited to 'src/Data') 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