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

import Control.Applicative (Applicative(..))
import Data.Bool
import Data.Eq (Eq(..))
import Data.Foldable (Foldable)
import Data.Function ((.), flip)
import Data.Functor (Functor(..), (<$>))
import Data.Int (Int)
import Data.Maybe (Maybe(..), isJust)
import Data.Monoid (Monoid(..))
import Data.Proxy (Proxy(..))
import Data.Traversable (Traversable(..))
import Data.Tuple (fst, snd)
import Data.Type.Equality ((:~:)(..))
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)