{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances   #-}

-- | Provides singletons and general type-level utilities. singletons
-- are value-level representations of types.
--
-- <http://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf Eisenberg, Richard A., and Stephanie Weirich. “Dependently Typed Programming with Singletons.” In Proceedings of the 2012 Haskell Symposium, 117–130. Haskell ’12. New York, NY, USA: ACM, 2012. doi:10.1145/2364506.2364522.>
module TypeLevel.Singletons
  (The(Truey, Falsy, Nily, (:-))
  ,KnownSing(..)
  ,(*.)
  ,(+.)
  ,(^.)
  ,(-.)
  ,(<=.)
  ,totalOrder
  ,type (<=)
  ,type (Lit.+)
  ,type (Lit.*)
  ,type (Lit.^)
  ,Lit.Nat)
  where

import Data.Kind
import qualified GHC.TypeLits as Lit
import Data.Proxy
import Data.Type.Equality

import Data.Coerce
import Unsafe.Coerce

-- | A data family for singletons. The cute name allows code like this:
--
-- @addZeroZero :: The Nat n -> n + 0 :~: n@
--
data family The k :: k -> *

data instance The Bool x where
    Falsy :: The Bool 'False
    Truey :: The Bool 'True

infixr 5 :-
data instance The [k] xs where
    Nily :: The [k] '[]
    (:-) :: The k x -> The [k] xs -> The [k] (x ': xs)

-- | Class for singletons which can be generated.
class KnownSing (x :: k) where
    sing :: The k x

instance KnownSing 'True where
    sing = Truey

instance KnownSing 'False where
    sing = Falsy

instance KnownSing '[] where
    sing = Nily

instance (KnownSing xs, KnownSing x) =>
         KnownSing (x ': xs) where
    sing = sing :- sing

-- | This is just a newtype wrapper for 'Integer'. As such, it
-- is only valid if the programmer can't construct values where the
-- type index doesn't match the contained value. For that reason,
-- the constructor is not exported.
--
-- The reason for this setup is to allow properties and invariants to be proven
-- about the numbers involved, while actual computation can  be carried out
-- efficiently on the values at runtime.
--
-- See the implementation of "Data.Heap.Indexed.Leftist" for an example of
-- the uses of this type.
newtype instance The Lit.Nat n where
        NatSing :: Integer -> The Lit.Nat n

instance Lit.KnownNat n => KnownSing n where
    sing = NatSing $ Prelude.fromInteger $ Lit.natVal (Proxy :: Proxy n)

-- | Add two numbers, on both the value and type level.
infixl 6 +.
(+.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m)
(+.) =
    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m))
        (Prelude.+)
{-# INLINE (+.) #-}

-- | Multiply two numbers, on both the value and type level.
infixl 7 *.
(*.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m)
(*.) =
    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m))
        (Prelude.*)
{-# INLINE (*.) #-}

-- | Raise a number to a power, on the type-level and value-level.
infixr 8 ^.
(^.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m)
(^.) =
    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m))
        (Prelude.^)
{-# INLINE (^.) #-}

-- | Subtract two numbers, on the type-level and value-level, with a
-- proof that overflow can't occur.
infixl 6 -.
(-.) :: (m Lit.<= n) => The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m)
(-.) =
    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m))
        (Prelude.-)
{-# INLINE (-.) #-}


-- | Test order between two numbers, and provide a proof of that
-- order with the result.
infix 4 <=.
(<=.) :: The Lit.Nat n -> The Lit.Nat m -> The Bool (n Lit.<=? m)
(<=.) (NatSing x :: The Lit.Nat n) (NatSing y :: The Lit.Nat m)
  | x <= y = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'True) of
      Refl -> Truey
  | otherwise = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'False) of
      Refl -> Falsy
{-# INLINE (<=.) #-}

-- | A proof of a total order on the naturals.
totalOrder ::  p n -> q m -> (n Lit.<=? m) :~: 'False -> (m Lit.<=? n) :~: 'True
totalOrder (_ :: p n) (_ :: q m) Refl = unsafeCoerce Refl :: (m Lit.<=? n) :~: 'True

-- | A proof that x is less than or equal to y.
type x <= y = (x Lit.<=? y) :~: 'True