{-# LANGUAGE DataKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}
{-# OPTIONS_GHC -fobject-code #-}

{- | Set-theoretic ordinals for built-in type-level naturals

  Since 1.0.0.0
-}
module Data.Type.Ordinal
  ( -- * Data-types
    Ordinal (..),
    pattern OZ,
    pattern OS,

    -- * Quasi Quoter
    -- $quasiquotes
    od,

    -- * Conversion from cardinals to ordinals.
    sNatToOrd',
    sNatToOrd,
    ordToNatural,
    unsafeNaturalToOrd',
    unsafeNaturalToOrd,
    reallyUnsafeNaturalToOrd,
    naturalToOrd,
    naturalToOrd',
    ordToSNat,
    inclusion,
    inclusion',

    -- * Ordinal arithmetics
    (@+),
    enumOrdinal,

    -- * Elimination rules for @'Ordinal' 'Z'@.
    absurdOrd,
    vacuousOrd,
  )
where

import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Data.Proxy (Proxy (Proxy))
import Data.Type.Equality
import Data.Type.Natural
import Data.Typeable (Typeable)
import Language.Haskell.TH.Quote
import Numeric.Natural ( Natural )
import Unsafe.Coerce
import Proof.Propositional (IsTrue (Witness))
import Data.Type.Natural.Lemma.Order (lneqZeroAbsurd)
import Data.Void (absurd)

{- | Set-theoretic (finite) ordinals:

 > n = {0, 1, ..., n-1}

 So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.

   Since 1.0.0.0
-}
data Ordinal (n :: Nat) where
  OLt :: (n < m) => SNat (n :: Nat) -> Ordinal m

{-# COMPLETE OLt #-}

fromOLt ::
  forall n m.
  ((Succ n < Succ m), KnownNat m) =>
  SNat (n :: Nat) ->
  Ordinal m
fromOLt :: forall (n :: Nat) (m :: Nat).
(Succ n < Succ m, KnownNat m) =>
SNat n -> Ordinal m
fromOLt SNat n
n = SNat n -> Ordinal m
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
n

{- | Pattern synonym representing the 0-th ordinal.

   Since 1.0.0.0
-}
pattern OZ :: forall (n :: Nat). (0 < n) => Ordinal n
pattern $mOZ :: forall {r} {n :: Nat}.
(0 < n) =>
Ordinal n -> ((# #) -> r) -> ((# #) -> r) -> r
$bOZ :: forall (n :: Nat). (0 < n) => Ordinal n
OZ <- OLt Zero where OZ = SNat 0 -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat 0
sZero

{- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.

   Since 1.0.0.0
-}
pattern OS :: forall (t :: Nat). (KnownNat t) => Ordinal t -> Ordinal (Succ t)
pattern $mOS :: forall {r} {t :: Nat}.
KnownNat t =>
Ordinal (Succ t) -> (Ordinal t -> r) -> ((# #) -> r) -> r
$bOS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)
OS n <-
  OLt (Succ (fromOLt -> n))
  where
    OS Ordinal t
o = Ordinal t -> Ordinal (t + 1)
forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)
succOrd Ordinal t
o

-- | Since 1.0.0.0
deriving instance Typeable Ordinal

{- |  Class synonym for Peano numerals with ordinals.

  Since 1.0.0.0
-}
instance (KnownNat n) => Num (Ordinal n) where
  Ordinal n
_ + :: Ordinal n -> Ordinal n -> Ordinal n
+ Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Finite ordinal is not closed under addition."
  Ordinal n
_ - :: Ordinal n -> Ordinal n -> Ordinal n
- Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Ordinal subtraction is not defined"
  negate :: Ordinal n -> Ordinal n
negate Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"There are no negative oridnals!"
  Ordinal n
_ * :: Ordinal n -> Ordinal n -> Ordinal n
* Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Finite ordinal is not closed under multiplication"
  abs :: Ordinal n -> Ordinal n
abs = Ordinal n -> Ordinal n
forall a. a -> a
id
  signum :: Ordinal n -> Ordinal n
signum = [Char] -> Ordinal n -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"What does Ordinal sign mean?"
  fromInteger :: Integer -> Ordinal n
fromInteger = Nat -> Ordinal n
forall (n :: Nat). KnownNat n => Nat -> Ordinal n
unsafeFromNatural' (Nat -> Ordinal n) -> (Integer -> Nat) -> Integer -> Ordinal n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral

unsafeFromNatural' :: forall n. KnownNat n => Natural -> Ordinal n
unsafeFromNatural' :: forall (n :: Nat). KnownNat n => Nat -> Ordinal n
unsafeFromNatural' Nat
k = Nat
-> (forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall r.
Nat -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Nat
k ((forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
 -> Ordinal n)
-> (forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall a b. (a -> b) -> a -> b
$ \SNat n
sk ->
  case SNat n
sk SNat n -> SNat n -> SBool (n <? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
%<? forall (n :: Nat). KnownNat n => SNat n
sNat @n of
    SBool (n <? n)
STrue -> SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk
    SBool (n <? n)
SFalse -> [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Ordinal n) -> [Char] -> Ordinal n
forall a b. (a -> b) -> a -> b
$ [Char]
"Index out of bounds: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Nat, Nat) -> [Char]
forall a. Show a => a -> [Char]
show (Nat
k, forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy)

-- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n))
instance
  (KnownNat n) =>
  Show (Ordinal (n :: Nat))
  where
  showsPrec :: Int -> Ordinal n -> [Char] -> [Char]
showsPrec Int
d Ordinal n
o = Char -> [Char] -> [Char]
showChar Char
'#' ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen Bool
True (Int -> Nat -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
d (Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
o) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char] -> [Char]
showString [Char]
" / " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
d (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)))

instance Eq (Ordinal (n :: Nat)) where
  Ordinal n
o == :: Ordinal n -> Ordinal n -> Bool
== Ordinal n
o' = Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
o Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
o'

instance Ord (Ordinal (n :: Nat)) where
  compare :: Ordinal n -> Ordinal n -> Ordering
compare = (Ordinal n -> Nat) -> Ordinal n -> Ordinal n -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural

instance
  (KnownNat n) =>
  Enum (Ordinal (n :: Nat))
  where
  fromEnum :: Ordinal n -> Int
fromEnum = Nat -> Int
forall a. Enum a => a -> Int
fromEnum (Nat -> Int) -> (Ordinal n -> Nat) -> Ordinal n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural
  toEnum :: Int -> Ordinal n
toEnum = Nat -> Ordinal n
forall (n :: Nat). KnownNat n => Nat -> Ordinal n
unsafeFromNatural' (Nat -> Ordinal n) -> (Int -> Nat) -> Int -> Ordinal n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  enumFrom :: Ordinal n -> [Ordinal n]
enumFrom = Ordinal n -> [Ordinal n]
forall (n :: Nat). KnownNat n => Ordinal n -> [Ordinal n]
enumFromOrd
  enumFromTo :: Ordinal n -> Ordinal n -> [Ordinal n]
enumFromTo = Ordinal n -> Ordinal n -> [Ordinal n]
forall (n :: Nat).
KnownNat n =>
Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd

-- | Since 1.0.0.0 (type changed)
enumFromToOrd ::
  forall (n :: Nat).
  (KnownNat n) =>
  Ordinal n ->
  Ordinal n ->
  [Ordinal n]
enumFromToOrd :: forall (n :: Nat).
KnownNat n =>
Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd Ordinal n
ok Ordinal n
ol =
  (Nat -> Ordinal n) -> [Nat] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map
    (SNat n -> Nat -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Nat -> Ordinal n
reallyUnsafeNaturalToOrd (SNat n -> Nat -> Ordinal n) -> SNat n -> Nat -> Ordinal n
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n)
    [Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
ok .. Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
ol]

-- | Since 1.0.0.0 (type changed)
enumFromOrd ::
  forall (n :: Nat).
  (KnownNat n) =>
  Ordinal n ->
  [Ordinal n]
enumFromOrd :: forall (n :: Nat). KnownNat n => Ordinal n -> [Ordinal n]
enumFromOrd Ordinal n
ord =
  (Nat -> Ordinal n) -> [Nat] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map
    (Proxy Any -> Nat -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Nat -> Ordinal n
reallyUnsafeNaturalToOrd Proxy Any
forall {k} (t :: k). Proxy t
Proxy)
    [Ordinal n -> Nat
forall (n :: Nat). Ordinal n -> Nat
ordToNatural Ordinal n
ord .. forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]

-- | Enumerate all @'Ordinal'@s less than @n@.
enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]
enumOrdinal :: forall (n :: Nat). SNat n -> [Ordinal n]
enumOrdinal SNat n
sn = SNat n -> (KnownNat n => [Ordinal n]) -> [Ordinal n]
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => [Ordinal n]) -> [Ordinal n])
-> (KnownNat n => [Ordinal n]) -> [Ordinal n]
forall a b. (a -> b) -> a -> b
$ (Nat -> Ordinal n) -> [Nat] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map (Proxy Any -> Nat -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Nat -> Ordinal n
reallyUnsafeNaturalToOrd Proxy Any
forall {k} (t :: k). Proxy t
Proxy) [Nat
0 .. SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
sn Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]

-- | Since 1.0.0.0 (type changed)
succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)
succOrd :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)
succOrd (OLt SNat n
k) = SNat (n + 1) -> Ordinal (n + 1)
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
k)
{-# INLINE succOrd #-}

instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where
  minBound :: Ordinal n
minBound = SNat 0 -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat 0
sZero

  maxBound :: Ordinal n
maxBound = SNat (n - 1) -> (KnownNat (n - 1) => Ordinal n) -> Ordinal n
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). KnownNat n => SNat n
sNat @n SNat n -> SNat 1 -> SNat (n - 1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- forall (n :: Nat). KnownNat n => SNat n
sNat @1) ((KnownNat (n - 1) => Ordinal n) -> Ordinal n)
-> (KnownNat (n - 1) => Ordinal n) -> Ordinal n
forall a b. (a -> b) -> a -> b
$ SNat (n - 1) -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat (n - 1) -> Ordinal n) -> SNat (n - 1) -> Ordinal n
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @(n - 1)

