forked from haskell/haskell-language-server
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Types.hs
477 lines (390 loc) · 15.8 KB
/
Types.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Ide.Plugin.Tactic.Types
( module Ide.Plugin.Tactic.Types
, module Ide.Plugin.Tactic.Debug
, OccName
, Name
, Type
, TyVar
, Span
, Range
) where
import Control.Lens hiding (Context, (.=))
import Control.Monad.Reader
import Control.Monad.State
import Data.Aeson
import Data.Coerce
import Data.Function
import Data.Generics.Product (field)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (fromMaybe)
import Data.Semigroup
import Data.Set (Set)
import qualified Data.Text as T
import Data.Text (Text)
import Data.Tree
import Development.IDE.GHC.Compat hiding (Node)
import Development.IDE.GHC.Orphans ()
import Development.IDE.Types.Location
import GHC.Generics
import GHC.SourceGen (var)
import Ide.Plugin.Tactic.Debug
import Ide.Plugin.Tactic.FeatureSet
import OccName
import Refinery.Tactic
import System.IO.Unsafe (unsafePerformIO)
import Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst)
import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
------------------------------------------------------------------------------
-- | The list of tactics exposed to the outside world. These are attached to
-- actual tactics via 'commandTactic' and are contextually provided to the
-- editor via 'commandProvider'.
data TacticCommand
= Auto
| Intros
| Destruct
| Homomorphism
| DestructLambdaCase
| HomomorphismLambdaCase
| DestructAll
| UseDataCon
| Refine
deriving (Eq, Ord, Show, Enum, Bounded)
-- | Generate a title for the command.
tacticTitle :: TacticCommand -> T.Text -> T.Text
tacticTitle Auto _ = "Attempt to fill hole"
tacticTitle Intros _ = "Introduce lambda"
tacticTitle Destruct var = "Case split on " <> var
tacticTitle Homomorphism var = "Homomorphic case split on " <> var
tacticTitle DestructLambdaCase _ = "Lambda case split"
tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
tacticTitle DestructAll _ = "Split all function arguments"
tacticTitle UseDataCon dcon = "Use constructor " <> dcon
tacticTitle Refine _ = "Refine hole"
------------------------------------------------------------------------------
-- | Plugin configuration for tactics
data Config = Config
{ cfg_feature_set :: FeatureSet
, cfg_max_use_ctor_actions :: Int
}
emptyConfig :: Config
emptyConfig = Config defaultFeatures 5
instance ToJSON Config where
toJSON Config{..} = object
[ "features" .= prettyFeatureSet cfg_feature_set
, "max_use_ctor_actions" .= cfg_max_use_ctor_actions
]
instance FromJSON Config where
parseJSON = withObject "Config" $ \obj -> do
cfg_feature_set <-
parseFeatureSet . fromMaybe "" <$> obj .:? "features"
cfg_max_use_ctor_actions <-
fromMaybe 5 <$> obj .:? "max_use_ctor_actions"
pure $ Config{..}
------------------------------------------------------------------------------
-- | A wrapper around 'Type' which supports equality and ordering.
newtype CType = CType { unCType :: Type }
instance Eq CType where
(==) = eqType `on` unCType
instance Ord CType where
compare = nonDetCmpType `on` unCType
instance Show CType where
show = unsafeRender . unCType
instance Show OccName where
show = unsafeRender
instance Show Name where
show = unsafeRender
instance Show Type where
show = unsafeRender
instance Show Var where
show = unsafeRender
instance Show TCvSubst where
show = unsafeRender
instance Show DataCon where
show = unsafeRender
instance Show Class where
show = unsafeRender
instance Show (HsExpr GhcPs) where
show = unsafeRender
instance Show (Pat GhcPs) where
show = unsafeRender
instance Show (LHsSigType GhcPs) where
show = unsafeRender
------------------------------------------------------------------------------
-- | The state that should be shared between subgoals. Extracts move towards
-- the root, judgments move towards the leaves, and the state moves *sideways*.
data TacticState = TacticState
{ ts_skolems :: !(Set TyVar)
-- ^ The known skolems.
, ts_unifier :: !TCvSubst
, ts_unique_gen :: !UniqSupply
} deriving stock (Show, Generic)
instance Show UniqSupply where
show _ = "<uniqsupply>"
------------------------------------------------------------------------------
-- | A 'UniqSupply' to use in 'defaultTacticState'
unsafeDefaultUniqueSupply :: UniqSupply
unsafeDefaultUniqueSupply =
unsafePerformIO $ mkSplitUniqSupply '🚒'
{-# NOINLINE unsafeDefaultUniqueSupply #-}
defaultTacticState :: TacticState
defaultTacticState =
TacticState
{ ts_skolems = mempty
, ts_unifier = emptyTCvSubst
, ts_unique_gen = unsafeDefaultUniqueSupply
}
------------------------------------------------------------------------------
-- | Generate a new 'Unique'
freshUnique :: MonadState TacticState m => m Unique
freshUnique = do
(uniq, supply) <- gets $ takeUniqFromSupply . ts_unique_gen
modify' $! field @"ts_unique_gen" .~ supply
pure uniq
------------------------------------------------------------------------------
-- | Describes where hypotheses came from. Used extensively to prune stupid
-- solutions from the search space.
data Provenance
= -- | An argument given to the topmost function that contains the current
-- hole. Recursive calls are restricted to values whose provenance lines up
-- with the same argument.
TopLevelArgPrv
OccName -- ^ Binding function
Int -- ^ Argument Position
Int -- ^ of how many arguments total?
-- | A binding created in a pattern match.
| PatternMatchPrv PatVal
-- | A class method from the given context.
| ClassMethodPrv
(Uniquely Class) -- ^ Class
-- | A binding explicitly written by the user.
| UserPrv
-- | The recursive hypothesis. Present only in the context of the recursion
-- tactic.
| RecursivePrv
-- | A hypothesis which has been disallowed for some reason. It's important
-- to keep these in the hypothesis set, rather than filtering it, in order
-- to continue tracking downstream provenance.
| DisallowedPrv DisallowReason Provenance
deriving stock (Eq, Show, Generic, Ord)
------------------------------------------------------------------------------
-- | Why was a hypothesis disallowed?
data DisallowReason
= WrongBranch Int
| Shadowed
| RecursiveCall
| AlreadyDestructed
deriving stock (Eq, Show, Generic, Ord)
------------------------------------------------------------------------------
-- | Provenance of a pattern value.
data PatVal = PatVal
{ pv_scrutinee :: Maybe OccName
-- ^ Original scrutinee which created this PatVal. Nothing, for lambda
-- case.
, pv_ancestry :: Set OccName
-- ^ The set of values which had to be destructed to discover this term.
-- Always contains the scrutinee.
, pv_datacon :: Uniquely DataCon
-- ^ The datacon which introduced this term.
, pv_position :: Int
-- ^ The position of this binding in the datacon's arguments.
} deriving stock (Eq, Show, Generic, Ord)
------------------------------------------------------------------------------
-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord'
-- instances.
newtype Uniquely a = Uniquely { getViaUnique :: a }
deriving Show via a
instance Uniquable a => Eq (Uniquely a) where
(==) = (==) `on` getUnique . getViaUnique
instance Uniquable a => Ord (Uniquely a) where
compare = nonDetCmpUnique `on` getUnique . getViaUnique
newtype Hypothesis a = Hypothesis
{ unHypothesis :: [HyInfo a]
}
deriving stock (Functor, Eq, Show, Generic, Ord)
deriving newtype (Semigroup, Monoid)
------------------------------------------------------------------------------
-- | The provenance and type of a hypothesis term.
data HyInfo a = HyInfo
{ hi_name :: OccName
, hi_provenance :: Provenance
, hi_type :: a
}
deriving stock (Functor, Eq, Show, Generic, Ord)
------------------------------------------------------------------------------
-- | Map a function over the provenance.
overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance f (HyInfo name prv ty) = HyInfo name (f prv) ty
------------------------------------------------------------------------------
-- | The current bindings and goal for a hole to be filled by refinery.
data Judgement' a = Judgement
{ _jHypothesis :: !(Hypothesis a)
, _jBlacklistDestruct :: !Bool
, _jWhitelistSplit :: !Bool
, _jIsTopHole :: !Bool
, _jGoal :: !a
}
deriving stock (Eq, Generic, Functor, Show)
type Judgement = Judgement' CType
newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
deriving (Functor, Applicative, Monad, MonadReader Context)
------------------------------------------------------------------------------
-- | Orphan instance for producing holes when attempting to solve tactics.
instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where
hole = pure . pure . noLoc $ var "_"
------------------------------------------------------------------------------
-- | Reasons a tactic might fail.
data TacticError
= UndefinedHypothesis OccName
| GoalMismatch String CType
| UnsolvedSubgoals [Judgement]
| UnificationError CType CType
| NoProgress
| NoApplicableTactic
| IncorrectDataCon DataCon
| RecursionOnWrongParam OccName Int OccName
| UnhelpfulDestruct OccName
| UnhelpfulSplit OccName
| TooPolymorphic
| NotInScope OccName
deriving stock (Eq)
instance Show TacticError where
show (UndefinedHypothesis name) =
occNameString name <> " is not available in the hypothesis."
show (GoalMismatch tac (CType typ)) =
mconcat
[ "The tactic "
, tac
, " doesn't apply to goal type "
, unsafeRender typ
]
show (UnsolvedSubgoals _) =
"There were unsolved subgoals"
show (UnificationError (CType t1) (CType t2)) =
mconcat
[ "Could not unify "
, unsafeRender t1
, " and "
, unsafeRender t2
]
show NoProgress =
"Unable to make progress"
show NoApplicableTactic =
"No tactic could be applied"
show (IncorrectDataCon dcon) =
"Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"
show (RecursionOnWrongParam call p arg) =
"Recursion on wrong param (" <> show call <> ") on arg"
<> show p <> ": " <> show arg
show (UnhelpfulDestruct n) =
"Destructing patval " <> show n <> " leads to no new types"
show (UnhelpfulSplit n) =
"Splitting constructor " <> show n <> " leads to no new goals"
show TooPolymorphic =
"The tactic isn't applicable because the goal is too polymorphic"
show (NotInScope name) =
"Tried to do something with the out of scope name " <> show name
------------------------------------------------------------------------------
type TacticsM = TacticT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
type RuleM = RuleT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
type Rule = RuleM (Synthesized (LHsExpr GhcPs))
type Trace = Rose String
------------------------------------------------------------------------------
-- | The extract for refinery. Represents a "synthesized attribute" in the
-- context of attribute grammars. In essence, 'Synthesized' describes
-- information we'd like to pass from leaves of the tactics search upwards.
-- This includes the actual AST we've generated (in 'syn_val').
data Synthesized a = Synthesized
{ syn_trace :: Trace
-- ^ A tree describing which tactics were used produce the 'syn_val'.
-- Mainly for debugging when you get the wrong answer, to see the other
-- things it tried.
, syn_scoped :: Hypothesis CType
-- ^ All of the bindings created to produce the 'syn_val'.
, syn_used_vals :: Set OccName
-- ^ The values used when synthesizing the 'syn_val'.
, syn_recursion_count :: Sum Int
-- ^ The number of recursive calls
, syn_val :: a
}
deriving (Eq, Show, Functor, Foldable, Traversable, Generic)
mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a
mapTrace f (Synthesized tr sc uv rc a) = Synthesized (f tr) sc uv rc a
------------------------------------------------------------------------------
-- | This might not be lawful, due to the semigroup on 'Trace' maybe not being
-- lawful. But that's only for debug output, so it's not anything I'm concerned
-- about.
instance Applicative Synthesized where
pure = Synthesized mempty mempty mempty mempty
Synthesized tr1 sc1 uv1 rc1 f <*> Synthesized tr2 sc2 uv2 rc2 a =
Synthesized (tr1 <> tr2) (sc1 <> sc2) (uv1 <> uv2) (rc1 <> rc2) $ f a
------------------------------------------------------------------------------
-- | The Reader context of tactics and rules
data Context = Context
{ ctxDefiningFuncs :: [(OccName, CType)]
-- ^ The functions currently being defined
, ctxModuleFuncs :: [(OccName, CType)]
-- ^ Everything defined in the current module
, ctxFeatureSet :: FeatureSet
}
deriving stock (Eq, Ord, Show)
------------------------------------------------------------------------------
-- | An empty context
emptyContext :: Context
emptyContext = Context mempty mempty mempty
newtype Rose a = Rose (Tree a)
deriving stock (Eq, Functor, Generic)
instance Show (Rose String) where
show = unlines . dropEveryOther . lines . drawTree . coerce
dropEveryOther :: [a] -> [a]
dropEveryOther [] = []
dropEveryOther [a] = [a]
dropEveryOther (a : _ : as) = a : dropEveryOther as
------------------------------------------------------------------------------
-- | This might not be lawful! I didn't check, and it feels sketchy.
instance (Eq a, Monoid a) => Semigroup (Rose a) where
Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)
sconcat (a :| as) = rose mempty $ a : as
instance (Eq a, Monoid a) => Monoid (Rose a) where
mempty = Rose $ Node mempty mempty
rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs
rose a rs = Rose $ Node a $ coerce rs
------------------------------------------------------------------------------
-- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic'
data RunTacticResults = RunTacticResults
{ rtr_trace :: Trace
, rtr_extract :: LHsExpr GhcPs
, rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
, rtr_jdg :: Judgement
, rtr_ctx :: Context
} deriving Show
data AgdaMatch = AgdaMatch
{ amPats :: [Pat GhcPs]
, amBody :: HsExpr GhcPs
}
deriving (Show)
data UserFacingMessage
= TacticErrors
| TimedOut
| NothingToDo
| InfrastructureError Text
deriving Eq
instance Show UserFacingMessage where
show TacticErrors = "Wingman couldn't find a solution"
show TimedOut = "Wingman timed out while trying to find a solution"
show NothingToDo = "Nothing to do"
show (InfrastructureError t) = "Internal error: " <> T.unpack t