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 s -> String
show AString s
AString = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @s)
instance Pretty (AString s) where
  pretty :: forall ann. AString s -> Doc ann
pretty = forall a ann. Show a => a -> Doc ann
viaShow
instance Eq (AString s) where
  AString s
_ == :: AString s -> AString s -> Bool
== AString s
_ = Bool
True
instance Ord (AString s) where
  compare :: AString s -> AString s -> Ordering
compare AString s
_ AString s
_ = Ordering
EQ
instance NFData (AString s) where
  rnf :: AString s -> ()
rnf AString s
a = seq :: forall a b. a -> b -> b
seq AString s
a ()
instance Hashable (AString sym) where
  hashWithSalt :: Int -> AString sym -> Int
hashWithSalt Int
s AString sym
AString = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @sym))

instance ToJSON (AString s) where
  toJSON :: AString s -> Value
toJSON AString s
AString = forall a. ToJSON a => a -> Value
toJSON (String -> Text
T.pack (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @s)))

instance KnownSymbol s => FromJSON (AString s) where
  parseJSON :: Value -> Parser (AString s)
parseJSON = forall a. String -> (Text -> Parser a) -> Value -> Parser a
withText String
"string literal type" forall a b. (a -> b) -> a -> b
$ \Text
s -> do
    let sym :: String
sym = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @s)
    if Text
s forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
sym
      then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (s :: Symbol). KnownSymbol s => AString s
AString
      else forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"wrong string, got: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
s forall a. Semigroup a => a -> a -> a
<> String
" expected " forall a. Semigroup a => a -> a -> a
<> String
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 n -> String
show AnInteger n
AnInteger = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
instance Pretty (AnInteger n) where
  pretty :: forall ann. AnInteger n -> Doc ann
pretty = forall a ann. Show a => a -> Doc ann
viaShow
instance Eq (AnInteger n) where
  AnInteger n
_ == :: AnInteger n -> AnInteger n -> Bool
== AnInteger n
_ = Bool
True
instance Ord (AnInteger n) where
  compare :: AnInteger n -> AnInteger n -> Ordering
compare AnInteger n
_ AnInteger n
_ = Ordering
EQ
instance NFData (AnInteger s) where
  rnf :: AnInteger s -> ()
rnf AnInteger s
a = seq :: forall a b. a -> b -> b
seq AnInteger s
a ()
instance Hashable (AnInteger i) where
  hashWithSalt :: Int -> AnInteger i -> Int
hashWithSalt Int
s AnInteger i
AnInteger = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @i))

instance ToJSON (AnInteger n) where
  toJSON :: AnInteger n -> Value
toJSON AnInteger n
AnInteger = forall a. ToJSON a => a -> Value
toJSON (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n))

instance KnownNat n => FromJSON (AnInteger n) where
  parseJSON :: Value -> Parser (AnInteger n)
parseJSON = forall a. String -> (Scientific -> Parser a) -> Value -> Parser a
withScientific String
"integer literal type" forall a b. (a -> b) -> a -> b
$ \Scientific
n -> do
    let nat :: Integer
nat = forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
    if forall a b. (RealFrac a, Integral b) => a -> b
truncate Scientific
n forall a. Eq a => a -> a -> Bool
== Integer
nat
      then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (n :: Nat). KnownNat n => AnInteger n
AnInteger
      else forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"wrong integer, got: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Scientific
n forall a. Semigroup a => a -> a -> a
<> String
" expected " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Integer
nat