lude

commit e6a72b4809b29d1a2dba3d5766001ef2b3df7e41
parent 0448aa3d8f2e5c22bbeda64f267c84e6aced55ac
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri, 16 Oct 2026 10:12:05 -0700

Natural, Haskell.Natural: add patterns and reorganize; Integer, Haskell.Integer: init

Diffstat:
M
src/Lude.hs
 | 
1
+
A
src/Lude/Haskell/Integer.hs
 | 
28
++++++++++++++++++++++++++++
A
src/Lude/Haskell/Natural.hs
 | 
22
++++++++++++++++++++++
A
src/Lude/Integer.hs
 | 
10
++++++++++
M
src/Lude/Natural.hs
 | 
5
++++-

5 files changed, 65 insertions(+), 1 deletion(-)
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -10,6 +10,7 @@ import Lude.Error as X
 import Lude.Function as X
 import Lude.Haskell as X
 import Lude.IO as X
+import Lude.Integer as X
 import Lude.List as X
 import Lude.Maybe as X
 import Lude.Natural as X
diff --git a/src/Lude/Haskell/Integer.hs b/src/Lude/Haskell/Integer.hs
@@ -0,0 +1,28 @@
+module Lude.Haskell.Integer (
+    Integer,
+    pattern IntegerNegSucc,
+    pattern IntegerZero,
+    pattern IntegerPosSucc,
+    integerSign,
+) where
+
+import Numeric.Natural (Natural)
+import Prelude (Integer, fromInteger, fromIntegral, negate, (+), (-), (<), (==))
+
+--------------------------------------------------------------------------------
+
+pattern IntegerNegSucc :: Natural -> Integer
+pattern IntegerNegSucc n <- (integerSign -> NegSucc n) where IntegerNegSucc n = -fromIntegral (n + 1)
+pattern IntegerZero :: Integer
+pattern IntegerZero <- (integerSign -> Zero) where IntegerZero = 0
+pattern IntegerPosSucc :: Natural -> Integer
+pattern IntegerPosSucc n <- (integerSign -> PosSucc n) where IntegerPosSucc n = fromIntegral (n + 1)
+{-# COMPLETE IntegerNegSucc, IntegerZero, IntegerPosSucc #-}
+
+-- TODO: Generalize to ordered rings
+data Sign = NegSucc Natural | Zero | PosSucc Natural
+integerSign :: Integer -> Sign
+integerSign = \case
+    0 -> Zero
+    n | n < 0 -> NegSucc (fromInteger (-n) - 1)
+    n -> PosSucc (fromInteger n - 1)
diff --git a/src/Lude/Haskell/Natural.hs b/src/Lude/Haskell/Natural.hs
@@ -0,0 +1,22 @@
+module Lude.Haskell.Natural (
+    Natural,
+    pattern NaturalZero,
+    pattern NaturalSucc,
+    naturalPred,
+) where
+
+import Numeric.Natural (Natural)
+import Prelude (Maybe (..), fromInteger, (+), (-), (==))
+
+--------------------------------------------------------------------------------
+
+pattern NaturalZero :: Natural
+pattern NaturalZero <- (naturalPred -> Nothing) where NaturalZero = 0
+pattern NaturalSucc :: Natural -> Natural
+pattern NaturalSucc n <- (naturalPred -> Just n) where NaturalSucc n = n + 1
+{-# COMPLETE NaturalZero, NaturalSucc #-}
+
+naturalPred :: Natural -> Maybe Natural
+naturalPred = \case
+    0 -> Nothing
+    n -> Just (n - 1)
diff --git a/src/Lude/Integer.hs b/src/Lude/Integer.hs
@@ -0,0 +1,10 @@
+module Lude.Integer (
+    Integer,
+    pattern IntegerNegSucc,
+    pattern IntegerZero,
+    pattern IntegerPosSucc,
+) where
+
+import Lude.Haskell.Integer
+
+--------------------------------------------------------------------------------
diff --git a/src/Lude/Natural.hs b/src/Lude/Natural.hs
@@ -1,7 +1,10 @@
 module Lude.Natural (
     Natural,
+    pattern NaturalZero,
+    pattern NaturalSucc,
+    naturalPred,
 ) where
 
-import Numeric.Natural (Natural)
+import Lude.Haskell.Natural
 
 --------------------------------------------------------------------------------