diff options
author | Tom Smeding <tom@tomsmeding.com> | 2024-05-30 22:20:57 +0200 |
---|---|---|
committer | Tom Smeding <tom@tomsmeding.com> | 2024-05-30 22:20:57 +0200 |
commit | f0752d67cd188f438280e1f0c692dc1f5f14a190 (patch) | |
tree | 2dd05c13aef3b3c6384bfa091b14633bc86e65a4 /src/Data/Array/Nested/Convert.hs | |
parent | 19eab026f4f4c6a2d38ceb1fffa6062ba2637a46 (diff) |
Refactor Nested (modules, function names)
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
-rw-r--r-- | src/Data/Array/Nested/Convert.hs | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs new file mode 100644 index 0000000..cb22c32 --- /dev/null +++ b/src/Data/Array/Nested/Convert.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +module Data.Array.Nested.Convert where + +import Data.Type.Equality + +import Data.Array.Mixed.Lemmas +import Data.Array.Mixed.Shape +import Data.Array.Nested.Lemmas +import Data.Array.Nested.Mixed +import Data.Array.Nested.Ranked +import Data.Array.Nested.Shape +import Data.Array.Nested.Shaped + + +stoRanked :: Elt a => Shaped sh a -> Ranked (Rank sh) a +stoRanked sarr@(Shaped arr) + | Refl <- lemRankMapJust (sshape sarr) + = mtoRanked arr + +rcastToShaped :: Elt a => Ranked (Rank sh) a -> ShS sh -> Shaped sh a +rcastToShaped (Ranked arr) targetsh + | Refl <- lemRankReplicate (shxRank (shCvtSX targetsh)) + , Refl <- lemRankMapJust targetsh + = mcastToShaped arr targetsh |