From ffa91484573a2c2be3f6ae2190c768e7a77e8b5c Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 3 Apr 2024 15:06:52 +0200 Subject: Simple usage example --- src/Data/Array/Nested/Internal.hs | 5 +++++ src/Data/Nat.hs | 17 +++++++++++++++++ 2 files changed, 22 insertions(+) (limited to 'src') 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 -- cgit v1.2.3-70-g09d2