module Data.Type.Ordinal
(
Ordinal (..),
sNatToOrd', sNatToOrd, ordToInt, ordToSNat,
ordToSNat', CastedOrdinal(..),
unsafeFromInt, inclusion, inclusion',
(@+), enumOrdinal,
absurdOrd, vacuousOrd, vacuousOrdM,
od
) where
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
import Data.Type.Natural.Compat
#endif
import Control.Monad (liftM)
import Data.Constraint
import Data.Singletons.Prelude
import Data.Type.Monomorphic
import Data.Type.Natural
import Data.Typeable (Typeable)
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Unsafe.Coerce
data Ordinal n where
OZ :: Ordinal ('S n)
OS :: Ordinal n -> Ordinal ('S n)
deriving instance Typeable Ordinal
instance Read (Ordinal 'Z) where
readsPrec _ _ = []
instance SingI n => Num (Ordinal n) where
_ + _ = error "Finite ordinal is not closed under addition."
_ _ = error "Ordinal subtraction is not defined"
negate OZ = OZ
negate _ = error "There are no negative oridnals!"
OZ * _ = OZ
_ * OZ = OZ
_ * _ = error "Finite ordinal is not closed under multiplication"
abs = id
signum = error "What does Ordinal sign mean?"
fromInteger = unsafeFromInt . fromInteger
deriving instance Read (Ordinal n) => Read (Ordinal ('S n))
deriving instance Show (Ordinal n)
deriving instance Eq (Ordinal n)
deriving instance Ord (Ordinal n)
instance SingI n => Enum (Ordinal n) where
fromEnum = ordToInt
toEnum = unsafeFromInt
enumFrom = enumFromOrd
enumFromTo = enumFromToOrd
enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd ok ol =
let k = ordToInt ok
l = ordToInt ol
in take (l k + 1) $ enumFromOrd ok
enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n]
enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n)
enumOrdinal :: SNat n -> [Ordinal n]
enumOrdinal SZ = []
enumOrdinal (SS n) = OZ : map OS (enumOrdinal n)
instance SingI n => Bounded (Ordinal ('S n)) where
minBound = OZ
maxBound =
case propToBoolLeq $ leqRefl (sing :: SNat n) of
Dict -> sNatToOrd (sing :: SNat n)
unsafeFromInt :: forall n. SingI n => Int -> Ordinal n
unsafeFromInt n =
case (promote n :: Monomorphic (Sing :: Nat -> *)) of
Monomorphic sn ->
case SS sn %:<<= (sing :: SNat n) of
STrue -> sNatToOrd' (sing :: SNat n) sn
SFalse -> error "Bound over!"
sNatToOrd' :: ('S m :<<= n) ~ 'True => SNat n -> SNat m -> Ordinal n
sNatToOrd' (SS _) SZ = OZ
sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
sNatToOrd' _ _ = bugInGHC
#endif
sNatToOrd :: (SingI n, ('S m :<<= n) ~ 'True) => SNat m -> Ordinal n
sNatToOrd = sNatToOrd' sing
data CastedOrdinal n where
CastedOrdinal :: ('S m :<<= n) ~ 'True => SNat m -> CastedOrdinal n
ordToSNat' :: Ordinal n -> CastedOrdinal n
ordToSNat' OZ = CastedOrdinal SZ
ordToSNat' (OS on) =
case ordToSNat' on of
CastedOrdinal m ->
CastedOrdinal (SS m)
ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
ordToSNat OZ = Monomorphic SZ
ordToSNat (OS n) =
case ordToSNat n of
Monomorphic sn ->
case singInstance sn of
SingInstance -> Monomorphic (SS sn)
ordToInt :: Ordinal n -> Int
ordToInt OZ = 0
ordToInt (OS n) = 1 + ordToInt n
inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m
inclusion' _ = unsafeCoerce
inclusion :: ((n :<<= m) ~ 'True) => Ordinal n -> Ordinal m
inclusion on = unsafeCoerce on
(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
OZ @+ n =
let sn = sing :: SNat n
sm = sing :: SNat m
in case propToBoolLeq (plusLeqR sn sm) of
Dict -> inclusion n
OS n @+ m =
case sing :: SNat n of
SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
_ -> bugInGHC
#endif
absurdOrd :: Ordinal 'Z -> a
absurdOrd cs = case cs of {}
vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a
vacuousOrd = fmap absurdOrd
vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a
vacuousOrdM = liftM absurdOrd
od :: QuasiQuoter
od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read
, quoteType = error "No type quoter for Ordinals"
, quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read
, quoteDec = error "No declaration quoter for Ordinals"
}