Skip to content

Remove unnecessary pluginId setting and user Better Map functions in tactics plugin #669

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Dec 13, 2020
Merged

Remove unnecessary pluginId setting and user Better Map functions in tactics plugin #669

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
091cf2c
Remove unnecessary pluginId setting
jhrcek Dec 13, 2020
9c337a8
User more suitable Map functions in tactics plugin
jhrcek Dec 13, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions plugins/default/src/Ide/Plugin/Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,7 @@ import Type.Reflection (Typeable)
descriptor :: PluginId -> PluginDescriptor
descriptor plId =
(defaultPluginDescriptor plId)
{ pluginId = plId,
pluginCodeLensProvider = Just provider,
{ pluginCodeLensProvider = Just provider,
pluginCommands = [evalCommand]
}

Expand Down
3 changes: 1 addition & 2 deletions plugins/default/src/Ide/Plugin/ModuleName.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,7 @@ import System.FilePath (
descriptor :: PluginId -> PluginDescriptor
descriptor plId =
(defaultPluginDescriptor plId)
{ pluginId = plId
, pluginCodeLensProvider = Just codeLens
{ pluginCodeLensProvider = Just codeLens
, pluginCommands = [PluginCommand editCommandName editCommandName command]
}

Expand Down
4 changes: 2 additions & 2 deletions plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,9 +154,9 @@ destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
destruct' f term jdg = do
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
let hy = jHypothesis jdg
case find ((== term) . fst) $ toList hy of
case M.lookup term hy of
Nothing -> throwError $ UndefinedHypothesis term
Just (_, hi_type -> t) -> do
Just (hi_type -> t) -> do
useOccName jdg term
(tr, ms)
<- destructMatches
Expand Down
2 changes: 1 addition & 1 deletion plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ filterSameTypeFromOtherPositions dcon pos jdg =
(findDconPositionVals jdg dcon pos)
(WrongBranch pos)
jdg
tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy
tys = S.fromList $ hi_type <$> M.elems hy
to_remove =
M.filter (flip S.member tys . hi_type) (jHypothesis jdg)
M.\\ hy
Expand Down
2 changes: 1 addition & 1 deletion plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
in case isPatternMatch $ hi_provenance hi of
True ->
pruning subtactic $ \jdgs ->
let getHyTypes = S.fromList . fmap (hi_type . snd) . M.toList . jHypothesis
let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis
new_hy = foldMap getHyTypes jdgs
old_hy = getHyTypes jdg
in case S.null $ new_hy S.\\ old_hy of
Expand Down