aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Data/Array/Mixed.hs62
-rw-r--r--src/Data/Array/Nested.hs6
-rw-r--r--src/Data/Array/Nested/Internal.hs72
-rw-r--r--src/Data/INat.hs95
-rw-r--r--src/Data/Nat.hs87
5 files changed, 166 insertions, 156 deletions
diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index 2bbf81d..049a0c4 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -17,16 +17,16 @@ import Data.Kind
import Data.Proxy
import Data.Type.Equality
import qualified Data.Vector.Storable as VS
-import qualified GHC.TypeLits as GHC
+import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
-import Data.Nat
+import Data.INat
--- | The 'GHC.SNat' pattern synonym is complete, but it doesn't have a
+-- | The 'SNat' pattern synonym is complete, but it doesn't have a
-- @COMPLETE@ pragma. This copy of it does.
-pattern GHC_SNat :: () => GHC.KnownNat n => GHC.SNat n
-pattern GHC_SNat = GHC.SNat
+pattern GHC_SNat :: () => KnownNat n => SNat n
+pattern GHC_SNat = SNat
{-# COMPLETE GHC_SNat #-}
@@ -42,7 +42,7 @@ lemAppAssoc :: Proxy a -> Proxy b -> Proxy c -> (a ++ b) ++ c :~: a ++ (b ++ c)
lemAppAssoc _ _ _ = unsafeCoerce Refl
-type IxX :: [Maybe GHC.Nat] -> Type
+type IxX :: [Maybe Nat] -> Type
data IxX sh where
IZX :: IxX '[]
(::@) :: Int -> IxX sh -> IxX (Just n : sh)
@@ -52,23 +52,23 @@ infixr 5 ::@
infixr 5 ::?
-- | The part of a shape that is statically known.
-type StaticShapeX :: [Maybe GHC.Nat] -> Type
+type StaticShapeX :: [Maybe Nat] -> Type
data StaticShapeX sh where
SZX :: StaticShapeX '[]
- (:$@) :: GHC.SNat n -> StaticShapeX sh -> StaticShapeX (Just n : sh)
+ (:$@) :: SNat n -> StaticShapeX sh -> StaticShapeX (Just n : sh)
(:$?) :: () -> StaticShapeX sh -> StaticShapeX (Nothing : sh)
deriving instance Show (StaticShapeX sh)
infixr 5 :$@
infixr 5 :$?
-- | Evidence for the static part of a shape.
-type KnownShapeX :: [Maybe GHC.Nat] -> Constraint
+type KnownShapeX :: [Maybe Nat] -> Constraint
class KnownShapeX sh where
knownShapeX :: StaticShapeX sh
instance KnownShapeX '[] where
knownShapeX = SZX
-instance (GHC.KnownNat n, KnownShapeX sh) => KnownShapeX (Just n : sh) where
- knownShapeX = GHC.natSing :$@ knownShapeX
+instance (KnownNat n, KnownShapeX sh) => KnownShapeX (Just n : sh) where
+ knownShapeX = natSing :$@ knownShapeX
instance KnownShapeX sh => KnownShapeX (Nothing : sh) where
knownShapeX = () :$? knownShapeX
@@ -76,8 +76,8 @@ type family Rank sh where
Rank '[] = Z
Rank (_ : sh) = S (Rank sh)
-type XArray :: [Maybe GHC.Nat] -> Type -> Type
-data XArray sh a = XArray (S.Array (GNat (Rank sh)) a)
+type XArray :: [Maybe Nat] -> Type -> Type
+data XArray sh a = XArray (S.Array (FromINat (Rank sh)) a)
deriving (Show)
zeroIdx :: StaticShapeX sh -> IxX sh
@@ -165,19 +165,19 @@ ssxIotaFrom i (_ :$@ ssh) = i : ssxIotaFrom (i+1) ssh
ssxIotaFrom i (_ :$? ssh) = i : ssxIotaFrom (i+1) ssh
lemRankApp :: StaticShapeX sh1 -> StaticShapeX sh2
- -> GNat (Rank (sh1 ++ sh2)) :~: GNat (Rank sh1) GHC.+ GNat (Rank sh2)
+ -> FromINat (Rank (sh1 ++ sh2)) :~: FromINat (Rank sh1) + FromINat (Rank sh2)
lemRankApp _ _ = unsafeCoerce Refl -- TODO improve this
lemRankAppComm :: StaticShapeX sh1 -> StaticShapeX sh2
- -> GNat (Rank (sh1 ++ sh2)) :~: GNat (Rank (sh2 ++ sh1))
+ -> FromINat (Rank (sh1 ++ sh2)) :~: FromINat (Rank (sh2 ++ sh1))
lemRankAppComm _ _ = unsafeCoerce Refl -- TODO improve this
-lemKnownNatRank :: IxX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRank :: IxX sh -> Dict KnownINat (Rank sh)
lemKnownNatRank IZX = Dict
lemKnownNatRank (_ ::@ sh) | Dict <- lemKnownNatRank sh = Dict
lemKnownNatRank (_ ::? sh) | Dict <- lemKnownNatRank sh = Dict
-lemKnownNatRankSSX :: StaticShapeX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRankSSX :: StaticShapeX sh -> Dict KnownINat (Rank sh)
lemKnownNatRankSSX SZX = Dict
lemKnownNatRankSSX (_ :$@ ssh) | Dict <- lemKnownNatRankSSX ssh = Dict
lemKnownNatRankSSX (_ :$? ssh) | Dict <- lemKnownNatRankSSX ssh = Dict
@@ -201,14 +201,14 @@ shape (XArray arr) = go (knownShapeX @sh) (S.shapeL arr)
where
go :: StaticShapeX sh' -> [Int] -> IxX sh'
go SZX [] = IZX
- go (n :$@ ssh) (_ : l) = fromIntegral (GHC.fromSNat n) ::@ go ssh l
+ go (n :$@ ssh) (_ : l) = fromIntegral (fromSNat n) ::@ go ssh l
go (() :$? ssh) (n : l) = n ::? go ssh l
go _ _ = error "Invalid shapeL"
fromVector :: forall sh a. S.Unbox a => IxX sh -> VS.Vector a -> XArray sh a
fromVector sh v
| Dict <- lemKnownNatRank sh
- , Dict <- gknownNat (Proxy @(Rank sh))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh))
= XArray (S.fromVector (shapeLshape sh) v)
toVector :: S.Unbox a => XArray sh a -> VS.Vector a
@@ -242,7 +242,7 @@ index xarr i
append :: forall sh a. (KnownShapeX sh, S.Unbox a) => XArray sh a -> XArray sh a -> XArray sh a
append (XArray a) (XArray b)
| Dict <- lemKnownNatRankSSX (knownShapeX @sh)
- , Dict <- gknownNat (Proxy @(Rank sh))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh))
= XArray (S.append a b)
rerank :: forall sh sh1 sh2 a b.
@@ -252,14 +252,14 @@ rerank :: forall sh sh1 sh2 a b.
-> XArray (sh ++ sh1) a -> XArray (sh ++ sh2) b
rerank ssh ssh1 ssh2 f (XArray arr)
| Dict <- lemKnownNatRankSSX ssh
- , Dict <- gknownNat (Proxy @(Rank sh))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh))
, Dict <- lemKnownNatRankSSX ssh2
- , Dict <- gknownNat (Proxy @(Rank sh2))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh2))
, Refl <- lemRankApp ssh ssh1
, Refl <- lemRankApp ssh ssh2
, Dict <- lemKnownNatRankSSX (ssxAppend ssh ssh2) -- these two should be redundant but the
- , Dict <- gknownNat (Proxy @(Rank (sh ++ sh2))) -- solver is not clever enough
- = XArray (S.rerank @(GNat (Rank sh)) @(GNat (Rank sh1)) @(GNat (Rank sh2))
+ , Dict <- knownNatFromINat (Proxy @(Rank (sh ++ sh2))) -- solver is not clever enough
+ = XArray (S.rerank @(FromINat (Rank sh)) @(FromINat (Rank sh1)) @(FromINat (Rank sh2))
(\a -> unXArray (f (XArray a)))
arr)
where
@@ -279,14 +279,14 @@ rerank2 :: forall sh sh1 sh2 a b c.
-> XArray (sh ++ sh1) a -> XArray (sh ++ sh1) b -> XArray (sh ++ sh2) c
rerank2 ssh ssh1 ssh2 f (XArray arr1) (XArray arr2)
| Dict <- lemKnownNatRankSSX ssh
- , Dict <- gknownNat (Proxy @(Rank sh))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh))
, Dict <- lemKnownNatRankSSX ssh2
- , Dict <- gknownNat (Proxy @(Rank sh2))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh2))
, Refl <- lemRankApp ssh ssh1
, Refl <- lemRankApp ssh ssh2
, Dict <- lemKnownNatRankSSX (ssxAppend ssh ssh2) -- these two should be redundant but the
- , Dict <- gknownNat (Proxy @(Rank (sh ++ sh2))) -- solver is not clever enough
- = XArray (S.rerank2 @(GNat (Rank sh)) @(GNat (Rank sh1)) @(GNat (Rank sh2))
+ , Dict <- knownNatFromINat (Proxy @(Rank (sh ++ sh2))) -- solver is not clever enough
+ = XArray (S.rerank2 @(FromINat (Rank sh)) @(FromINat (Rank sh1)) @(FromINat (Rank sh2))
(\a b -> unXArray (f (XArray a) (XArray b)))
arr1 arr2)
where
@@ -296,7 +296,7 @@ rerank2 ssh ssh1 ssh2 f (XArray arr1) (XArray arr2)
transpose :: forall sh a. KnownShapeX sh => [Int] -> XArray sh a -> XArray sh a
transpose perm (XArray arr)
| Dict <- lemKnownNatRankSSX (knownShapeX @sh)
- , Dict <- gknownNat (Proxy @(Rank sh))
+ , Dict <- knownNatFromINat (Proxy @(Rank sh))
= XArray (S.transpose perm arr)
transpose2 :: forall sh1 sh2 a.
@@ -306,9 +306,9 @@ transpose2 ssh1 ssh2 (XArray arr)
| Refl <- lemRankApp ssh1 ssh2
, Refl <- lemRankApp ssh2 ssh1
, Dict <- lemKnownNatRankSSX (ssxAppend ssh1 ssh2)
- , Dict <- gknownNat (Proxy @(Rank (sh1 ++ sh2)))
+ , Dict <- knownNatFromINat (Proxy @(Rank (sh1 ++ sh2)))
, Dict <- lemKnownNatRankSSX (ssxAppend ssh2 ssh1)
- , Dict <- gknownNat (Proxy @(Rank (sh2 ++ sh1)))
+ , Dict <- knownNatFromINat (Proxy @(Rank (sh2 ++ sh1)))
, Refl <- lemRankAppComm ssh1 ssh2
, let n1 = ssxLength ssh1
= XArray (S.transpose (ssxIotaFrom n1 ssh2 ++ ssxIotaFrom 0 ssh1) arr)
diff --git a/src/Data/Array/Nested.hs b/src/Data/Array/Nested.hs
index aa7c7f9..0de3884 100644
--- a/src/Data/Array/Nested.hs
+++ b/src/Data/Array/Nested.hs
@@ -27,8 +27,8 @@ module Data.Array.Nested (
Elt(mshape, mindex, mindexPartial, mlift),
Primitive(..),
- -- * Natural numbers
- module Data.Nat,
+ -- * Inductive natural numbers
+ module Data.INat,
-- * Further utilities / re-exports
type (++),
@@ -39,4 +39,4 @@ import qualified Data.Vector.Unboxed as VU
import Data.Array.Mixed
import Data.Array.Nested.Internal
-import Data.Nat
+import Data.INat
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index 41fb1fd..15d72f0 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -21,7 +21,7 @@ TODO:
* We should be more consistent in whether functions take a 'StaticShapeX'
argument or a 'KnownShapeX' constraint.
-* Document the choice of using 'Nat' for ranks and 'GHC.Nat' for shapes. Point
+* Document the choice of using 'INat' for ranks and 'Nat' for shapes. Point
being that we need to do induction over the former, but the latter need to be
able to get large.
@@ -38,11 +38,11 @@ import Data.Type.Equality
import qualified Data.Vector.Storable as VS
import qualified Data.Vector.Storable.Mutable as VSM
import Foreign.Storable (Storable)
-import qualified GHC.TypeLits as GHC
+import GHC.TypeLits
import Data.Array.Mixed (XArray, IxX(..), KnownShapeX(..), StaticShapeX(..), type (++), pattern GHC_SNat)
import qualified Data.Array.Mixed as X
-import Data.Nat
+import Data.INat
type family Replicate n a where
@@ -53,25 +53,25 @@ type family MapJust l where
MapJust '[] = '[]
MapJust (x : xs) = Just x : MapJust xs
-lemKnownReplicate :: forall n. KnownNat n => Proxy n -> Dict KnownShapeX (Replicate n Nothing)
-lemKnownReplicate _ = X.lemKnownShapeX (go (knownNat @n))
+lemKnownReplicate :: forall n. KnownINat n => Proxy n -> Dict KnownShapeX (Replicate n Nothing)
+lemKnownReplicate _ = X.lemKnownShapeX (go (inatSing @n))
where
- go :: SNat m -> StaticShapeX (Replicate m Nothing)
+ go :: SINat m -> StaticShapeX (Replicate m Nothing)
go SZ = SZX
go (SS n) = () :$? go n
-lemRankReplicate :: forall n. KnownNat n => Proxy n -> X.Rank (Replicate n (Nothing @GHC.Nat)) :~: n
-lemRankReplicate _ = go (knownNat @n)
+lemRankReplicate :: forall n. KnownINat n => Proxy n -> X.Rank (Replicate n (Nothing @Nat)) :~: n
+lemRankReplicate _ = go (inatSing @n)
where
- go :: SNat m -> X.Rank (Replicate m (Nothing @GHC.Nat)) :~: m
+ go :: SINat m -> X.Rank (Replicate m (Nothing @Nat)) :~: m
go SZ = Refl
go (SS n) | Refl <- go n = Refl
-lemReplicatePlusApp :: forall n m a. KnownNat n => Proxy n -> Proxy m -> Proxy a
- -> Replicate (n + m) a :~: Replicate n a ++ Replicate m a
-lemReplicatePlusApp _ _ _ = go (knownNat @n)
+lemReplicatePlusApp :: forall n m a. KnownINat n => Proxy n -> Proxy m -> Proxy a
+ -> Replicate (n +! m) a :~: Replicate n a ++ Replicate m a
+lemReplicatePlusApp _ _ _ = go (inatSing @n)
where
- go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a
+ go :: SINat n' -> Replicate (n' +! m) a :~: Replicate n' a ++ Replicate m a
go SZ = Refl
go (SS n) | Refl <- go n = Refl
@@ -93,7 +93,7 @@ newtype Primitive a = Primitive a
--
-- Many of the methods for working on 'Mixed' arrays come from the 'Elt' type
-- class.
-type Mixed :: [Maybe GHC.Nat] -> Type -> Type
+type Mixed :: [Maybe Nat] -> Type -> Type
data family Mixed sh a
newtype instance Mixed sh (Primitive a) = M_Primitive (XArray sh a)
@@ -117,7 +117,7 @@ deriving instance Show (Mixed (sh1 ++ sh2) a) => Show (Mixed sh1 (Mixed sh2 a))
-- | Internal helper data family mirrorring 'Mixed' that consists of mutable
-- vectors instead of 'XArray's.
-type MixedVecs :: Type -> [Maybe GHC.Nat] -> Type -> Type
+type MixedVecs :: Type -> [Maybe Nat] -> Type -> Type
data family MixedVecs s sh a
newtype instance MixedVecs s sh (Primitive a) = MV_Primitive (VS.MVector s a)
@@ -315,7 +315,7 @@ mgenerate sh f
where
checkBounds :: IxX sh' -> StaticShapeX sh' -> Bool
checkBounds IZX SZX = True
- checkBounds (n ::@ sh') (n' :$@ ssh') = n == fromIntegral (GHC.fromSNat n') && checkBounds sh' ssh'
+ checkBounds (n ::@ sh') (n' :$@ ssh') = n == fromIntegral (fromSNat n') && checkBounds sh' ssh'
checkBounds (_ ::? sh') (() :$? ssh') = checkBounds sh' ssh'
mtranspose :: forall sh a. (KnownShapeX sh, Elt a) => [Int] -> Mixed sh a -> Mixed sh a
@@ -325,29 +325,31 @@ mtranspose perm =
-- | A rank-typed array: the number of dimensions of the array (its /rank/) is
--- represented on the type level as a 'Nat'.
+-- represented on the type level as a 'INat'.
--
-- Valid elements of a ranked arrays are described by the 'Elt' type class.
-- Because 'Ranked' itself is also an instance of 'Elt', nested arrays are
-- supported (and are represented as a single, flattened, struct-of-arrays
-- array internally).
--
--- Note that this 'Nat' is not a "GHC.TypeLits" natural, because we want a
+-- Note that this 'INat' is not a "GHC.TypeLits" natural, because we want a
-- type-level natural that supports induction.
--
-- 'Ranked' is a newtype around a 'Mixed' of 'Nothing's.
-type Ranked :: Nat -> Type -> Type
+type Ranked :: INat -> Type -> Type
newtype Ranked n a = Ranked (Mixed (Replicate n Nothing) a)
deriving instance Show (Mixed (Replicate n Nothing) a) => Show (Ranked n a)
-- | A shape-typed array: the full shape of the array (the sizes of its
--- dimensions) is represented on the type level as a list of 'Nat's.
+-- dimensions) is represented on the type level as a list of 'Nat's. Note that
+-- these are "GHC.TypeLits" naturals, because we do not need induction over
+-- them and we want very large arrays to be possible.
--
-- Like for 'Ranked', the valid elements are described by the 'Elt' type class,
-- and 'Shaped' itself is again an instance of 'Elt' as well.
--
-- 'Shaped' is a newtype around a 'Mixed' of 'Just's.
-type Shaped :: [GHC.Nat] -> Type -> Type
+type Shaped :: [Nat] -> Type -> Type
newtype Shaped sh a = Shaped (Mixed (MapJust sh) a)
deriving instance Show (Mixed (MapJust sh) a) => Show (Shaped sh a)
@@ -364,7 +366,7 @@ newtype instance MixedVecs s sh (Shaped sh' a) = MV_Shaped (MixedVecs s sh (Mixe
-- 'Ranked' and 'Shaped' can already be used at the top level of an array nest;
-- these instances allow them to also be used as elements of arrays, thus
-- making them first-class in the API.
-instance (KnownNat n, Elt a) => Elt (Ranked n a) where
+instance (KnownINat n, Elt a) => Elt (Ranked n a) where
mshape (M_Ranked arr) | Dict <- lemKnownReplicate (Proxy @n) = mshape arr
mindex (M_Ranked arr) i | Dict <- lemKnownReplicate (Proxy @n) = Ranked (mindex arr i)
@@ -431,14 +433,14 @@ instance (KnownNat n, Elt a) => Elt (Ranked n a) where
-- | The shape of a shape-typed array given as a list of 'SNat' values.
data SShape sh where
ShNil :: SShape '[]
- ShCons :: GHC.SNat n -> SShape sh -> SShape (n : sh)
+ 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 (GHC.KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons GHC.natSing knownShape
+instance (KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons natSing knownShape
sshapeKnown :: SShape sh -> Dict KnownShape sh
sshapeKnown ShNil = Dict
@@ -531,7 +533,7 @@ rewriteMixed Refl x = x
-- ====== API OF RANKED ARRAYS ====== --
-- | An index into a rank-typed array.
-type IxR :: Nat -> Type
+type IxR :: INat -> Type
data IxR n where
IZR :: IxR Z
(:::) :: Int -> IxR n -> IxR (S n)
@@ -547,7 +549,7 @@ ixCvtRX IZR = IZX
ixCvtRX (n ::: idx) = n ::? ixCvtRX idx
-rshape :: forall n a. (KnownNat n, Elt a) => Ranked n a -> IxR n
+rshape :: forall n a. (KnownINat n, Elt a) => Ranked n a -> IxR n
rshape (Ranked arr)
| Dict <- lemKnownReplicate (Proxy @n)
, Refl <- lemRankReplicate (Proxy @n)
@@ -556,19 +558,19 @@ rshape (Ranked arr)
rindex :: Elt a => Ranked n a -> IxR n -> a
rindex (Ranked arr) idx = mindex arr (ixCvtRX idx)
-rindexPartial :: forall n m a. (KnownNat n, Elt a) => Ranked (n + m) a -> IxR n -> Ranked m a
+rindexPartial :: forall n m a. (KnownINat n, Elt a) => Ranked (n +! m) a -> IxR n -> Ranked m a
rindexPartial (Ranked arr) idx =
Ranked (mindexPartial @a @(Replicate n Nothing) @(Replicate m Nothing)
(rewriteMixed (lemReplicatePlusApp (Proxy @n) (Proxy @m) (Proxy @Nothing)) arr)
(ixCvtRX idx))
-rgenerate :: forall n a. (KnownNat n, Elt a) => IxR n -> (IxR n -> a) -> Ranked n a
+rgenerate :: forall n a. (KnownINat n, Elt a) => IxR n -> (IxR n -> a) -> Ranked n a
rgenerate sh f
| Dict <- lemKnownReplicate (Proxy @n)
, Refl <- lemRankReplicate (Proxy @n)
= Ranked (mgenerate (ixCvtRX sh) (f . ixCvtXR))
-rlift :: forall n1 n2 a. (KnownNat n2, Elt a)
+rlift :: forall n1 n2 a. (KnownINat n2, Elt a)
=> (forall sh' b. KnownShapeX sh' => Proxy sh' -> XArray (Replicate n1 Nothing ++ sh') b -> XArray (Replicate n2 Nothing ++ sh') b)
-> Ranked n1 a -> Ranked n2 a
rlift f (Ranked arr)
@@ -576,7 +578,7 @@ rlift f (Ranked arr)
= Ranked (mlift f arr)
rsumOuter1 :: forall n a.
- (Storable a, Num a, KnownNat n, forall sh. Coercible (Mixed sh a) (XArray sh a))
+ (Storable a, Num a, KnownINat n, forall sh. Coercible (Mixed sh a) (XArray sh a))
=> Ranked (S n) a -> Ranked n a
rsumOuter1 (Ranked arr)
| Dict <- lemKnownReplicate (Proxy @n)
@@ -586,7 +588,7 @@ rsumOuter1 (Ranked arr)
. coerce @(Mixed (Replicate (S n) Nothing) a) @(XArray (Replicate (S n) Nothing) a)
$ arr
-rtranspose :: forall n a. (KnownNat n, Elt a) => [Int] -> Ranked n a -> Ranked n a
+rtranspose :: forall n a. (KnownINat n, Elt a) => [Int] -> Ranked n a -> Ranked n a
rtranspose perm (Ranked arr)
| Dict <- lemKnownReplicate (Proxy @n)
= Ranked (mtranspose perm arr)
@@ -600,7 +602,7 @@ rtranspose perm (Ranked arr)
-- (traditionally called \"@Fin@\"). Note that because the shape of a
-- shape-typed array is known statically, you can also retrieve the array shape
-- from a 'KnownShape' dictionary.
-type IxS :: [GHC.Nat] -> Type
+type IxS :: [Nat] -> Type
data IxS sh where
IZS :: IxS '[]
(::$) :: Int -> IxS sh -> IxS (n : sh)
@@ -608,7 +610,7 @@ infixr 5 ::$
cvtSShapeIxS :: SShape sh -> IxS sh
cvtSShapeIxS ShNil = IZS
-cvtSShapeIxS (ShCons n sh) = fromIntegral (GHC.fromSNat n) ::$ cvtSShapeIxS sh
+cvtSShapeIxS (ShCons n sh) = fromIntegral (fromSNat n) ::$ cvtSShapeIxS sh
ixCvtXS :: SShape sh -> IxX (MapJust sh) -> IxS sh
ixCvtXS ShNil IZX = IZS
@@ -644,13 +646,13 @@ slift f (Shaped arr)
= Shaped (mlift f arr)
ssumOuter1 :: forall sh n a.
- (Storable a, Num a, GHC.KnownNat n, KnownShape sh, forall sh'. Coercible (Mixed sh' a) (XArray sh' a))
+ (Storable a, Num a, KnownNat n, KnownShape sh, forall sh'. Coercible (Mixed sh' a) (XArray sh' a))
=> Shaped (n : sh) a -> Shaped sh a
ssumOuter1 (Shaped arr)
| Dict <- lemKnownMapJust (Proxy @sh)
= Shaped
. coerce @(XArray (MapJust sh) a) @(Mixed (MapJust sh) a)
- . X.sumOuter (GHC.natSing @n :$@ SZX) (knownShapeX @(MapJust sh))
+ . X.sumOuter (natSing @n :$@ SZX) (knownShapeX @(MapJust sh))
. coerce @(Mixed (Just n : MapJust sh) a) @(XArray (Just n : MapJust sh) a)
$ arr
diff --git a/src/Data/INat.hs b/src/Data/INat.hs
new file mode 100644
index 0000000..f7523ee
--- /dev/null
+++ b/src/Data/INat.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+module Data.INat where
+
+import Data.Proxy
+import Numeric.Natural
+import GHC.TypeLits
+
+
+-- | Evidence for the constraint @c a@.
+data Dict c a where
+ Dict :: c a => Dict c a
+
+-- | An inductive peano natural number. Intended to be used at the type level.
+data INat = Z | S INat
+ deriving (Show)
+
+-- | Singleton for a 'INat'.
+data SINat n where
+ SZ :: SINat Z
+ SS :: SINat n -> SINat (S n)
+deriving instance Show (SINat n)
+
+-- | A singleton 'SINat' corresponding to @n@.
+class KnownINat n where inatSing :: SINat n
+instance KnownINat Z where inatSing = SZ
+instance KnownINat n => KnownINat (S n) where inatSing = SS inatSing
+
+-- | Explicitly bidirectional pattern synonym that converts between a singleton
+-- 'SINat' and evidence of a 'KnownINat' constraint. Analogous to 'GHC.SNat'.
+pattern SINat' :: () => KnownINat n => SINat n
+pattern SINat' <- (snatKnown -> Dict)
+ where SINat' = inatSing
+
+-- | A 'KnownINat' dictionary is just a singleton natural, so we can create
+-- evidence of 'KnownNat' given an 'SINat'.
+snatKnown :: SINat n -> Dict KnownINat n
+snatKnown SZ = Dict
+snatKnown (SS n) | Dict <- snatKnown n = Dict
+
+-- | Convert a 'INat' to a normal number.
+fromINat :: INat -> Natural
+fromINat Z = 0
+fromINat (S n) = 1 + fromINat n
+
+-- | Convert an 'SINat' to a normal number.
+fromSINat :: SINat n -> Natural
+fromSINat SZ = 0
+fromSINat (SS n) = 1 + fromSINat n
+
+-- | The value of a known inductive natural as a value-level integer.
+inatVal :: forall n. KnownINat n => Proxy n -> Natural
+inatVal _ = fromSINat (inatSing @n)
+
+-- | Add two 'INat's
+type family n +! m where
+ Z +! m = m
+ S n +! m = S (n +! m)
+
+-- | Convert a 'INat' to a "GHC.TypeLits" 'G.Nat'.
+type family FromINat n where
+ FromINat Z = 0
+ FromINat (S n) = 1 + FromINat n
+
+-- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits"
+-- 'G.Nat' is also known.
+knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n)
+knownNatFromINat (Proxy @n) = go (SINat' @n)
+ where
+ go :: SINat m -> Dict KnownNat (FromINat m)
+ go SZ = Dict
+ go (SS n) | Dict <- go n = Dict
+
+-- * Some type-level inductive naturals
+
+type I0 = Z
+type I1 = S I0
+type I2 = S I1
+type I3 = S I2
+type I4 = S I3
+type I5 = S I4
+type I6 = S I5
+type I7 = S I6
+type I8 = S I7
+type I9 = S I8
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
deleted file mode 100644
index b154f67..0000000
--- a/src/Data/Nat.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-module Data.Nat where
-
-import Data.Proxy
-import Numeric.Natural
-import qualified GHC.TypeLits as G
-
-
--- | Evidence for the constraint @c a@.
-data Dict c a where
- Dict :: c a => Dict c a
-
--- | A peano natural number. Intended to be used at the type level.
-data Nat = Z | S Nat
- deriving (Show)
-
--- | Singleton for a 'Nat'.
-data SNat n where
- SZ :: SNat Z
- SS :: SNat n -> SNat (S n)
-deriving instance Show (SNat n)
-
--- | A singleton 'SNat' corresponding to @n@.
-class KnownNat n where knownNat :: SNat n
-instance KnownNat Z where knownNat = SZ
-instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
-
--- | Convert a 'Nat' to a normal number.
-unNat :: Nat -> Natural
-unNat Z = 0
-unNat (S n) = 1 + unNat n
-
--- | Convert an 'SNat' to a normal number.
-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
-snatKnown SZ = Dict
-snatKnown (SS n) | Dict <- snatKnown n = Dict
-
--- | Add two 'Nat's
-type family n + m where
- Z + m = m
- S n + m = S (n + m)
-
--- | Convert a 'Nat' to a "GHC.TypeLits" 'G.Nat'.
-type family GNat n where
- GNat Z = 0
- GNat (S n) = 1 G.+ GNat n
-
--- | If an inductive 'Nat' is known, then the corresponding "GHC.TypeLits"
--- 'G.Nat' is also known.
-gknownNat :: KnownNat n => Proxy n -> Dict G.KnownNat (GNat n)
-gknownNat (Proxy @n) = go (knownNat @n)
- where
- 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
generated by cgit v1.2.3-70-g09d2 (git 2.47.0) at 2024-11-22 18:07:43 +0100