{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Utils.Natural
 ( (+<=)
 , nat
 , Index(..)
 , (<=)
 , (<=?)
 , (+)
 , (-)
 , module GHC.TypeNats
 , Known
 ) where

import Data.Bool
import Data.Eq (Eq(..))
import Data.Maybe (Maybe(..), isJust)
import Data.Proxy (Proxy(..))
import GHC.TypeNats
import Numeric.Natural (Natural)
import Text.Show (Show(..))
import Unsafe.Coerce (unsafeCoerce)
import qualified Data.Ord as Ord
import qualified Prelude as Num

import Utils.Constraint

-- | Convenient wrapper around 'natVal' to be used with @TypeApplications@.
nat :: forall (n::Nat). KnownNat n => Natural
nat = natVal (Proxy::Proxy n)

-- * Type 'Known'
-- | Convenient alias.
type Known = KnownNat

-- * Proofs
-- | Proofs implied by @(i'+'j'<='n)@
(+<=) :: (i+j<=n) => Proof (i<=n, j<=n, j<=n-i, i<=n-j)
(+<=) = unsafeCoerce (Proof::Proof ((),(),(),()))

-- | Proofs implied by @(i'<='j)@.
(<=) :: forall i j.
 KnownNat i => KnownNat j =>
 (i<=j) => Proof ( KnownNat (j-i)
                 , ((j-i)+i) ~ j
                 , ((i+j)-i) ~ j
                 , (i+(j-i)) ~ j )
(<=) | SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
     = unsafeCoerce (Proof::Proof (KnownNat jmi, (), (), ()))

-- ** Operators
(+) :: forall i j. KnownNat i => KnownNat j => Proof (KnownNat (i+j))
(+) | SomeNat (_ipj::Proxy ipj) <- someNatVal (nat @i Num.+ nat @j)
    = unsafeCoerce (Proof::Proof (KnownNat ipj))

infixl 6 -
(-) :: forall i j. (j<=i) => KnownNat i => KnownNat j => Proof (KnownNat (i-j))
(-) | SomeNat (_imj::Proxy imj) <- someNatVal (nat @i Num.- nat @j)
    = unsafeCoerce (Proof::Proof (KnownNat imj))

infix 4 <=?
(<=?) :: forall i j.
 KnownNat i => KnownNat j =>
 Maybe (Proof ( i<=j
              , KnownNat (j-i)
              , ((j-i)+i) ~ j
              , ((i+j)-i) ~ j
              , (i+(j-i)) ~ j ))
(<=?) | nat @i Ord.<= nat @j
      , SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
      = Just (unsafeCoerce (Proof::Proof ((),KnownNat jmi,(),(),())))
      | otherwise = Nothing

-- * Type 'Index'
data Index len where
 Index :: (KnownNat i, (i+1<=len)) => Proxy i -> Index len
instance Eq (Index len) where
	Index i == Index j = isJust (sameNat i j)
instance Show (Index len) where
	showsPrec p (Index i) = showsPrec p (natVal i)