{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Language.LSP.Protocol.Message.Method where

import Data.Aeson.Types
import Data.Function (on)
import Data.GADT.Compare
import Data.List (isPrefixOf)
import Data.Proxy
import Data.Type.Equality
import GHC.Exts (Int (..), dataToTag#)
import GHC.TypeLits (
  KnownSymbol,
  sameSymbol,
  symbolVal,
 )
import Language.LSP.Protocol.Internal.Method
import Language.LSP.Protocol.Message.Meta
import Language.LSP.Protocol.Utils.Misc
import Prettyprinter
import Unsafe.Coerce

---------------
-- SomeMethod
---------------

-- | Is this an "optional" method which servers and clients are allowed to ignore?
isOptionalMethod :: SomeMethod -> Bool
-- See https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#dollarRequests
isOptionalMethod :: SomeMethod -> Bool
isOptionalMethod SomeMethod
m = [Char]
"$/" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` SomeMethod -> [Char]
someMethodToMethodString SomeMethod
m

deriving stock instance Show SomeMethod
instance Eq SomeMethod where
  == :: SomeMethod -> SomeMethod -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SomeMethod -> [Char]
someMethodToMethodString
instance Ord SomeMethod where
  compare :: SomeMethod -> SomeMethod -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SomeMethod -> [Char]
someMethodToMethodString

instance ToJSON SomeMethod where
  toJSON :: SomeMethod -> Value
toJSON SomeMethod
sm = forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ SomeMethod -> [Char]
someMethodToMethodString SomeMethod
sm

instance FromJSON SomeMethod where
  parseJSON :: Value -> Parser SomeMethod
parseJSON Value
v = do
    [Char]
s <- forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Char] -> SomeMethod
methodStringToSomeMethod [Char]
s

deriving via ViaJSON SomeMethod instance Pretty SomeMethod

---------------
-- SMethod
---------------

-- This instance is written manually rather than derived to avoid a dependency
-- on 'dependent-sum-template'.
instance GEq SMethod where
  geq :: forall (a :: Method f t) (b :: Method f t).
SMethod a -> SMethod b -> Maybe (a :~: b)
geq SMethod a
x SMethod b
y = case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare SMethod a
x SMethod b
y of
    GOrdering a b
GLT -> forall a. Maybe a
Nothing
    GOrdering a b
GEQ -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    GOrdering a b
GGT -> forall a. Maybe a
Nothing

-- This instance is written manually rather than derived to avoid a dependency
-- on 'dependent-sum-template'.
instance GCompare SMethod where
  gcompare :: forall (a :: Method f t) (b :: Method f t).
SMethod a -> SMethod b -> GOrdering a b
gcompare (SMethod_CustomMethod Proxy s
x) (SMethod_CustomMethod Proxy s
y) = case forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal Proxy s
x forall a. Ord a => a -> a -> Ordering
`compare` forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal Proxy s
y of
    Ordering
LT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> forall a b. a -> b
unsafeCoerce forall {k} (a :: k). GOrdering a a
GEQ
    Ordering
GT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  -- This is much more compact than matching on every pair of constructors, which
  -- is what we would need to do for GHC to 'see' that this is correct. Nonetheless
  -- it is safe: since there is only one constructor of 'SMethod' for each 'Method',
  -- the argument types can only be equal if the constructor tag is equal.
  gcompare SMethod a
x SMethod b
y = case Int# -> Int
I# (forall a. a -> Int#
dataToTag# SMethod a
x) forall a. Ord a => a -> a -> Ordering
`compare` Int# -> Int
I# (forall a. a -> Int#
dataToTag# SMethod b
y) of
    Ordering
LT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> forall a b. a -> b
unsafeCoerce forall {k} (a :: k). GOrdering a a
GEQ
    Ordering
GT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT

instance Eq (SMethod m) where
  -- This defers to 'GEq', ensuring that this version is compatible.
  == :: SMethod m -> SMethod m -> Bool
(==) = forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance Ord (SMethod m) where
  -- This defers to 'GCompare', ensuring that this version is compatible.
  compare :: SMethod m -> SMethod m -> Ordering
compare = forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

deriving stock instance Show (SMethod m)

instance ToJSON (SMethod m) where
  toJSON :: SMethod m -> Value
toJSON SMethod m
m = forall a. ToJSON a => a -> Value
toJSON (forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> SomeMethod
SomeMethod SMethod m
m)

instance KnownSymbol s => FromJSON (SMethod ('Method_CustomMethod s :: Method f t)) where
  parseJSON :: Value -> Parser (SMethod ('Method_CustomMethod s))
parseJSON Value
v = do
    SomeMethod
sm <- forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case SomeMethod
sm of
      SomeMethod (SMethod_CustomMethod Proxy s
x) -> case forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol Proxy s
x (forall {k} (t :: k). Proxy t
Proxy :: Proxy s) of
        Just s :~: s
Refl -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {f :: MessageDirection} {t :: MessageKind} (s :: Symbol).
KnownSymbol s =>
Proxy s -> SMethod ('Method_CustomMethod s)
SMethod_CustomMethod Proxy s
x
        Maybe (s :~: s)
Nothing -> forall a. Monoid a => a
mempty
      SomeMethod
_ -> forall a. Monoid a => a
mempty

-- TODO: generate these with everything else?
-- Generates lots of instances like this in terms of the FromJSON SomeMethod instance
-- instance FromJSON (SMethod Method_X)
makeSingletonFromJSON 'SomeMethod ''SMethod ['SMethod_CustomMethod]

deriving via ViaJSON (SMethod m) instance Pretty (SMethod m)

---------------
-- Extras
---------------

-- Some useful type synonyms
type SClientMethod (m :: Method ClientToServer t) = SMethod m
type SServerMethod (m :: Method ServerToClient t) = SMethod m

data SomeClientMethod = forall t (m :: Method ClientToServer t). SomeClientMethod (SMethod m)
deriving stock instance Show SomeClientMethod

data SomeServerMethod = forall t (m :: Method ServerToClient t). SomeServerMethod (SMethod m)
deriving stock instance Show SomeServerMethod

someClientMethod :: SMethod m -> Maybe SomeClientMethod
someClientMethod :: forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> Maybe SomeClientMethod
someClientMethod SMethod m
s = case forall (f :: MessageDirection) (t :: MessageKind)
       (m :: Method f t).
SMethod m -> SMessageDirection f
messageDirection SMethod m
s of
  SMessageDirection f
SClientToServer -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: MessageKind) (m :: Method 'ClientToServer t).
SMethod m -> SomeClientMethod
SomeClientMethod SMethod m
s
  SMessageDirection f
SServerToClient -> forall a. Maybe a
Nothing
  -- See Note [Parsing methods that go both ways]
  SMessageDirection f
SBothDirections -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: MessageKind) (m :: Method 'ClientToServer t).
SMethod m -> SomeClientMethod
SomeClientMethod forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce SMethod m
s

someServerMethod :: SMethod m -> Maybe SomeServerMethod
someServerMethod :: forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> Maybe SomeServerMethod
someServerMethod SMethod m
s = case forall (f :: MessageDirection) (t :: MessageKind)
       (m :: Method f t).
SMethod m -> SMessageDirection f
messageDirection SMethod m
s of
  SMessageDirection f
SServerToClient -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: MessageKind) (m :: Method 'ServerToClient t).
SMethod m -> SomeServerMethod
SomeServerMethod SMethod m
s
  SMessageDirection f
SClientToServer -> forall a. Maybe a
Nothing
  -- See Note [Parsing methods that go both ways]
  SMessageDirection f
SBothDirections -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: MessageKind) (m :: Method 'ServerToClient t).
SMethod m -> SomeServerMethod
SomeServerMethod forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce SMethod m
s

instance FromJSON SomeClientMethod where
  parseJSON :: Value -> Parser SomeClientMethod
parseJSON Value
v = do
    (SomeMethod SMethod m
sm) <- forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> Maybe SomeClientMethod
someClientMethod SMethod m
sm of
      Just SomeClientMethod
scm -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeClientMethod
scm
      Maybe SomeClientMethod
Nothing -> forall a. Monoid a => a
mempty

instance ToJSON SomeClientMethod where
  toJSON :: SomeClientMethod -> Value
toJSON (SomeClientMethod SMethod m
sm) = forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ SomeMethod -> [Char]
someMethodToMethodString forall a b. (a -> b) -> a -> b
$ forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> SomeMethod
SomeMethod SMethod m
sm

deriving via ViaJSON SomeClientMethod instance Pretty SomeClientMethod

instance FromJSON SomeServerMethod where
  parseJSON :: Value -> Parser SomeServerMethod
parseJSON Value
v = do
    (SomeMethod SMethod m
sm) <- forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> Maybe SomeServerMethod
someServerMethod SMethod m
sm of
      Just SomeServerMethod
scm -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeServerMethod
scm
      Maybe SomeServerMethod
Nothing -> forall a. Monoid a => a
mempty

instance ToJSON SomeServerMethod where
  toJSON :: SomeServerMethod -> Value
toJSON (SomeServerMethod SMethod m
sm) = forall a. ToJSON a => a -> Value
toJSON forall a b. (a -> b) -> a -> b
$ SomeMethod -> [Char]
someMethodToMethodString forall a b. (a -> b) -> a -> b
$ forall {f :: MessageDirection} {t :: MessageKind}
       (m :: Method f t).
SMethod m -> SomeMethod
SomeMethod SMethod m
sm

deriving via ViaJSON SomeServerMethod instance Pretty SomeServerMethod

{- Note [Parsing methods that go both ways]

In order to parse a method as a client or server method, we use 'messageDirection'
to get a proof that the message direction is what we say it is. But this just doesn't
work for the both directions case: because we are awkwardly representing "both directions"
as "the type variable is free". So the types don't line up and we use an awful hack.

A better solution might be to move away from using an unconstrained type parameter to
mean "both directions".
-}