From ffa91484573a2c2be3f6ae2190c768e7a77e8b5c Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Wed, 3 Apr 2024 15:06:52 +0200
Subject: Simple usage example

---
 ox-arrays.cabal                   | 10 ++++++++++
 src/Data/Array/Nested/Internal.hs |  5 +++++
 src/Data/Nat.hs                   | 17 +++++++++++++++++
 test/Main.hs                      | 21 +++++++++++++++++++++
 4 files changed, 53 insertions(+)
 create mode 100644 test/Main.hs

diff --git a/ox-arrays.cabal b/ox-arrays.cabal
index 5bdff7d..972917a 100644
--- a/ox-arrays.cabal
+++ b/ox-arrays.cabal
@@ -20,3 +20,13 @@ library
   hs-source-dirs: src
   default-language: Haskell2010
   ghc-options: -Wall
+
+test-suite test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  build-depends:
+    ox-arrays,
+    base
+  hs-source-dirs: test
+  default-language: Haskell2010
+  ghc-options: -Wall
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index 7d4621a..fa40921 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -425,12 +425,17 @@ data SShape sh where
   ShNil :: SShape '[]
   ShCons :: SNat n -> SShape sh -> SShape (n : sh)
 deriving instance Show (SShape sh)
+infixr 5 `ShCons`
 
 -- | A statically-known shape of a shape-typed array.
 class KnownShape sh where knownShape :: SShape sh
 instance KnownShape '[] where knownShape = ShNil
 instance (KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons knownNat knownShape
 
+sshapeKnown :: SShape sh -> Dict KnownShape sh
+sshapeKnown ShNil = Dict
+sshapeKnown (ShCons n sh) | Dict <- snatKnown n, Dict <- sshapeKnown sh = Dict
+
 lemKnownMapJust :: forall sh. KnownShape sh => Proxy sh -> Dict KnownShapeX (MapJust sh)
 lemKnownMapJust _ = X.lemKnownShapeX (go (knownShape @sh))
   where
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index 5dacc8a..b154f67 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -44,6 +44,10 @@ unSNat :: SNat n -> Natural
 unSNat SZ = 0
 unSNat (SS n) = 1 + unSNat n
 
+-- | Convert an 'SNat' to an integer.
+unSNat' :: SNat n -> Int
+unSNat' = fromIntegral . unSNat
+
 -- | A 'KnownNat' dictionary is just a singleton natural, so we can create
 -- evidence of 'KnownNat' given an 'SNat'.
 snatKnown :: SNat n -> Dict KnownNat n
@@ -68,3 +72,16 @@ gknownNat (Proxy @n) = go (knownNat @n)
     go :: SNat m -> Dict G.KnownNat (GNat m)
     go SZ = Dict
     go (SS n) | Dict <- go n = Dict
+
+-- * Some type-level naturals
+
+type N0 = Z
+type N1 = S N0
+type N2 = S N1
+type N3 = S N2
+type N4 = S N3
+type N5 = S N4
+type N6 = S N5
+type N7 = S N6
+type N8 = S N7
+type N9 = S N8
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
index 0000000..156e0a5
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
+module Main where
+
+import Data.Array.Nested
+
+
+arr :: Ranked N2 (Shaped [N2, N3] (Double, Int))
+arr = rgenerate (3 ::: 4 ::: IZR) $ \(i ::: j ::: IZR) ->
+        sgenerate @[N2, N3] (2 ::$ 3 ::$ IZS) $ \(k ::$ l ::$ IZS) ->
+          let s = i + j + k + l
+          in (fromIntegral s, s)
+
+foo :: (Double, Int)
+foo = arr `rindex` (2 ::: 1 ::: IZR) `sindex` (1 ::$ 1 ::$ IZS)
+
+main :: IO ()
+main = do
+  print arr
+  print foo
-- 
cgit v1.2.3-70-g09d2