diff options
| -rw-r--r-- | ox-arrays.cabal | 10 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 5 | ||||
| -rw-r--r-- | src/Data/Nat.hs | 17 | ||||
| -rw-r--r-- | test/Main.hs | 21 |
4 files changed, 53 insertions, 0 deletions
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 |