{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

-- | A plugin that uses tactics to synthesize code
module Wingman.Plugin where

import           Control.Monad
import           Development.IDE.Core.Shake (IdeState (..))
import           Ide.Types
import           Language.LSP.Types
import           Prelude hiding (span)
import           Wingman.AbstractLSP
import           Wingman.AbstractLSP.TacticActions (makeTacticInteraction)
import           Wingman.EmptyCase
import           Wingman.LanguageServer
import           Wingman.LanguageServer.Metaprogram (hoverProvider)
import           Wingman.StaticPlugin


descriptor :: PluginId -> PluginDescriptor IdeState
descriptor :: PluginId -> PluginDescriptor IdeState
descriptor PluginId
plId
  = [Interaction]
-> PluginDescriptor IdeState -> PluginDescriptor IdeState
installInteractions
      ( Interaction
emptyCaseInteraction
      Interaction -> [Interaction] -> [Interaction]
forall a. a -> [a] -> [a]
: (TacticCommand -> Interaction) -> [TacticCommand] -> [Interaction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TacticCommand -> Interaction
makeTacticInteraction [TacticCommand
forall a. Bounded a => a
minBound .. TacticCommand
forall a. Bounded a => a
maxBound]
      )
  (PluginDescriptor IdeState -> PluginDescriptor IdeState)
-> PluginDescriptor IdeState -> PluginDescriptor IdeState
forall a b. (a -> b) -> a -> b
$ (PluginId -> PluginDescriptor IdeState
forall ideState. PluginId -> PluginDescriptor ideState
defaultPluginDescriptor PluginId
plId)
      { pluginHandlers :: PluginHandlers IdeState
pluginHandlers = SClientMethod 'TextDocumentHover
-> PluginMethodHandler IdeState 'TextDocumentHover
-> PluginHandlers IdeState
forall (m :: Method 'FromClient 'Request) ideState.
PluginMethod m =>
SClientMethod m
-> PluginMethodHandler ideState m -> PluginHandlers ideState
mkPluginHandler SClientMethod 'TextDocumentHover
STextDocumentHover PluginMethodHandler IdeState 'TextDocumentHover
hoverProvider
      , pluginRules :: Rules ()
pluginRules = PluginId -> Rules ()
wingmanRules PluginId
plId
      , pluginConfigDescriptor :: ConfigDescriptor
pluginConfigDescriptor =
          ConfigDescriptor
defaultConfigDescriptor
            { configCustomConfig :: CustomConfig
configCustomConfig = Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
-> CustomConfig
forall (r :: [PropertyKey]). Properties r -> CustomConfig
mkCustomConfig Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties
            }
      , pluginModifyDynflags :: DynFlagsModifications
pluginModifyDynflags = DynFlagsModifications
staticPlugin
      }