From 8b59d8ef4ff97936f2a753d1ce345e0404c26b2b Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Thu, 30 May 2024 22:47:52 +0200
Subject: Clearer module purposes

Thanks Mikolaj for discussion
---
 src/Data/Array/Nested/Internal/Convert.hs | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 src/Data/Array/Nested/Internal/Convert.hs

(limited to 'src/Data/Array/Nested/Internal/Convert.hs')

diff --git a/src/Data/Array/Nested/Internal/Convert.hs b/src/Data/Array/Nested/Internal/Convert.hs
new file mode 100644
index 0000000..e101981
--- /dev/null
+++ b/src/Data/Array/Nested/Internal/Convert.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.Array.Nested.Internal.Convert where
+
+import Data.Type.Equality
+
+import Data.Array.Mixed.Lemmas
+import Data.Array.Mixed.Shape
+import Data.Array.Nested.Internal.Lemmas
+import Data.Array.Nested.Internal.Mixed
+import Data.Array.Nested.Internal.Ranked
+import Data.Array.Nested.Internal.Shape
+import Data.Array.Nested.Internal.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
-- 
cgit v1.2.3-70-g09d2