diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md index 6a1c00b561..d2c158925f 100644 --- a/plugins/hls-tactics-plugin/COMMANDS.md +++ b/plugins/hls-tactics-plugin/COMMANDS.md @@ -310,6 +310,30 @@ case e of Right b -> Right (_ :: y) ``` +## idiom + +arguments: tactic. +deterministic. + +> Lift a tactic into idiom brackets. + + +### Example + +Given: + +```haskell +f :: a -> b -> Int + +_ :: Maybe Int +``` + +running `idiom (apply f)` will produce: + +```haskell +f <$> (_ :: Maybe a) <*> (_ :: Maybe b) +``` + ## intro arguments: single binding. diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 3b143d96ae..bda08c539b 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -331,3 +331,16 @@ nonrecLet occjdgs jdg = do (zip (fmap fst occjdgs) occexts) <*> fmap unLoc ext + +------------------------------------------------------------------------------ +-- | Converts a function application into applicative form +idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs +idiomize x = noLoc $ case unLoc x of + HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 -> + op (bvar' $ occName x) "<$>" (unLoc gshgp3) + HsApp _ gsigp gshgp3 -> + op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3) + RecordCon _ con flds -> + unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar noExtField con) $ fmap unLoc flds + y -> y + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index 0c12e5f7c4..7e4696376d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -66,6 +66,12 @@ isSplitWhitelisted = _jWhitelistSplit withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t +------------------------------------------------------------------------------ +-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing +-- it. +withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a +withModifiedGoal f = field @"_jGoal" %~ f + ------------------------------------------------------------------------------ -- | Add some new type equalities to the local judgement. diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 676c829d22..a1d4eca4d4 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -98,6 +98,17 @@ commands = "\\x y z -> (_ :: d)" ] + , command "idiom" Deterministic Tactic + "Lift a tactic into idiom brackets." + (pure . idiom) + [ Example + Nothing + ["(apply f)"] + [EHI "f" "a -> b -> Int"] + (Just "Maybe Int") + "f <$> (_ :: Maybe a) <*> (_ :: Maybe b)" + ] + , command "intro" Deterministic (Bind One) "Construct a lambda expression, binding an argument with the given name." (pure . intros' . IntroduceOnlyNamed . pure) @@ -415,7 +426,7 @@ oneTactic = tactic :: Parser (TacticsM ()) -tactic = P.makeExprParser oneTactic operators +tactic = P.makeExprParser oneTactic operators operators :: [[P.Operator Parser (TacticsM ())]] operators = diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 6e27b05cd4..b063962760 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -9,9 +9,10 @@ module Wingman.Tactics import Control.Applicative (Alternative(empty), (<|>)) import Control.Lens ((&), (%~), (<>~)) import Control.Monad (filterM, unless) +import Control.Monad (when) import Control.Monad.Extra (anyM) import Control.Monad.Reader.Class (MonadReader (ask)) -import Control.Monad.State.Strict (StateT(..), runStateT) +import Control.Monad.State.Strict (StateT(..), runStateT, execStateT) import Data.Bool (bool) import Data.Foldable import Data.Functor ((<&>)) @@ -640,3 +641,51 @@ hyDiff m = do g' <- unHypothesis . jEntireHypothesis <$> goal pure $ Hypothesis $ take (length g' - g_len) g' + +------------------------------------------------------------------------------ +-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if +-- the current goal is +-- +-- (_ :: [r]) +-- +-- then @idiom apply@ will remove the applicative context, resulting in a hole: +-- +-- (_ :: r) +-- +-- and then use @apply@ to solve it. Let's say this results in: +-- +-- (f (_ :: a) (_ :: b)) +-- +-- Finally, @idiom@ lifts this back into the original applicative: +-- +-- (f <$> (_ :: [a]) <*> (_ :: [b])) +-- +-- Idiom will fail fast if the current goal doesn't have an applicative +-- instance. +idiom :: TacticsM () -> TacticsM () +idiom m = do + jdg <- goal + let hole = unCType $ jGoal jdg + when (isFunction hole) $ + failure $ GoalMismatch "idiom" $ jGoal jdg + case splitAppTy_maybe hole of + Just (applic, ty) -> do + minst <- getKnownInstance (mkClsOcc "Applicative") + . pure + $ applic + case minst of + Nothing -> failure $ GoalMismatch "idiom" $ CType applic + Just (_, _) -> do + rule $ \jdg -> do + expr <- subgoalWith (withNewGoal (CType ty) jdg) m + case unLoc $ syn_val expr of + HsApp{} -> pure $ fmap idiomize expr + RecordCon{} -> pure $ fmap idiomize expr + _ -> unsolvable $ GoalMismatch "idiom" $ jGoal jdg + rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType) + Nothing -> + failure $ GoalMismatch "idiom" $ jGoal jdg + +subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs)) +subgoalWith jdg t = RuleT $ flip execStateT jdg $ unTacticT t + diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 2fdf6a8936..a641da410b 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -40,6 +40,8 @@ spec = do metaTest 7 53 "MetaDeepOf" metaTest 2 34 "MetaWithArg" metaTest 2 18 "MetaLetSimple" + metaTest 5 9 "MetaIdiom" + metaTest 7 9 "MetaIdiomRecord" metaTest 2 12 "IntrosTooMany" diff --git a/plugins/hls-tactics-plugin/test/golden/MetaIdiom.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaIdiom.expected.hs new file mode 100644 index 0000000000..21569c7c19 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaIdiom.expected.hs @@ -0,0 +1,6 @@ +foo :: Int -> Int -> Int +foo = undefined + +test :: Maybe Int +test = (foo <$> _w0) <*> _w1 + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaIdiom.hs b/plugins/hls-tactics-plugin/test/golden/MetaIdiom.hs new file mode 100644 index 0000000000..f9506cb03b --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaIdiom.hs @@ -0,0 +1,6 @@ +foo :: Int -> Int -> Int +foo = undefined + +test :: Maybe Int +test = [wingman| idiom (use foo) |] + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.expected.hs new file mode 100644 index 0000000000..e39e9a9fab --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.expected.hs @@ -0,0 +1,8 @@ +data Rec = Rec + { a :: Int + , b :: Bool + } + +test :: Maybe Rec +test = (Rec <$> _w0) <*> _w1 + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.hs b/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.hs new file mode 100644 index 0000000000..87397da160 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.hs @@ -0,0 +1,8 @@ +data Rec = Rec + { a :: Int + , b :: Bool + } + +test :: Maybe Rec +test = [wingman| idiom (ctor Rec) |] +