aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTom Smeding <t.j.smeding@uu.nl>2024-04-03 15:06:52 +0200
committerTom Smeding <t.j.smeding@uu.nl>2024-04-03 15:06:52 +0200
commitffa91484573a2c2be3f6ae2190c768e7a77e8b5c (patch)
tree361f08f2f65eda1128c5d03da2a45305d66e0351 /src
parent6520c4e4bc39b7315f4f9416fe68b883cfdde8ec (diff)
Simple usage example
Diffstat (limited to 'src')
-rw-r--r--src/Data/Array/Nested/Internal.hs5
-rw-r--r--src/Data/Nat.hs17
2 files changed, 22 insertions, 0 deletions
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