{- | Converts @'Natural'@s into @'Ordinal n'@.
   If the given natural is greater or equal to @n@, raises exception.

   Since 1.0.0.0
-}
unsafeNaturalToOrd ::
  forall (n :: Nat).
  (KnownNat n) =>
  Natural ->
  Ordinal n
unsafeNaturalToOrd :: forall (n :: Nat). KnownNat n => Nat -> Ordinal n
unsafeNaturalToOrd Nat
k =
  Ordinal n -> Maybe (Ordinal n) -> Ordinal n
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeNaturalToOrd Out of bound") (Maybe (Ordinal n) -> Ordinal n) -> Maybe (Ordinal n) -> Ordinal n
forall a b. (a -> b) -> a -> b
$
    Nat -> Maybe (Ordinal n)
forall (n :: Nat). KnownNat n => Nat -> Maybe (Ordinal n)
naturalToOrd Nat
k

-- | Since 1.0.0.0
unsafeNaturalToOrd' ::
  forall proxy (n :: Nat).
  (KnownNat n) =>
  proxy n ->
  Natural ->
  Ordinal n
unsafeNaturalToOrd' :: forall (proxy :: Nat -> Type) (n :: Nat).
KnownNat n =>
proxy n -> Nat -> Ordinal n
unsafeNaturalToOrd' proxy n
_ = Nat -> Ordinal n
forall (n :: Nat). KnownNat n => Nat -> Ordinal n
unsafeNaturalToOrd

