module Language.LSP.Protocol.Types.Singletons where

import Control.DeepSeq
import Data.Aeson
import Data.Hashable
import Data.Proxy
import Data.Text qualified as T
import GHC.TypeLits (
  KnownNat,
  KnownSymbol,
  Nat,
  Symbol,
  natVal,
  symbolVal,
 )
import Prettyprinter

{- | A type whose only inhabitant is a single, statically-known string.

 This corresponds to types like @"hello"@ in the LSP specification that
 are exactly types with a single inhabitant.
-}
data AString (s :: Symbol) where
  AString :: KnownSymbol s => AString s

instance Show (AString s) where
  show AString = symbolVal (Proxy @s)
instance Pretty (AString s) where
  pretty = viaShow
instance Eq (AString s) where
  _ == _ = True
instance Ord (AString s) where
  compare _ _ = EQ
instance NFData (AString s) where
  rnf a = seq a ()
instance Hashable (AString sym) where
  hashWithSalt s AString = hashWithSalt s (symbolVal (Proxy @sym))

instance ToJSON (AString s) where
  toJSON AString = toJSON (T.pack (symbolVal (Proxy @s)))

instance KnownSymbol s => FromJSON (AString s) where
  parseJSON = withText "string literal type" $ \s -> do
    let sym = symbolVal (Proxy @s)
    if s == T.pack sym
      then pure AString
      else fail $ "wrong string, got: " <> show s <> " expected " <> sym

{- | A type whose only inhabitant is a single, statically-known integer.

 This corresponds to types like @1@ in the LSP specification that
 are exactly types with a single inhabitant.
-}
data AnInteger (n :: Nat) where
  AnInteger :: KnownNat n => AnInteger n

instance Show (AnInteger n) where
  show AnInteger = show $ natVal (Proxy @n)
instance Pretty (AnInteger n) where
  pretty = viaShow
instance Eq (AnInteger n) where
  _ == _ = True
instance Ord (AnInteger n) where
  compare _ _ = EQ
instance NFData (AnInteger s) where
  rnf a = seq a ()
instance Hashable (AnInteger i) where
  hashWithSalt s AnInteger = hashWithSalt s (natVal (Proxy @i))

instance ToJSON (AnInteger n) where
  toJSON AnInteger = toJSON (natVal (Proxy @n))

instance KnownNat n => FromJSON (AnInteger n) where
  parseJSON = withScientific "integer literal type" $ \n -> do
    let nat = natVal (Proxy @n)
    if truncate n == nat
      then pure AnInteger
      else fail $ "wrong integer, got: " <> show n <> " expected " <> show nat