Wingman idioms (#2607)

* Allow idiom brackets

* Allow record construction idioms

* expected result

* Fix noExtField

Author: isovector

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.  

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
+

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.

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 =

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
+

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"
 

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
+

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) |]
+

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
+

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) |]
+