{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-}

{- | Converts @'Natural'@s into @'Ordinal' n@, WITHOUT any boundary check.
   This function may easily violate type-safety. Use with care!
-}
reallyUnsafeNaturalToOrd ::
  forall pxy (n :: Nat).
  (KnownNat n) =>
  pxy ->
  Natural ->
  Ordinal n
reallyUnsafeNaturalToOrd :: forall pxy (n :: Nat). KnownNat n => pxy -> Nat -> Ordinal n
reallyUnsafeNaturalToOrd pxy
_ Nat
k =
  Nat
-> (forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall r.
Nat -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Nat
k ((forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
 -> Ordinal n)
-> (forall {n :: Nat}. KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall a b. (a -> b) -> a -> b
$ \(SNat n
sk :: SNat k) ->
    (OrdCond (CmpNat n n) 'True 'False 'False :~: 'True)
-> ((OrdCond (CmpNat n n) 'True 'False 'False ~ 'True) =>
    Ordinal n)
-> Ordinal n
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((() :~: ()) -> OrdCond (CmpNat n n) 'True 'False 'False :~: 'True
forall a b. a -> b
unsafeCoerce (() :~: ()
forall {k} (a :: k). a :~: a
Refl :: () :~: ()) :: (k <? n) :~: 'True) (((OrdCond (CmpNat n n) 'True 'False 'False ~ 'True) => Ordinal n)
 -> Ordinal n)
-> ((OrdCond (CmpNat n n) 'True 'False 'False ~ 'True) =>
    Ordinal n)
-> Ordinal n
forall a b. (a -> b) -> a -> b
$
      SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk

{- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.

   Since 1.0.0.0
-}
sNatToOrd' :: (m < n) => SNat (n :: Nat) -> SNat m -> Ordinal n
sNatToOrd' :: forall (m :: Nat) (n :: Nat).
(m < n) =>
SNat n -> SNat m -> Ordinal n
sNatToOrd' SNat n
_ = SNat m -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt
{-# INLINE sNatToOrd' #-}

-- | 'sNatToOrd'' with @n@ inferred.
sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n
sNatToOrd :: forall (n :: Nat) (m :: Nat).
(KnownNat n, m < n) =>
SNat m -> Ordinal n
sNatToOrd = SNat n -> SNat m -> Ordinal n
forall (m :: Nat) (n :: Nat).
(m < n) =>
SNat n -> SNat m -> Ordinal n
sNatToOrd' SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat

-- | Since 1.0.0.0
naturalToOrd ::
  forall n.
  (KnownNat n) =>
  Natural ->
  Maybe (Ordinal (n :: Nat))
naturalToOrd :: forall (n :: Nat). KnownNat n => Nat -> Maybe (Ordinal n)
naturalToOrd = SNat n -> Nat -> Maybe (Ordinal n)
forall (n :: Nat). SNat n -> Nat -> Maybe (Ordinal n)
naturalToOrd' (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)

naturalToOrd' ::
  SNat (n :: Nat) ->
  Natural ->
  Maybe (Ordinal n)
naturalToOrd' :: forall (n :: Nat). SNat n -> Nat -> Maybe (Ordinal n)
naturalToOrd' SNat n
sn Nat
k = Nat
-> (forall {n :: Nat}. KnownNat n => SNat n -> Maybe (Ordinal n))
-> Maybe (Ordinal n)
forall r.
Nat -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Nat
k ((forall {n :: Nat}. KnownNat n => SNat n -> Maybe (Ordinal n))
 -> Maybe (Ordinal n))
-> (forall {n :: Nat}. KnownNat n => SNat n -> Maybe (Ordinal n))
-> Maybe (Ordinal n)
forall a b. (a -> b) -> a -> b
$ \(SNat n
sk :: SNat pk) ->
  case SNat n
sk SNat n -> SNat n -> SBool (n <? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
%<? SNat n
sn of
    SBool (n <? n)
STrue -> Ordinal n -> Maybe (Ordinal n)
forall a. a -> Maybe a
Just (SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk)
    SBool (n <? n)
_ -> Maybe (Ordinal n)
forall a. Maybe a
Nothing

{- | Convert @Ordinal n@ into monomorphic @SNat@

 Since 1.0.0.0
-}
ordToSNat :: Ordinal (n :: Nat) -> SomeSNat
ordToSNat :: forall (n :: Nat). Ordinal n -> SomeSNat
ordToSNat (OLt SNat n
n) = SNat n -> (KnownNat n => SomeSNat) -> SomeSNat
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => SomeSNat) -> SomeSNat)
-> (KnownNat n => SomeSNat) -> SomeSNat
forall a b. (a -> b) -> a -> b
$ SNat n -> SomeSNat
forall (n :: Nat). KnownNat n => SNat n -> SomeSNat
SomeSNat SNat n
n
{-# INLINE ordToSNat #-}

ordToNatural ::
  Ordinal (n :: Nat) ->
  Natural
ordToNatural :: forall (n :: Nat). Ordinal n -> Nat
ordToNatural (OLt SNat n
n) = SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n

{- | Inclusion function for ordinals.

   Since 1.0.0.0(constraint was weakened since last released)
-}
inclusion' :: (n <= m) => SNat m -> Ordinal n -> Ordinal m
inclusion' :: forall (n :: Nat) (m :: Nat).
(n <= m) =>
SNat m -> Ordinal n -> Ordinal m
inclusion' SNat m
_ = Ordinal n -> Ordinal m
forall a b. a -> b
unsafeCoerce
{-# INLINE inclusion' #-}

{- | Inclusion function for ordinals with codomain inferred.

   Since 1.0.0.0(constraint was weakened since last released)
-}
inclusion :: (n <= m) => Ordinal n -> Ordinal m
inclusion :: forall (n :: Nat) (m :: Nat). (n <= m) => Ordinal n -> Ordinal m
inclusion (OLt SNat n
a) = SNat n -> Ordinal m
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
a
{-# INLINE inclusion #-}

{- | Ordinal addition.

   Since 1.0.0.0(type changed)
-}
(@+) ::
  forall (n :: Nat) m.
  (KnownNat n, KnownNat m) =>
  Ordinal n ->
  Ordinal m ->
  Ordinal (n + m)
OLt SNat n
k @+ :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Ordinal n -> Ordinal m -> Ordinal (n + m)
@+ OLt SNat n
l = SNat (n + n) -> Ordinal (n + m)
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat (n + n) -> Ordinal (n + m))
-> SNat (n + n) -> Ordinal (n + m)
forall a b. (a -> b) -> a -> b
$ SNat n
k SNat n -> SNat n -> SNat (n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
l

{- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.

 Since 1.0.0.0
-}
absurdOrd :: Ordinal 0 -> a
absurdOrd :: forall a. Ordinal 0 -> a
absurdOrd (OLt SNat n
sn) = Void -> a
forall a. Void -> a
absurd (Void -> a) -> Void -> a
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (n <? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd SNat n
sn IsTrue 'True
IsTrue (n <? 0)
Witness

{- | @'absurdOrd'@ for value in 'Functor'.

   Since 1.0.0.0
-}
vacuousOrd :: (Functor f) => f (Ordinal 0) -> f a
vacuousOrd :: forall (f :: Type -> Type) a. Functor f => f (Ordinal 0) -> f a
vacuousOrd = (Ordinal 0 -> a) -> f (Ordinal 0) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Ordinal 0 -> a
forall a. Ordinal 0 -> a
absurdOrd

{- $quasiquotes #quasiquoters#

   This section provides QuasiQuoter and general generator for ordinals.
   Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT
   checks boundary; with @'od'@, we can use literal with
   boundary check.
   For example, with @-XQuasiQuotes@ language extension enabled,
   @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error,
   whilst @12 :: Ordinal 1@ compiles but raises run-time error.
   So, to enforce correctness, we recommend to use these quoters
   instead of bare @'Num'@ numerals.
-}

-- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@.
od :: QuasiQuoter
od :: QuasiQuoter
od =
  QuasiQuoter
    { quoteExp :: [Char] -> Q Exp
quoteExp = \[Char]
s -> [|OLt $(QuasiQuoter -> [Char] -> Q Exp
quoteExp QuasiQuoter
snat [Char]
s)|]
    , quoteType :: [Char] -> Q Type
quoteType = [Char] -> [Char] -> Q Type
forall a. HasCallStack => [Char] -> a
error [Char]
"No type quoter for Ordinals"
    , quotePat :: [Char] -> Q Pat
quotePat = \[Char]
s -> [p|OLt ((%~ $(QuasiQuoter -> [Char] -> Q Exp
quoteExp QuasiQuoter
snat [Char]
s)) -> Equal)|]
    , quoteDec :: [Char] -> Q [Dec]
quoteDec = [Char] -> [Char] -> Q [Dec]
forall a. HasCallStack => [Char] -> a
error [Char]
"No declaration quoter for Ordinals"
    }

-- >>> 42