module Data.Type.Natural.Core where
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
import Data.Type.Natural.Compat
#endif
import Data.Constraint hiding ((:-))
import Data.Promotion.Prelude.Ord ((:<=))
import Data.Type.Natural.Definitions hiding ((:<=))
import Prelude (Bool (..), Eq (..), Show (..), ($))
import Proof.Propositional (IsTrue)
import Unsafe.Coerce
data Leq (n :: Nat) (m :: Nat) where
ZeroLeq :: SNat m -> Leq Zero m
SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m)
type LeqTrueInstance a b = IsTrue (a :<= b)
(%-) :: (m :<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)
n %- SZ = n
SS n %- SS m = n %- m
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
_ %- _ = bugInGHC
#endif
infixl 6 %-
deriving instance Show (SNat n)
deriving instance Eq (SNat n)
data (a :: Nat) :<: (b :: Nat) where
ZeroLtSucc :: Zero :<: 'S m
SuccLtSucc :: n :<: m -> 'S n :<: 'S m
deriving instance Show (a :<: b)
propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
boolToClassLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m
boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
propToClassLeq :: Leq n m -> LeqInstance n m
propToClassLeq _ = unsafeCoerce (Dict :: Dict ())
type LeqInstance n m = IsTrue (n :<= m)
boolToPropLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> Leq n m
boolToPropLeq SZ m = ZeroLeq m
boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
boolToPropLeq _ _ = bugInGHC
#endif
leqRhs :: Leq n m -> SNat m
leqRhs (ZeroLeq m) = m
leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq
leqLhs :: Leq n m -> SNat n
leqLhs (ZeroLeq _) = SZ
leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq