#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
#endif
module Data.Type.Ordinal
(
Ordinal (..),
sNatToOrd', sNatToOrd, ordToInt, ordToSNat,
ordToSNat', CastedOrdinal(..),
unsafeFromInt, inclusion, inclusion',
(@+), enumOrdinal,
absurdOrd, vacuousOrd, vacuousOrdM,
od
) where
import Data.Constraint
import Data.Type.Monomorphic
import Data.Type.Natural hiding (promote)
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Proof.Equational (coerce)
import Unsafe.Coerce
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
import Data.Singletons.Prelude
import Data.Typeable (Typeable)
#endif
import Control.Monad (liftM)
data Ordinal n where
OZ :: Ordinal (S n)
OS :: Ordinal n -> Ordinal (S n)
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
deriving instance Typeable Ordinal
#endif
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 ->
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
case singInstance sn of
SingInstance ->
#endif
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
sNatToOrd' _ _ = bugInGHC
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 ->
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
case singInstance m of
SingInstance ->
#endif
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
_ -> bugInGHC
absurdOrd :: Ordinal Z -> a
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
absurdOrd cs = case cs of {}
#else
absurdOrd _ = error "Impossible!"
#endif
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"
}