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

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

    sLog2 :: Sing x -> Sing (TN.Log2 x)
    sLog2 :: Sing x -> Sing (Log2 x)
    sLog2 sx :: 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
             0 -> String -> SNat (Log2 x)
    forall a. HasCallStack => String -> a
    error "log2 of 0"
             _ -> 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 k1 k (f :: k1 ~> k). 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 sx :: Sing x
    sx sy :: 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 k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 DivSym0
    forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
    sDiv
    instance SingI x => SingI (DivSym1 x) where
      sing :: Sing (DivSym1 x)
    sing = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
    forall k1 k (f :: k1 ~> k). 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 sx :: Sing x
    sx sy :: 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 k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 ModSym0
    forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Mod x y)
    sMod
    instance SingI x => SingI (ModSym1 x) where
      sing :: Sing (ModSym1 x)
    sing = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
    forall k1 k (f :: k1 ~> k). 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 (Apply (ModSym1 x) t)
    forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Mod x y)
    sMod (Sing x -> Sing t -> Sing (Apply (ModSym1 x) t))
    -> Sing x -> Sing t -> Sing (Apply (ModSym1 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 sx :: Sing x
    sx sy :: 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
            (q :: Natural
    q,r :: 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 '(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`