{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Control.Category.NatOrd(
    (:<=:)(..),
    (:>=:),

    Finite'(..), shift',
    fromFinite, toFinite
) where

import Prelude hiding (id, (.))
import Control.Category
import Data.Kind (Type)

import Data.Proxy (Proxy(..))

import GHC.TypeNats hiding (pattern SNat)
import GHC.TypeNats.Extra

import Data.Finite
import Control.Category.Dual (Dual)

-- | Inductively defined "less than or equals" relation
type (:<=:) :: Nat -> Nat -> Type
data (:<=:) n m where
    ReflLE :: m :<=: m
    SuccLE :: !(m :<=: n) -> m :<=: (1 + n)

infix 4 :<=:

instance Category (:<=:) where
    id :: a :<=: a
    id :: forall (a :: Nat). a :<=: a
id = a :<=: a
forall (a :: Nat). a :<=: a
ReflLE
    
    (.) :: (b :<=: c) -> (a :<=: b) -> a :<=: c
    b :<=: c
ReflLE . :: forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :<=: c) -> (a :<=: b) -> a :<=: c
. a :<=: b
ab = a :<=: b
a :<=: c
ab
    SuccLE b :<=: n
bc . a :<=: b
ab = (a :<=: n) -> a :<=: (1 + n)
forall (m :: Nat) (m :: Nat). (m :<=: m) -> m :<=: (1 + m)
SuccLE (b :<=: n
bc (b :<=: n) -> (a :<=: b) -> a :<=: n
forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :<=: c) -> (a :<=: b) -> a :<=: c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a :<=: b
ab)

-- | "greater than or equals"
type (:>=:) = Dual (:<=:)

infix 4 :>=:

-- | Given a type-level @n :: Nat@, @Finite' n@ is the collection of all values
--   of type @m :<=: n@ for some @m :: Nat@.
data Finite' n where
    Finite' :: (m :<=: n) -> Finite' (1 + n)

shift' :: Finite' n -> Finite' (1 + n)
shift' :: forall (n :: Nat). Finite' n -> Finite' (1 + n)
shift' (Finite' m :<=: n
le) = (m :<=: n) -> Finite' (1 + n)
forall (m :: Nat) (n :: Nat). (m :<=: n) -> Finite' (1 + n)
Finite' ((m :<=: n) -> m :<=: (1 + n)
forall (m :: Nat) (m :: Nat). (m :<=: m) -> m :<=: (1 + m)
SuccLE m :<=: n
le)

fromFinite :: forall n. KnownNat n => Finite n -> Finite' n
fromFinite :: forall (n :: Nat). KnownNat n => Finite n -> Finite' n
fromFinite Finite n
k = case forall (n :: Nat). KnownNat n => SNat n
natSing @n of
    SNat n
Zero -> Finite 0 -> Finite' n
forall any. Finite 0 -> any
absurdFinite Finite n
Finite 0
k
    Succ SNat m
n' -> SNat m -> (KnownNat m => Finite' n) -> Finite' n
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
n' ((KnownNat m => Finite' n) -> Finite' n)
-> (KnownNat m => Finite' n) -> Finite' n
forall a b. (a -> b) -> a -> b
$ case Finite (m + 1) -> Maybe (Finite m)
forall (n :: Nat). Finite (n + 1) -> Maybe (Finite n)
unshift Finite n
Finite (m + 1)
k of
        Maybe (Finite m)
Nothing -> (m :<=: m) -> Finite' (1 + m)
forall (m :: Nat) (n :: Nat). (m :<=: n) -> Finite' (1 + n)
Finite' m :<=: m
forall (a :: Nat). a :<=: a
ReflLE
        Just Finite m
k' -> Finite' m -> Finite' (1 + m)
forall (n :: Nat). Finite' n -> Finite' (1 + n)
shift' (Finite m -> Finite' m
forall (n :: Nat). KnownNat n => Finite n -> Finite' n
fromFinite Finite m
k')

toFinite :: KnownNat n => Finite' n -> Finite n
toFinite :: forall (n :: Nat). KnownNat n => Finite' n -> Finite n
toFinite (Finite' m :<=: n
nm) = case m :<=: n
nm of
    m :<=: n
ReflLE -> Finite n
Finite (1 + m)
forall (m :: Nat). KnownNat m => Finite (1 + m)
zeroFinite
    SuccLE m :<=: n
n'm -> Finite n -> Finite (n + 1)
forall (n :: Nat). Finite n -> Finite (n + 1)
shift (Finite n -> Finite (n + 1)) -> Finite n -> Finite (n + 1)
forall a b. (a -> b) -> a -> b
$ Finite' n -> Finite n
forall (n :: Nat). KnownNat n => Finite' n -> Finite n
toFinite ((m :<=: n) -> Finite' (1 + n)
forall (m :: Nat) (n :: Nat). (m :<=: n) -> Finite' (1 + n)
Finite' m :<=: n
n'm)

absurdFinite :: Finite 0 -> any
absurdFinite :: forall any. Finite 0 -> any
absurdFinite Finite 0
n = [Char] -> any
forall a. HasCallStack => [Char] -> a
error ([Char] -> any) -> [Char] -> any
forall a b. (a -> b) -> a -> b
$ [Char]
"Finite 0 is uninhabited: getFinite n = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Finite 0 -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite Finite 0
n)

zeroFinite :: (KnownNat m) => Finite (1 + m)
zeroFinite :: forall (m :: Nat). KnownNat m => Finite (1 + m)
zeroFinite = Proxy 0 -> Finite Integer (1 + m)
forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
(KnownNat n, KnownNat m, (n + 1) <= m) =>
proxy n -> Finite m
natToFinite (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0)