module Data.Type.Nat where
import Data.Type.Boolean
import Data.Type.Equality
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.Nat
data Nat :: N -> * where
Z_ :: Nat Z
S_ :: !(Nat n) -> Nat (S n)
deriving instance Eq (Nat n)
deriving instance Ord (Nat n)
deriving instance Show (Nat n)
instance Eq1 Nat
instance Ord1 Nat
instance Show1 Nat
instance Read1 Nat where
readsPrec1 d = readParen (d > 10) $ \s0 ->
[ (Some Z_,s1)
| ("Z_",s1) <- lex s0
] ++
[ (n >>- Some . S_,s2)
| ("S_",s1) <- lex s0
, (n,s2) <- readsPrec1 11 s1
]
instance Known Nat Z where
known = Z_
instance Known Nat n => Known Nat (S n) where
type KnownC Nat (S n) = Known Nat n
known = S_ known
instance Witness ØC (Known Nat n) (Nat n) where
(\\) r = \case
Z_ -> r
S_ x -> r \\ x
instance TestEquality Nat where
testEquality = \case
Z_ -> \case
Z_ -> Just Refl
S_ _ -> Nothing
S_ x -> \case
Z_ -> Nothing
S_ y -> testEquality x y //? qed
instance BoolEquality Nat where
boolEquality = \case
Z_ -> \case
Z_ -> True_
S_ _ -> False_
S_ x -> \case
Z_ -> False_
S_ y -> x .== y
pred' :: Nat (S x) -> Nat x
pred' (S_ x) = x
onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)
onNatPred f (S_ x) = S_ $ f x
_Z :: Z :~: Z
_Z = Refl
_S :: x :~: y -> S x :~: S y
_S Refl = Refl
_s :: S x :~: S y -> x :~: y
_s Refl = Refl
_ZneS :: Z :~: S x -> Void
_ZneS = impossible
addZ :: Nat x -> (x + Z) :~: x
addZ = \case
Z_ -> Refl
S_ x -> _S $ addZ x
addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
addS = \case
Z_ -> pure Refl
S_ x -> _S . addS x
(.+) :: Nat x -> Nat y -> Nat (x + y)
(.+) = \case
Z_ -> id
S_ x -> S_ . (x .+)
infixr 6 .+
(.*) :: Nat x -> Nat y -> Nat (x * y)
(.*) = \case
Z_ -> const Z_
S_ x -> (.+) <$> (x .*) <*> id
infixr 7 .*
(.^) :: Nat x -> Nat y -> Nat (x ^ y)
(.^) x = \case
Z_ -> S_ Z_
S_ y -> (x .^ y) .* x
infixl 8 .^
elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n
elimNat z s = \case
Z_ -> z
S_ x -> s x $ elimNat z s x
natVal :: Nat n -> Int
natVal = \case
Z_ -> 0
S_ x -> succ $ natVal x