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