diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-06-29 13:44:42 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-06-29 13:44:42 +0200 |
| commit | e2798d8924c0ec087bf149ed32e35b92892e2f15 (patch) | |
| tree | 3ff2213baa90077263ef021148e978e65d7db4f9 | |
| parent | dc0270a1fd5db180df88023bb2628b046447df0d (diff) | |
Add existential conversions to ShS
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index fd59ba6..2438f68 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -14,7 +15,7 @@ module Data.Array.Nested.Convert ( ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShX, shrFromShX2, listrCast, ixrCast, shrCast, -- ** To shaped - ixsFromIxR, ixsFromIxR', ixsFromIxX, ixsFromIxX', shsFromShX, shsFromSSX, + ixsFromIxR, ixsFromIxR', ixsFromIxX, ixsFromIxX', withShsFromShR, shsFromShX, withShsFromShX, shsFromSSX, ixsCast, -- ** To mixed ixxFromIxR, ixxFromIxS, shxFromShR, shxFromShS, @@ -101,8 +102,30 @@ ixsFromIxX' ZSS ZIX = ZIS ixsFromIxX' (_ :$$ sh) (n :.% idx) = n :.$ ixsFromIxX' sh idx ixsFromIxX' _ _ = error "ixsFromIxX': index rank does not match shape rank" +-- | Produce an existential 'ShS' from an 'IShR'. +withShsFromShR :: IShR n -> (forall sh. Rank sh ~ n => ShS sh -> r) -> r +withShsFromShR ZSR k = k ZSS +withShsFromShR (n :$: sh) k = + withShsFromShR sh $ \sh' -> + withSomeSNat (fromIntegral @Int @Integer n) $ \case + Just sn@SNat -> k (sn :$$ sh') + Nothing -> error $ "withShsFromShR: negative dimension size (" ++ show n ++ ")" + -- shsFromShX re-exported +-- | Produce an existential 'ShS' from an 'IShX'. If you already know that +-- @sh'@ is @MapJust@ of something, use 'shsFromShX' instead. +withShsFromShX :: IShX sh' -> (forall sh. Rank sh ~ Rank sh' => ShS sh -> r) -> r +withShsFromShX ZSX k = k ZSS +withShsFromShX (SKnown sn@SNat :$% sh) k = + withShsFromShX sh $ \sh' -> + k (sn :$$ sh') +withShsFromShX (SUnknown n :$% sh) k = + withShsFromShX sh $ \sh' -> + withSomeSNat (fromIntegral @Int @Integer n) $ \case + Just sn@SNat -> k (sn :$$ sh') + Nothing -> error $ "withShsFromShX: negative SUnknown dimension size (" ++ show n ++ ")" + shsFromSSX :: StaticShX (MapJust sh) -> ShS sh shsFromSSX = shsFromShX Prelude.. shxFromSSX |