{-# 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, 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.Bool.Singletons
import           Data.Eq.Singletons
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

$(singletonsOnly [d|
  class Show a where
    showsPrec :: Natural -> 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 :: Char -> SymbolS
  showChar = consSymbol

  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

  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 :: Natural -> 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 Natural where
  type ShowsPrec _ n x = ShowsNat n x

instance SShow Natural where
  sShowsPrec :: forall (t :: Natural) (t :: Natural) (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 Natural
n = Sing t -> Demote Natural
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 Natural
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
Demote Symbol
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)

$(promoteOnly [d|
  showsCharPrec :: Natural -> Char -> SymbolS
  showsCharPrec _ '\'' = showString "'\\''"
  showsCharPrec _ c    = showChar '\'' . showLitChar c . showChar '\''

  showCharList :: [Char] -> SymbolS
  showCharList cs = showChar '"' . showLitString cs . showChar '"'

  -- -| Like 'showCharList', but for 'Symbol's.
  showSymbol :: Symbol -> SymbolS
  showSymbol sym = showChar '"' . showLitSymbol sym . showChar '"'

  -- -| Convert a character to a string using only printable characters,
  -- using Haskell source-language escape conventions.  For example:
  --
  -- > showLitChar '\n' s  =  "\\n" ++ s
  --
  showLitChar                :: Char -> SymbolS
  showLitChar c s | c > '\DEL' =  showChar '\\' (protectEsc isDec (shows (charToNat c)) s)
  showLitChar '\DEL'         s =  showString "\\DEL" s
  showLitChar '\\'           s =  showString "\\\\" s
  showLitChar c s | c >= ' '   =  showChar c s
  showLitChar '\a'           s =  showString "\\a" s
  showLitChar '\b'           s =  showString "\\b" s
  showLitChar '\f'           s =  showString "\\f" s
  showLitChar '\n'           s =  showString "\\n" s
  showLitChar '\r'           s =  showString "\\r" s
  showLitChar '\t'           s =  showString "\\t" s
  showLitChar '\v'           s =  showString "\\v" s
  showLitChar '\SO'          s =  protectEsc (== 'H') (showString "\\SO") s
  showLitChar c              s =  showString ('\\' `consSymbol` (asciiTab!!charToNat c)) s
          -- I've done manual eta-expansion here, because otherwise it's
          -- impossible to stop (asciiTab!!charToNat) getting floated out as an MFE

  showLitString :: String -> SymbolS
  -- -| Same as 'showLitChar', but for strings
  -- It converts the string to a string using Haskell escape conventions
  -- for non-printable characters. Does not add double-quotes around the
  -- whole thing; the caller should do that.
  -- The main difference from showLitChar (apart from the fact that the
  -- argument is a string not a list) is that we must escape double-quotes
  showLitString []         s = s
  showLitString ('"' : cs) s = showString "\\\"" (showLitString cs s)
  showLitString (c   : cs) s = showLitChar c (showLitString cs s)
     -- Making 's' an explicit parameter makes it clear to GHC that
     -- showLitString has arity 2, which avoids it allocating an extra lambda
     -- The sticking point is the recursive call to (showLitString cs), which
     -- it can't figure out would be ok with arity 2.

  -- -| Like 'showLitString', but for 'Symbol's.
  showLitSymbol :: Symbol -> SymbolS
  showLitSymbol sym s = case unconsSymbol sym of
    Nothing        -> s
    Just ('"', cs) -> showString "\\\"" (showLitSymbol cs s)
    Just (c,   cs) -> showLitChar c (showLitSymbol cs s)

  isDec :: Char -> Bool
  isDec c = c >= '0' && c <= '9'

  protectEsc :: (Char -> Bool) -> SymbolS -> SymbolS
  protectEsc p f             = f . cont
                               -- where cont s@(c:_) | p c = "\\&" ++ s
                               --       cont s             = s
                               where cont s = case unconsSymbol s of
                                       Just (c, _) | p c -> "\\&" <> s
                                       Nothing           -> s

  asciiTab :: [Symbol]
  asciiTab = -- Using an array drags in the array module.  listArray ('\NUL', ' ')
             ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
              "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",
              "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
              "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US",
              "SP"]
  |])

instance PShow Char where
  type ShowsPrec p c x = ShowsCharPrec p c x
  type ShowList cs x = ShowCharList cs x

instance SShow Char where
  sShowsPrec :: forall (t :: Natural) (t :: Char) (t :: Symbol).
Sing t
-> Sing t
-> Sing t
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)
sShowsPrec Sing t
sp Sing t
sc Sing t
sx =
    let p :: Demote Natural
p  = Sing t -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sp
        c :: Demote Char
c  = Sing t -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sc
        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 (Int -> Char -> String -> String
forall a. Show a => Int -> a -> String -> String
P.showsPrec (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
Demote Natural
p) Char
Demote Char
c (Text -> String
T.unpack Text
Demote Symbol
x))
    in
    case SomeSymbol
ex of
      SomeSymbol (Proxy n
_ :: Proxy s) -> SSymbol n -> SSymbol (ShowsCharPrec t t t)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing s)

  sShowList :: forall (t :: String) (t :: Symbol).
Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t)
sShowList Sing t
scs Sing t
sx =
    let cs :: Demote String
cs = Sing t -> Demote String
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
scs
        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 (String -> String -> String
forall a. Show a => [a] -> String -> String
P.showList String
Demote String
cs (Text -> String
T.unpack Text
Demote Symbol
x))
    in
    case SomeSymbol
ex of
      SomeSymbol (Proxy n
_ :: Proxy s) -> SSymbol n
-> SSymbol (ConsSymbol '"' (ShowLitString t (ConsSymbol '"' t)))
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing s)

instance PShow Symbol where
  type ShowsPrec _ s x = ShowSymbol s x

instance SShow Symbol where
  sShowsPrec :: forall (t :: Natural) (t :: Symbol) (t :: Symbol).
Sing t
-> Sing t
-> Sing t
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)
sShowsPrec Sing t
_ Sing t
ss Sing t
sx =
    let s :: Demote Symbol
s  = Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
ss
        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 (Text -> String
forall a. Show a => a -> String
P.show Text
Demote Symbol
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
Demote Symbol
x)
    in
    case SomeSymbol
ex of
      SomeSymbol (Proxy n
_ :: Proxy s) -> SSymbol n
-> SSymbol
     (ConsSymbol
        '"'
        (Case_6989586621680267184 t (ConsSymbol '"' t) (UnconsSymbol 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 ])