module Data.Type.Ordinal
(
Ordinal (..),
sNatToOrd', sNatToOrd, ordToInt, ordToSNat,
(@+)
) where
import Data.Type.Monomorphic
import Data.Type.Natural
data Ordinal n where
OZ :: Ordinal (S n)
OS :: Ordinal n -> Ordinal (S n)
instance Read (Ordinal Z) where
readsPrec _ _ = []
deriving instance Read (Ordinal n) => Read (Ordinal (S n))
deriving instance Show (Ordinal n)
deriving instance Eq (Ordinal n)
deriving instance Ord (Ordinal n)
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 :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
sNatToOrd = sNatToOrd' sing
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' (SS SZ) OZ = OZ
inclusion' (SS (SS _)) OZ = OZ
inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (sS n) m
inclusion' _ _ = bugInGHC
inclusion :: ((n :<<= m) ~ True, SingRep m) => Ordinal n -> Ordinal m
inclusion = inclusion' sing
(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
OZ @+ n =
let sn = sing :: SNat n
sm = sing :: SNat m
in case singInstance (sn %+ sm) of
SingInstance ->
case propToBoolLeq (plusLeqR sn sm) of
LeqTrueInstance -> inclusion n
OS n @+ m =
case sing :: SNat n of
SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m
_ -> bugInGHC