{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Type.Nat
-- Copyright   :  Copyright (C) 2015 Kyle Carter
-- License     :  BSD3
--
-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
-- Stability   :  experimental
-- Portability :  RankNTypes
--
-- A @singleton@-esque type for representing Peano natural numbers.
--
-----------------------------------------------------------------------------

module Data.Type.Nat where

import Data.Type.Boolean
import Data.Type.Equality
-- import Data.Type.Quantifier
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.Nat
-- import Type.Class.Categories

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
    ]

-- | @'Z_'@ is the canonical construction of a @'Nat' Z@.
instance Known Nat Z where
  known = Z_

-- | If @n@ is a canonical construction of @Nat n@,
-- @'S_' n@ is the canonical construction of @Nat (S n)@.
instance Known Nat n => Known Nat (S n) where
  type KnownC Nat (S n) = Known Nat n
  known = S_ known

-- | A @Nat n@ is a 'Witness' that there is a canonical
-- construction for @Nat n@.
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

-- | A proof that 'Z' is also a right identity
-- for the addition of type-level 'Nat's.
addZ :: Nat x -> (x + Z) :~: x
addZ = \case
  Z_   -> Refl
  S_ x -> _S $ addZ x
{-# INLINE addZ #-}

addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
addS = \case
  Z_   -> pure Refl
  S_ x -> _S . addS x
{-# INLINE addS #-}

(.+) :: 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