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

-----------------------------------------------------------------------------
-- |
-- 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
  + :: Nat -> Nat -> Nat
(+)         = Nat -> Nat -> Nat
forall a. a
no_term_level_nats
  (-)         = Nat -> Nat -> Nat
forall a. a
no_term_level_nats
  * :: Nat -> Nat -> Nat
(*)         = Nat -> Nat -> Nat
forall a. a
no_term_level_nats
  negate :: Nat -> Nat
negate      = Nat -> Nat
forall a. a
no_term_level_nats
  abs :: Nat -> Nat
abs         = Nat -> Nat
forall a. a
no_term_level_nats
  signum :: Nat -> Nat
signum      = Nat -> Nat
forall a. a
no_term_level_nats
  fromInteger :: Integer -> Nat
fromInteger = Integer -> Nat
forall a. a
no_term_level_nats

instance Eq Nat where
  == :: Nat -> Nat -> Bool
(==)        = Nat -> Nat -> Bool
forall a. a
no_term_level_nats

instance Ord Nat where
  compare :: Nat -> Nat -> Ordering
compare     = Nat -> Nat -> Ordering
forall a. a
no_term_level_nats

instance Enum Nat where
  toEnum :: Int -> Nat
toEnum         = Int -> Nat
forall a. a
no_term_level_nats
  fromEnum :: Nat -> Int
fromEnum       = Nat -> Int
forall a. a
no_term_level_nats
  enumFromTo :: Nat -> Nat -> [Nat]
enumFromTo     = Nat -> Nat -> [Nat]
forall a. a
no_term_level_nats
  enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
enumFromThenTo = Nat -> Nat -> Nat -> [Nat]
forall a. a
no_term_level_nats

instance Show Nat where
  showsPrec :: Int -> Nat -> ShowS
showsPrec      = Int -> Nat -> ShowS
forall a. a
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
  == :: Symbol -> Symbol -> Bool
(==)        = Symbol -> Symbol -> Bool
forall a. a
no_term_level_syms

instance Ord Symbol where
  compare :: Symbol -> Symbol -> Ordering
compare     = Symbol -> Symbol -> Ordering
forall a. a
no_term_level_syms

instance IsString Symbol where
  fromString :: String -> Symbol
fromString  = String -> Symbol
forall a. a
no_term_level_syms

instance Semigroup Symbol where
  <> :: Symbol -> Symbol -> Symbol
(<>) = Symbol -> Symbol -> Symbol
forall a. a
no_term_level_syms

instance Monoid Symbol where
  mempty :: Symbol
mempty = Symbol
forall a. a
no_term_level_syms

instance Show Symbol where
  showsPrec :: Int -> Symbol -> ShowS
showsPrec = Int -> Symbol -> ShowS
forall a. a
no_term_level_syms

no_term_level_nats :: a
no_term_level_nats :: a
no_term_level_nats = String -> a
forall a. HasCallStack => String -> a
error String
"The kind `Nat` may not be used at the term level."

no_term_level_syms :: a
no_term_level_syms :: a
no_term_level_syms = String -> a
forall a. HasCallStack => String -> a
error String
"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 :: Natural -> Natural
genLog2 Natural
x = Natural -> Natural -> Natural
forall t b. (Num b, Integral t) => b -> t -> b
exactLoop Natural
0 Natural
x
  where
  exactLoop :: b -> t -> b
exactLoop b
s t
i
    | t
i t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1     = b
s
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2      = b
s
    | Bool
otherwise  =
        let s1 :: b
s1 = b
s b -> b -> b
forall a. Num a => a -> a -> a
+ b
1
        in b
s1 b -> b -> b
`seq` case t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
i t
2 of
                      (t
j,t
r)
                        | t
r t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0    -> b -> t -> b
exactLoop b
s1 t
j
                        | Bool
otherwise -> b -> t -> b
forall t b. (Num b, Integral t) => b -> t -> b
underLoop b
s1 t
j

  underLoop :: t -> t -> t
underLoop t
s t
i
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2  = t
s
    | Bool
otherwise = let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 in t
s1 t -> t -> t
`seq` t -> t -> t
underLoop t
s1 (t -> t -> t
forall a. Integral a => a -> a -> a
div t
i t
2)


sLog2 :: Sing x -> Sing (TN.Log2 x)
sLog2 :: Sing x -> Sing (Log2 x)
sLog2 Sing x
sx =
    let x :: Demote Nat
x   = Sing x -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
    in case Demote Nat
x of
         Demote Nat
