commit 197dab3b229815a74a8098b672a1d2eb1a491806
parent db6d10b99f3a092cb6b2ddc16c0aa166bf5c083d
Author: Robert Russell <robert@rr3.xyz>
Date: Sat, 5 Jul 2025 16:16:29 -0700
Hide unsafe constructors
Diffstat:
8 files changed, 135 insertions(+), 115 deletions(-)
diff --git a/src/Naturals/Finat.hs b/src/Naturals/Finat.hs
@@ -1,35 +1,5 @@
module Naturals.Finat (
- Finat (..),
- finatMirror,
+ module Naturals.Finat.Unsafe,
) where
-import GHC.Natural
-import Unsafe.Coerce
-
-import Naturals.IsFin
-import Naturals.Nat
-import Naturals.Natural
-import Naturals.Peano
-import Naturals.Snat
-
--- | Finite (@Peano@-indexed) prefixes of @Nat@.
-newtype Finat (n :: Peano) = FinatUnsafe Nat deriving newtype (Show, Eq)
-
-instance ToNat (Finat n) where
- toNat (FinatUnsafe n) = n
-
-instance ToNatural (Finat n) where
- toNatural = wordToNatural . fromNat . toNat
-
-instance IsFin Finat where
- finZero = FinatUnsafe 0
-
- finSucc = FinatUnsafe . succ . toNat
-
- finPeel (FinatUnsafe 0) = unsafeCoerce FZeroOp
- finPeel (FinatUnsafe n) = unsafeCoerce FSuccOp . FinatUnsafe . pred $ n
-
- finWeaken (FinatUnsafe n) = FinatUnsafe n
-
-finatMirror :: Snat n -> Finat n -> Finat n
-finatMirror (SnatUnsafe n) (FinatUnsafe i) = FinatUnsafe (n - i - 1)
+import Naturals.Finat.Unsafe hiding (FinatUnsafe)
diff --git a/src/Naturals/Finat/Unsafe.hs b/src/Naturals/Finat/Unsafe.hs
@@ -0,0 +1,35 @@
+module Naturals.Finat.Unsafe (
+ Finat (..),
+ finatMirror,
+) where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsFin
+import Naturals.Nat
+import Naturals.Natural
+import Naturals.Peano
+import Naturals.Snat.Unsafe
+
+-- | Finite (@Peano@-indexed) prefixes of @Nat@.
+newtype Finat (n :: Peano) = FinatUnsafe Nat deriving newtype (Show, Eq)
+
+instance ToNat (Finat n) where
+ toNat (FinatUnsafe n) = n
+
+instance ToNatural (Finat n) where
+ toNatural = wordToNatural . fromNat . toNat
+
+instance IsFin Finat where
+ finZero = FinatUnsafe 0
+
+ finSucc = FinatUnsafe . succ . toNat
+
+ finPeel (FinatUnsafe 0) = unsafeCoerce FZeroOp
+ finPeel (FinatUnsafe n) = unsafeCoerce FSuccOp . FinatUnsafe . pred $ n
+
+ finWeaken (FinatUnsafe n) = FinatUnsafe n
+
+finatMirror :: Snat n -> Finat n -> Finat n
+finatMirror (SnatUnsafe n) (FinatUnsafe i) = FinatUnsafe (n - i - 1)
diff --git a/src/Naturals/Finatural.hs b/src/Naturals/Finatural.hs
@@ -1,31 +1,5 @@
module Naturals.Finatural (
- Finatural (..),
- finaturalMirror,
+ module Naturals.Finatural.Unsafe,
) where
-import GHC.Natural
-import Unsafe.Coerce
-
-import Naturals.IsFin
-import Naturals.Natural
-import Naturals.Peano
-import Naturals.Snatural
-
--- | Finite (@Peano@-indexed) prefixes of @Natural@.
-newtype Finatural (n :: Peano) = FinaturalUnsafe Natural deriving newtype (Show, Eq)
-
-instance ToNatural (Finatural n) where
- toNatural (FinaturalUnsafe n) = n
-
-instance IsFin Finatural where
- finZero = FinaturalUnsafe 0
-
- finSucc = FinaturalUnsafe . succ . toNatural
-
- finPeel (FinaturalUnsafe 0) = unsafeCoerce FZeroOp
- finPeel (FinaturalUnsafe n) = unsafeCoerce FSuccOp . FinaturalUnsafe . pred $ n
-
- finWeaken (FinaturalUnsafe n) = FinaturalUnsafe n
-
-finaturalMirror :: Snatural n -> Finatural n -> Finatural n
-finaturalMirror (SnaturalUnsafe n) (FinaturalUnsafe i) = FinaturalUnsafe (n - i - 1)
+import Naturals.Finatural.Unsafe hiding (FinaturalUnsafe)
diff --git a/src/Naturals/Finatural/Unsafe.hs b/src/Naturals/Finatural/Unsafe.hs
@@ -0,0 +1,31 @@
+module Naturals.Finatural.Unsafe (
+ Finatural (..),
+ finaturalMirror,
+) where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsFin
+import Naturals.Natural
+import Naturals.Peano
+import Naturals.Snatural.Unsafe
+
+-- | Finite (@Peano@-indexed) prefixes of @Natural@.
+newtype Finatural (n :: Peano) = FinaturalUnsafe Natural deriving newtype (Show, Eq)
+
+instance ToNatural (Finatural n) where
+ toNatural (FinaturalUnsafe n) = n
+
+instance IsFin Finatural where
+ finZero = FinaturalUnsafe 0
+
+ finSucc = FinaturalUnsafe . succ . toNatural
+
+ finPeel (FinaturalUnsafe 0) = unsafeCoerce FZeroOp
+ finPeel (FinaturalUnsafe n) = unsafeCoerce FSuccOp . FinaturalUnsafe . pred $ n
+
+ finWeaken (FinaturalUnsafe n) = FinaturalUnsafe n
+
+finaturalMirror :: Snatural n -> Finatural n -> Finatural n
+finaturalMirror (SnaturalUnsafe n) (FinaturalUnsafe i) = FinaturalUnsafe (n - i - 1)
diff --git a/src/Naturals/Snat.hs b/src/Naturals/Snat.hs
@@ -1,33 +1,5 @@
module Naturals.Snat (
- Snat (..),
+ module Naturals.Snat.Unsafe,
) where
-import GHC.Natural
-import Unsafe.Coerce
-
-import Naturals.IsSpeano
-import Naturals.Nat
-import Naturals.Natural
-import Naturals.Peano
-
--- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
-newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show)
-
-instance Eq (Snat n) where
- _ == _ = True
-
-instance ToNat (Snat n) where
- toNat (SnatUnsafe n) = n
-
-instance ToNatural (Snat n) where
- toNatural = wordToNatural . fromNat . toNat
-
-instance IsSpeano Snat where
- speanoZero = SnatUnsafe 0
-
- speanoSucc = SnatUnsafe . succ . toNat
-
- speanoPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
- speanoPeel (SnatUnsafe n) = unsafeCoerce SuccOp . SnatUnsafe . pred $ n
-
- speanoAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
+import Naturals.Snat.Unsafe hiding (SnatUnsafe)
diff --git a/src/Naturals/Snat/Unsafe.hs b/src/Naturals/Snat/Unsafe.hs
@@ -0,0 +1,33 @@
+module Naturals.Snat.Unsafe (
+ Snat (..),
+) where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsSpeano
+import Naturals.Nat
+import Naturals.Natural
+import Naturals.Peano
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
+newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show)
+
+instance Eq (Snat n) where
+ _ == _ = True
+
+instance ToNat (Snat n) where
+ toNat (SnatUnsafe n) = n
+
+instance ToNatural (Snat n) where
+ toNatural = wordToNatural . fromNat . toNat
+
+instance IsSpeano Snat where
+ speanoZero = SnatUnsafe 0
+
+ speanoSucc = SnatUnsafe . succ . toNat
+
+ speanoPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
+ speanoPeel (SnatUnsafe n) = unsafeCoerce SuccOp . SnatUnsafe . pred $ n
+
+ speanoAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
diff --git a/src/Naturals/Snatural.hs b/src/Naturals/Snatural.hs
@@ -1,28 +1,5 @@
module Naturals.Snatural (
- Snatural (..),
+ module Naturals.Snatural.Unsafe,
) where
-import Unsafe.Coerce
-
-import Naturals.IsSpeano
-import Naturals.Natural
-import Naturals.Peano
-
--- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
-newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving newtype (Show)
-
-instance Eq (Snatural n) where
- _ == _ = True
-
-instance ToNatural (Snatural n) where
- toNatural (SnaturalUnsafe n) = n
-
-instance IsSpeano Snatural where
- speanoZero = SnaturalUnsafe 0
-
- speanoSucc = SnaturalUnsafe . succ . toNatural
-
- speanoPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
- speanoPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp . SnaturalUnsafe . pred $ n
-
- speanoAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
+import Naturals.Snatural.Unsafe hiding (SnaturalUnsafe)
diff --git a/src/Naturals/Snatural/Unsafe.hs b/src/Naturals/Snatural/Unsafe.hs
@@ -0,0 +1,28 @@
+module Naturals.Snatural.Unsafe (
+ Snatural (..),
+) where
+
+import Unsafe.Coerce
+
+import Naturals.IsSpeano
+import Naturals.Natural
+import Naturals.Peano
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
+newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving newtype (Show)
+
+instance Eq (Snatural n) where
+ _ == _ = True
+
+instance ToNatural (Snatural n) where
+ toNatural (SnaturalUnsafe n) = n
+
+instance IsSpeano Snatural where
+ speanoZero = SnaturalUnsafe 0
+
+ speanoSucc = SnaturalUnsafe . succ . toNatural
+
+ speanoPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
+ speanoPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp . SnaturalUnsafe . pred $ n
+
+ speanoAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
