{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs #-}
{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}
{-# OPTIONS_GHC -Wno-warnings-deprecations #-}
module Data.Type.Ordinal.Peano
(
Ordinal, pattern OLt, pattern OZ, pattern OS,
od,
sNatToOrd', sNatToOrd, inclusion, inclusion',
ordToNatural, unsafeNaturalToOrd, naturalToOrd, naturalToOrd',
(@+), enumOrdinal,
absurdOrd, vacuousOrd,
ordToInt, unsafeFromInt
) where
import Data.Type.Natural.Singleton.Compat
import Numeric.Natural (Natural)
import Data.Singletons.Prelude (SingI, Sing (..))
import Data.Singletons.Prelude.Enum (PEnum (..))
import qualified Data.Type.Ordinal as O
import Data.Type.Natural
import Language.Haskell.TH.Quote (QuasiQuoter)
type Ordinal (n :: Nat) = O.Ordinal n
pattern OLt :: () => forall (n1 :: Nat). ((n1 < t) ~ 'True)
=> Sing n1 -> O.Ordinal t
pattern OLt n = O.OLt n
pattern OZ :: forall (n :: Nat). ()
=> ('Z < n) ~ 'True => O.Ordinal n
pattern OZ = O.OZ
pattern OS :: forall (t :: Nat). (SingI t)
=> () => O.Ordinal t -> O.Ordinal (Succ t)
pattern OS n = O.OS n
od :: QuasiQuoter
od = O.odLit
{-# INLINE od #-}
sNatToOrd' :: (m < n) ~ 'True => Sing n -> Sing m -> Ordinal n
sNatToOrd' = O.sNatToOrd'
{-# INLINE sNatToOrd' #-}
sNatToOrd :: (SingI n, (m < n) ~ 'True) => Sing m -> Ordinal n
sNatToOrd = O.sNatToOrd
{-# INLINE sNatToOrd #-}
ordToInt :: Ordinal n -> Int
ordToInt = O.ordToInt
{-# INLINE ordToInt #-}
unsafeFromInt :: SingI n
=> Int -> Ordinal n
unsafeFromInt = O.unsafeFromInt
{-# INLINE unsafeFromInt #-}
inclusion :: (n <= m) ~ 'True => Ordinal n -> Ordinal m
inclusion = O.inclusion
{-# INLINE inclusion #-}
inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m
inclusion' = O.inclusion'
{-# INLINE inclusion' #-}
(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m)
(@+) = (O.@+)
{-# INLINE (@+) #-}
enumOrdinal :: Sing n -> [Ordinal n]
enumOrdinal = O.enumOrdinal
{-# INLINE enumOrdinal #-}
absurdOrd :: Ordinal 'Z -> a
absurdOrd = O.absurdOrd
{-# INLINE absurdOrd #-}
vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a
vacuousOrd = O.vacuousOrd
{-# INLINE vacuousOrd #-}
ordToNatural :: Ordinal (n :: Nat) -> Natural
ordToNatural = O.ordToNatural
{-# INLINE ordToNatural #-}
unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n
unsafeNaturalToOrd = O.unsafeNaturalToOrd
naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n)
naturalToOrd = O.naturalToOrd
naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n)
naturalToOrd' = O.naturalToOrd'