0 -> String -> SNat (Log2 x)
forall a. HasCallStack => String -> a
error String
"log2 of 0"
         Demote Nat
_ -> case Natural -> SomeNat
TN.someNatVal (Natural -> Natural
genLog2 Natural
Demote Nat
x) of
                SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Log2 x)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing res)
$(genDefunSymbols [''TN.Log2])
instance SingI Log2Sym0 where
  sing :: Sing Log2Sym0
sing = SingFunction1 Log2Sym0 -> Sing Log2Sym0
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (x :: Nat). Sing x -> Sing (Log2 x)
SingFunction1 Log2Sym0
sLog2

sDiv :: Sing x -> Sing y -> Sing (Div x y)
sDiv :: Sing x -> Sing y -> Sing (Div x y)
sDiv Sing x
sx Sing y
sy =
    let x :: Demote Nat
x   = Sing x -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Nat
y   = Sing y -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        res :: SomeNat
res = Natural -> SomeNat
TN.someNatVal (Natural
Demote Nat
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
Demote Nat
y)
    in case SomeNat
res of
         SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Div x y)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing res)
infixl 7 `sDiv`
$(genDefunSymbols [''Div])
instance SingI DivSym0 where
  sing :: Sing DivSym0
sing = SingFunction2 DivSym0 -> Sing DivSym0
forall a1 a2 b (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun2 forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
SingFunction2 DivSym0
sDiv
instance SingI x => SingI (DivSym1 x) where
  sing :: Sing (DivSym1 x)
sing = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (DivSym1 x) -> Sing (DivSym1 x))
-> SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Div x t)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
sDiv (SingI x => Sing x
forall k (a :: k). SingI a => Sing a
sing @x)

sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod Sing x
sx Sing y
sy =
    let x :: Demote Nat
x   = Sing x -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Nat
y   = Sing y -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        res :: SomeNat
res = Natural -> SomeNat
TN.someNatVal (Natural
Demote Nat
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
Demote Nat
y)
    in case SomeNat
res of
         SomeNat (Proxy n
_ :: Proxy res) -> SNat n -> SNat (Mod x y)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing res)
infixl 7 `sMod`
$(genDefunSymbols [''Mod])
instance SingI ModSym0 where
  sing :: Sing ModSym0
sing = SingFunction2 ModSym0 -> Sing ModSym0
forall a1 a2 b (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun2 forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Mod x y)
SingFunction2 ModSym0
sMod
instance SingI x => SingI (ModSym1 x) where
  sing :: Sing (ModSym1 x)
sing = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ModSym1 x) -> Sing (ModSym1 x))
-> SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Mod x t)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Mod x y)
sMod (Sing x -> Sing t -> Sing (Mod x t))
-> Sing x -> Sing t -> Sing (Mod x t)
forall a b. (a -> b) -> a -> b
$ SingI x => Sing x
forall k (a :: k). SingI a => Sing a
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 :: Sing x -> Sing y -> Sing (DivMod x y)
sDivMod Sing x
sx Sing y
sy =
    let x :: Demote Nat
x     = Sing x -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Nat
y     = Sing y -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        (Natural
q,Natural
r) = Natural
Demote Nat
x Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
Demote Nat
y
        qRes :: SomeNat
qRes  = Natural -> SomeNat
TN.someNatVal Natural
q
        rRes :: SomeNat
rRes  = Natural -> SomeNat
TN.someNatVal Natural
r
    in case (SomeNat
qRes, SomeNat
rRes) of
         (SomeNat (Proxy n
_ :: Proxy q), SomeNat (Proxy n
_ :: Proxy r))
           -> STuple2 '(n, n) -> STuple2 (Tuple2Sym2 (Div x y) (Mod x y))
forall a b. a -> b
unsafeCoerce (Sing n -> Sing n -> STuple2 '(n, n)
forall a b (n :: a) (n :: b). Sing n -> Sing n -> STuple2 '(n, n)
STuple2 (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing q) (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing r))

sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem = Sing x -> Sing y -> Sing (QuotRem x y)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (DivMod x y)
sDivMod

sQuot :: Sing x -> Sing y -> Sing (Quot x y)
sQuot :: Sing x -> Sing y -> Sing (Quot x y)
sQuot = Sing x -> Sing y -> Sing (Quot x y)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
sDiv
infixl 7 `sQuot`

sRem :: Sing x -> Sing y -> Sing (Rem x y)
sRem :: Sing x -> Sing y -> Sing (Rem x y)
sRem = Sing x -> Sing y -> Sing (Rem x y)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Mod x y)
sMod
infixl 7 `sRem`