Add SS' :: SNat n -> SNat (S n)

phadej · Nov 9, 2024 · 3119dd5 · 3119dd5
1 parent 4cfb8b1
commit 3119dd5
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -3,13 +3,15 @@
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
 {-# LANGUAGE Trustworthy          #-}
 {-# 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
 -------------------------------------------------------------------------------