Skip to content

Commit 9c337a8

Browse files
committed
User more suitable Map functions in tactics plugin
1 parent 091cf2c commit 9c337a8

File tree

3 files changed

+4
-4
lines changed

3 files changed

+4
-4
lines changed

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)