{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, ConstraintKinds,
             GADTs, TypeApplications, TypeFamilies, UndecidableInstances,
             DataKinds, PolyKinds #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.TypeLits
-- Copyright   :  (C) 2014 Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines and exports singletons useful for the Nat and Symbol kinds.
--
----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wno-orphans #-}

module Data.Singletons.TypeLits (
  Nat, Symbol,
  Sing, SNat(..), SSymbol(..), withKnownNat, withKnownSymbol,
  Error, sError,
  ErrorWithoutStackTrace, sErrorWithoutStackTrace,
  Undefined, sUndefined,
  KnownNat, natVal,
  KnownSymbol, symbolVal,

  type (^), (%^),
  type (<=?), (%<=?),

  TN.Log2, sLog2,
  Div, sDiv, Mod, sMod, DivMod, sDivMod,
  Quot, sQuot, Rem, sRem, QuotRem, sQuotRem,

  -- * Defunctionalization symbols
  ErrorSym0, ErrorSym1,
  ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
  UndefinedSym0,
  KnownNatSym0, KnownNatSym1,
  KnownSymbolSym0, KnownSymbolSym1,
  type (^@#@$), type (^@#@$$), type (^@#@$$$),
  type (<=?@#@$), type (<=?@#@$$), type (<=?@#@$$$),
  Log2Sym0, Log2Sym1,
  DivSym0, DivSym1, DivSym2,
  ModSym0, ModSym1, ModSym2,
  DivModSym0, DivModSym1, DivModSym2,
  QuotSym0, QuotSym1, QuotSym2,
  RemSym0, RemSym1, RemSym2,
  QuotRemSym0, QuotRemSym1, QuotRemSym2
  ) where

import Data.Singletons.Internal
import Data.Singletons.Prelude.Tuple
import Data.Singletons.Promote
import Data.Singletons.ShowSing ()      -- for Show instances
import Data.Singletons.TypeLits.Internal

import Data.String (IsString(..))
import qualified GHC.TypeNats as TN
import GHC.TypeNats (Div, Mod, SomeNat(..))
import Numeric.Natural (Natural)

import Unsafe.Coerce

-- | This bogus 'Num' instance is helpful for people who want to define
-- functions over Nats that will only be used at the type level or
-- as singletons. A correct SNum instance for Nat singletons exists.
instance Num Nat where
  (+)         = no_term_level_nats
  (-)         = no_term_level_nats
  (*)         = no_term_level_nats
  negate      = no_term_level_nats
  abs         = no_term_level_nats
  signum      = no_term_level_nats
  fromInteger = no_term_level_nats

instance Eq Nat where
  (==)        = no_term_level_nats

instance Ord Nat where
  compare     = no_term_level_nats

instance Enum Nat where
  toEnum         = no_term_level_nats
  fromEnum       = no_term_level_nats
  enumFromTo     = no_term_level_nats
  enumFromThenTo = no_term_level_nats

instance Show Nat where
  showsPrec      = no_term_level_nats

-- | This bogus instance is helpful for people who want to define
-- functions over Symbols that will only be used at the type level or
-- as singletons.
instance Eq Symbol where
  (==)        = no_term_level_syms

instance Ord Symbol where
  compare     = no_term_level_syms

instance IsString Symbol where
  fromString  = no_term_level_syms

instance Semigroup Symbol where
  (<>) = no_term_level_syms

instance Monoid Symbol where
  mempty = no_term_level_syms

instance Show Symbol where
  showsPrec = no_term_level_syms

no_term_level_nats :: a
no_term_level_nats = error "The kind `Nat` may not be used at the term level."

no_term_level_syms :: a
no_term_level_syms = error "The kind `Symbol` may not be used at the term level."

-- These are often useful in TypeLits-heavy code
$(genDefunSymbols [''KnownNat, ''KnownSymbol])

------------------------------------------------------------
-- Log2, Div, Mod, DivMod, and friends
------------------------------------------------------------

{- | Adapted from GHC's source code.

Compute the logarithm of a number in the given base, rounded down to the
closest integer. -}
genLog2 :: Natural -> Natural
genLog2 x = exactLoop 0 x
  where
  exactLoop s i
    | i == 1     = s
    | i < 2      = s
    | otherwise  =
        let s1 = s + 1
        in s1 `seq` case divMod i 2 of
                      (j,r)
                        | r == 0    -> exactLoop s1 j
                        | otherwise -> underLoop s1 j

  underLoop s i
    | i < 2  = s
    | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i 2)


sLog2 :: Sing x -> Sing (TN.Log2 x)
sLog2 sx =
    let x   = fromSing sx
    in case x of
         0 -> error "log2 of 0"
         _ -> case TN.someNatVal (genLog2 x) of
                SomeNat (_ :: Proxy res) -> unsafeCoerce (SNat :: Sing res)
$(genDefunSymbols [''TN.Log2])
instance SingI Log2Sym0 where
  sing = singFun1 sLog2

sDiv :: Sing x -> Sing y -> Sing (Div x y)
sDiv sx sy =
    let x   = fromSing sx
        y   = fromSing sy
        res = TN.someNatVal (x `div` y)
    in case res of
         SomeNat (_ :: Proxy res) -> unsafeCoerce (SNat :: Sing res)
infixl 7 `sDiv`
$(genDefunSymbols [''Div])
instance SingI DivSym0 where
  sing = singFun2 sDiv
instance SingI x => SingI (DivSym1 x) where
  sing = singFun1 $ sDiv (sing @x)

sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod sx sy =
    let x   = fromSing sx
        y   = fromSing sy
        res = TN.someNatVal (x `mod` y)
    in case res of
         SomeNat (_ :: Proxy res) -> unsafeCoerce (SNat :: Sing res)
infixl 7 `sMod`
$(genDefunSymbols [''Mod])
instance SingI ModSym0 where
  sing = singFun2 sMod
instance SingI x => SingI (ModSym1 x) where
  sing = singFun1 $ sMod $ sing @x

$(promoteOnly [d|
  divMod :: Nat -> Nat -> (Nat, Nat)
  divMod x y = (div x y, mod x y)

  quotRem :: Nat -> Nat -> (Nat, Nat)
  quotRem = divMod

  quot :: Nat -> Nat -> Nat
  quot = div
  infixl 7 `quot`

  rem :: Nat -> Nat -> Nat
  rem = mod
  infixl 7 `rem`
  |])

sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
sDivMod sx sy =
    let x     = fromSing sx
        y     = fromSing sy
        (q,r) = x `divMod` y
        qRes  = TN.someNatVal q
        rRes  = TN.someNatVal r
    in case (qRes, rRes) of
         (SomeNat (_ :: Proxy q), SomeNat (_ :: Proxy r))
           -> unsafeCoerce (STuple2 (SNat :: Sing q) (SNat :: Sing r))

sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem = sDivMod

sQuot :: Sing x -> Sing y -> Sing (Quot x y)
sQuot = sDiv
infixl 7 `sQuot`

sRem :: Sing x -> Sing y -> Sing (Rem x y)
sRem = sMod
infixl 7 `sRem`