-
-
Notifications
You must be signed in to change notification settings - Fork 347
/
CodeGen.hs
191 lines (168 loc) · 6.42 KB
/
CodeGen.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
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
module Ide.Plugin.Tactic.CodeGen
( module Ide.Plugin.Tactic.CodeGen
, module Ide.Plugin.Tactic.CodeGen.Utils
) where
import Control.Lens ((+~))
import Control.Monad.Except
import Data.Generics.Product (field)
import Data.List
import qualified Data.Set as S
import Data.Traversable
import DataCon
import Development.IDE.GHC.Compat
import GHC.Exts
import GHC.SourceGen.Binds
import GHC.SourceGen.Expr
import GHC.SourceGen.Overloaded
import GHC.SourceGen.Pat
import Ide.Plugin.Tactic.CodeGen.Utils
import Ide.Plugin.Tactic.GHC
import Ide.Plugin.Tactic.Judgements
import Ide.Plugin.Tactic.Machinery
import Ide.Plugin.Tactic.Naming
import Ide.Plugin.Tactic.Types
import Type hiding (Var)
------------------------------------------------------------------------------
-- | Doing recursion incurs a small penalty in the score.
countRecursiveCall :: TacticState -> TacticState
countRecursiveCall = field @"ts_recursion_count" +~ 1
destructMatches
:: (DataCon -> Judgement -> Rule)
-- ^ How to construct each match
-> Maybe OccName
-- ^ Scrutinee
-> CType
-- ^ Type being destructed
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches f scrut t jdg = do
let hy = jEntireHypothesis jdg
g = jGoal jdg
case splitTyConApp_maybe $ unCType t of
Nothing -> throwError $ GoalMismatch "destruct" g
Just (tc, apps) -> do
let dcs = tyConDataCons tc
case dcs of
[] -> throwError $ GoalMismatch "destruct" g
_ -> fmap unzipTrace $ for dcs $ \dc -> do
let args = dataConInstOrigArgTys' dc apps
names <- mkManyGoodNames (hyNamesInScope hy) args
let hy' = patternHypothesis scrut dc jdg
$ zip names
$ coerce args
j = introduce hy'
$ withNewGoal g jdg
Synthesized tr sc uv sg <- f dc j
pure
$ Synthesized
( rose ("match " <> show dc <> " {" <>
intercalate ", " (fmap show names) <> "}")
$ pure tr)
(sc <> hy')
uv
$ match [mkDestructPat dc names]
$ unLoc sg
------------------------------------------------------------------------------
-- | Produces a pattern for a data con and the names of its fields.
mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs
mkDestructPat dcon names
| isTupleDataCon dcon =
tuple pat_args
| otherwise =
infixifyPatIfNecessary dcon $
conP
(coerceName $ dataConName dcon)
pat_args
where
pat_args = fmap bvar' names
infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary dcon x
| dataConIsInfix dcon =
case x of
ConPatIn op (PrefixCon [lhs, rhs]) ->
ConPatIn op $ InfixCon lhs rhs
y -> y
| otherwise = x
unzipTrace :: [Synthesized a] -> Synthesized [a]
unzipTrace = sequenceA
-- | Essentially same as 'dataConInstOrigArgTys' in GHC,
-- but only accepts universally quantified types as the second arguments
-- and automatically introduces existentials.
--
-- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'.
-- We need some tweaks if the compiler changes the implementation.
dataConInstOrigArgTys'
:: DataCon
-- ^ 'DataCon'structor
-> [Type]
-- ^ /Universally/ quantified type arguments to a result type.
-- It /MUST NOT/ contain any dictionaries, coercion and existentials.
--
-- For example, for @MkMyGADT :: b -> MyGADT a c@, we
-- must pass @[a, c]@ as this argument but not @b@, as @b@ is an existential.
-> [Type]
-- ^ Types of arguments to the DataCon with returned type is instantiated with the second argument.
dataConInstOrigArgTys' con uniTys =
let exvars = dataConExTys con
in dataConInstOrigArgTys con $
uniTys ++ fmap mkTyVarTy exvars
-- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys'
-- unifies the second argument with DataCon's universals followed by existentials.
-- If the definition of 'dataConInstOrigArgTys' changes,
-- this place must be changed accordingly.
------------------------------------------------------------------------------
-- | Combinator for performing case splitting, and running sub-rules on the
-- resulting matches.
destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destruct' f hi jdg = do
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
let term = hi_name hi
Synthesized tr sc uv ms
<- destructMatches
f
(Just term)
(hi_type hi)
$ disallowing AlreadyDestructed [term] jdg
pure
$ Synthesized
(rose ("destruct " <> show term) $ pure tr)
sc
(S.insert term uv)
$ noLoc
$ case' (var' term) ms
------------------------------------------------------------------------------
-- | Combinator for performign case splitting, and running sub-rules on the
-- resulting matches.
destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' f jdg = do
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
let g = jGoal jdg
case splitFunTy_maybe (unCType g) of
Just (arg, _) | isAlgType arg ->
fmap (fmap noLoc lambdaCase) <$>
destructMatches f Nothing (CType arg) jdg
_ -> throwError $ GoalMismatch "destructLambdaCase'" g
------------------------------------------------------------------------------
-- | Construct a data con with subgoals for each field.
buildDataCon
:: Judgement
-> DataCon -- ^ The data con to build
-> [Type] -- ^ Type arguments for the data con
-> RuleM (Synthesized (LHsExpr GhcPs))
buildDataCon jdg dc tyapps = do
let args = dataConInstOrigArgTys' dc tyapps
Synthesized tr sc uv sgs
<- fmap unzipTrace
$ traverse ( \(arg, n) ->
newSubgoal
. filterSameTypeFromOtherPositions dc n
. blacklistingDestruct
. flip withNewGoal jdg
$ CType arg
) $ zip args [0..]
pure
$ Synthesized (rose (show dc) $ pure tr) sc uv
$ mkCon dc sgs