{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Text.Show.Singletons
-- Copyright   :  (C) 2017 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines the SShow singleton version of the Show type class.
--
-----------------------------------------------------------------------------

module Text.Show.Singletons (
  PShow(..), SShow(..), SymbolS, SChar, show_,
  Shows, sShows,
  ShowListWith, sShowListWith,
  ShowChar, sShowChar,
  ShowString, sShowString,
  ShowParen, sShowParen,
  ShowSpace, sShowSpace,
  ShowCommaSpace, sShowCommaSpace,
  AppPrec, sAppPrec,
  AppPrec1, sAppPrec1,

  -- * Defunctionalization symbols
  ShowsPrecSym0, ShowsPrecSym1, ShowsPrecSym2, ShowsPrecSym3,
  Show_Sym0, Show_Sym1,
  ShowListSym0, ShowListSym1, ShowListSym2,
  ShowsSym0, ShowsSym1, ShowsSym2,
  ShowListWithSym0, ShowListWithSym1, ShowListWithSym2, ShowListWithSym3,
  ShowCharSym0, ShowCharSym1, ShowCharSym2,
  ShowStringSym0, ShowStringSym1, ShowStringSym2,
  ShowParenSym0, ShowParenSym1, ShowParenSym2,
  ShowSpaceSym0, ShowSpaceSym1,
  ShowCommaSpaceSym0, ShowCommaSpaceSym1,
  AppPrecSym0, AppPrec1Sym0
  ) where

import           Data.Kind
import           Data.List.NonEmpty (NonEmpty)
import           Data.List.Singletons.Internal
import           Data.Ord (Down)
import           Data.Ord.Singletons
import           Data.Proxy
import           Data.Semigroup.Singletons.Internal
import           Data.Singletons
import           Data.Singletons.Base.Instances
import           Data.Singletons.TH
import qualified Data.Text as T
import           GHC.Base.Singletons
import           GHC.Num.Singletons
import           GHC.TypeLits
import           GHC.TypeLits.Singletons
import qualified Prelude as P
import           Prelude hiding (Show(..))
import           Unsafe.Coerce (unsafeCoerce)

-- | The @shows@ functions return a function that prepends the
-- output 'Symbol' to an existing 'Symbol'.  This allows constant-time
-- concatenation of results using function composition.
type SymbolS :: Type
type SymbolS = Symbol -> Symbol

-- | GHC currently has no notion of type-level 'Char's, so we fake them with
-- single-character 'Symbol's.
type SChar :: Type
type SChar = Symbol

$(singletonsOnly [d|
  class Show a where
    showsPrec :: Nat -> a -> SymbolS
    show_     :: a -> Symbol
    showList  :: [a] -> SymbolS

    showsPrec _ x s = show_ x <> s
    show_ x         = shows x ""
    showList ls   s = showListWith shows ls s

  shows :: Show a => a -> SymbolS
  shows s = showsPrec 0 s

  showListWith :: (a -> SymbolS) -> [a] -> SymbolS
  showListWith _     []     s = "[]" <> s
  showListWith showx (x:xs) s = "["  <> showx x (showl xs)
    where
      showl []     = "]" <> s
      showl (y:ys) = "," <> showx y (showl ys)

  showChar :: SChar -> SymbolS
  showChar = (<>)

  showString :: Symbol -> SymbolS
  showString = (<>)

  showParen :: Bool -> SymbolS -> SymbolS
  showParen b p = if b then showChar "(" . p . showChar ")" else p

  showSpace :: SymbolS
  showSpace = \xs -> " " <> xs

  showCommaSpace :: SymbolS
  showCommaSpace = showString ", "

  appPrec, appPrec1 :: Nat
  appPrec  = 10
  appPrec1 = 11

  instance Show a => Show [a] where
    showsPrec _ = showList

  -- -| This is not an ideal Show instance for Symbol, since the Show instance
  -- for String escapes special characters. Unfortunately, GHC lacks the ability
  -- to case on individual characters in a Symbol (at least, not without GHC
  -- plugins), so this is the best we can do for the time being.
  instance Show Symbol where
    showsPrec _ = showString

  show_tuple :: [SymbolS] -> SymbolS
  show_tuple ss = showChar "("
                . foldr1 (\s r -> s . showChar "," . r) ss
                . showChar ")"

  instance (Show a, Show b) => Show (a,b)  where
    showsPrec _ (a,b) s = show_tuple [shows a, shows b] s

  instance (Show a, Show b, Show c) => Show (a, b, c) where
    showsPrec _ (a,b,c) s = show_tuple [shows a, shows b, shows c] s

  instance (Show a, Show b, Show c, Show d) => Show (a, b, c, d) where
    showsPrec _ (a,b,c,d) s = show_tuple [shows a, shows b, shows c, shows d] s

  instance (Show a, Show b, Show c, Show d, Show e) => Show (a, b, c, d, e) where
    showsPrec _ (a,b,c,d,e) s = show_tuple [shows a, shows b, shows c, shows d, shows e] s

  instance (Show a, Show b, Show c, Show d, Show e, Show f) => Show (a,b,c,d,e,f) where
    showsPrec _ (a,b,c,d,e,f) s = show_tuple [shows a, shows b, shows c, shows d, shows e, shows f] s

  instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g)
          => Show (a,b,c,d,e,f,g) where
    showsPrec _ (a,b,c,d,e,f,g) s
          = show_tuple [shows a, shows b, shows c, shows d, shows e, shows f, shows g] s

  deriving instance Show a => Show (Down a)
  |])

$(promoteOnly [d|
  showsNat :: Nat -> SymbolS
  showsNat 0 = showChar "0"
  showsNat 1 = showChar "1"
  showsNat 2 = showChar "2"
  showsNat 3 = showChar "3"
  showsNat 4 = showChar "4"
  showsNat 5 = showChar "5"
  showsNat 6 = showChar "6"
  showsNat 7 = showChar "7"
  showsNat 8 = showChar "8"
  showsNat 9 = showChar "9"
  showsNat n = showsNat (n `div` 10) . showsNat (n `mod` 10)
  |])

instance PShow Nat where
  type ShowsPrec _ n x = ShowsNat n x

instance SShow Nat where
  sShowsPrec :: forall (t :: Nat) (t :: Nat) (t :: Symbol).
Sing t
-> Sing t
-> Sing t
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)
sShowsPrec Sing t
_ Sing t
sn Sing t
sx =
    let n :: Demote Nat
n = Sing t -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sn
        x :: Demote Symbol
x = Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sx
        ex :: SomeSymbol
ex = String -> SomeSymbol
someSymbolVal (Natural -> String
forall a. Show a => a -> String
P.show Natural
Demote Nat
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Demote Symbol
Text
x)
    in
    case SomeSymbol
ex of
      SomeSymbol (Proxy n
_ :: Proxy s) -> SSymbol n -> SSymbol (ShowsNat t t)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing s)

-- | 'P.show', but with an extra underscore so that its promoted counterpart
-- ('Show_') will not clash with the 'Show' class.
show_ :: P.Show a => a -> String
show_ :: forall a. Show a => a -> String
show_ = a -> String
forall a. Show a => a -> String
P.show

$(singShowInstances [ ''(), ''Maybe, ''Either, ''NonEmpty, ''Bool,
                      ''Ordering, ''Void ])