Skip to content

Commit c2f2d2f

Browse files
authored
Merge pull request #669 from jhrcek/jhrcek/minor-simplifications
Remove unnecessary pluginId setting and user Better Map functions in tactics plugin
2 parents 9a742e2 + 9c337a8 commit c2f2d2f

File tree

5 files changed

+6
-8
lines changed

5 files changed

+6
-8
lines changed

Diff for: plugins/default/src/Ide/Plugin/Eval.hs

+1-2
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,7 @@ import Type.Reflection (Typeable)
8585
descriptor :: PluginId -> PluginDescriptor
8686
descriptor plId =
8787
(defaultPluginDescriptor plId)
88-
{ pluginId = plId,
89-
pluginCodeLensProvider = Just provider,
88+
{ pluginCodeLensProvider = Just provider,
9089
pluginCommands = [evalCommand]
9190
}
9291

Diff for: plugins/default/src/Ide/Plugin/ModuleName.hs

+1-2
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,7 @@ import System.FilePath (
9595
descriptor :: PluginId -> PluginDescriptor
9696
descriptor plId =
9797
(defaultPluginDescriptor plId)
98-
{ pluginId = plId
99-
, pluginCodeLensProvider = Just codeLens
98+
{ pluginCodeLensProvider = Just codeLens
10099
, pluginCommands = [PluginCommand editCommandName editCommandName command]
101100
}
102101

Diff for: plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

+2-2
Original file line numberDiff line numberDiff line change
@@ -154,9 +154,9 @@ destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
154154
destruct' f term jdg = do
155155
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
156156
let hy = jHypothesis jdg
157-
case find ((== term) . fst) $ toList hy of
157+
case M.lookup term hy of
158158
Nothing -> throwError $ UndefinedHypothesis term
159-
Just (_, hi_type -> t) -> do
159+
Just (hi_type -> t) -> do
160160
useOccName jdg term
161161
(tr, ms)
162162
<- destructMatches

Diff for: plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,7 @@ filterSameTypeFromOtherPositions dcon pos jdg =
211211
(findDconPositionVals jdg dcon pos)
212212
(WrongBranch pos)
213213
jdg
214-
tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy
214+
tys = S.fromList $ hi_type <$> M.elems hy
215215
to_remove =
216216
M.filter (flip S.member tys . hi_type) (jHypothesis jdg)
217217
M.\\ hy

Diff for: plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
110110
in case isPatternMatch $ hi_provenance hi of
111111
True ->
112112
pruning subtactic $ \jdgs ->
113-
let getHyTypes = S.fromList . fmap (hi_type . snd) . M.toList . jHypothesis
113+
let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis
114114
new_hy = foldMap getHyTypes jdgs
115115
old_hy = getHyTypes jdg
116116
in case S.null $ new_hy S.\\ old_hy of

0 commit comments

Comments
 (0)