From 2a1f1b209674056e8045e3f6d578268c19480307 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 19 Jan 2022 12:24:47 -0800
Subject: [PATCH 1/4] Allow idiom brackets

---
 plugins/hls-tactics-plugin/COMMANDS.md        | 24 +++++++++
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 12 +++++
 .../src/Wingman/Judgements.hs                 |  6 +++
 .../src/Wingman/Metaprogramming/Parser.hs     | 13 ++++-
 .../hls-tactics-plugin/src/Wingman/Tactics.hs | 50 ++++++++++++++++++-
 .../test/CodeAction/RunMetaprogramSpec.hs     |  1 +
 .../test/golden/MetaIdiom.expected.hs         |  6 +++
 .../test/golden/MetaIdiom.hs                  |  6 +++
 8 files changed, 116 insertions(+), 2 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaIdiom.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaIdiom.hs

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..64e15acda6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -331,3 +331,15 @@ 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 ext con flds -> error "TODO sandy -- allow updates"
+  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..a3e43bf076 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,50 @@ 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
+              _       -> 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..5360373b09 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -40,6 +40,7 @@ spec = do
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
     metaTest  2 18 "MetaLetSimple"
+    metaTest  5  9 "MetaIdiom"
 
     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) |]
+

From 030d63f79dfee757ae0a86cd3bb93747e4c04daf Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 19 Jan 2022 12:48:21 -0800
Subject: [PATCH 2/4] Allow record construction idioms

---
 plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs         | 3 ++-
 plugins/hls-tactics-plugin/src/Wingman/Tactics.hs         | 3 ++-
 .../test/CodeAction/RunMetaprogramSpec.hs                 | 1 +
 plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.hs | 8 ++++++++
 4 files changed, 13 insertions(+), 2 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.hs

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 64e15acda6..ded76e0d22 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -340,6 +340,7 @@ idiomize x = noLoc $ case unLoc x of
     op (bvar' $ occName x) "<$>" (unLoc gshgp3)
   HsApp _ gsigp gshgp3 ->
     op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)
-  RecordCon ext con flds -> error "TODO sandy -- allow updates"
+  RecordCon _ con flds ->
+    unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar NoExtField con) $ fmap unLoc flds
   y -> y
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index a3e43bf076..b063962760 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -679,7 +679,8 @@ idiom m = do
           rule $ \jdg -> do
             expr <- subgoalWith (withNewGoal (CType ty) jdg) m
             case unLoc $ syn_val expr of
-              HsApp{} -> pure $ fmap idiomize expr
+              HsApp{}     -> pure $ fmap idiomize expr
+              RecordCon{} -> pure $ fmap idiomize expr
               _       -> unsolvable $ GoalMismatch "idiom" $ jGoal jdg
           rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType)
     Nothing ->
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index 5360373b09..a641da410b 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -41,6 +41,7 @@ spec = do
     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/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) |]
+

From c576a3798e056fbecead65e8b9fd3dc1b885a63d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 19 Jan 2022 12:53:05 -0800
Subject: [PATCH 3/4] expected result

---
 .../test/golden/MetaIdiomRecord.expected.hs               | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaIdiomRecord.expected.hs

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
+

From 0252ca0bcc1ada94ce3746146f6f5a0030099032 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 19 Jan 2022 13:30:39 -0800
Subject: [PATCH 4/4] Fix noExtField

---
 plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index ded76e0d22..bda08c539b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -341,6 +341,6 @@ idiomize x = noLoc $ case unLoc x of
   HsApp _ gsigp gshgp3 ->
     op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)
   RecordCon _ con flds ->
-    unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar NoExtField con) $ fmap unLoc flds
+    unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar noExtField con) $ fmap unLoc flds
   y -> y