diff options
author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-05-11 15:07:00 +0200 |
---|---|---|
committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-05-11 15:07:00 +0200 |
commit | 8813be523b6c8095c4c04c15b43e91a915c1c7c3 (patch) | |
tree | aa11a856d002d140641d18874b8606b669e63242 /src/Data/Array/Mixed/Shape.hs | |
parent | 3298f8b2da0bb3abf38fc57f66c1b9732a3ddc8a (diff) |
Fill in missing Head and HEAD
Diffstat (limited to 'src/Data/Array/Mixed/Shape.hs')
-rw-r--r-- | src/Data/Array/Mixed/Shape.hs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs index 99a137d..b49e005 100644 --- a/src/Data/Array/Mixed/Shape.hs +++ b/src/Data/Array/Mixed/Shape.hs @@ -130,6 +130,9 @@ listxToList :: ListX sh' (Const i) -> [i] listxToList ZX = [] listxToList (Const i ::% is) = i : listxToList is +listxHead :: ListX (mn ': sh) f -> f mn +listxHead (i ::% _) = i + listxTail :: ListX (n : sh) i -> ListX sh i listxTail (_ ::% sh) = sh @@ -201,6 +204,9 @@ ixxZero' (_ :$% sh) = 0 :.% ixxZero' sh ixxFromList :: forall sh i. StaticShX sh -> [i] -> IxX sh i ixxFromList = coerce (listxFromList @_ @i) +ixxHead :: IxX (n : sh) i -> i +ixxHead (IxX list) = getConst (listxHead list) + ixxTail :: IxX (n : sh) i -> IxX sh i ixxTail (IxX list) = IxX (listxTail list) @@ -372,6 +378,9 @@ shxToList (smn :$% sh) = fromSMayNat' smn : shxToList sh shxAppend :: forall sh sh' i. ShX sh i -> ShX sh' i -> ShX (sh ++ sh') i shxAppend = coerce (listxAppend @_ @(SMayNat i SNat)) +shxHead :: ShX (n : sh) i -> SMayNat i SNat n +shxHead (ShX list) = listxHead list + shxTail :: ShX (n : sh) i -> ShX sh i shxTail (ShX list) = ShX (listxTail list) @@ -474,6 +483,9 @@ ssxAppend :: StaticShX sh -> StaticShX sh' -> StaticShX (sh ++ sh') ssxAppend ZKX sh' = sh' ssxAppend (n :!% sh) sh' = n :!% ssxAppend sh sh' +ssxHead :: StaticShX (n : sh) -> SMayNat () SNat n +ssxHead (StaticShX list) = listxHead list + ssxTail :: StaticShX (n : sh) -> StaticShX sh ssxTail (_ :!% ssh) = ssh |