8
8
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
9
9
{-# LANGUAGE MultiParamTypeClasses #-}
10
10
{-# LANGUAGE OverloadedStrings #-}
11
+ {-# LANGUAGE RecordWildCards #-}
11
12
{-# LANGUAGE TypeApplications #-}
13
+
12
14
{-# OPTIONS_GHC -fno-warn-orphans #-}
13
15
14
16
module Ide.Plugin.Tactic.Types
@@ -22,29 +24,88 @@ module Ide.Plugin.Tactic.Types
22
24
, Range
23
25
) where
24
26
25
- import Control.Lens hiding (Context , (.=) )
26
- import Control.Monad.Reader
27
- import Control.Monad.State
28
- import Data.Coerce
29
- import Data.Function
30
- import Data.Generics.Product (field )
31
- import Data.List.NonEmpty (NonEmpty (.. ))
32
- import Data.Semigroup
33
- import Data.Set (Set )
34
- import Data.Tree
35
- import Development.IDE.GHC.Compat hiding (Node )
36
- import Development.IDE.GHC.Orphans ()
37
- import Development.IDE.Types.Location
38
- import GHC.Generics
39
- import GHC.SourceGen (var )
40
- import Ide.Plugin.Tactic.Debug
41
- import Ide.Plugin.Tactic.FeatureSet (FeatureSet )
42
- import OccName
43
- import Refinery.Tactic
44
- import System.IO.Unsafe (unsafePerformIO )
45
- import Type (TCvSubst , Var , eqType , nonDetCmpType , emptyTCvSubst )
46
- import UniqSupply (takeUniqFromSupply , mkSplitUniqSupply , UniqSupply )
47
- import Unique (nonDetCmpUnique , Uniquable , getUnique , Unique )
27
+ import Control.Lens hiding (Context , (.=) )
28
+ import Control.Monad.Reader
29
+ import Control.Monad.State
30
+ import Data.Aeson
31
+ import Data.Coerce
32
+ import Data.Function
33
+ import Data.Generics.Product (field )
34
+ import Data.List.NonEmpty (NonEmpty (.. ))
35
+ import Data.Maybe (fromMaybe )
36
+ import Data.Semigroup
37
+ import Data.Set (Set )
38
+ import qualified Data.Text as T
39
+ import Data.Tree
40
+ import Development.IDE.GHC.Compat hiding (Node )
41
+ import Development.IDE.GHC.Orphans ()
42
+ import Development.IDE.Types.Location
43
+ import GHC.Generics
44
+ import GHC.SourceGen (var )
45
+ import Ide.Plugin.Tactic.Debug
46
+ import Ide.Plugin.Tactic.FeatureSet
47
+ import Ide.Plugin.Tactic.FeatureSet (FeatureSet )
48
+ import OccName
49
+ import Refinery.Tactic
50
+ import System.IO.Unsafe (unsafePerformIO )
51
+ import Type (TCvSubst , Var , eqType , nonDetCmpType , emptyTCvSubst )
52
+ import UniqSupply (takeUniqFromSupply , mkSplitUniqSupply , UniqSupply )
53
+ import Unique (nonDetCmpUnique , Uniquable , getUnique , Unique )
54
+
55
+
56
+ ------------------------------------------------------------------------------
57
+ -- | The list of tactics exposed to the outside world. These are attached to
58
+ -- actual tactics via 'commandTactic' and are contextually provided to the
59
+ -- editor via 'commandProvider'.
60
+ data TacticCommand
61
+ = Auto
62
+ | Intros
63
+ | Destruct
64
+ | Homomorphism
65
+ | DestructLambdaCase
66
+ | HomomorphismLambdaCase
67
+ | DestructAll
68
+ | UseDataCon
69
+ | Refine
70
+ deriving (Eq , Ord , Show , Enum , Bounded )
71
+
72
+ -- | Generate a title for the command.
73
+ tacticTitle :: TacticCommand -> T. Text -> T. Text
74
+ tacticTitle Auto _ = " Attempt to fill hole"
75
+ tacticTitle Intros _ = " Introduce lambda"
76
+ tacticTitle Destruct var = " Case split on " <> var
77
+ tacticTitle Homomorphism var = " Homomorphic case split on " <> var
78
+ tacticTitle DestructLambdaCase _ = " Lambda case split"
79
+ tacticTitle HomomorphismLambdaCase _ = " Homomorphic lambda case split"
80
+ tacticTitle DestructAll _ = " Split all function arguments"
81
+ tacticTitle UseDataCon dcon = " Use constructor " <> dcon
82
+ tacticTitle Refine _ = " Refine hole"
83
+
84
+
85
+ ------------------------------------------------------------------------------
86
+ -- | Plugin configuration for tactics
87
+ data Config = Config
88
+ { cfg_feature_set :: FeatureSet
89
+ , cfg_max_use_ctor_actions :: Int
90
+ }
91
+
92
+ emptyConfig :: Config
93
+ emptyConfig = Config defaultFeatures 5
94
+
95
+
96
+ instance ToJSON Config where
97
+ toJSON Config {.. } = object
98
+ [ " features" .= prettyFeatureSet cfg_feature_set
99
+ , " max_use_ctor_actions" .= cfg_max_use_ctor_actions
100
+ ]
101
+
102
+ instance FromJSON Config where
103
+ parseJSON = withObject " Config" $ \ obj -> do
104
+ cfg_feature_set <-
105
+ parseFeatureSet . fromMaybe " " <$> obj .:? " features"
106
+ cfg_max_use_ctor_actions <-
107
+ fromMaybe 5 <$> obj .:? " max_use_ctor_actions"
108
+ pure $ Config {.. }
48
109
49
110
50
111
------------------------------------------------------------------------------
0 commit comments