From 3119dd5ed482cba403ad6469b1e0d6dd75353768 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <oleg.grenrus@iki.fi>
Date: Sat, 9 Nov 2024 13:36:47 +0200
Subject: [PATCH] Add SS' :: SNat n -> SNat (S n)

---
 fin/ChangeLog.md         |  4 ++++
 fin/fin.cabal            |  3 +--
 fin/src/Data/Fin.hs      |  2 +-
 fin/src/Data/Type/Nat.hs | 33 ++++++++++++++++++++++++++++++++-
 4 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/fin/ChangeLog.md b/fin/ChangeLog.md
index 0f00aaf..c072426 100644
--- a/fin/ChangeLog.md
+++ b/fin/ChangeLog.md
@@ -1,5 +1,9 @@
 # Version history for fin
 
+## 0.3.2
+
+- Add `SS' :: SNat n -> SNat (S n)`, pattern synonym with explicit argument.
+
 ## 0.3.1
 
 - Support GHC-8.6.5...9.10.1
diff --git a/fin/fin.cabal b/fin/fin.cabal
index 612bb8b..1534c77 100644
--- a/fin/fin.cabal
+++ b/fin/fin.cabal
@@ -1,7 +1,6 @@
 cabal-version:      2.2
 name:               fin
-version:            0.3.1
-x-revision:         1
+version:            0.3.2
 synopsis:           Nat and Fin: peano naturals and finite numbers
 category:           Data, Dependent Types, Singletons, Math
 description:
diff --git a/fin/src/Data/Fin.hs b/fin/src/Data/Fin.hs
index e50603e..51e3945 100644
--- a/fin/src/Data/Fin.hs
+++ b/fin/src/Data/Fin.hs
@@ -81,7 +81,7 @@ import qualified Test.QuickCheck       as QC
 -- >>> import qualified Data.Universe.Helpers as U
 -- >>> import Data.EqP (eqp)
 -- >>> import Data.OrdP (comparep)
--- >>> :set -XTypeApplications
+-- >>> :set -XTypeApplications -XGADTs
 
 -------------------------------------------------------------------------------
 -- Type
diff --git a/fin/src/Data/Type/Nat.hs b/fin/src/Data/Type/Nat.hs
index 1a1cf6c..04d9e23 100644
--- a/fin/src/Data/Type/Nat.hs
+++ b/fin/src/Data/Type/Nat.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
@@ -10,6 +11,7 @@
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns         #-}
 -- | 'Nat' numbers. @DataKinds@ stuff.
 --
 -- This module re-exports "Data.Nat", and adds type-level things.
@@ -23,7 +25,7 @@ module Data.Type.Nat (
     explicitShow,
     explicitShowsPrec,
     -- * Singleton
-    SNat(..),
+    SNat(SZ,SS,SS'),
     snatToNat,
     snatToNatural,
     -- * Implicit
@@ -177,6 +179,35 @@ snatToNatural :: forall n. SNat n -> Natural
 snatToNatural SZ = 0
 snatToNatural SS = unKonst (induction (Konst 0) (kmap succ) :: Konst Natural n)
 
+-------------------------------------------------------------------------------
+-- Explicit constructor
+-------------------------------------------------------------------------------
+
+data SNat_ (n :: Nat) where
+    SZ_ :: SNat_ 'Z
+    SS_ :: SNat n -> SNat_ ('S n)
+
+snat_ :: SNat n -> SNat_ n
+snat_ SZ = SZ_
+snat_ SS = SS_ snat
+
+-- | A pattern with explicit argument
+--
+-- >>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n
+-- >>> predSNat (SS' (SS' SZ))
+-- SS
+--
+-- >>> reflect $ predSNat (SS' (SS' SZ))
+-- 1
+--
+--
+-- @since 0.3.2
+pattern SS' :: () => (m ~ 'S n) => SNat n -> SNat m
+pattern SS' n <- (snat_ -> SS_ n)
+  where SS' n = withSNat n SS
+
+{-# COMPLETE SZ, SS' #-}
+
 -------------------------------------------------------------------------------
 -- Equality
 -------------------------------------------------------------------------------