From 3527cd21b35cbb8c00ea7680f597225cfe2e6154 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 3 Oct 2020 11:20:44 -0700
Subject: [PATCH 01/61] WIP recursion

This changes the heuristics so we get a reasonable fmap @[], but breaks
note.
---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 35 +++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  |  4 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  5 ++
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 48 ++++++++++++++-----
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 32 +++++++++----
 6 files changed, 86 insertions(+), 40 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 1f1f3ea449..09c64c325d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -1,22 +1,24 @@
 {-# LANGUAGE FlexibleContexts #-}
 module Ide.Plugin.Tactic.CodeGen where
 
-import Control.Monad.Except
-import Data.List
-import Data.Traversable
-import DataCon
-import Development.IDE.GHC.Compat
-import GHC.Exts
-import GHC.SourceGen.Binds
-import GHC.SourceGen.Expr
-import GHC.SourceGen.Overloaded
-import GHC.SourceGen.Pat
-import Ide.Plugin.Tactic.Judgements
-import Ide.Plugin.Tactic.Machinery
-import Ide.Plugin.Tactic.Naming
-import Ide.Plugin.Tactic.Types
-import Name
-import Type hiding (Var)
+import           Control.Monad.Except
+import           Control.Monad.State.Class (modify)
+import           Data.List
+import qualified Data.Set as S
+import           Data.Traversable
+import           DataCon
+import           Development.IDE.GHC.Compat
+import           GHC.Exts
+import           GHC.SourceGen.Binds
+import           GHC.SourceGen.Expr
+import           GHC.SourceGen.Overloaded
+import           GHC.SourceGen.Pat
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Naming
+import           Ide.Plugin.Tactic.Types
+import           Name
+import           Type hiding (Var)
 
 
 destructMatches
@@ -48,6 +50,7 @@ destructMatches f f2 t jdg = do
                 $ introducingPat (zip names $ coerce args)
                 $ withNewGoal g jdg
           sg <- f dc j
+          modify $ withIntroducedVals $ mappend $ S.fromList names
           pure $ match [pat] $ unLoc sg
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index f1cccae928..2c8b48227a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -34,8 +34,8 @@ getFunBindId (AbsBinds _ _ _ abes _ _ _)
 getFunBindId _ = []
 
 
-getCurrentDefinitions :: MonadReader Context m => m [OccName]
-getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs
+getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
+getCurrentDefinitions = asks $ ctxDefiningFuncs
 
 getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
 getModuleHypothesis = asks ctxModuleFuncs
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 51c1cef988..19b040877d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -52,6 +52,11 @@ introducing ns jdg@Judgement{..} = jdg
   { _jHypothesis = M.fromList ns <> _jHypothesis
   }
 
+withHypothesis :: (Map OccName a -> Map OccName a) -> Judgement' a -> Judgement' a
+withHypothesis f jdg@Judgement{..} = jdg
+  { _jHypothesis = f _jHypothesis
+  }
+
 ------------------------------------------------------------------------------
 -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals.
 introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 65885324c0..2ddc06944f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -79,7 +79,7 @@ runTactic ctx jdg t =
 scoreSolution :: TacticState -> [Judgement] -> Int
 scoreSolution TacticState{..} holes
   -- TODO(sandy): should this be linear?
-  = S.size ts_used_vals - length holes * 5
+  = negate (traceShowId $ S.size (ts_intro_vals S.\\ ts_used_vals)) - length holes * 5
 
 
 runTacticTWithState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 89cb181275..b4f2498ca8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -39,14 +39,8 @@ import           Type hiding (Var)
 
 ------------------------------------------------------------------------------
 -- | Use something in the hypothesis to fill the hole.
--- TODO(sandy): deprecate this
 assumption :: TacticsM ()
-assumption = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case find ((== g) . snd) $ toList hy of
-    Just (v, _) -> pure $ noLoc $ var' v
-    Nothing -> throwError $ GoalMismatch "assumption" g
+assumption = attemptOn allNames assume
 
 
 ------------------------------------------------------------------------------
@@ -71,6 +65,27 @@ useOccName jdg name =
     Nothing -> pure ()
 
 
+------------------------------------------------------------------------------
+-- | Restrict a tactic to looking only at pattern vals and functions
+simpler :: TacticsM () -> TacticsM ()
+simpler t = do
+  jdg <- goal
+  let funcs = M.filter (isFunction . unCType) $ jHypothesis jdg
+      hy' = jPatHypothesis jdg <> funcs
+  traceM $ mappend "!!! yo: " $ show hy'
+  localTactic t $ withHypothesis $ const hy'
+
+
+recursion :: TacticsM ()
+recursion = do
+  defs <- getCurrentDefinitions
+  traceM $ mappend "!!! recursion: " $ show defs
+  attemptOn (const $ fmap fst defs) $ \name -> do
+    traceM $ mappend "!!! recursing: " $ show name
+    localTactic (apply' name) (introducing defs)
+    simpler assumption
+
+
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
 intro :: TacticsM ()
@@ -81,6 +96,7 @@ intro = rule $ \jdg -> do
     Just (a, b) -> do
       v <- pure $ mkGoodName (getInScope hy) a
       let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg
+      modify $ withIntroducedVals $ mappend $ S.singleton v
       sg <- newSubgoal jdg'
       pure $ noLoc $ lambda [bvar' v] $ unLoc sg
     _ -> throwError $ GoalMismatch "intro" g
@@ -97,6 +113,7 @@ intros = rule $ \jdg -> do
     (as, b) -> do
       vs <- mkManyGoodNames hy as
       let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg
+      modify $ withIntroducedVals $ mappend $ S.fromList vs
       sg <- newSubgoal jdg'
       pure
         . noLoc
@@ -142,6 +159,7 @@ apply' func = rule $ \jdg -> do
     Just (CType ty) -> do
         let (args, ret) = splitFunTys ty
         unify g (CType ret)
+        useOccName jdg func
         sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
         pure . noLoc
              . foldl' (@@) (var' func)
@@ -186,13 +204,20 @@ attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
 attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)
 
 
+localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
+localTactic t f = do
+  TacticT $ StateT $ \jdg ->
+    runStateT (unTacticT t) $ f jdg
+
+
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
 auto = do
   current <- getCurrentDefinitions
-  TacticT $ StateT $ \jdg ->
-    runStateT (unTacticT $ auto' 5) $ disallowing current jdg
+  traceM $ mappend "!!!auto defs:" $ show current
+  localTactic (auto' 4) $ disallowing $ fmap fst current
+
 
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
@@ -207,9 +232,8 @@ auto' n = do
         progress ((==) `on` jGoal) NoProgress (destruct aname)
         loop
     , split >> loop
-    , attemptOn allNames $ \name -> do
-        assume name
-        loop
+    , assumption >> loop
+    , recursion
     ]
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 291d732fad..1cb3e35db7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE DeriveFunctor                  #-}
-{-# LANGUAGE DeriveGeneric                  #-}
-{-# LANGUAGE DerivingStrategies             #-}
-{-# LANGUAGE FlexibleInstances              #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving     #-}
-{-# LANGUAGE MultiParamTypeClasses          #-}
-{-# LANGUAGE TypeSynonymInstances           #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE TypeSynonymInstances       #-}
+{-# OPTIONS_GHC -fno-warn-orphans       #-}
 
 module Ide.Plugin.Tactic.Types
   ( module Ide.Plugin.Tactic.Types
@@ -40,23 +41,31 @@ instance Eq CType where
 instance Ord CType where
   compare = nonDetCmpType `on` unCType
 
+instance Show CType where
+  show  = unsafeRender . unCType
+
+instance Show OccName where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
     { ts_skolems   :: !([TyVar])
     , ts_unifier   :: !(TCvSubst)
     , ts_used_vals :: !(Set OccName)
+    , ts_intro_vals :: !(Set OccName)
     }
 
 instance Semigroup TacticState where
-  TacticState a1 b1 c1 <> TacticState a2 b2 c2
+  TacticState a1 b1 c1 d1 <> TacticState a2 b2 c2 d2
     = TacticState
         (a1 <> a2)
         (unionTCvSubst b1 b2)
         (c1 <> c2)
+        (d1 <> d2)
 
 instance Monoid TacticState where
-  mempty = TacticState mempty emptyTCvSubst mempty
+  mempty = TacticState mempty emptyTCvSubst mempty mempty
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
@@ -64,6 +73,11 @@ withUsedVals f ts = ts
   { ts_used_vals = f $ ts_used_vals ts
   }
 
+withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
+withIntroducedVals f ts = ts
+  { ts_intro_vals = f $ ts_intro_vals ts
+  }
+
 
 ------------------------------------------------------------------------------
 -- | The current bindings and goal for a hole to be filled by refinery.

From da2d7296d5dde6717869fd2ec92616fb026796c9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:12:41 -0700
Subject: [PATCH 02/61] Better scoring heuristic

I was forgetting to count destruct as usage
---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 12 ++++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 25 ++++++++++++++++---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  6 -----
 test/functional/Tactic.hs                     |  1 +
 test/testdata/tactic/GoldenListFmap.hs        |  2 ++
 .../tactic/GoldenListFmap.hs.expected         |  5 ++++
 6 files changed, 41 insertions(+), 10 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenListFmap.hs
 create mode 100644 test/testdata/tactic/GoldenListFmap.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 09c64c325d..c868028a1b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -2,8 +2,10 @@
 module Ide.Plugin.Tactic.CodeGen where
 
 import           Control.Monad.Except
+import           Control.Monad.State (MonadState)
 import           Control.Monad.State.Class (modify)
 import           Data.List
+import qualified Data.Map as M
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
@@ -21,6 +23,13 @@ import           Name
 import           Type hiding (Var)
 
 
+useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
+useOccName jdg name =
+  case M.lookup name $ jHypothesis jdg of
+    Just{}  -> modify $ withUsedVals $ S.insert name
+    Nothing -> pure ()
+
+
 destructMatches
     :: (DataCon -> Judgement -> Rule)
        -- ^ How to construct each match
@@ -62,7 +71,8 @@ destruct' f term jdg = do
   let hy = jHypothesis jdg
   case find ((== term) . fst) $ toList hy of
     Nothing -> throwError $ UndefinedHypothesis term
-    Just (_, t) ->
+    Just (_, t) -> do
+      useOccName jdg term
       fmap noLoc $ case' (var' term) <$>
         destructMatches f (destructing term) t jdg
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 2ddc06944f..4d560f78b7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveFunctor         #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE DerivingStrategies    #-}
+{-# LANGUAGE DerivingVia           #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE LambdaCase            #-}
@@ -76,10 +77,28 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
-scoreSolution :: TacticState -> [Judgement] -> Int
+scoreSolution
+    :: TacticState
+    -> [Judgement]
+    -> ( Penalize Int  -- number of holes
+       , Reward Bool  -- all bindings used
+       , Reward Int   -- number used bindings
+       , Penalize Int   -- number used bindings
+       )
 scoreSolution TacticState{..} holes
-  -- TODO(sandy): should this be linear?
-  = negate (traceShowId $ S.size (ts_intro_vals S.\\ ts_used_vals)) - length holes * 5
+  = traceShowId
+    ( Penalize $ length holes
+    , Reward $ S.null $ traceShowId $ ts_intro_vals S.\\ ts_used_vals
+    , Reward $ S.size ts_used_vals
+    , Penalize $ S.size ts_intro_vals
+    )
+
+
+newtype Penalize a = Penalize a
+  deriving (Eq, Ord, Show) via (Down a)
+
+newtype Reward a = Reward a
+  deriving (Eq, Ord, Show) via a
 
 
 runTacticTWithState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index b4f2498ca8..f5856fc8dc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -58,12 +58,6 @@ assume name = rule $ \jdg -> do
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
-useOccName jdg name =
-  case M.lookup name $ jHypothesis jdg of
-    Just{}  -> modify $ withUsedVals $ S.insert name
-    Nothing -> pure ()
-
 
 ------------------------------------------------------------------------------
 -- | Restrict a tactic to looking only at pattern vals and functions
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index e770ad8a41..ae4379a9fb 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -93,6 +93,7 @@ tests = testGroup
   , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto ""
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
+  , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenListFmap.hs b/test/testdata/tactic/GoldenListFmap.hs
new file mode 100644
index 0000000000..85293daaf4
--- /dev/null
+++ b/test/testdata/tactic/GoldenListFmap.hs
@@ -0,0 +1,2 @@
+fmapList :: (a -> b) -> [a] -> [b]
+fmapList = _
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
new file mode 100644
index 0000000000..26766d57c3
--- /dev/null
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -0,0 +1,5 @@
+fmapList :: (a -> b) -> [a] -> [b]
+fmapList = (\ fab l_a
+   -> case l_a of
+        [] -> []
+        ((:) a l_a3) -> (:) (fab a) (fmapList fab l_a3))

From b805aa9bc364e0ccf5a3d0030c49d529db17a0ff Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:14:48 -0700
Subject: [PATCH 03/61] Don't trace scoring

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 4d560f78b7..afc4ab3058 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -86,9 +86,8 @@ scoreSolution
        , Penalize Int   -- number used bindings
        )
 scoreSolution TacticState{..} holes
-  = traceShowId
-    ( Penalize $ length holes
-    , Reward $ S.null $ traceShowId $ ts_intro_vals S.\\ ts_used_vals
+  = ( Penalize $ length holes
+    , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
     , Reward $ S.size ts_used_vals
     , Penalize $ S.size ts_intro_vals
     )

From 1dbec5b849b67d3dcf6eae3938d78dcd6881f765 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:33:10 -0700
Subject: [PATCH 04/61] Add fromMaybe test

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 6 +++---
 test/functional/Tactic.hs                          | 1 +
 test/testdata/tactic/GoldenFromMaybe.hs            | 2 ++
 test/testdata/tactic/GoldenFromMaybe.hs.expected   | 5 +++++
 4 files changed, 11 insertions(+), 3 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFromMaybe.hs
 create mode 100644 test/testdata/tactic/GoldenFromMaybe.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index afc4ab3058..6f1b9d2034 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -81,9 +81,9 @@ scoreSolution
     :: TacticState
     -> [Judgement]
     -> ( Penalize Int  -- number of holes
-       , Reward Bool  -- all bindings used
-       , Reward Int   -- number used bindings
-       , Penalize Int   -- number used bindings
+       , Reward Bool   -- all bindings used
+       , Reward Int    -- number used bindings
+       , Penalize Int  -- number of introduced bindings
        )
 scoreSolution TacticState{..} holes
   = ( Penalize $ length holes
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index ae4379a9fb..b70efb3376 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -94,6 +94,7 @@ tests = testGroup
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
   , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
+  , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs b/test/testdata/tactic/GoldenFromMaybe.hs
new file mode 100644
index 0000000000..e3046a29c3
--- /dev/null
+++ b/test/testdata/tactic/GoldenFromMaybe.hs
@@ -0,0 +1,2 @@
+fromMaybe :: a -> Maybe a -> a
+fromMaybe = _
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs.expected b/test/testdata/tactic/GoldenFromMaybe.hs.expected
new file mode 100644
index 0000000000..1375967a70
--- /dev/null
+++ b/test/testdata/tactic/GoldenFromMaybe.hs.expected
@@ -0,0 +1,5 @@
+fromMaybe :: a -> Maybe a -> a
+fromMaybe = (\ a ma
+   -> case ma of
+        Nothing -> a
+        (Just a2) -> a2)

From 803c8d70cf8daba17ab05c3e0107a06c18af159c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 14:07:58 -0700
Subject: [PATCH 05/61] wtf; recursion stack frame doesnt seem to work

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  8 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 10 ++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 44 +++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 74 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 21 +++---
 5 files changed, 108 insertions(+), 49 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index c868028a1b..0b5c8c370b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -68,6 +68,7 @@ destructMatches f f2 t jdg = do
 -- resulting matches.
 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
     Nothing -> throwError $ UndefinedHypothesis term
@@ -82,6 +83,7 @@ destruct' f term jdg = do
 -- resulting matches.
 destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' f jdg = do
+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
@@ -99,7 +101,11 @@ buildDataCon
     -> RuleM (LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
-  sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
+  sgs <- traverse ( newSubgoal
+                  . blacklistingDestruct
+                  . flip withNewGoal jdg
+                  . CType
+                  ) args
   pure
     . noLoc
     . foldl' (@@)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 19b040877d..50b4829f67 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -42,6 +42,14 @@ destructing n jdg@Judgement{..} = jdg
   { _jDestructed = _jDestructed <> S.singleton n
   }
 
+blacklistingDestruct :: Judgement -> Judgement
+blacklistingDestruct jdg = jdg
+  { _jBlacklistDestruct = True
+  }
+
+isDestructBlacklisted :: Judgement -> Bool
+isDestructBlacklisted = _jBlacklistDestruct
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t jdg = jdg
   { _jGoal = t
@@ -90,5 +98,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 6f1b9d2034..9d156e197f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,9 +18,9 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
-import           Control.Monad.Except (throwError)
+import           Control.Monad.Error.Class
 import           Control.Monad.Reader
-import           Control.Monad.State (gets, modify)
+import           Control.Monad.State.Class (gets, modify, MonadState)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
@@ -62,21 +62,55 @@ runTactic
     -> Either [TacticError] (LHsExpr GhcPs)
 runTactic ctx jdg t =
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
-        tacticState = mempty { ts_skolems = skolems }
+        tacticState = defaultTacticState { ts_skolems = skolems }
     in case partitionEithers
           . flip runReader ctx
           . unExtractM
           $ runTacticTWithState t jdg tacticState of
       (errs, []) -> Left $ errs
       (_, solns) -> do
+        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ intercalate "\n" $ fmap (unsafeRender . fst) $ solns
-        case sortBy (comparing $ Down . uncurry scoreSolution . snd) solns of
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (unsafeRender . fst) sorted
+        case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
           _ -> Left []
 
 
+recursionStackFrame
+    :: (MonadError TacticError m, MonadState TacticState m)
+    => m a
+    -> m (Bool, a)
+recursionStackFrame ma = do
+  modify $ withRecursionStack (False :)
+  finally
+    ( do
+      a <- ma
+      r <- gets $ head . ts_recursion_stack
+      pure (r, a)
+    )
+    (modify $ withRecursionStack tail)
+
+
+finally :: MonadError e m => m a -> m () -> m a
+finally action cleanup = do
+  a <-
+    action `catchError` \e -> do
+      cleanup
+      throwError e
+  cleanup
+  pure a
+
+
+setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
+setRecursionFrameData b = do
+  modify $ withRecursionStack $ \case
+    (_ : bs) -> b : bs
+    []       -> []
+
+
+
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index f5856fc8dc..e6cebe3360 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -34,6 +34,7 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Control.Monad
 
 
 
@@ -52,33 +53,34 @@ assume name = rule $ \jdg -> do
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
+          when (M.member name $ jPatHypothesis jdg) $ do
+            -- traceM $ "!!!simpler: " <> show name
+            setRecursionFrameData True
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-
-------------------------------------------------------------------------------
--- | Restrict a tactic to looking only at pattern vals and functions
-simpler :: TacticsM () -> TacticsM ()
-simpler t = do
-  jdg <- goal
-  let funcs = M.filter (isFunction . unCType) $ jHypothesis jdg
-      hy' = jPatHypothesis jdg <> funcs
-  traceM $ mappend "!!! yo: " $ show hy'
-  localTactic t $ withHypothesis $ const hy'
-
-
 recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
-  traceM $ mappend "!!! recursion: " $ show defs
   attemptOn (const $ fmap fst defs) $ \name -> do
-    traceM $ mappend "!!! recursing: " $ show name
-    localTactic (apply' name) (introducing defs)
-    simpler assumption
-
+    localTactic (apply' name) $ introducing defs
+    (has_simple, _) <- recursionStackFrame assumption
+    case has_simple of
+      True -> traceM $ mappend "!!!recursion ok: " $ show defs
+      False -> do
+        traceM $ mappend "!!!recursion not ok >: " $ show defs
+        throwError NoProgress
+
+
+foo :: Int -> a -> a -> [[a]]
+foo n i b = map (take n) . take n $ go (i : repeat b)
+  where
+    go [] = [[]]
+    go [x] = [[x]]
+    go l@(x:y:ys) = l : map (y :) (go $ x:ys)
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
@@ -146,19 +148,25 @@ homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
 
 
 apply' :: OccName -> TacticsM ()
-apply' func = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case M.lookup func hy of
-    Just (CType ty) -> do
-        let (args, ret) = splitFunTys ty
-        unify g (CType ret)
-        useOccName jdg func
-        sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
-        pure . noLoc
-             . foldl' (@@) (var' func)
-             $ fmap unLoc sgs
-    Nothing -> throwError $ GoalMismatch "apply" g
+apply' func = do
+  rule $ \jdg -> do
+    let hy = jHypothesis jdg
+        g  = jGoal jdg
+    case M.lookup func hy of
+      Just (CType ty) -> do
+          let (args, ret) = splitFunTys ty
+          unify g (CType ret)
+          useOccName jdg func
+          sgs <- traverse ( newSubgoal
+                          . blacklistingDestruct
+                          . flip withNewGoal jdg
+                          . CType
+                          ) args
+          pure . noLoc
+              . foldl' (@@) (var' func)
+              $ fmap unLoc sgs
+      Nothing -> throwError $ GoalMismatch "apply" g
+  assumption
 
 
 ------------------------------------------------------------------------------
@@ -209,8 +217,10 @@ localTactic t f = do
 auto :: TacticsM ()
 auto = do
   current <- getCurrentDefinitions
-  traceM $ mappend "!!!auto defs:" $ show current
-  localTactic (auto' 4) $ disallowing $ fmap fst current
+  jdg <- goal
+  traceM $ mappend "!!!auto current:" $ show current
+  traceM $ mappend "!!!auto jdg:" $ show jdg
+  localTactic (auto' 5) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 1cb3e35db7..52a83780e3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -54,18 +54,18 @@ data TacticState = TacticState
     , ts_unifier   :: !(TCvSubst)
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
+    , ts_recursion_stack :: ![Bool]
     }
 
-instance Semigroup TacticState where
-  TacticState a1 b1 c1 d1 <> TacticState a2 b2 c2 d2
-    = TacticState
-        (a1 <> a2)
-        (unionTCvSubst b1 b2)
-        (c1 <> c2)
-        (d1 <> d2)
+defaultTacticState :: TacticState
+defaultTacticState =
+  TacticState mempty emptyTCvSubst mempty mempty mempty
 
-instance Monoid TacticState where
-  mempty = TacticState mempty emptyTCvSubst mempty mempty
+withRecursionStack
+  :: ([Bool] -> [Bool]) -> TacticState -> TacticState
+withRecursionStack f ts = ts
+  { ts_recursion_stack = f $ ts_recursion_stack ts
+  }
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
@@ -87,9 +87,10 @@ data Judgement' a = Judgement
     -- ^ These should align with keys of _jHypothesis
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
+  , _jBlacklistDestruct :: !(Bool)
   , _jGoal        :: !(a)
   }
-  deriving stock (Eq, Ord, Generic, Functor)
+  deriving stock (Eq, Ord, Generic, Functor, Show)
 
 type Judgement = Judgement' CType
 

From fe468f3cd401cefb59dfd5928ecd6f8f9b052fc0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:00:49 -0700
Subject: [PATCH 06/61] Better debugging and smarter apply'

---
 plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs   |  5 ++++-
 .../tactics/src/Ide/Plugin/Tactic/Machinery.hs   |  3 ++-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 16 +++++-----------
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs   | 11 ++++++++++-
 4 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index 6d1053c2c6..c81ea6e59a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -4,11 +4,12 @@ module Ide.Plugin.Tactic.Debug
   , traceM
   , traceShowId
   , trace
+  , traceMX
   ) where
 
 import Debug.Trace
 import DynFlags (unsafeGlobalDynFlags)
-import Outputable
+import Outputable hiding ((<>))
 
 ------------------------------------------------------------------------------
 -- | Print something
@@ -18,3 +19,5 @@ unsafeRender = unsafeRender' . ppr
 unsafeRender' :: SDoc -> String
 unsafeRender' = showSDoc unsafeGlobalDynFlags
 
+traceMX :: (Monad m, Show a) => String -> a -> m ()
+traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 9d156e197f..a2f5e74ec1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -35,6 +35,7 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import Control.Monad.State (MonadState(..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -71,7 +72,7 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (unsafeRender . fst) sorted
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e6cebe3360..bf788fea3f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE ViewPatterns          #-}
@@ -11,6 +12,7 @@ module Ide.Plugin.Tactic.Tactics
   ) where
 
 import           Control.Applicative
+import           Control.Monad
 import           Control.Monad.Except (throwError)
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
@@ -34,7 +36,6 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Control.Monad
 
 
 
@@ -54,7 +55,7 @@ assume name = rule $ \jdg -> do
       case ty == jGoal jdg of
         True  -> do
           when (M.member name $ jPatHypothesis jdg) $ do
-            -- traceM $ "!!!simpler: " <> show name
+            traceM $ "!!!simpler: " <> show name
             setRecursionFrameData True
           useOccName jdg name
           pure $ noLoc $ var' name
@@ -75,13 +76,6 @@ recursion = do
         throwError NoProgress
 
 
-foo :: Int -> a -> a -> [[a]]
-foo n i b = map (take n) . take n $ go (i : repeat b)
-  where
-    go [] = [[]]
-    go [x] = [[x]]
-    go l@(x:y:ys) = l : map (y :) (go $ x:ys)
-
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
 intro :: TacticsM ()
@@ -165,8 +159,8 @@ apply' func = do
           pure . noLoc
               . foldl' (@@) (var' func)
               $ fmap unLoc sgs
-      Nothing -> throwError $ GoalMismatch "apply" g
-  assumption
+      Nothing -> do
+        throwError $ GoalMismatch "apply" g
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 52a83780e3..b4195c6573 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -47,6 +47,15 @@ instance Show CType where
 instance Show OccName where
   show  = unsafeRender
 
+instance Show Var where
+  show  = unsafeRender
+
+instance Show TCvSubst where
+  show  = unsafeRender
+
+instance Show (LHsExpr GhcPs) where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
@@ -55,7 +64,7 @@ data TacticState = TacticState
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
     , ts_recursion_stack :: ![Bool]
-    }
+    } deriving stock Show
 
 defaultTacticState :: TacticState
 defaultTacticState =

From 68cda515d606690e979faba0e53e924281fecb85 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:15:16 -0700
Subject: [PATCH 07/61] filterT

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 41 +++++++++++++------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  8 +---
 2 files changed, 30 insertions(+), 19 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index a2f5e74ec1..1115a90a27 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -79,19 +79,34 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
-recursionStackFrame
-    :: (MonadError TacticError m, MonadState TacticState m)
-    => m a
-    -> m (Bool, a)
-recursionStackFrame ma = do
-  modify $ withRecursionStack (False :)
-  finally
-    ( do
-      a <- ma
-      r <- gets $ head . ts_recursion_stack
-      pure (r, a)
-    )
-    (modify $ withRecursionStack tail)
+recursiveCleanup
+    :: TacticState
+    -> Maybe TacticError
+recursiveCleanup s =
+  let r = head $ ts_recursion_stack s
+   in traceShowId $ case r of
+        True  -> Nothing
+        False -> Just NoProgress
+
+
+filterT
+    :: (Monad m, Show s, Show ext)
+    => (s -> Maybe err)
+    -> (s -> s)
+    -> TacticT jdg ext err s m ()
+    -> TacticT jdg ext err s m ()
+filterT p s' t = do
+  s0 <- get
+  traceMX "state0" s0
+  tactic $ \j -> unRuleT $ do
+    e <- RuleT $ proofState t j
+    s <- get
+    traceMX "state" s
+    traceMX "extract" e
+    modify s'
+    case p s of
+      Just err -> throwError err
+      Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index bf788fea3f..82a1d24536 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -68,12 +68,8 @@ recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     localTactic (apply' name) $ introducing defs
-    (has_simple, _) <- recursionStackFrame assumption
-    case has_simple of
-      True -> traceM $ mappend "!!!recursion ok: " $ show defs
-      False -> do
-        traceM $ mappend "!!!recursion not ok >: " $ show defs
-        throwError NoProgress
+    modify $ withRecursionStack (False :)
+    filterT recursiveCleanup (withRecursionStack tail) assumption
 
 
 ------------------------------------------------------------------------------

From a480c197a42a638818fb9b86ea2fd0800c7d065a Mon Sep 17 00:00:00 2001
From: TOTBWF <reed.mullanix@calabrio.com>
Date: Mon, 5 Oct 2020 14:40:27 -0700
Subject: [PATCH 08/61] Fix FilterT

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 28 +++++++------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  5 ++--
 2 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1115a90a27..11570f51cc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -89,24 +89,16 @@ recursiveCleanup s =
         False -> Just NoProgress
 
 
-filterT
-    :: (Monad m, Show s, Show ext)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p s' t = do
-  s0 <- get
-  traceMX "state0" s0
-  tactic $ \j -> unRuleT $ do
-    e <- RuleT $ proofState t j
-    s <- get
-    traceMX "state" s
-    traceMX "extract" e
-    modify s'
-    case p s of
-      Just err -> throwError err
-      Nothing -> pure e
+filterT :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+filterT p f t = check >> t
+    where
+      check = rule $ \j -> do
+          e <- subgoal j
+          s <- get
+          modify f
+          case p s of
+            Just err -> throwError err
+            Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 82a1d24536..cd84680451 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -67,9 +67,10 @@ recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
-    localTactic (apply' name) $ introducing defs
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) assumption
+    filterT recursiveCleanup (withRecursionStack tail) $ do
+        localTactic (apply' name) $ introducing defs
+        assumption
 
 
 ------------------------------------------------------------------------------

From 8fa2a8340c737f2c6c87acef8e695ce8bd512c19 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:51:27 -0700
Subject: [PATCH 09/61] derive foldr

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 33 +++++++------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  6 ++--
 2 files changed, 16 insertions(+), 23 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1115a90a27..cf6cb5891e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -88,25 +88,16 @@ recursiveCleanup s =
         True  -> Nothing
         False -> Just NoProgress
 
-
-filterT
-    :: (Monad m, Show s, Show ext)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p s' t = do
-  s0 <- get
-  traceMX "state0" s0
-  tactic $ \j -> unRuleT $ do
-    e <- RuleT $ proofState t j
-    s <- get
-    traceMX "state" s
-    traceMX "extract" e
-    modify s'
-    case p s of
-      Just err -> throwError err
-      Nothing -> pure e
+filterT :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+filterT p f t = check >> t
+    where
+      check = rule $ \j -> do
+          e <- subgoal j
+          s <- get
+          modify f
+          case p s of
+            Just err -> throwError err
+            Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
@@ -132,14 +123,14 @@ scoreSolution
     -> [Judgement]
     -> ( Penalize Int  -- number of holes
        , Reward Bool   -- all bindings used
-       , Reward Int    -- number used bindings
        , Penalize Int  -- number of introduced bindings
+       , Reward Int    -- number used bindings
        )
 scoreSolution TacticState{..} holes
   = ( Penalize $ length holes
     , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
-    , Reward $ S.size ts_used_vals
     , Penalize $ S.size ts_intro_vals
+    , Reward $ S.size ts_used_vals
     )
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 82a1d24536..58fda28b93 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -67,9 +67,11 @@ recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
-    localTactic (apply' name) $ introducing defs
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) assumption
+    filterT recursiveCleanup (withRecursionStack tail) $ do
+      localTactic (apply' name) $ introducing defs
+      assumption
+
 
 
 ------------------------------------------------------------------------------

From a6e40e1a35384f21333b5e52121a888afc07b2af Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 15:25:14 -0700
Subject: [PATCH 10/61] Test for foldr

---
 test/functional/Tactic.hs                    | 9 +++++----
 test/testdata/tactic/GoldenFoldr.hs          | 2 ++
 test/testdata/tactic/GoldenFoldr.hs.expected | 5 +++++
 3 files changed, 12 insertions(+), 4 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFoldr.hs
 create mode 100644 test/testdata/tactic/GoldenFoldr.hs.expected

diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index b70efb3376..f11717209e 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -86,15 +86,16 @@ tests = testGroup
       [ (not, DestructLambdaCase, "")
       ]
   , goldenTest "GoldenIntros.hs"            2 8  Intros ""
-  , goldenTest "GoldenEitherAuto.hs"        2 11 Auto   ""
-  , goldenTest "GoldenJoinCont.hs"          4 12 Auto   ""
-  , goldenTest "GoldenIdentityFunctor.hs"   3 11 Auto   ""
-  , goldenTest "GoldenIdTypeFam.hs"         7 11 Auto   ""
+  , goldenTest "GoldenEitherAuto.hs"        2 11 Auto ""
+  , goldenTest "GoldenJoinCont.hs"          4 12 Auto ""
+  , goldenTest "GoldenIdentityFunctor.hs"   3 11 Auto ""
+  , goldenTest "GoldenIdTypeFam.hs"         7 11 Auto ""
   , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto ""
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
   , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
   , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
+  , goldenTest "GoldenFoldr.hs"             2 10 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFoldr.hs b/test/testdata/tactic/GoldenFoldr.hs
new file mode 100644
index 0000000000..bade9c1e7a
--- /dev/null
+++ b/test/testdata/tactic/GoldenFoldr.hs
@@ -0,0 +1,2 @@
+foldr2 :: (a -> b -> b) -> b -> [a] -> b
+foldr2 = _
diff --git a/test/testdata/tactic/GoldenFoldr.hs.expected b/test/testdata/tactic/GoldenFoldr.hs.expected
new file mode 100644
index 0000000000..fe0463b75f
--- /dev/null
+++ b/test/testdata/tactic/GoldenFoldr.hs.expected
@@ -0,0 +1,5 @@
+foldr2 :: (a -> b -> b) -> b -> [a] -> b
+foldr2 = (\ f_b b l_a
+   -> case l_a of
+        [] -> b
+        ((:) a l_a4) -> f_b a (foldr2 f_b b l_a4))

From 7981a717d333664b1ffd0217814792d7e6b55654 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 15:29:44 -0700
Subject: [PATCH 11/61] Fix JoinCont test

---
 test/testdata/tactic/GoldenJoinCont.hs          | 2 +-
 test/testdata/tactic/GoldenJoinCont.hs.expected | 7 ++-----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/test/testdata/tactic/GoldenJoinCont.hs b/test/testdata/tactic/GoldenJoinCont.hs
index a0cdb05da6..f2c63714da 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs
+++ b/test/testdata/tactic/GoldenJoinCont.hs
@@ -1,4 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
-joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
+joinCont :: Cont r (Cont r a) -> Cont r a
 joinCont = _
diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected
index 306591b32c..ebf84d1371 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs.expected
+++ b/test/testdata/tactic/GoldenJoinCont.hs.expected
@@ -1,7 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
-joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
-joinCont = (\ fac fbc eab fcd
-   -> case eab of
-        (Left a) -> fcd (fac a)
-        (Right b) -> fcd (fbc b))
+joinCont :: Cont r (Cont r a) -> Cont r a
+joinCont = (\ f_r far -> f_r (\ f_r2 -> f_r2 far))

From 69d122bd689534eb07e719ee2736b765c8146d9a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 16:09:06 -0700
Subject: [PATCH 12/61] Use generic-lens

---
 haskell-language-server.cabal                 |  1 +
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 51 +++++++++----------
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 11 ----
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 19 +------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 33 +++++++-----
 5 files changed, 47 insertions(+), 68 deletions(-)

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index d931e72140..dfdf0789b3 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -158,6 +158,7 @@ executable haskell-language-server
     , refinery                 ^>=0.2
     , ghc-exactprint
     , fingertree
+    , generic-lens
 
   if flag(agpl)
     build-depends: brittany
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 50b4829f67..ed4d22bf69 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -1,8 +1,11 @@
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE ViewPatterns    #-}
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE RecordWildCards  #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns     #-}
 
 module Ide.Plugin.Tactic.Judgements where
 
+import Control.Lens hiding (Context)
 import           Data.Char
 import           Data.Coerce
 import           Data.Map (Map)
@@ -14,6 +17,7 @@ import           Ide.Plugin.Tactic.Types
 import           OccName
 import           SrcLoc
 import           Type
+import Data.Generics.Product (field)
 
 
 ------------------------------------------------------------------------------
@@ -38,46 +42,41 @@ hasDestructed :: Judgement -> OccName -> Bool
 hasDestructed j n = S.member n $ _jDestructed j
 
 destructing :: OccName -> Judgement -> Judgement
-destructing n jdg@Judgement{..} = jdg
-  { _jDestructed = _jDestructed <> S.singleton n
-  }
+destructing n = field @"_jDestructed" <>~ S.singleton n
 
 blacklistingDestruct :: Judgement -> Judgement
-blacklistingDestruct jdg = jdg
-  { _jBlacklistDestruct = True
-  }
+blacklistingDestruct =
+  field @"_jBlacklistDestruct" .~ True
 
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
 withNewGoal :: a -> Judgement' a -> Judgement' a
-withNewGoal t jdg = jdg
-  { _jGoal = t
-  }
+withNewGoal t = field @"_jGoal" .~ t
 
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
-introducing ns jdg@Judgement{..} = jdg
-  { _jHypothesis = M.fromList ns <> _jHypothesis
-  }
+introducing ns =
+  field @"_jHypothesis" <>~ M.fromList ns
 
-withHypothesis :: (Map OccName a -> Map OccName a) -> Judgement' a -> Judgement' a
-withHypothesis f jdg@Judgement{..} = jdg
-  { _jHypothesis = f _jHypothesis
-  }
+withHypothesis
+    :: (Map OccName a -> Map OccName a)
+    -> Judgement' a
+    -> Judgement' a
+withHypothesis f =
+  field @"_jHypothesis" %~ f
 
 ------------------------------------------------------------------------------
 -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals.
 introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a
-introducingPat ns jdg@Judgement{..} = jdg
-  { _jHypothesis  = M.fromList ns <> _jHypothesis
-  , _jPatternVals = S.fromList (fmap fst ns) <> _jPatternVals
-  }
+introducingPat ns jdg = jdg
+  & field @"_jHypothesis"  <>~ M.fromList ns
+  & field @"_jPatternVals" <>~ S.fromList (fmap fst ns)
 
 
 disallowing :: [OccName] -> Judgement' a -> Judgement' a
-disallowing ns jdg@Judgement{..} = jdg
-  { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns
-  }
+disallowing ns =
+  field @"_jHypothesis" %~ flip M.withoutKeys (S.fromList ns)
+
 
 jHypothesis :: Judgement' a -> Map OccName a
 jHypothesis = _jHypothesis
@@ -98,5 +97,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 4aca416713..290f730390 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -106,16 +106,6 @@ filterT p f t = check >> t
             Nothing -> pure e
 
 
-finally :: MonadError e m => m a -> m () -> m a
-finally action cleanup = do
-  a <-
-    action `catchError` \e -> do
-      cleanup
-      throwError e
-  cleanup
-  pure a
-
-
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
@@ -123,7 +113,6 @@ setRecursionFrameData b = do
     []       -> []
 
 
-
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 717f1c1510..b7819b33a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -11,7 +11,6 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
-import           Control.Applicative
 import           Control.Monad
 import           Control.Monad.Except (throwError)
 import           Control.Monad.State.Class
@@ -73,22 +72,6 @@ recursion = do
       assumption
 
 
-------------------------------------------------------------------------------
--- | Introduce a lambda.
-intro :: TacticsM ()
-intro = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case splitFunTy_maybe $ unCType g of
-    Just (a, b) -> do
-      v <- pure $ mkGoodName (getInScope hy) a
-      let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg
-      modify $ withIntroducedVals $ mappend $ S.singleton v
-      sg <- newSubgoal jdg'
-      pure $ noLoc $ lambda [bvar' v] $ unLoc sg
-    _ -> throwError $ GoalMismatch "intro" g
-
-
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
@@ -218,7 +201,7 @@ auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
-  intros <|> many_ intro
+  try intros
   choice
     [ attemptOn functionNames $ \fname -> do
         apply' fname
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index b4195c6573..99a05af917 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingStrategies         #-}
@@ -18,6 +20,8 @@ module Ide.Plugin.Tactic.Types
   , Range
   ) where
 
+import Control.Lens hiding (Context)
+import Data.Generics.Product (field)
 import Control.Monad.Reader
 import Data.Function
 import Data.Map (Map)
@@ -64,40 +68,43 @@ data TacticState = TacticState
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
     , ts_recursion_stack :: ![Bool]
-    } deriving stock Show
+    } deriving stock (Show, Generic)
+
 
 defaultTacticState :: TacticState
 defaultTacticState =
   TacticState mempty emptyTCvSubst mempty mempty mempty
 
+
 withRecursionStack
   :: ([Bool] -> [Bool]) -> TacticState -> TacticState
-withRecursionStack f ts = ts
-  { ts_recursion_stack = f $ ts_recursion_stack ts
-  }
+withRecursionStack f =
+  field @"ts_recursion_stack" %~ f
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
-withUsedVals f ts = ts
-  { ts_used_vals = f $ ts_used_vals ts
-  }
+withUsedVals f =
+  field @"ts_used_vals" %~ f
+
 
 withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
-withIntroducedVals f ts = ts
-  { ts_intro_vals = f $ ts_intro_vals ts
-  }
+withIntroducedVals f =
+  field @"ts_intro_vals" %~ f
+
 
 
 ------------------------------------------------------------------------------
 -- | The current bindings and goal for a hole to be filled by refinery.
 data Judgement' a = Judgement
-  { _jHypothesis  :: !(Map OccName a)
-  , _jDestructed  :: !(Set OccName)
+  { _jHypothesis :: !(Map OccName a)
+  , _jDestructed :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
-  , _jGoal        :: !(a)
+  , _jPositionMaps :: !(Map OccName [OccName])
+  , _jAncestry     :: !(Map OccName OccName)
+  , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)
 

From a781803c6b77cdbeb0a3bef7e29d0741fa81fb15 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 19:54:32 -0700
Subject: [PATCH 13/61] Positionally-aware recursion

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 15 ++++--
 .../tactics/src/Ide/Plugin/Tactic/Debug.hs    |  5 ++
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 48 ++++++++++++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 34 ++++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 52 ++++++++++++++-----
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  5 ++
 6 files changed, 137 insertions(+), 22 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 0b5c8c370b..3557e290c0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -33,7 +33,7 @@ useOccName jdg name =
 destructMatches
     :: (DataCon -> Judgement -> Rule)
        -- ^ How to construct each match
-    -> (Judgement -> Judgement)
+    -> ([(OccName, CType)] -> Judgement -> Judgement)
        -- ^ How to derive each match judgement
     -> CType
        -- ^ Type being destructed
@@ -51,12 +51,13 @@ destructMatches f f2 t jdg = do
         _ -> for dcs $ \dc -> do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
+          let hy' = zip names $ coerce args
 
           let pat :: Pat GhcPs
               pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
                   $ fmap bvar' names
-              j = f2
-                $ introducingPat (zip names $ coerce args)
+              j = f2 hy'
+                $ introducingPat hy'
                 $ withNewGoal g jdg
           sg <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
@@ -75,7 +76,11 @@ destruct' f term jdg = do
     Just (_, t) -> do
       useOccName jdg term
       fmap noLoc $ case' (var' term) <$>
-        destructMatches f (destructing term) t jdg
+        destructMatches
+          f
+          (\cs -> setParents term (fmap fst cs) . destructing term)
+          t
+          jdg
 
 
 ------------------------------------------------------------------------------
@@ -88,7 +93,7 @@ destructLambdaCase' f jdg = do
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
       fmap noLoc $ lambdaCase <$>
-        destructMatches f id (CType arg) jdg
+        destructMatches f (const id) (CType arg) jdg
     _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index c81ea6e59a..20acfc58ab 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -4,6 +4,7 @@ module Ide.Plugin.Tactic.Debug
   , traceM
   , traceShowId
   , trace
+  , traceX
   , traceMX
   ) where
 
@@ -21,3 +22,7 @@ unsafeRender' = showSDoc unsafeGlobalDynFlags
 
 traceMX :: (Monad m, Show a) => String -> a -> m ()
 traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
+
+traceX :: (Show a) => String -> a -> b -> b
+traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index ed4d22bf69..8a9c005d9b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE RecordWildCards  #-}
 {-# LANGUAGE TypeApplications #-}
@@ -58,6 +59,51 @@ introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+
+setParents
+    :: OccName    -- ^ parent
+    -> [OccName]  -- ^ children
+    -> Judgement
+    -> Judgement
+setParents p cs =
+  field @"_jAncestry" <>~ M.fromList (fmap (, p) cs)
+
+
+
+------------------------------------------------------------------------------
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
+-- in and of itself (see the note there.) Additionally, this doesn't check to
+-- make sure we're in the top-level scope, so it will set the recursive
+-- position mapping any time 'intros' is called.
+withPositionMapping :: Context -> [OccName] -> Judgement -> Judgement
+withPositionMapping ctx names j =
+  case M.member  defining (_jPositionMaps j) of
+    True  -> j
+    False ->
+      traceX "withPositionMapping hack" (defining, names)
+        $ j & field @"_jPositionMaps" . at defining ?~ names
+  where
+    defining = extremelyStupid__definingFunction ctx
+
+
+------------------------------------------------------------------------------
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined
+-- (eg, we might be in a where block). The head of this list is not guaranteed
+-- to be the one we're interested in.
+extremelyStupid__definingFunction :: Context -> OccName
+extremelyStupid__definingFunction =
+  fst . head . ctxDefiningFuncs
+
+
+withCurrentPosition :: Int -> Judgement -> Judgement
+withCurrentPosition i =
+  field @"_jCurrentPosition" ?~ i
+
+
 withHypothesis
     :: (Map OccName a -> Map OccName a)
     -> Judgement' a
@@ -97,5 +143,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty Nothing . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 290f730390..5a7378888e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,12 +18,15 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
+import           Control.Lens hiding (Context, matching, Empty)
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
-import           Control.Monad.State.Class (gets, modify, MonadState)
+import           Control.Monad.State (MonadState(..))
+import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
+import qualified Data.Map as M
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -35,7 +38,6 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
-import Control.Monad.State (MonadState(..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -79,12 +81,38 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
+--------------------------------------------------------------------------------
+-- TODO(sandy): this is probably the worst function I've ever written; sorry
+hasPositionalAncestry
+    :: Judgement
+    -> OccName     -- ^ defining fn
+    -> Int         -- ^ position
+    -> OccName     -- ^ thing to check ancestry
+    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
+                   -- just false if it's a descendent
+                   -- otherwise nothing
+hasPositionalAncestry jdg defn n name
+  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
+  = case name == ancestor of
+      True  -> Just True
+      False -> go ancestor name
+  | otherwise = Nothing
+  where
+    go ancestor who =
+      case M.lookup who $ _jAncestry  jdg of
+        Just parent ->
+          case parent == ancestor of
+            True  -> Just False
+            False -> go ancestor parent
+        Nothing -> Nothing
+
+
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
 recursiveCleanup s =
   let r = head $ ts_recursion_stack s
-   in traceShowId $ case r of
+   in case r of
         True  -> Nothing
         False -> Just NoProgress
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index b7819b33a6..80eafd3e37 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -11,8 +13,9 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
-import           Control.Monad
 import           Control.Monad.Except (throwError)
+import           Control.Monad.Reader (asks)
+import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
 import           Data.Function
@@ -37,7 +40,6 @@ import           TcType
 import           Type hiding (Var)
 
 
-
 ------------------------------------------------------------------------------
 -- | Use something in the hypothesis to fill the hole.
 assumption :: TacticsM ()
@@ -49,26 +51,41 @@ assumption = attemptOn allNames assume
 assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
+  defn <- asks extremelyStupid__definingFunction
   case M.lookup name $ jHypothesis jdg of
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
-          when (M.member name $ jPatHypothesis jdg) $ do
-            traceM $ "!!!simpler: " <> show name
-            setRecursionFrameData True
+          case _jCurrentPosition jdg of
+            -- If we have a current position (ie, we are in the context of
+            -- a recursive call):
+            Just pos ->
+              case hasPositionalAncestry jdg defn pos name of
+                -- If we are original arg, we're allowed to proceed.
+                Just True -> pure ()
+                -- If we are a descendent of the original arg, we are
+                -- guaranteed to be structurally smaller, and thus the
+                -- recursion won't be bottom.
+                Just False -> setRecursionFrameData True
+                -- Otherwise it doesn't make sense to use this variable,
+                -- because it is unrelated to the current argument in the
+                -- recursive call.
+                Nothing -> throwError $ RecursionOnWrongParam defn pos name
+            Nothing -> pure ()
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
+
 recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
     filterT recursiveCleanup (withRecursionStack tail) $ do
-      localTactic (apply' name) $ introducing defs
+      localTactic (apply' withCurrentPosition name) $ introducing defs
       assumption
 
 
@@ -78,11 +95,14 @@ intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
+  ctx <- ask
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intro" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg
+      let jdg' = withPositionMapping ctx vs
+               $ introducing (zip vs $ coerce as)
+               $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
       sg <- newSubgoal jdg'
       pure
@@ -121,8 +141,12 @@ homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
-apply' :: OccName -> TacticsM ()
-apply' func = do
+apply :: OccName -> TacticsM ()
+apply = apply' (const id)
+
+
+apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
+apply' f func = do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg
@@ -131,11 +155,13 @@ apply' func = do
           let (args, ret) = splitFunTys ty
           unify g (CType ret)
           useOccName jdg func
-          sgs <- traverse ( newSubgoal
+          sgs <- traverse ( \(i, t) ->
+                            newSubgoal
+                          . f i
                           . blacklistingDestruct
                           . flip withNewGoal jdg
-                          . CType
-                          ) args
+                          $ CType t
+                          ) $ zip [0..] args
           pure . noLoc
               . foldl' (@@) (var' func)
               $ fmap unLoc sgs
@@ -204,7 +230,7 @@ auto' n = do
   try intros
   choice
     [ attemptOn functionNames $ \fname -> do
-        apply' fname
+        apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
         progress ((==) `on` jGoal) NoProgress (destruct aname)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 99a05af917..8f4d805760 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -104,6 +104,7 @@ data Judgement' a = Judgement
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
   , _jAncestry     :: !(Map OccName OccName)
+  , _jCurrentPosition :: Maybe Int
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)
@@ -131,6 +132,7 @@ data TacticError
   | NoApplicableTactic
   | AlreadyDestructed OccName
   | IncorrectDataCon DataCon
+  | RecursionOnWrongParam OccName Int OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -160,6 +162,9 @@ instance Show TacticError where
       "Already destructed " <> unsafeRender name
     show (IncorrectDataCon dcon) =
       "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"
+    show (RecursionOnWrongParam call p arg) =
+      "Recursion on wrong param (" <> show call <> ") on arg"
+        <> show p <> ": " <> show arg
 
 
 ------------------------------------------------------------------------------

From 60ebb744ca9f31ad4c19a7dead4ecff6b57b7af4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 20:36:06 -0700
Subject: [PATCH 14/61] almost generate fmap for binary tree

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 2 +-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 5a7378888e..35d50c2cf8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -70,7 +70,7 @@ runTactic ctx jdg t =
           . flip runReader ctx
           . unExtractM
           $ runTacticTWithState t jdg tacticState of
-      (errs, []) -> Left $ errs
+      (errs, []) -> Left $ take 50 $ errs
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 80eafd3e37..69290d9361 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -59,7 +59,7 @@ assume name = rule $ \jdg -> do
           case _jCurrentPosition jdg of
             -- If we have a current position (ie, we are in the context of
             -- a recursive call):
-            Just pos ->
+            Just pos -> do
               case hasPositionalAncestry jdg defn pos name of
                 -- If we are original arg, we're allowed to proceed.
                 Just True -> pure ()
@@ -220,7 +220,7 @@ auto = do
   jdg <- goal
   traceM $ mappend "!!!auto current:" $ show current
   traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 5) $ disallowing $ fmap fst current
+  localTactic (auto' 4) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()

From 9714f7ecb4acb367c329b24718474bfd406cf659 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 21:03:24 -0700
Subject: [PATCH 15/61] timeout tactic if it's too slow

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs | 36 +++++++++++++++---------
 1 file changed, 22 insertions(+), 14 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 199cc1a609..52b64bb8b1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
@@ -50,6 +51,7 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           System.Timeout
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -266,20 +268,26 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        case runTactic ctx jdg
-              $ tac
-              $ mkVarOcc
-              $ T.unpack var_name of
-          Left err ->
-            pure $ (, Nothing)
-              $ Left
-              $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-          Right res -> do
-            let g = graft (RealSrcSpan span) res
-                response = transform dflags (clientCapabilities lf) uri g pm
-            pure $ case response of
-               Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
-               Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        x <- lift $ timeout 2e6 $
+          case runTactic ctx jdg
+                $ tac
+                $ mkVarOcc
+                $ T.unpack var_name of
+            Left err ->
+              pure $ (, Nothing)
+                $ Left
+                $ ResponseError InvalidRequest (T.pack $ show err) Nothing
+            Right res -> do
+              let g = graft (RealSrcSpan span) res
+                  response = transform dflags (clientCapabilities lf) uri g pm
+              pure $ case response of
+                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        pure $ case x of
+          Just y -> y
+          Nothing -> (, Nothing)
+                   $ Left
+                   $ ResponseError InvalidRequest "timed out" Nothing
 tacticCmd _ _ _ _ =
   pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
        , Nothing

From 3ac43d862f611a7c9ba0219a269ba2b656fcfc79 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 11:51:00 -0700
Subject: [PATCH 16/61] Simpler recursive hypothesis

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  1 +
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 31 +++++++++++++++++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 27 ----------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 25 +++------------
 4 files changed, 37 insertions(+), 47 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 3557e290c0..becb2690a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -127,3 +127,4 @@ var' = var . fromString . occNameString
 -- | Like 'bvar', but works over standard GHC 'OccName's.
 bvar' :: BVar a => OccName -> a
 bvar' = bvar . fromString . occNameString
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 8a9c005d9b..f1f7411033 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -59,6 +59,37 @@ introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+filterPosition :: OccName -> Int -> Judgement -> Judgement
+filterPosition defn pos jdg =
+    withHypothesis (M.filterWithKey go) jdg
+  where
+    go name _ = isJust $ hasPositionalAncestry jdg defn pos name
+
+--------------------------------------------------------------------------------
+-- TODO(sandy): this is probably the worst function I've ever written; sorry
+hasPositionalAncestry
+    :: Judgement
+    -> OccName     -- ^ defining fn
+    -> Int         -- ^ position
+    -> OccName     -- ^ thing to check ancestry
+    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
+                   -- just false if it's a descendent
+                   -- otherwise nothing
+hasPositionalAncestry jdg defn n name
+  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
+  = case name == ancestor of
+      True  -> Just True
+      False -> go ancestor name
+  | otherwise = Nothing
+  where
+    go ancestor who =
+      case M.lookup who $ _jAncestry  jdg of
+        Just parent ->
+          case parent == ancestor of
+            True  -> Just False
+            False -> go ancestor parent
+        Nothing -> Nothing
+
 
 setParents
     :: OccName    -- ^ parent
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 35d50c2cf8..51530bac25 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,7 +18,6 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
-import           Control.Lens hiding (Context, matching, Empty)
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State (MonadState(..))
@@ -26,7 +25,6 @@ import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
-import qualified Data.Map as M
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -81,31 +79,6 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
---------------------------------------------------------------------------------
--- TODO(sandy): this is probably the worst function I've ever written; sorry
-hasPositionalAncestry
-    :: Judgement
-    -> OccName     -- ^ defining fn
-    -> Int         -- ^ position
-    -> OccName     -- ^ thing to check ancestry
-    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
-                   -- just false if it's a descendent
-                   -- otherwise nothing
-hasPositionalAncestry jdg defn n name
-  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
-  = case name == ancestor of
-      True  -> Just True
-      False -> go ancestor name
-  | otherwise = Nothing
-  where
-    go ancestor who =
-      case M.lookup who $ _jAncestry  jdg of
-        Just parent ->
-          case parent == ancestor of
-            True  -> Just False
-            False -> go ancestor parent
-        Nothing -> Nothing
-
 
 recursiveCleanup
     :: TacticState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 69290d9361..04b19263ca 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -14,7 +14,6 @@ module Ide.Plugin.Tactic.Tactics
   ) where
 
 import           Control.Monad.Except (throwError)
-import           Control.Monad.Reader (asks)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
@@ -51,27 +50,13 @@ assumption = attemptOn allNames assume
 assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
-  defn <- asks extremelyStupid__definingFunction
   case M.lookup name $ jHypothesis jdg of
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
-          case _jCurrentPosition jdg of
-            -- If we have a current position (ie, we are in the context of
-            -- a recursive call):
-            Just pos -> do
-              case hasPositionalAncestry jdg defn pos name of
-                -- If we are original arg, we're allowed to proceed.
-                Just True -> pure ()
-                -- If we are a descendent of the original arg, we are
-                -- guaranteed to be structurally smaller, and thus the
-                -- recursion won't be bottom.
-                Just False -> setRecursionFrameData True
-                -- Otherwise it doesn't make sense to use this variable,
-                -- because it is unrelated to the current argument in the
-                -- recursive call.
-                Nothing -> throwError $ RecursionOnWrongParam defn pos name
-            Nothing -> pure ()
+          case M.member name (jPatHypothesis jdg) of
+            True  -> setRecursionFrameData True
+            False -> pure ()
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
@@ -85,8 +70,8 @@ recursion = do
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
     filterT recursiveCleanup (withRecursionStack tail) $ do
-      localTactic (apply' withCurrentPosition name) $ introducing defs
-      assumption
+      (localTactic (apply' (const id) name) $ introducing defs)
+        <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
 ------------------------------------------------------------------------------

From 89a488aca78e4a5f708b9bbd4e3c470263792e7e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 11:53:36 -0700
Subject: [PATCH 17/61] Remove current position from jdg

---
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 19 ++++++-------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  1 -
 3 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index f1f7411033..fe1936e9b2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -108,15 +108,13 @@ setParents p cs =
 -- in and of itself (see the note there.) Additionally, this doesn't check to
 -- make sure we're in the top-level scope, so it will set the recursive
 -- position mapping any time 'intros' is called.
-withPositionMapping :: Context -> [OccName] -> Judgement -> Judgement
-withPositionMapping ctx names j =
-  case M.member  defining (_jPositionMaps j) of
+withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
+withPositionMapping defn names j =
+  case M.member defn (_jPositionMaps j) of
     True  -> j
     False ->
-      traceX "withPositionMapping hack" (defining, names)
-        $ j & field @"_jPositionMaps" . at defining ?~ names
-  where
-    defining = extremelyStupid__definingFunction ctx
+      traceX "withPositionMapping hack" (defn, names)
+        $ j & field @"_jPositionMaps" . at defn ?~ names
 
 
 ------------------------------------------------------------------------------
@@ -130,11 +128,6 @@ extremelyStupid__definingFunction =
   fst . head . ctxDefiningFuncs
 
 
-withCurrentPosition :: Int -> Judgement -> Judgement
-withCurrentPosition i =
-  field @"_jCurrentPosition" ?~ i
-
-
 withHypothesis
     :: (Map OccName a -> Map OccName a)
     -> Judgement' a
@@ -174,5 +167,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty Nothing . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 04b19263ca..928828d513 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -85,7 +85,7 @@ intros = rule $ \jdg -> do
     ([], _) -> throwError $ GoalMismatch "intro" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = withPositionMapping ctx vs
+      let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
                $ introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 8f4d805760..7ba39ef2b4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -104,7 +104,6 @@ data Judgement' a = Judgement
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
   , _jAncestry     :: !(Map OccName OccName)
-  , _jCurrentPosition :: Maybe Int
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From c774fe190c1b79c9edd296195dfcea0f7a08c14a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 12:09:26 -0700
Subject: [PATCH 18/61] Restrict homomorphic splits to positional args

---
 plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs    | 13 +++++++++----
 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 13 ++++++-------
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs    |  7 +++++++
 test/functional/Tactic.hs                           |  2 ++
 test/testdata/tactic/GoldenFmapTree.hs              |  4 ++++
 test/testdata/tactic/GoldenFmapTree.hs.expected     |  7 +++++++
 test/testdata/tactic/GoldenSwap.hs                  |  2 ++
 test/testdata/tactic/GoldenSwap.hs.expected         |  2 ++
 8 files changed, 39 insertions(+), 11 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFmapTree.hs
 create mode 100644 test/testdata/tactic/GoldenFmapTree.hs.expected
 create mode 100644 test/testdata/tactic/GoldenSwap.hs
 create mode 100644 test/testdata/tactic/GoldenSwap.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index becb2690a6..191b4e7c3b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -52,11 +52,13 @@ destructMatches f f2 t jdg = do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
+              dcon_name = nameOccName $ dataConName dc
 
           let pat :: Pat GhcPs
-              pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
+              pat = conP (fromString $ occNameString dcon_name)
                   $ fmap bvar' names
               j = f2 hy'
+                $ withPositionMapping dcon_name names
                 $ introducingPat hy'
                 $ withNewGoal g jdg
           sg <- f dc j
@@ -106,11 +108,14 @@ buildDataCon
     -> RuleM (LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
-  sgs <- traverse ( newSubgoal
+      dcon_name = nameOccName $ dataConName dc
+  sgs <- traverse ( \(arg, n) ->
+                    newSubgoal
+                  . filterSameTypeFromOtherPositions dcon_name n
                   . blacklistingDestruct
                   . flip withNewGoal jdg
-                  . CType
-                  ) args
+                  $ CType arg
+                  ) $ zip args [0..]
   pure
     . noLoc
     . foldl' (@@)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index fe1936e9b2..5a3a6a11d8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -65,6 +65,12 @@ filterPosition defn pos jdg =
   where
     go name _ = isJust $ hasPositionalAncestry jdg defn pos name
 
+filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement
+filterSameTypeFromOtherPositions defn pos jdg =
+  let hy = jHypothesis $ filterPosition defn pos jdg
+      tys = S.fromList $ fmap snd $ M.toList hy
+   in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg
+
 --------------------------------------------------------------------------------
 -- TODO(sandy): this is probably the worst function I've ever written; sorry
 hasPositionalAncestry
@@ -101,13 +107,6 @@ setParents p cs =
 
 
 
-------------------------------------------------------------------------------
--- TODO(sandy): THIS THING IS A BIG BIG HACK
---
--- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
--- in and of itself (see the note there.) Additionally, this doesn't check to
--- make sure we're in the top-level scope, so it will set the recursive
--- position mapping any time 'intros' is called.
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
 withPositionMapping defn names j =
   case M.member defn (_jPositionMaps j) of
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 928828d513..e952c1ac41 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -76,6 +76,13 @@ recursion = do
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
+--
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
+-- in and of itself (see the note there.) Additionally, this doesn't check to
+-- make sure we're in the top-level scope, so it will set the recursive
+-- position mapping any time 'intros' is called.
 intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index f11717209e..5b5a6b4154 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -96,6 +96,8 @@ tests = testGroup
   , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
   , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
   , goldenTest "GoldenFoldr.hs"             2 10 Auto ""
+  , goldenTest "GoldenSwap.hs"              2 8  Auto ""
+  , goldenTest "GoldenFmapTree.hs"          4 11 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFmapTree.hs b/test/testdata/tactic/GoldenFmapTree.hs
new file mode 100644
index 0000000000..679e7902df
--- /dev/null
+++ b/test/testdata/tactic/GoldenFmapTree.hs
@@ -0,0 +1,4 @@
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+instance Functor Tree where
+   fmap = _
diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected
new file mode 100644
index 0000000000..4e8b97d735
--- /dev/null
+++ b/test/testdata/tactic/GoldenFmapTree.hs.expected
@@ -0,0 +1,7 @@
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+instance Functor Tree where
+   fmap = (\ fab ta
+      -> case ta of
+           (Leaf a) -> Leaf (fab a)
+           (Branch ta2 ta3) -> Branch (fmap fab ta2) (fmap fab ta3))
diff --git a/test/testdata/tactic/GoldenSwap.hs b/test/testdata/tactic/GoldenSwap.hs
new file mode 100644
index 0000000000..9243955c54
--- /dev/null
+++ b/test/testdata/tactic/GoldenSwap.hs
@@ -0,0 +1,2 @@
+swap :: (a, b) -> (b, a)
+swap = _
diff --git a/test/testdata/tactic/GoldenSwap.hs.expected b/test/testdata/tactic/GoldenSwap.hs.expected
new file mode 100644
index 0000000000..4281fc81d9
--- /dev/null
+++ b/test/testdata/tactic/GoldenSwap.hs.expected
@@ -0,0 +1,2 @@
+swap :: (a, b) -> (b, a)
+swap = (\ p_ab -> case p_ab of { ((,) a b) -> (,) b a })

From 4b682a265815f9e1c5954d7aec14b8b5caf7e7d0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 12:49:54 -0700
Subject: [PATCH 19/61] Silence a trace

---
 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 5a3a6a11d8..d5e5efa78a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -111,9 +111,7 @@ withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
 withPositionMapping defn names j =
   case M.member defn (_jPositionMaps j) of
     True  -> j
-    False ->
-      traceX "withPositionMapping hack" (defn, names)
-        $ j & field @"_jPositionMaps" . at defn ?~ names
+    False -> j & field @"_jPositionMaps" . at defn ?~ names
 
 
 ------------------------------------------------------------------------------

From ab2e592ee7f290674de45917144c94b6ccbe4907 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 10:12:13 -0700
Subject: [PATCH 20/61] Better data provenance

(thanks to @i-am-tom for the idea!)
---
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 38 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  2 +-
 2 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index d5e5efa78a..f03adb169a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -6,9 +6,11 @@
 
 module Ide.Plugin.Tactic.Judgements where
 
-import Control.Lens hiding (Context)
+import           Control.Lens hiding (Context)
+import           Data.Bool
 import           Data.Char
 import           Data.Coerce
+import           Data.Generics.Product (field)
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -18,7 +20,6 @@ import           Ide.Plugin.Tactic.Types
 import           OccName
 import           SrcLoc
 import           Type
-import Data.Generics.Product (field)
 
 
 ------------------------------------------------------------------------------
@@ -42,37 +43,43 @@ buildHypothesis
 hasDestructed :: Judgement -> OccName -> Bool
 hasDestructed j n = S.member n $ _jDestructed j
 
+
 destructing :: OccName -> Judgement -> Judgement
 destructing n = field @"_jDestructed" <>~ S.singleton n
 
+
 blacklistingDestruct :: Judgement -> Judgement
 blacklistingDestruct =
   field @"_jBlacklistDestruct" .~ True
 
+
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
+
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+
 filterPosition :: OccName -> Int -> Judgement -> Judgement
 filterPosition defn pos jdg =
     withHypothesis (M.filterWithKey go) jdg
   where
     go name _ = isJust $ hasPositionalAncestry jdg defn pos name
 
+
 filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement
 filterSameTypeFromOtherPositions defn pos jdg =
   let hy = jHypothesis $ filterPosition defn pos jdg
       tys = S.fromList $ fmap snd $ M.toList hy
    in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg
 
---------------------------------------------------------------------------------
--- TODO(sandy): this is probably the worst function I've ever written; sorry
+
 hasPositionalAncestry
     :: Judgement
     -> OccName     -- ^ defining fn
@@ -85,16 +92,12 @@ hasPositionalAncestry jdg defn n name
   | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
   = case name == ancestor of
       True  -> Just True
-      False -> go ancestor name
+      False ->
+        case M.lookup name $ _jAncestry jdg of
+          Just ancestry ->
+            bool Nothing (Just False) $ S.member ancestor ancestry
+          Nothing -> Nothing
   | otherwise = Nothing
-  where
-    go ancestor who =
-      case M.lookup who $ _jAncestry  jdg of
-        Just parent ->
-          case parent == ancestor of
-            True  -> Just False
-            False -> go ancestor parent
-        Nothing -> Nothing
 
 
 setParents
@@ -102,9 +105,12 @@ setParents
     -> [OccName]  -- ^ children
     -> Judgement
     -> Judgement
-setParents p cs =
-  field @"_jAncestry" <>~ M.fromList (fmap (, p) cs)
-
+setParents p cs jdg =
+  let ancestry = mappend (S.singleton p)
+               $ fromMaybe mempty
+               $ M.lookup p
+               $ _jAncestry jdg
+   in jdg & field @"_jAncestry" <>~ M.fromList (fmap (, ancestry) cs)
 
 
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 7ba39ef2b4..3ff4be9799 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -103,7 +103,7 @@ data Judgement' a = Judgement
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
-  , _jAncestry     :: !(Map OccName OccName)
+  , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From 5ddd36013226ed091d3b3e7150dc7d2ed064ecdd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 11:57:37 -0700
Subject: [PATCH 21/61] Support multiple positional binding sets

---
 plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs   |  4 ++++
 .../tactics/src/Ide/Plugin/Tactic/Judgements.hs  | 16 +++++++++-------
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs   |  2 +-
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index 20acfc58ab..ba91a7c1cb 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -5,6 +5,7 @@ module Ide.Plugin.Tactic.Debug
   , traceShowId
   , trace
   , traceX
+  , traceIdX
   , traceMX
   ) where
 
@@ -26,3 +27,6 @@ traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
 traceX :: (Show a) => String -> a -> b -> b
 traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
 
+traceIdX :: (Show a) => String -> a -> a
+traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index f03adb169a..90d3f0ddb3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -89,15 +89,19 @@ hasPositionalAncestry
                    -- just false if it's a descendent
                    -- otherwise nothing
 hasPositionalAncestry jdg defn n name
-  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
-  = case name == ancestor of
+  | not $ null ancestors
+  = case any (== name) ancestors of
       True  -> Just True
       False ->
         case M.lookup name $ _jAncestry jdg of
           Just ancestry ->
-            bool Nothing (Just False) $ S.member ancestor ancestry
+            bool Nothing (Just False) $ any (flip S.member ancestry) ancestors
           Nothing -> Nothing
   | otherwise = Nothing
+  where
+    ancestors = toListOf (_Just . traversed . ix n)
+              $ M.lookup defn
+              $ _jPositionMaps jdg
 
 
 setParents
@@ -114,10 +118,8 @@ setParents p cs jdg =
 
 
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
-withPositionMapping defn names j =
-  case M.member defn (_jPositionMaps j) of
-    True  -> j
-    False -> j & field @"_jPositionMaps" . at defn ?~ names
+withPositionMapping defn names =
+  field @"_jPositionMaps" . at defn <>~ Just [names]
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 3ff4be9799..e04815ac16 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -102,7 +102,7 @@ data Judgement' a = Judgement
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
-  , _jPositionMaps :: !(Map OccName [OccName])
+  , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
   }

From a3dc93532571820786095a814a2907bde6075f6b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 13:01:02 -0700
Subject: [PATCH 22/61] Prune destructing on pattern vals if they don't
 introduce new types

(thanks to @Lysxia for the insight)
---
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  4 ++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 21 ++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 22 ++++++++++++++++++-
 3 files changed, 46 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 90d3f0ddb3..2b45e40a8f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -157,6 +157,10 @@ jHypothesis :: Judgement' a -> Map OccName a
 jHypothesis = _jHypothesis
 
 
+isPatVal :: Judgement' a -> OccName -> Bool
+isPatVal j n = S.member n $ _jPatternVals j
+
+
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
 jPatHypothesis :: Judgement' a -> Map OccName a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 51530bac25..9f14cc1856 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -107,6 +107,27 @@ filterT p f t = check >> t
             Nothing -> pure e
 
 
+gather
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m a
+    -> ([(a, jdg)] -> TacticT jdg ext err s m a)
+    -> TacticT jdg ext err s m a
+gather t f = tactic $ \j -> do
+    s <- get
+    results <- lift $ proofs s $ proofState t j
+    msum $ flip fmap results $ \case
+        Left err -> throwError err
+        Right (_, jdgs) -> proofState (f jdgs) j
+
+
+pruning
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m ()
+    -> ([jdg] -> Maybe err)
+    -> TacticT jdg ext err s m ()
+pruning t p = gather t (maybe (pure ()) throwError . p . fmap snd)
+
+
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e952c1ac41..e944a2d681 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -103,6 +103,26 @@ intros = rule $ \jdg -> do
         $ unLoc sg
 
 
+------------------------------------------------------------------------------
+-- | Case split, and leave holes in the matches.
+destructAuto :: OccName -> TacticsM ()
+destructAuto name = do
+  jdg <- goal
+  case hasDestructed jdg name of
+    True -> throwError $ AlreadyDestructed name
+    False ->
+      let subtactic = rule $ destruct' (const subgoal) name
+       in case isPatVal jdg name of
+            True  ->
+              pruning subtactic $ \jdgs ->
+                let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis
+                    new_hy = foldMap getHyTypes jdgs
+                    old_hy = getHyTypes jdg
+                 in case S.null (traceIdX "newly introduced bindings" $ new_hy S.\\old_hy) of
+                      True  -> Just NoProgress
+                      False -> Nothing
+            False -> subtactic
+
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: OccName -> TacticsM ()
@@ -225,7 +245,7 @@ auto' n = do
         apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
-        progress ((==) `on` jGoal) NoProgress (destruct aname)
+        progress ((==) `on` jGoal) NoProgress (destructAuto aname)
         loop
     , split >> loop
     , assumption >> loop

From abd365fdcf4e39ba8f1f78901ae6cf654353e7a1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:15:02 -0700
Subject: [PATCH 23/61] Fix pruning to actually run the tactic

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 2 +-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 9 ++++-----
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs     | 3 +++
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 9f14cc1856..254ef19ccd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -125,7 +125,7 @@ pruning
     => TacticT jdg ext err s m ()
     -> ([jdg] -> Maybe err)
     -> TacticT jdg ext err s m ()
-pruning t p = gather t (maybe (pure ()) throwError . p . fmap snd)
+pruning t p = gather t $ maybe t throwError . p . fmap snd
 
 
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e944a2d681..81689857e0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -17,7 +17,6 @@ import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
-import           Data.Function
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
@@ -113,13 +112,13 @@ destructAuto name = do
     False ->
       let subtactic = rule $ destruct' (const subgoal) name
        in case isPatVal jdg name of
-            True  ->
+            True ->
               pruning subtactic $ \jdgs ->
                 let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis
                     new_hy = foldMap getHyTypes jdgs
                     old_hy = getHyTypes jdg
-                 in case S.null (traceIdX "newly introduced bindings" $ new_hy S.\\old_hy) of
-                      True  -> Just NoProgress
+                 in case S.null $ new_hy S.\\ old_hy of
+                      True  -> Just $ UnhelpfulDestruct name
                       False -> Nothing
             False -> subtactic
 
@@ -245,7 +244,7 @@ auto' n = do
         apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
-        progress ((==) `on` jGoal) NoProgress (destructAuto aname)
+        destructAuto aname
         loop
     , split >> loop
     , assumption >> loop
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index e04815ac16..c7d722f5e4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -132,6 +132,7 @@ data TacticError
   | AlreadyDestructed OccName
   | IncorrectDataCon DataCon
   | RecursionOnWrongParam OccName Int OccName
+  | UnhelpfulDestruct OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -164,6 +165,8 @@ instance Show TacticError where
     show (RecursionOnWrongParam call p arg) =
       "Recursion on wrong param (" <> show call <> ") on arg"
         <> show p <> ": " <> show arg
+    show (UnhelpfulDestruct n) =
+      "Destructing patval " <> show n <> " leads to no new types"
 
 
 ------------------------------------------------------------------------------

From 8d530324e1b9309301cafd4170c762873e74dbc1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:30:59 -0700
Subject: [PATCH 24/61] Count duplicates

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 13 ++++++++++++-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   |  4 ++--
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 254ef19ccd..73f32f1417 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -24,7 +24,9 @@ import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
-import           Data.List (intercalate, sortBy)
+import           Data.Function (on)
+import           Data.List (groupBy, intercalate, sortBy)
+import           Data.Maybe (listToMaybe, fromMaybe)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -73,6 +75,7 @@ runTactic ctx jdg t =
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
         traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
+        traceMX "duplicates" $ countDuplicates solns
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
@@ -135,6 +138,14 @@ setRecursionFrameData b = do
     []       -> []
 
 
+countDuplicates :: Show a => [a] -> [Int]
+countDuplicates
+    = sortBy (comparing Down)
+    . fmap length
+    . groupBy ((==) `on` show)
+    . sortBy (comparing show)
+
+
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 81689857e0..2d325b76a0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -88,7 +88,7 @@ intros = rule $ \jdg -> do
       g  = jGoal jdg
   ctx <- ask
   case tcSplitFunTys $ unCType g of
-    ([], _) -> throwError $ GoalMismatch "intro" g
+    ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
       let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
@@ -187,7 +187,7 @@ split = do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
-    Nothing -> throwError $ GoalMismatch "getGoalTyCon" g
+    Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs

From b8b0d0dc77ec1ae3f0e823ee7920e2fa1377eb5d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:35:34 -0700
Subject: [PATCH 25/61] ?

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 73f32f1417..b8a160429a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -24,9 +24,7 @@ import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
-import           Data.Function (on)
-import           Data.List (groupBy, intercalate, sortBy)
-import           Data.Maybe (listToMaybe, fromMaybe)
+import           Data.List (intercalate, sortBy)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -75,14 +73,12 @@ runTactic ctx jdg t =
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
         traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
-        traceMX "duplicates" $ countDuplicates solns
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
           _ -> Left []
 
 
-
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
@@ -138,14 +134,6 @@ setRecursionFrameData b = do
     []       -> []
 
 
-countDuplicates :: Show a => [a] -> [Int]
-countDuplicates
-    = sortBy (comparing Down)
-    . fmap length
-    . groupBy ((==) `on` show)
-    . sortBy (comparing show)
-
-
 scoreSolution
     :: TacticState
     -> [Judgement]

From ec13e9fcd43f41f94fdd686e1f34ae8a23420c60 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 23:06:00 -0700
Subject: [PATCH 26/61] Don't allow splitting if it doesn't buy you anything

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  2 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 11 +++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 25 ++++++++++++++++---
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  4 +++
 5 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 52b64bb8b1..d06fb16282 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -268,7 +268,7 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e6 $
+        x <- lift $ timeout 2e8 $
           case runTactic ctx jdg
                 $ tac
                 $ mkVarOcc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 2b45e40a8f..ab152cd7c5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -53,10 +53,19 @@ blacklistingDestruct =
   field @"_jBlacklistDestruct" .~ True
 
 
+unwhitelistingSplit :: Judgement -> Judgement
+unwhitelistingSplit =
+  field @"_jWhitelistSplit" .~ False
+
+
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
 
+isSplitWhitelisted :: Judgement -> Bool
+isSplitWhitelisted = _jWhitelistSplit
+
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
@@ -176,5 +185,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False True mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index b8a160429a..eae8613874 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -72,7 +72,7 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 50 $  fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 2d325b76a0..c5f5ac853e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -36,6 +36,8 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Name (nameOccName)
+import DataCon
 
 
 ------------------------------------------------------------------------------
@@ -192,6 +194,23 @@ split = do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs
 
+------------------------------------------------------------------------------
+-- | Choose between each of the goal's data constructors.
+splitAuto :: TacticsM ()
+splitAuto = do
+  jdg <- goal
+  let g = jGoal jdg
+  case splitTyConApp_maybe $ unCType g of
+    Nothing -> throwError $ GoalMismatch "split" g
+    Just (tc, _) -> do
+      let dcs = tyConDataCons tc
+      case isSplitWhitelisted jdg of
+        True -> choice $ fmap splitDataCon dcs
+        False -> choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+          case any ((/= jGoal jdg)  . jGoal) jdgs of
+            True  -> Nothing
+            False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+
 
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
@@ -201,7 +220,7 @@ splitDataCon dc = rule $ \jdg -> do
   case splitTyConApp_maybe $ unCType g of
     Just (tc, apps) -> do
       case elem dc $ tyConDataCons tc of
-        True -> buildDataCon jdg dc apps
+        True -> buildDataCon (unwhitelistingSplit jdg) dc apps
         False -> throwError $ IncorrectDataCon dc
     Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
@@ -231,7 +250,7 @@ auto = do
   jdg <- goal
   traceM $ mappend "!!!auto current:" $ show current
   traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 4) $ disallowing $ fmap fst current
+  localTactic (auto' 5) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()
@@ -246,7 +265,7 @@ auto' n = do
     , attemptOn algebraicNames $ \aname -> do
         destructAuto aname
         loop
-    , split >> loop
+    , splitAuto >> loop
     , assumption >> loop
     , recursion
     ]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index c7d722f5e4..624ecc9e76 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -102,6 +102,7 @@ data Judgement' a = Judgement
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
+  , _jWhitelistSplit :: !(Bool)
   , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
@@ -133,6 +134,7 @@ data TacticError
   | IncorrectDataCon DataCon
   | RecursionOnWrongParam OccName Int OccName
   | UnhelpfulDestruct OccName
+  | UnhelpfulSplit OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -167,6 +169,8 @@ instance Show TacticError where
         <> show p <> ": " <> show arg
     show (UnhelpfulDestruct n) =
       "Destructing patval " <> show n <> " leads to no new types"
+    show (UnhelpfulSplit n) =
+      "Splitting constructor " <> show n <> " leads to no new goals"
 
 
 ------------------------------------------------------------------------------

From 683c7914e937ba3d9258486e102b92b36fa4be7c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 8 Oct 2020 10:33:32 -0700
Subject: [PATCH 27/61] Known fmap strategy

---
 haskell-language-server.cabal                 |  2 +
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  1 +
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs | 18 +++++++++
 .../src/Ide/Plugin/Tactic/KnownStrategies.hs  | 37 +++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 34 ++++++-----------
 5 files changed, 69 insertions(+), 23 deletions(-)
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index dfdf0789b3..4cca9280fd 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -93,11 +93,13 @@ executable haskell-language-server
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
     Ide.Plugin.Tactic
+    Ide.Plugin.Tactic.Auto
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.Context
     Ide.Plugin.Tactic.Debug
     Ide.Plugin.Tactic.GHC
     Ide.Plugin.Tactic.Judgements
+    Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.Machinery
     Ide.Plugin.Tactic.Naming
     Ide.Plugin.Tactic.Range
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index d06fb16282..2d1dc085c4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -39,6 +39,7 @@ import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin (mkLspCommand)
+import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
new file mode 100644
index 0000000000..40ff05b089
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -0,0 +1,18 @@
+module Ide.Plugin.Tactic.Auto where
+
+import Control.Applicative
+import Ide.Plugin.Tactic.Context
+import Ide.Plugin.Tactic.Judgements
+import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+
+
+------------------------------------------------------------------------------
+-- | Automatically solve a goal.
+auto :: TacticsM ()
+auto = do
+  current <- getCurrentDefinitions
+  knownStrategies
+    <|> (localTactic (auto' 4) $ disallowing $ fmap fst current)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
new file mode 100644
index 0000000000..0855cd97e8
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Ide.Plugin.Tactic.KnownStrategies where
+
+import Control.Monad.Error.Class
+import Ide.Plugin.Tactic.Context (getCurrentDefinitions)
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+import OccName (mkVarOcc)
+import Refinery.Tactic
+
+
+knownStrategies :: TacticsM ()
+knownStrategies = choice
+  [ deriveFmap
+  ]
+
+
+known :: String -> TacticsM () -> TacticsM ()
+known name t = do
+  getCurrentDefinitions >>= \case
+    [(def, _)] | def == mkVarOcc name -> do
+      traceMX "running known strategy" name
+      t
+    _ -> throwError NoApplicableTactic
+
+
+deriveFmap :: TacticsM ()
+deriveFmap = known "fmap" $ do
+  try intros
+  overAlgebraicTerms homo
+  choice
+    [ overFunctions apply >> auto' 2
+    , assumption
+    , recursion
+    ]
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index c5f5ac853e..7ea75eb1fb 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -21,6 +21,7 @@ import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
 import qualified Data.Set as S
+import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
 import           GHC.SourceGen.Expr
@@ -32,12 +33,11 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
+import           Name (nameOccName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Name (nameOccName)
-import DataCon
 
 
 ------------------------------------------------------------------------------
@@ -242,27 +242,16 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
-------------------------------------------------------------------------------
--- | Automatically solve a goal.
-auto :: TacticsM ()
-auto = do
-  current <- getCurrentDefinitions
-  jdg <- goal
-  traceM $ mappend "!!!auto current:" $ show current
-  traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 5) $ disallowing $ fmap fst current
-
-
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
   try intros
   choice
-    [ attemptOn functionNames $ \fname -> do
+    [ overFunctions $ \fname -> do
         apply fname
         loop
-    , attemptOn algebraicNames $ \aname -> do
+    , overAlgebraicTerms $ \aname -> do
         destructAuto aname
         loop
     , splitAuto >> loop
@@ -270,15 +259,14 @@ auto' n = do
     , recursion
     ]
 
+overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
+overFunctions =
+  attemptOn $ M.keys . M.filter (isFunction . unCType) . jHypothesis
 
-functionNames :: Judgement -> [OccName]
-functionNames  =
-  M.keys . M.filter (isFunction . unCType) . jHypothesis
-
-
-algebraicNames :: Judgement -> [OccName]
-algebraicNames =
-  M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
+overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
+overAlgebraicTerms =
+  attemptOn $
+    M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
 
 
 allNames :: Judgement -> [OccName]

From 4114d03aa9aba971f0ec962c6aad34832029b746 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 13:19:19 -0700
Subject: [PATCH 28/61] Commit to a known solution if one exists

---
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs      | 8 ++++++--
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 3 +++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 40ff05b089..6a51601a39 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -6,13 +6,17 @@ import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
+import Refinery.Tactic
 
 
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
 auto = do
+  jdg <- goal
   current <- getCurrentDefinitions
-  knownStrategies
-    <|> (localTactic (auto' 4) $ disallowing $ fmap fst current)
+  traceMX "goal" jdg
+  commit
+    knownStrategies
+    (localTactic (auto' 4) $ disallowing $ fmap fst current)
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index eae8613874..04e1cf4cac 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -182,6 +182,9 @@ proofs' s p = go s [] p
           in go s' goals p
       go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
       go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
+      go s goals (Commit p1 p2) = go s goals p1 >>= \case
+          (rights -> []) -> go s goals p2
+          solns -> pure solns
       go _ _ Empty = pure []
       go _ _ (Failure err) = pure [throwError err]
       go s goals (Axiom ext) = pure [Right (ext, (s, goals))]

From 6ff650473d56d5298f8825f6e878c13111e6ea39 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:12:15 -0700
Subject: [PATCH 29/61] Compute top level position vals

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs | 45 ++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 2d1dc085c4..06782e36d8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -21,8 +21,12 @@ import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
+import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
+import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
@@ -52,6 +56,7 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           SrcLoc (containsSpan)
 import           System.Timeout
 
 
@@ -252,6 +257,7 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  traceMX "holes!" $ isRhsHole rss $ tm_typechecked_source $ tmrModule tcmod
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
@@ -301,3 +307,42 @@ fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
+
+------------------------------------------------------------------------------
+-- | Compute top-level position vals of a function
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
+isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
+  (Match _
+      (FunRhs (L _ name) _ _)         -- function name
+      ps                              -- patterns
+      (GRHSs _
+        [L _ (GRHS _ []
+               (L (RealSrcSpan span)  -- body with no guards and a single defn
+                  (HsVar _ (L _ hole))))] _)
+          :: Match GhcTc (LHsExpr GhcTc))
+    | containsSpan span rss           -- which contains our span
+    , isHole $ occName hole           -- and the span is a hole
+    -> First $ do
+        patnames <- traverse getPatName ps
+        pure (occName name, patnames)
+  _ -> mempty
+  ) tcs
+
+
+-- TODO(sandy): Make this more robust
+isHole :: OccName -> Bool
+isHole = isPrefixOf "_" . occNameString
+
+
+getPatName :: Pat GhcTc -> Maybe OccName
+getPatName = \case
+   VarPat _ x    -> Just $ occName $ unLoc x
+   LazyPat _ p   -> getPatName p
+   AsPat _ x _   -> Just $ occName $ unLoc x
+   ParPat _ p    -> getPatName p
+   BangPat _ p   -> getPatName p
+   ViewPat _ _ p -> getPatName p
+   SigPat _ p _  -> getPatName p
+   XPat p        -> getPatName $ unLoc p
+   _             -> Nothing
+

From 29858b0bab568237a603d74c5f8eb9613303f775 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:30:01 -0700
Subject: [PATCH 30/61] Add tophole to jdg

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 56 ++++++++++++++-----
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs |  1 -
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 19 ++++++-
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  1 +
 4 files changed, 60 insertions(+), 17 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 06782e36d8..1dbccedfa0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE PatternSynonyms     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeApplications    #-}
@@ -257,14 +258,26 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
-  traceMX "holes!" $ isRhsHole rss $ tm_typechecked_source $ tmrModule tcmod
+  -- traceMX "holes!" $ isRhsHole rss $
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
+      tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
               tcg
       hyps = hypothesisFromBindings rss binds
-  pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags)
+  pure ( resulting_range
+       , mkFirstJudgement
+           hyps
+           (isRhsHole rss tcs)
+           (maybe
+              mempty
+              (uncurry M.singleton . fmap pure)
+                $ getRhsPosVals rss tcs)
+           goal
+       , ctx
+       , dflags
+       )
 
 
 
@@ -308,20 +321,24 @@ liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
 
+------------------------------------------------------------------------------
+-- | Is this hole immediately to the right of an equals sign?
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
+isRhsHole rss tcs = everything (||) (mkQ False $ \case
+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span
+  _ -> False
+  ) tcs
+
+
 ------------------------------------------------------------------------------
 -- | Compute top-level position vals of a function
-isRhsHole :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
-isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
-  (Match _
-      (FunRhs (L _ name) _ _)         -- function name
-      ps                              -- patterns
-      (GRHSs _
-        [L _ (GRHS _ []
-               (L (RealSrcSpan span)  -- body with no guards and a single defn
-                  (HsVar _ (L _ hole))))] _)
-          :: Match GhcTc (LHsExpr GhcTc))
-    | containsSpan span rss           -- which contains our span
-    , isHole $ occName hole           -- and the span is a hole
+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
+getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
+  TopLevelRHS name ps
+      (L (RealSrcSpan span)  -- body with no guards and a single defn
+         (HsVar _ (L _ hole)))
+    | containsSpan rss span  -- which contains our span
+    , isHole $ occName hole  -- and the span is a hole
     -> First $ do
         patnames <- traverse getPatName ps
         pure (occName name, patnames)
@@ -329,6 +346,17 @@ isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
   ) tcs
 
 
+------------------------------------------------------------------------------
+-- | Should make sure it's a fun bind
+pattern TopLevelRHS :: OccName -> [Pat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
+pattern TopLevelRHS name ps body <-
+  Match _
+    (FunRhs (L _ (occName -> name)) _ _)
+    ps
+    (GRHSs _
+      [L _ (GRHS _ [] body)] _)
+
+
 -- TODO(sandy): Make this more robust
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 6a51601a39..4aadd75ee2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -1,6 +1,5 @@
 module Ide.Plugin.Tactic.Auto where
 
-import Control.Applicative
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index ab152cd7c5..57cf95e7ed 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -184,6 +184,21 @@ jGoal = _jGoal
 substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
-mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False True mempty mempty . CType
+mkFirstJudgement
+    :: M.Map OccName CType
+    -> Bool  -- ^ are we in the top level rhs hole?
+    -> M.Map OccName [[OccName]]  -- ^ existing pos vals
+    -> Type
+    -> Judgement' CType
+mkFirstJudgement hy top posvals goal = Judgement
+  { _jHypothesis        = hy
+  , _jDestructed        = mempty
+  , _jPatternVals       = mempty
+  , _jBlacklistDestruct = False
+  , _jWhitelistSplit    = True
+  , _jPositionMaps      = posvals
+  , _jAncestry          = mempty
+  , _jIsTopHole         = top
+  , _jGoal              = CType goal
+  }
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 624ecc9e76..cca6fe8247 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -105,6 +105,7 @@ data Judgement' a = Judgement
   , _jWhitelistSplit :: !(Bool)
   , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
+  , _jIsTopHole    :: !Bool
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From 929bcc94f34791c1f948b4286cfc5335e7a24338 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:36:16 -0700
Subject: [PATCH 31/61] Cleanup ugly hack in intros! \o/

---
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  6 ++++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  4 +++-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 19 +++++++++----------
 3 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 57cf95e7ed..32ad70bc2e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -169,6 +169,12 @@ jHypothesis = _jHypothesis
 isPatVal :: Judgement' a -> OccName -> Bool
 isPatVal j n = S.member n $ _jPatternVals j
 
+isTopHole :: Judgement' a -> Bool
+isTopHole = _jIsTopHole
+
+unsetIsTopHole :: Judgement' a -> Judgement' a
+unsetIsTopHole = field @"_jIsTopHole" .~ False
+
 
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 04e1cf4cac..8228feee00 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -50,7 +50,9 @@ newSubgoal
     -> RuleM (LHsExpr GhcPs)
 newSubgoal j = do
     unifier <- gets ts_unifier
-    subgoal $ substJdg unifier j
+    subgoal
+      $ substJdg unifier
+      $ unsetIsTopHole j
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7ea75eb1fb..2fd8aef1e4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -38,6 +38,7 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Data.Bool (bool)
 
 
 ------------------------------------------------------------------------------
@@ -77,13 +78,6 @@ recursion = do
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
---
--- TODO(sandy): THIS THING IS A BIG BIG HACK
---
--- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
--- in and of itself (see the note there.) Additionally, this doesn't check to
--- make sure we're in the top-level scope, so it will set the recursive
--- position mapping any time 'intros' is called.
 intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
@@ -93,11 +87,16 @@ intros = rule $ \jdg -> do
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
-               $ introducing (zip vs $ coerce as)
+      let jdg' = introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
-      sg <- newSubgoal jdg'
+      sg <- newSubgoal
+          $ bool
+              id
+              (withPositionMapping
+                (extremelyStupid__definingFunction ctx) vs)
+              (isTopHole jdg)
+          $ jdg'
       pure
         . noLoc
         . lambda (fmap bvar' vs)

From 3272a1ea651db264120f7be10ffe0742c3185358 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:50:01 -0700
Subject: [PATCH 32/61] Fix improperly pruning split of split

---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 2fd8aef1e4..4b20cdfb01 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -203,12 +203,18 @@ splitAuto = do
     Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
-      case isSplitWhitelisted jdg of
-        True -> choice $ fmap splitDataCon dcs
-        False -> choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-          case any ((/= jGoal jdg)  . jGoal) jdgs of
-            True  -> Nothing
-            False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+      -- TODO(sandy): Figure out the right strategy for pruning splits of
+      -- splits
+      choice $ fmap splitDataCon dcs
+      -- case isSplitWhitelisted jdg of
+      --   True -> choice $ fmap splitDataCon dcs
+      --   False -> do
+      --     choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+      --       case all ((== jGoal jdg)  . jGoal) jdgs of
+      --         False  -> Nothing
+      --         True -> do
+      --           traceMX "unhelpful split" $ nameOccName $ dataConName dc
+      --           Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From 30c9b580093433bfdc9a2ec671decdc5309de2d2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 00:36:26 -0700
Subject: [PATCH 33/61] Tracing

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  6 +--
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs |  3 +-
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 27 +++++++----
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 20 ++++++++-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 45 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 36 ++++++++++++---
 6 files changed, 98 insertions(+), 39 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 1dbccedfa0..27171fe7fd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -258,7 +258,6 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
-  -- traceMX "holes!" $ isRhsHole rss $
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
@@ -297,9 +296,10 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right res -> do
-              let g = graft (RealSrcSpan span) res
+            Right (tr, ext) -> do
+              let g = graft (RealSrcSpan span) ext
                   response = transform dflags (clientCapabilities lf) uri g pm
+              traceMX "trace" tr
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
                 Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 4aadd75ee2..392bcf3c80 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -3,6 +3,7 @@ module Ide.Plugin.Tactic.Auto where
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Machinery
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import Refinery.Tactic
@@ -11,7 +12,7 @@ import Refinery.Tactic
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
-auto = do
+auto = tracing "auto" $ do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 191b4e7c3b..7bae665f54 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleContexts #-}
 module Ide.Plugin.Tactic.CodeGen where
 
@@ -38,7 +39,7 @@ destructMatches
     -> CType
        -- ^ Type being destructed
     -> Judgement
-    -> RuleM [RawMatch]
+    -> RuleM (Trace, [RawMatch])
 destructMatches f f2 t jdg = do
   let hy = jHypothesis jdg
       g  = jGoal jdg
@@ -48,7 +49,7 @@ destructMatches f f2 t jdg = do
       let dcs = tyConDataCons tc
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
-        _ -> for dcs $ \dc -> do
+        _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
@@ -61,9 +62,15 @@ destructMatches f f2 t jdg = do
                 $ withPositionMapping dcon_name names
                 $ introducingPat hy'
                 $ withNewGoal g jdg
-          sg <- f dc j
+          (tr, sg) <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
-          pure $ match [pat] $ unLoc sg
+          pure $ (tr, match [pat] $ unLoc sg)
+
+
+unzipTrace :: [(Trace, a)] -> (Trace, [a])
+unzipTrace l =
+  let (trs, as) = unzip l
+   in (rose mempty trs, as)
 
 
 ------------------------------------------------------------------------------
@@ -77,7 +84,7 @@ destruct' f term jdg = do
     Nothing -> throwError $ UndefinedHypothesis term
     Just (_, t) -> do
       useOccName jdg term
-      fmap noLoc $ case' (var' term) <$>
+      fmap (fmap noLoc $ case' (var' term)) <$>
         destructMatches
           f
           (\cs -> setParents term (fmap fst cs) . destructing term)
@@ -94,7 +101,7 @@ destructLambdaCase' f jdg = do
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
-      fmap noLoc $ lambdaCase <$>
+      fmap (fmap noLoc $ lambdaCase) <$>
         destructMatches f (const id) (CType arg) jdg
     _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
@@ -105,11 +112,13 @@ buildDataCon
     :: Judgement
     -> DataCon            -- ^ The data con to build
     -> [Type]             -- ^ Type arguments for the data con
-    -> RuleM (LHsExpr GhcPs)
+    -> RuleM (Trace, LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
       dcon_name = nameOccName $ dataConName dc
-  sgs <- traverse ( \(arg, n) ->
+  (tr, sgs)
+      <- fmap unzipTrace
+       $ traverse ( \(arg, n) ->
                     newSubgoal
                   . filterSameTypeFromOtherPositions dcon_name n
                   . blacklistingDestruct
@@ -117,6 +126,7 @@ buildDataCon jdg dc apps = do
                   $ CType arg
                   ) $ zip args [0..]
   pure
+    . (tr,)
     . noLoc
     . foldl' (@@)
         (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
@@ -128,6 +138,7 @@ buildDataCon jdg dc apps = do
 var' :: Var a => OccName -> a
 var' = var . fromString . occNameString
 
+
 ------------------------------------------------------------------------------
 -- | Like 'bvar', but works over standard GHC 'OccName's.
 bvar' :: BVar a => OccName -> a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 8228feee00..588445ebb7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -36,6 +36,8 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import Control.Arrow
+import Control.Monad.State.Strict (StateT (..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -47,7 +49,7 @@ substCTy subst = coerce . substTy subst . coerce
 -- goal.
 newSubgoal
     :: Judgement
-    -> RuleM (LHsExpr GhcPs)
+    -> Rule
 newSubgoal j = do
     unifier <- gets ts_unifier
     subgoal
@@ -62,7 +64,7 @@ runTactic
     :: Context
     -> Judgement
     -> TacticsM ()       -- ^ Tactic to use
-    -> Either [TacticError] (LHsExpr GhcPs)
+    -> Either [TacticError] (Trace, LHsExpr GhcPs)
 runTactic ctx jdg t =
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
         tacticState = defaultTacticState { ts_skolems = skolems }
@@ -81,6 +83,20 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
+tracePrim :: String -> Trace
+tracePrim = flip rose []
+
+
+tracing
+    :: Functor m
+    => String
+    -> TacticT jdg (Trace, ext) err s m a
+    -> TacticT jdg (Trace, ext) err s m a
+tracing s (TacticT m)
+  = TacticT $ StateT $ \jdg ->
+      mapExtract' (first $ rose s . pure) $ runStateT m jdg
+
+
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 4b20cdfb01..7b4dd2855f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveGeneric         #-}
@@ -17,6 +18,7 @@ import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Data.Bool (bool)
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
@@ -33,12 +35,11 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (nameOccName)
+import           Name (occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Data.Bool (bool)
 
 
 ------------------------------------------------------------------------------
@@ -60,14 +61,14 @@ assume name = rule $ \jdg -> do
             True  -> setRecursionFrameData True
             False -> pure ()
           useOccName jdg name
-          pure $ noLoc $ var' name
+          pure $ (tracePrim $ "assume:" <> occNameString name, ) $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
 
 recursion :: TacticsM ()
-recursion = do
+recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
@@ -79,7 +80,7 @@ recursion = do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = rule $ \jdg -> do
+intros = tracing "intros" $ rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
   ctx <- ask
@@ -90,7 +91,8 @@ intros = rule $ \jdg -> do
       let jdg' = introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
-      sg <- newSubgoal
+      (tr, sg)
+        <- newSubgoal
           $ bool
               id
               (withPositionMapping
@@ -98,6 +100,7 @@ intros = rule $ \jdg -> do
               (isTopHole jdg)
           $ jdg'
       pure
+        . (tr, )
         . noLoc
         . lambda (fmap bvar' vs)
         $ unLoc sg
@@ -106,7 +109,7 @@ intros = rule $ \jdg -> do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destructAuto :: OccName -> TacticsM ()
-destructAuto name = do
+destructAuto name = tracing "destruct(auto)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -126,7 +129,7 @@ destructAuto name = do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: OccName -> TacticsM ()
-destruct name = do
+destruct name = tracing "destruct(user)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -136,20 +139,20 @@ destruct name = do
 ------------------------------------------------------------------------------
 -- | Case split, using the same data constructor in the matches.
 homo :: OccName -> TacticsM ()
-homo = rule . destruct' (\dc jdg ->
+homo = tracing "homo" . rule . destruct' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
 ------------------------------------------------------------------------------
 -- | LambdaCase split, and leave holes in the matches.
 destructLambdaCase :: TacticsM ()
-destructLambdaCase = rule $ destructLambdaCase' (const subgoal)
+destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal)
 
 
 ------------------------------------------------------------------------------
 -- | LambdaCase split, using the same data constructor in the matches.
 homoLambdaCase :: TacticsM ()
-homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
+homoLambdaCase = tracing "homoLambdaCase" $ rule $ destructLambdaCase' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
@@ -158,7 +161,7 @@ apply = apply' (const id)
 
 
 apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
-apply' f func = do
+apply' f func = tracing ("apply':" <> show func) $ do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg
@@ -167,16 +170,20 @@ apply' f func = do
           let (args, ret) = splitFunTys ty
           unify g (CType ret)
           useOccName jdg func
-          sgs <- traverse ( \(i, t) ->
+          (tr, sgs)
+              <- fmap unzipTrace
+               $ traverse ( \(i, t) ->
                             newSubgoal
                           . f i
                           . blacklistingDestruct
                           . flip withNewGoal jdg
                           $ CType t
                           ) $ zip [0..] args
-          pure . noLoc
-              . foldl' (@@) (var' func)
-              $ fmap unLoc sgs
+          pure
+            . (tr, )
+            . noLoc
+            . foldl' (@@) (var' func)
+            $ fmap unLoc sgs
       Nothing -> do
         throwError $ GoalMismatch "apply" g
 
@@ -184,7 +191,7 @@ apply' f func = do
 ------------------------------------------------------------------------------
 -- | Choose between each of the goal's data constructors.
 split :: TacticsM ()
-split = do
+split = tracing "split(user)" $ do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
@@ -196,7 +203,7 @@ split = do
 ------------------------------------------------------------------------------
 -- | Choose between each of the goal's data constructors.
 splitAuto :: TacticsM ()
-splitAuto = do
+splitAuto = tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
@@ -220,7 +227,7 @@ splitAuto = do
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
 splitDataCon :: DataCon -> TacticsM ()
-splitDataCon dc = rule $ \jdg -> do
+splitDataCon dc = tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
     Just (tc, apps) -> do
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index cca6fe8247..7cce195acc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -26,13 +26,15 @@ import Control.Monad.Reader
 import Data.Function
 import Data.Map (Map)
 import Data.Set (Set)
-import Development.IDE.GHC.Compat
+import Development.IDE.GHC.Compat hiding (Node)
 import Development.IDE.Types.Location
 import GHC.Generics
 import Ide.Plugin.Tactic.Debug
 import OccName
 import Refinery.Tactic
 import Type
+import Data.Tree
+import Data.Coerce
 
 
 ------------------------------------------------------------------------------
@@ -60,6 +62,9 @@ instance Show TCvSubst where
 instance Show (LHsExpr GhcPs) where
   show  = unsafeRender
 
+instance Show DataCon where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
@@ -118,8 +123,8 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
 
 ------------------------------------------------------------------------------
 -- | Orphan instance for producing holes when attempting to solve tactics.
-instance MonadExtract (LHsExpr GhcPs) ExtractM where
-  hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_"
+instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where
+  hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_")
 
 
 ------------------------------------------------------------------------------
@@ -175,9 +180,11 @@ instance Show TacticError where
 
 
 ------------------------------------------------------------------------------
-type TacticsM  = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
-type RuleM     = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
-type Rule      = RuleM (LHsExpr GhcPs)
+type TacticsM  = TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
+type RuleM     = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
+type Rule      = RuleM (Trace, LHsExpr GhcPs)
+
+type Trace = Rose String
 
 
 ------------------------------------------------------------------------------
@@ -190,3 +197,20 @@ data Context = Context
   }
   deriving stock (Eq, Ord)
 
+
+newtype Rose a = Rose (Tree a)
+  deriving stock (Eq, Functor, Generic)
+
+instance Show (Rose String) where
+  show = drawTree . coerce
+
+instance Semigroup a => Semigroup (Rose a) where
+  Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)
+
+instance Monoid a => Monoid (Rose a) where
+  mempty = Rose $ Node mempty mempty
+
+rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
+rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs
+rose a rs = Rose $ Node a $ coerce rs
+

From 6b8a0b9f464458e203c23071bee89fb63b739936 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 00:53:49 -0700
Subject: [PATCH 34/61] unpack introduced bindings

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 23 ++++++++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  4 ++--
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 7bae665f54..85373a9f61 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -64,7 +64,11 @@ destructMatches f f2 t jdg = do
                 $ withNewGoal g jdg
           (tr, sg) <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
-          pure $ (tr, match [pat] $ unLoc sg)
+          pure ( rose ("match " <> show dc <> " {" <>
+                          intercalate ", " (fmap show names) <> "}")
+                    $ pure tr
+               , match [pat] $ unLoc sg
+               )
 
 
 unzipTrace :: [(Trace, a)] -> (Trace, [a])
@@ -84,12 +88,15 @@ destruct' f term jdg = do
     Nothing -> throwError $ UndefinedHypothesis term
     Just (_, t) -> do
       useOccName jdg term
-      fmap (fmap noLoc $ case' (var' term)) <$>
-        destructMatches
-          f
-          (\cs -> setParents term (fmap fst cs) . destructing term)
-          t
-          jdg
+      (tr, ms)
+          <- destructMatches
+               f
+               (\cs -> setParents term (fmap fst cs) . destructing term)
+               t
+               jdg
+      pure ( rose ("destruct " <> show term) $ pure tr
+           , noLoc $ case' (var' term) ms
+           )
 
 
 ------------------------------------------------------------------------------
@@ -126,7 +133,7 @@ buildDataCon jdg dc apps = do
                   $ CType arg
                   ) $ zip args [0..]
   pure
-    . (tr,)
+    . (rose (show dc) $ pure tr,)
     . noLoc
     . foldl' (@@)
         (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7b4dd2855f..0a39a47aae 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -80,7 +80,7 @@ recursion = tracing "recursion" $ do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = tracing "intros" $ rule $ \jdg -> do
+intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
   ctx <- ask
@@ -100,7 +100,7 @@ intros = tracing "intros" $ rule $ \jdg -> do
               (isTopHole jdg)
           $ jdg'
       pure
-        . (tr, )
+        . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, )
         . noLoc
         . lambda (fmap bvar' vs)
         $ unLoc sg

From 872cfec1c5097ce6c49282872f9f8725cee67128 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 01:07:32 -0700
Subject: [PATCH 35/61] Slightly better format

---
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs        | 12 +++++++-----
 .../tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs |  6 +++---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs     |  4 ++--
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 392bcf3c80..3e4a28d21f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -3,20 +3,22 @@ module Ide.Plugin.Tactic.Auto where
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
-import Ide.Plugin.Tactic.Machinery
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import Refinery.Tactic
+import Ide.Plugin.Tactic.Machinery (tracing)
 
 
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
-auto = tracing "auto" $ do
+auto = do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
-  commit
-    knownStrategies
-    (localTactic (auto' 4) $ disallowing $ fmap fst current)
+  commit knownStrategies
+    . tracing "auto"
+    . localTactic (auto' 4)
+    . disallowing
+    $ fmap fst current
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
index 0855cd97e8..610740aba3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
@@ -8,6 +8,7 @@ import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import OccName (mkVarOcc)
 import Refinery.Tactic
+import Ide.Plugin.Tactic.Machinery (tracing)
 
 
 knownStrategies :: TacticsM ()
@@ -19,9 +20,8 @@ knownStrategies = choice
 known :: String -> TacticsM () -> TacticsM ()
 known name t = do
   getCurrentDefinitions >>= \case
-    [(def, _)] | def == mkVarOcc name -> do
-      traceMX "running known strategy" name
-      t
+    [(def, _)] | def == mkVarOcc name ->
+      tracing ("known " <> name) t
     _ -> throwError NoApplicableTactic
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 0a39a47aae..dc6358fec8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -61,7 +61,7 @@ assume name = rule $ \jdg -> do
             True  -> setRecursionFrameData True
             False -> pure ()
           useOccName jdg name
-          pure $ (tracePrim $ "assume:" <> occNameString name, ) $ noLoc $ var' name
+          pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
@@ -161,7 +161,7 @@ apply = apply' (const id)
 
 
 apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
-apply' f func = tracing ("apply':" <> show func) $ do
+apply' f func = tracing ("apply' " <> show func) $ do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg

From 8a416d978ebc777f030acd2d933109a817849545 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 01:13:58 -0700
Subject: [PATCH 36/61] compress ppr tree

---
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 7cce195acc..5cfd62b5a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -202,7 +202,12 @@ newtype Rose a = Rose (Tree a)
   deriving stock (Eq, Functor, Generic)
 
 instance Show (Rose String) where
-  show = drawTree . coerce
+  show = unlines . dropEveryOther . lines . drawTree . coerce
+
+dropEveryOther :: [a] -> [a]
+dropEveryOther []           = []
+dropEveryOther [a]          = [a]
+dropEveryOther (a : _ : as) = a : dropEveryOther as
 
 instance Semigroup a => Semigroup (Rose a) where
   Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)

From 8e690047025ec05e92c69a3536cba9669f3e18e2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 00:42:03 -0700
Subject: [PATCH 37/61] Fix splitAuto

---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index dc6358fec8..0703fa2a94 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -35,7 +35,7 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (occNameString)
+import           Name (nameOccName, occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -200,8 +200,11 @@ split = tracing "split(user)" $ do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs
 
+
 ------------------------------------------------------------------------------
--- | Choose between each of the goal's data constructors.
+-- | Choose between each of the goal's data constructors. Different than
+-- 'split' because it won't split a data con if it doesn't result in any new
+-- goals.
 splitAuto :: TacticsM ()
 splitAuto = tracing "split(auto)" $ do
   jdg <- goal
@@ -210,18 +213,15 @@ splitAuto = tracing "split(auto)" $ do
     Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
-      -- TODO(sandy): Figure out the right strategy for pruning splits of
-      -- splits
-      choice $ fmap splitDataCon dcs
-      -- case isSplitWhitelisted jdg of
-      --   True -> choice $ fmap splitDataCon dcs
-      --   False -> do
-      --     choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-      --       case all ((== jGoal jdg)  . jGoal) jdgs of
-      --         False  -> Nothing
-      --         True -> do
-      --           traceMX "unhelpful split" $ nameOccName $ dataConName dc
-      --           Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+      case isSplitWhitelisted jdg of
+        True -> choice $ fmap splitDataCon dcs
+        False -> do
+          choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+            case any (/= jGoal jdg) $ traceIdX "goals" $ fmap jGoal jdgs of
+              False  -> Nothing
+              True -> do
+                traceMX "unhelpful split" $ nameOccName $ dataConName dc
+                Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From a84195c1db03a9f024ca08d3aaa79368c097e413 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 11:39:51 -0700
Subject: [PATCH 38/61] Cleanup traces

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs           | 3 +--
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs      | 1 +
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 7 ++++++-
 plugins/tactics/src/Ide/TreeTransform.hs           | 3 +--
 4 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 27171fe7fd..c7ebd3cad3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -296,10 +296,9 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right (tr, ext) -> do
+            Right (_, ext) -> do
               let g = graft (RealSrcSpan span) ext
                   response = transform dflags (clientCapabilities lf) uri g pm
-              traceMX "trace" tr
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
                 Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 3e4a28d21f..0a22255e60 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -16,6 +16,7 @@ auto = do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
+  traceMX "ctx" current
   commit knownStrategies
     . tracing "auto"
     . localTactic (auto' 4)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 588445ebb7..7a02fa1d66 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -76,7 +76,12 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 50 $  fmap (show . fst) sorted
+        traceM
+            $ mappend "!!!solns: "
+            $ intercalate "\n"
+            $ reverse
+            $ take 5
+            $ fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/TreeTransform.hs b/plugins/tactics/src/Ide/TreeTransform.hs
index 012426de68..80b0062ff5 100644
--- a/plugins/tactics/src/Ide/TreeTransform.hs
+++ b/plugins/tactics/src/Ide/TreeTransform.hs
@@ -12,7 +12,6 @@ import           BasicTypes (appPrec)
 import           Control.Monad
 import           Control.Monad.Trans.Class
 import qualified Data.Text as T
-import           Debug.Trace
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Rules
 import           Development.IDE.Core.Shake
@@ -104,7 +103,7 @@ fixAnns ParsedModule {..} =
 annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs)
 annotate dflags expr = do
   uniq <- show <$> uniqueSrcSpanT
-  let rendered = traceId $ render dflags expr
+  let rendered = render dflags expr
   (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered
   let anns' = setPrecedingLines expr' 0 1 anns
   pure (anns', expr')

From 5f44746777e7f708c46b7c0d65332a3effd794ad Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 11:40:30 -0700
Subject: [PATCH 39/61] Fix autosplit

---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 0703fa2a94..364eb6718f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -217,11 +217,9 @@ splitAuto = tracing "split(auto)" $ do
         True -> choice $ fmap splitDataCon dcs
         False -> do
           choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-            case any (/= jGoal jdg) $ traceIdX "goals" $ fmap jGoal jdgs of
-              False  -> Nothing
-              True -> do
-                traceMX "unhelpful split" $ nameOccName $ dataConName dc
-                Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+            case any (/= jGoal jdg) $ fmap jGoal jdgs of
+              False -> Nothing
+              True  -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From 4eca10df5a3f5a8904ce5509e8e67d3f5809c8ba Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 15 Oct 2020 20:44:19 -0700
Subject: [PATCH 40/61] Update refinery

---
 cabal.project                                 |  2 +-
 haskell-language-server.cabal                 |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  9 +-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 84 ++-----------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  2 +-
 stack-8.10.1.yaml                             |  2 +-
 stack-8.10.2.yaml                             |  2 +-
 stack-8.6.4.yaml                              |  2 +-
 stack-8.6.5.yaml                              |  2 +-
 stack-8.8.2.yaml                              |  2 +-
 stack-8.8.3.yaml                              |  2 +-
 stack-8.8.4.yaml                              |  2 +-
 stack.yaml                                    |  2 +-
 13 files changed, 21 insertions(+), 94 deletions(-)

diff --git a/cabal.project b/cabal.project
index 334c3417f5..6323590cf8 100644
--- a/cabal.project
+++ b/cabal.project
@@ -20,6 +20,6 @@ package ghcide
 
 write-ghc-environment-files: never
 
-index-state: 2020-10-08T12:51:21Z
+index-state: 2020-10-16T04:00:00Z
 
 allow-newer: data-tree-print:base
diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index e2d3f2fd72..4f75fad4c6 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -158,7 +158,7 @@ executable haskell-language-server
     , transformers
     , unordered-containers
     , ghc-source-gen
-    , refinery                 ^>=0.2
+    , refinery                 ^>=0.3
     , ghc-exactprint
     , fingertree
     , generic-lens
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index f755b79a24..f89a9964dd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -49,7 +49,7 @@ destructMatches f f2 t jdg = do
       let dcs = tyConDataCons tc
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
-        _ -> for dcs $ \dc -> do
+        _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstOrigArgTys' dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
@@ -131,8 +131,7 @@ buildDataCon
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Trace, LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
-<<<<<<< HEAD
-  let args = dataConInstArgTys dc apps
+  let args = dataConInstOrigArgTys' dc apps
       dcon_name = nameOccName $ dataConName dc
   (tr, sgs)
       <- fmap unzipTrace
@@ -143,10 +142,6 @@ buildDataCon jdg dc apps = do
                   . flip withNewGoal jdg
                   $ CType arg
                   ) $ zip args [0..]
-=======
-  let args = dataConInstOrigArgTys' dc apps
-  sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
->>>>>>> master
   pure
     . (rose (show dc) $ pure tr,)
     . noLoc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 7a02fa1d66..972cb8a574 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -17,11 +17,12 @@ module Ide.Plugin.Tactic.Machinery
   ( module Ide.Plugin.Tactic.Machinery
   ) where
 
-import           Control.Applicative
+import           Control.Arrow
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
+import           Control.Monad.State.Strict (StateT (..))
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
@@ -36,8 +37,6 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
-import Control.Arrow
-import Control.Monad.State.Strict (StateT (..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -71,10 +70,10 @@ runTactic ctx jdg t =
     in case partitionEithers
           . flip runReader ctx
           . unExtractM
-          $ runTacticTWithState t jdg tacticState of
+          $ runTacticT t jdg tacticState of
       (errs, []) -> Left $ take 50 $ errs
-      (_, solns) -> do
-        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
+      (_, fmap assoc23 -> solns) -> do
+        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) $ solns
         -- TODO(sandy): remove this trace sometime
         traceM
             $ mappend "!!!solns: "
@@ -87,6 +86,9 @@ runTactic ctx jdg t =
           -- guaranteed to not be empty
           _ -> Left []
 
+assoc23 :: (a, b, c) -> (a, (b, c))
+assoc23 (a, b, c) = (a, (b, c))
+
 
 tracePrim :: String -> Trace
 tracePrim = flip rose []
@@ -112,44 +114,6 @@ recursiveCleanup s =
         False -> Just NoProgress
 
 
-filterT
-    :: (Monad m)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p f t = check >> t
-    where
-      check = rule $ \j -> do
-          e <- subgoal j
-          s <- get
-          modify f
-          case p s of
-            Just err -> throwError err
-            Nothing -> pure e
-
-
-gather
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m a
-    -> ([(a, jdg)] -> TacticT jdg ext err s m a)
-    -> TacticT jdg ext err s m a
-gather t f = tactic $ \j -> do
-    s <- get
-    results <- lift $ proofs s $ proofState t j
-    msum $ flip fmap results $ \case
-        Left err -> throwError err
-        Right (_, jdgs) -> proofState (f jdgs) j
-
-
-pruning
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m ()
-    -> ([jdg] -> Maybe err)
-    -> TacticT jdg ext err s m ()
-pruning t p = gather t $ maybe t throwError . p . fmap snd
-
-
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
@@ -180,38 +144,6 @@ newtype Reward a = Reward a
   deriving (Eq, Ord, Show) via a
 
 
-runTacticTWithState
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m ()
-    -> jdg
-    -> s
-    -> m [Either err (ext, (s, [jdg]))]
-runTacticTWithState t j s = proofs' s $ fmap snd $ proofState t j
-
-
-proofs'
-    :: (MonadExtract ext m)
-    => s
-    -> ProofStateT ext ext err s m goal
-    -> m [(Either err (ext, (s, [goal])))]
-proofs' s p = go s [] p
-    where
-      go s goals (Subgoal goal k) = do
-         h <- hole
-         (go s (goals ++ [goal]) $ k h)
-      go s goals (Effect m) = go s goals =<< m
-      go s goals (Stateful f) =
-          let (s', p) = f s
-          in go s' goals p
-      go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
-      go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
-      go s goals (Commit p1 p2) = go s goals p1 >>= \case
-          (rights -> []) -> go s goals p2
-          solns -> pure solns
-      go _ _ Empty = pure []
-      go _ _ (Failure err) = pure [throwError err]
-      go s goals (Axiom ext) = pure [Right (ext, (s, goals))]
-
 
 ------------------------------------------------------------------------------
 -- | We need to make sure that we don't try to unify any skolems.
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 364eb6718f..4fcccbb61b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -72,7 +72,7 @@ recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) $ do
+    ensure recursiveCleanup (withRecursionStack tail) $ do
       (localTactic (apply' (const id) name) $ introducing defs)
         <@> fmap (localTactic assumption . filterPosition name) [0..]
 
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index e462e45fca..8353abf148 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -21,7 +21,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.12.2.0
 - semigroups-0.18.5
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index a594da29c8..66fa833fb6 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -19,7 +19,7 @@ extra-deps:
 - fourmolu-0.2.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.12.2.0
 - semigroups-0.18.5
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index 97051012b9..9796b068ef 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -46,7 +46,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 888670dd8f..1a0b67c2b2 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index 0d6a229d1f..94ad80cd99 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -38,7 +38,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index 1468ae7444..c01a2649e1 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -30,7 +30,7 @@ extra-deps:
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index ebf11425f1..57518e9e24 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -30,7 +30,7 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack.yaml b/stack.yaml
index 888670dd8f..1a0b67c2b2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0

From de0cfb912eef276b9de4702226bf2e8f3c2e51e8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:21:05 -0700
Subject: [PATCH 41/61] Attempt GHC compatability

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs     | 23 -----------
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 41 +++++++++++++++++++-
 2 files changed, 39 insertions(+), 25 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index c7ebd3cad3..82b91d942b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -345,31 +345,8 @@ getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
   ) tcs
 
 
-------------------------------------------------------------------------------
--- | Should make sure it's a fun bind
-pattern TopLevelRHS :: OccName -> [Pat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
-pattern TopLevelRHS name ps body <-
-  Match _
-    (FunRhs (L _ (occName -> name)) _ _)
-    ps
-    (GRHSs _
-      [L _ (GRHS _ [] body)] _)
-
 
 -- TODO(sandy): Make this more robust
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
 
-
-getPatName :: Pat GhcTc -> Maybe OccName
-getPatName = \case
-   VarPat _ x    -> Just $ occName $ unLoc x
-   LazyPat _ p   -> getPatName p
-   AsPat _ x _   -> Just $ occName $ unLoc x
-   ParPat _ p    -> getPatName p
-   BangPat _ p   -> getPatName p
-   ViewPat _ _ p -> getPatName p
-   SigPat _ p _  -> getPatName p
-   XPat p        -> getPatName $ unLoc p
-   _             -> Nothing
-
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 9d1c34851b..8e1fa57a0a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,11 +1,14 @@
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns    #-}
 
 module Ide.Plugin.Tactic.GHC where
 
 import Data.Maybe (isJust)
+import Development.IDE.GHC.Compat
+import OccName
 import TcType
 import TyCoRep
-import TyCon
 import Type
 import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import Unique
@@ -67,3 +70,37 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
 
+fromPatCompat :: PatCompat pass -> Pat pass
+#if __GLASGOW_HASKELL__ <= 808
+type PatCompat = Pat
+fromPatCompat = id
+#elif
+type PatCompat = LPat
+fromPatCompat = unLoc
+#endif
+
+------------------------------------------------------------------------------
+-- | Should make sure it's a fun bind
+pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
+pattern TopLevelRHS name ps body <-
+  Match _
+    (FunRhs (L _ (occName -> name)) _ _)
+    ps
+    (GRHSs _
+      [L _ (GRHS _ [] body)] _)
+
+getPatName :: PatCompat GhcTc -> Maybe OccName
+getPatName (fromPatCompat -> p0) =
+  case p0 of
+    VarPat  _ x   -> Just $ occName $ unLoc x
+    LazyPat _ p   -> getPatName p
+    AsPat   _ x _ -> Just $ occName $ unLoc x
+    ParPat  _ p   -> getPatName p
+    BangPat _ p   -> getPatName p
+    ViewPat _ _ p -> getPatName p
+#if __GLASGOW_HASKELL__ >= 808
+    SigPat  _ p _ -> getPatName p
+#endif
+    XPat    p     -> getPatName $ unLoc p
+    _             -> Nothing
+

From 1b70cee68fd42059a138b791777c9d61729277e6 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:43:29 -0700
Subject: [PATCH 42/61] cpp nightmares

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 8e1fa57a0a..5007147301 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -71,10 +71,10 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
 lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
-#if __GLASGOW_HASKELL__ <= 808
+#if __GLASGOW_HASKELL__ >= 808
 type PatCompat = Pat
 fromPatCompat = id
-#elif
+#else
 type PatCompat = LPat
 fromPatCompat = unLoc
 #endif

From b700c35c5219305accabcd451b3ca7a0efc056d6 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:52:34 -0700
Subject: [PATCH 43/61] type syn of type syn

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 5007147301..1296a9d6d5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -72,10 +72,10 @@ lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
 #if __GLASGOW_HASKELL__ >= 808
-type PatCompat = Pat
+type PatCompat pass = Pat pass
 fromPatCompat = id
 #else
-type PatCompat = LPat
+type PatCompat pass = LPat pass
 fromPatCompat = unLoc
 #endif
 

From 25b9133dffa0ffea6106f41df891b13dc6a44de9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:53:30 -0700
Subject: [PATCH 44/61] wtfff

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 1296a9d6d5..9381d180d5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -71,7 +71,7 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
 lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
-#if __GLASGOW_HASKELL__ >= 808
+#if __GLASGOW_HASKELL__ == 808
 type PatCompat pass = Pat pass
 fromPatCompat = id
 #else

From baac4508e9ef28cd07af7b75ae4d2c68c111eb6d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 11:09:32 -0700
Subject: [PATCH 45/61] maybe this time

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 9381d180d5..85a96adfca 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -70,7 +70,7 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
 
-fromPatCompat :: PatCompat pass -> Pat pass
+fromPatCompat :: PatCompat GhcTc -> Pat GhcTc
 #if __GLASGOW_HASKELL__ == 808
 type PatCompat pass = Pat pass
 fromPatCompat = id
@@ -100,7 +100,7 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-#endif
     XPat    p     -> getPatName $ unLoc p
+#endif
     _             -> Nothing
 

From c6e10fddbc78b06c2607f03eb9933a655f6fc19b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 12:00:27 -0700
Subject: [PATCH 46/61] omg plzz 810

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 85a96adfca..c5933e6240 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -100,7 +100,11 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-    XPat    p     -> getPatName $ unLoc p
+    XPat    p     -> getPatName $
+#if __GLASGOW_HASKELL__ < 810
+      unLoc
+#endif
+            p
 #endif
     _             -> Nothing
 

From c26f9bae021c3cc8819f737c60f6b3b129b7fcba Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 12:13:49 -0700
Subject: [PATCH 47/61] dsgjdsgidgjis

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index c5933e6240..7f89e4c0c9 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -100,11 +100,9 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-    XPat    p     -> getPatName $
-#if __GLASGOW_HASKELL__ < 810
-      unLoc
 #endif
-            p
+#if __GLASGOW_HASKELL__ == 808
+    XPat   p      -> getPatName $ unLoc p
 #endif
     _             -> Nothing
 

From 0ac041bacc49268305bc8b7370990da8e0e9f1ef Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 09:25:26 -0700
Subject: [PATCH 48/61] Get known metaprogramming files

---
 haskell-language-server.cabal                 |  1 +
 .../src/Ide/Plugin/Tactic/Metaprogramming.hs  | 35 +++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index 4f75fad4c6..29d0392d75 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -102,6 +102,7 @@ executable haskell-language-server
     Ide.Plugin.Tactic.Judgements
     Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.Machinery
+    Ide.Plugin.Tactic.Metaprogramming
     Ide.Plugin.Tactic.Naming
     Ide.Plugin.Tactic.Range
     Ide.Plugin.Tactic.Tactics
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
new file mode 100644
index 0000000000..03d7da3bf8
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Ide.Plugin.Tactic.Metaprogramming where
+
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import           System.Directory
+import           System.FilePath ((<.>), (</>))
+import Control.Monad.Extra (unlessM)
+
+
+configDir :: IO FilePath
+configDir = do
+  dir <- getXdgDirectory XdgConfig "hls-tactics-plugin"
+  unlessM (doesDirectoryExist dir) $ createDirectory dir
+  let scratch = dir </> scratchName
+  unlessM (doesFileExist scratch) $ T.writeFile scratch ""
+  pure dir
+
+
+scratchName :: FilePath
+scratchName = "scratch" <.> "htp"
+
+
+getScratchContents :: IO T.Text
+getScratchContents = do
+  dir <- configDir
+  T.readFile $ dir </> scratchName
+
+
+getKnownFiles :: IO [FilePath]
+getKnownFiles = do
+  dir <- configDir
+  fmap (dir </>) . filter (/= scratchName) <$> listDirectory dir
+

From 2ce3bf1878b70babc157037e13dede4b68aaeae2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 09:53:09 -0700
Subject: [PATCH 49/61] metaprogram and cache

---
 .../src/Ide/Plugin/Tactic/Metaprogramming.hs  | 47 ++++++++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 27 +++++++++++
 2 files changed, 58 insertions(+), 16 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
index 03d7da3bf8..cce985c6ab 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -2,34 +2,49 @@
 
 module Ide.Plugin.Tactic.Metaprogramming where
 
+import           Control.Monad
+import           Control.Monad.Extra (unlessM)
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Maybe (catMaybes)
 import qualified Data.Text as T
 import qualified Data.Text.IO as T
+import           Data.Time (UTCTime)
+import           Data.Traversable
+import           Ide.Plugin.Tactic.Types
 import           System.Directory
-import           System.FilePath ((<.>), (</>))
-import Control.Monad.Extra (unlessM)
+import           System.FilePath ((</>))
+
+
+buildCache :: Map FilePath (UTCTime, T.Text) -> MetaprogramCache
+buildCache files = MetaprogramCache $ M.fromList $ do
+  (fp, (mtime, contents))  <- M.toList files
+  case parseMetaprogram fp mtime contents of
+    Left err -> do
+      traceM $ "WARNING: unable to parse " <> fp <> ": " <> err
+      mzero
+    Right mp -> pure (fp, mp)
+
+
+-- updateCache :: Map FilePath (UTCTime, T.Text) -> MetaprogramCache  -> MetaprogramCache
+-- updateCache
 
 
 configDir :: IO FilePath
 configDir = do
   dir <- getXdgDirectory XdgConfig "hls-tactics-plugin"
   unlessM (doesDirectoryExist dir) $ createDirectory dir
-  let scratch = dir </> scratchName
-  unlessM (doesFileExist scratch) $ T.writeFile scratch ""
   pure dir
 
 
-scratchName :: FilePath
-scratchName = "scratch" <.> "htp"
-
-
-getScratchContents :: IO T.Text
-getScratchContents = do
-  dir <- configDir
-  T.readFile $ dir </> scratchName
+getKnownFiles :: IO (Map FilePath UTCTime)
+getKnownFiles = do
+  dir    <- configDir
+  files  <- fmap (dir </>) <$> listDirectory dir
+  mtimes <- for files getModificationTime
+  pure $ M.fromList $ zip files mtimes
 
 
-getKnownFiles :: IO [FilePath]
-getKnownFiles = do
-  dir <- configDir
-  fmap (dir </>) . filter (/= scratchName) <$> listDirectory dir
+parseMetaprogram :: FilePath -> UTCTime -> T.Text -> Either String Metaprogram
+parseMetaprogram fp mtime = const $ Left "unimplemented"
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 5cfd62b5a6..1a1c073fc6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -35,6 +35,10 @@ import Refinery.Tactic
 import Type
 import Data.Tree
 import Data.Coerce
+import Data.Text (Text)
+import Data.Time (UTCTime)
+import Control.Arrow
+import Data.Ord (comparing)
 
 
 ------------------------------------------------------------------------------
@@ -219,3 +223,26 @@ rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
 rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs
 rose a rs = Rose $ Node a $ coerce rs
 
+
+------------------------------------------------------------------------------
+
+data Metaprogram = Metaprogram
+  { mp_name             :: !Text
+  , mp_original_path    :: !FilePath
+  , mp_mtime            :: !UTCTime
+  , mp_known_by_auto    :: !Bool
+  , mp_show_code_action :: !Bool
+  , mp_program          :: !(TacticsM ())
+  }
+
+instance Eq Metaprogram where
+  (==) = (==) `on` (mp_original_path &&& mp_mtime)
+
+instance Ord Metaprogram where
+  compare = comparing mp_original_path <> comparing mp_mtime
+
+
+newtype MetaprogramCache = MetaprogramCache
+  { getMetaprogramCache :: Map FilePath Metaprogram
+  }
+

From 5a04900a6081e1e615bca0f24db7cfc734c58e97 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 11:00:34 -0700
Subject: [PATCH 50/61] Shake rules for the metaprogram cache

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 55 ++++++++++++++++-
 .../src/Ide/Plugin/Tactic/Metaprogramming.hs  | 32 +++-------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 61 ++++++++++---------
 3 files changed, 94 insertions(+), 54 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 82b91d942b..a6ff2f8901 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE DerivingStrategies  #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
@@ -7,6 +8,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE ViewPatterns        #-}
 
 -- | A plugin that uses tactics to synthesize code
@@ -34,11 +36,11 @@ import           Data.Traversable
 import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Service (runAction)
-import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
+import           Development.IDE.Core.Shake (defineEarlyCutoff, define, use, useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
-import           Development.Shake (Action)
+import           Development.Shake (RuleResult, Rules, Action)
 import           DynFlags (xopt)
 import qualified FastString
 import           GHC.Generics (Generic)
@@ -59,6 +61,13 @@ import           Language.Haskell.LSP.Types
 import           OccName
 import           SrcLoc (containsSpan)
 import           System.Timeout
+import Data.Hashable (Hashable)
+import Control.DeepSeq (NFData)
+import Data.Binary (Binary)
+import Ide.Plugin.Tactic.Metaprogramming
+import Development.IDE (getFileContents)
+import qualified Data.ByteString.Char8 as BS
+import Development.IDE (ShowDiagnostic(ShowDiag))
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -71,8 +80,50 @@ descriptor plId = (defaultPluginDescriptor plId)
               (tacticCmd $ commandTactic tc))
               [minBound .. maxBound]
     , pluginCodeActionProvider = Just codeActionProvider
+    , pluginRules = tacticRules
     }
 
+data GetMetaprogram = GetMetaprogram
+  deriving stock (Show, Generic, Eq, Ord)
+  deriving anyclass (Hashable, NFData, Binary)
+
+type instance RuleResult GetMetaprogram = Metaprogram
+
+data GetMetaprogramCache = GetMetaprogramCache
+  deriving stock (Show, Generic, Eq, Ord)
+  deriving anyclass (Hashable, NFData, Binary)
+
+type instance RuleResult GetMetaprogramCache = MetaprogramCache
+
+tacticRules :: Rules ()
+tacticRules = do
+  defineEarlyCutoff $ \GetMetaprogram nfp -> do
+    (mtime, Just contents) <- getFileContents nfp
+    pure
+      $ (Just $ BS.pack $ show mtime ,)
+      $ case parseMetaprogram contents of
+          Left err ->
+            ( [ (nfp
+                , ShowDiag
+                , Diagnostic
+                    (Range (Position 0 0) (Position 0 0))
+                    Nothing
+                    Nothing
+                    Nothing
+                    (T.pack err)
+                    Nothing
+                    Nothing
+                )
+              ]
+            , Nothing
+            )
+          Right mp -> ([], Just mp)
+  define $ \GetMetaprogramCache _ -> do
+    files <- liftIO getKnownFiles
+    mps <- fmap catMaybes $ traverse (use GetMetaprogram) files
+    pure ([], Just $ buildCache mps)
+
+
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
index cce985c6ab..94f4adc35e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -2,32 +2,19 @@
 
 module Ide.Plugin.Tactic.Metaprogramming where
 
-import           Control.Monad
 import           Control.Monad.Extra (unlessM)
-import           Data.Map (Map)
 import qualified Data.Map as M
-import           Data.Maybe (catMaybes)
 import qualified Data.Text as T
-import qualified Data.Text.IO as T
-import           Data.Time (UTCTime)
-import           Data.Traversable
 import           Ide.Plugin.Tactic.Types
+import           Language.Haskell.LSP.Types
 import           System.Directory
 import           System.FilePath ((</>))
 
 
-buildCache :: Map FilePath (UTCTime, T.Text) -> MetaprogramCache
-buildCache files = MetaprogramCache $ M.fromList $ do
-  (fp, (mtime, contents))  <- M.toList files
-  case parseMetaprogram fp mtime contents of
-    Left err -> do
-      traceM $ "WARNING: unable to parse " <> fp <> ": " <> err
-      mzero
-    Right mp -> pure (fp, mp)
-
-
--- updateCache :: Map FilePath (UTCTime, T.Text) -> MetaprogramCache  -> MetaprogramCache
--- updateCache
+buildCache :: [Metaprogram] -> MetaprogramCache
+buildCache mps = MetaprogramCache $ M.fromList $ do
+  mp <- mps
+  pure (mp_name mp, mp)
 
 
 configDir :: IO FilePath
@@ -37,14 +24,13 @@ configDir = do
   pure dir
 
 
-getKnownFiles :: IO (Map FilePath UTCTime)
+getKnownFiles :: IO [NormalizedFilePath]
 getKnownFiles = do
   dir    <- configDir
   files  <- fmap (dir </>) <$> listDirectory dir
-  mtimes <- for files getModificationTime
-  pure $ M.fromList $ zip files mtimes
+  pure $ fmap toNormalizedFilePath files
 
 
-parseMetaprogram :: FilePath -> UTCTime -> T.Text -> Either String Metaprogram
-parseMetaprogram fp mtime = const $ Left "unimplemented"
+parseMetaprogram :: T.Text -> Either String Metaprogram
+parseMetaprogram = const $ Left "unimplemented"
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 1a1c073fc6..736c73fa4c 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,11 +1,13 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE BangPatterns               #-}
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE DeriveAnyClass             #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
 {-# OPTIONS_GHC -fno-warn-orphans       #-}
 
@@ -20,25 +22,24 @@ module Ide.Plugin.Tactic.Types
   , Range
   ) where
 
-import Control.Lens hiding (Context)
-import Data.Generics.Product (field)
-import Control.Monad.Reader
-import Data.Function
-import Data.Map (Map)
-import Data.Set (Set)
-import Development.IDE.GHC.Compat hiding (Node)
-import Development.IDE.Types.Location
-import GHC.Generics
-import Ide.Plugin.Tactic.Debug
-import OccName
-import Refinery.Tactic
-import Type
-import Data.Tree
-import Data.Coerce
-import Data.Text (Text)
-import Data.Time (UTCTime)
-import Control.Arrow
-import Data.Ord (comparing)
+import           Control.Lens hiding (Context)
+import           Control.Monad.Reader
+import           Data.Coerce
+import           Data.Function
+import           Data.Generics.Product (field)
+import           Data.Map (Map)
+import           Data.Set (Set)
+import           Data.Text (Text)
+import qualified Data.Text as T
+import           Data.Tree
+import           Development.IDE.GHC.Compat hiding (Node)
+import           Development.IDE.Types.Location
+import           GHC.Generics
+import           Ide.Plugin.Tactic.Debug
+import           OccName
+import           Refinery.Tactic
+import           Type
+import Control.DeepSeq
 
 
 ------------------------------------------------------------------------------
@@ -123,7 +124,7 @@ type Judgement = Judgement' CType
 
 
 newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
-    deriving (Functor, Applicative, Monad, MonadReader Context)
+  deriving newtype (Functor, Applicative, Monad, MonadReader Context)
 
 ------------------------------------------------------------------------------
 -- | Orphan instance for producing holes when attempting to solve tactics.
@@ -228,21 +229,23 @@ rose a rs = Rose $ Node a $ coerce rs
 
 data Metaprogram = Metaprogram
   { mp_name             :: !Text
-  , mp_original_path    :: !FilePath
-  , mp_mtime            :: !UTCTime
   , mp_known_by_auto    :: !Bool
   , mp_show_code_action :: !Bool
   , mp_program          :: !(TacticsM ())
   }
 
-instance Eq Metaprogram where
-  (==) = (==) `on` (mp_original_path &&& mp_mtime)
+instance NFData Metaprogram where
+  rnf (!(Metaprogram !_ !_ !_ !_)) = ()
 
-instance Ord Metaprogram where
-  compare = comparing mp_original_path <> comparing mp_mtime
+
+instance Show Metaprogram where
+  show = T.unpack . mp_name
 
 
 newtype MetaprogramCache = MetaprogramCache
-  { getMetaprogramCache :: Map FilePath Metaprogram
+  { getMetaprogramCache :: Map Text Metaprogram
   }
+  deriving stock (Show, Generic)
+  deriving newtype (Semigroup, Monoid)
+  deriving anyclass (NFData)
 

From 0861f114d568b65b71b4b79608a784ccc4c07597 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 11:22:23 -0700
Subject: [PATCH 51/61] Hook up metaprograms

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 65 +++++++++++++------
 .../src/Ide/Plugin/Tactic/TestTypes.hs        |  3 +
 2 files changed, 49 insertions(+), 19 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index a6ff2f8901..cb07774877 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -18,6 +18,7 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
+import Control.Monad.Error.Class
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Trans
@@ -106,7 +107,8 @@ tacticRules = do
             ( [ (nfp
                 , ShowDiag
                 , Diagnostic
-                    (Range (Position 0 0) (Position 0 0))
+                    (Range (Position 0 0)
+                           (Position 0 0))
                     Nothing
                     Nothing
                     Nothing
@@ -130,7 +132,14 @@ tacticDesc name = "fill the hole using the " <> name <> " tactic"
 ------------------------------------------------------------------------------
 -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
 -- UI.
-type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
+type TacticProvider
+    = DynFlags
+   -> MetaprogramCache
+   -> PluginId
+   -> Uri
+   -> Range
+   -> Judgement
+   -> IO [CAResult]
 
 
 ------------------------------------------------------------------------------
@@ -166,17 +175,23 @@ commandProvider HomomorphismLambdaCase =
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
+commandProvider RunMetaprogram =
+  allMetaprograms $ \mp ->
+    provide RunMetaprogram mp
 
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: TacticCommand -> OccName -> TacticsM ()
-commandTactic Auto         = const auto
-commandTactic Intros       = const intros
-commandTactic Destruct     = destruct
-commandTactic Homomorphism = homo
-commandTactic DestructLambdaCase     = const destructLambdaCase
-commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic :: TacticCommand -> Maybe Metaprogram -> OccName -> TacticsM ()
+commandTactic Auto _ _                   = auto
+commandTactic Intros _ _                 = intros
+commandTactic Destruct _ occ             = destruct occ
+commandTactic Homomorphism _ occ         = homo occ
+commandTactic DestructLambdaCase _ _     = destructLambdaCase
+commandTactic HomomorphismLambdaCase _ _ = homoLambdaCase
+commandTactic RunMetaprogram (Just mp) _ = mp_program mp
+-- TODO(sandy): better error here
+commandTactic RunMetaprogram Nothing _   = throwError NoApplicableTactic
 
 
 ------------------------------------------------------------------------------
@@ -204,10 +219,12 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right $ List []) $ do
         (_, jdg, _, dflags) <- judgementForHole state nfp range
+        mpc <- MaybeT $ runIde state $ use GetMetaprogramCache nfp
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
             dflags
+            mpc
             plId
             uri
             range
@@ -224,7 +241,7 @@ codeActions = List . fmap CACodeAction
 -- | Terminal constructor for providing context-sensitive tactics. Tactics
 -- given by 'provide' are always available.
 provide :: TacticCommand -> T.Text -> TacticProvider
-provide tc name _ plId uri range _ = do
+provide tc name _ _ plId uri range _ = do
   let title = tacticTitle tc name
       params = TacticParams { file = uri , range = range , var_name = name }
   cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
@@ -239,9 +256,9 @@ provide tc name _ plId uri range _ = do
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 requireExtension :: Extension -> TacticProvider -> TacticProvider
-requireExtension ext tp dflags plId uri range jdg =
+requireExtension ext tp dflags mpc plId uri range jdg =
   case xopt ext dflags of
-    True  -> tp dflags plId uri range jdg
+    True  -> tp dflags mpc plId uri range jdg
     False -> pure []
 
 
@@ -249,9 +266,9 @@ requireExtension ext tp dflags plId uri range jdg =
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp dflags plId uri range jdg =
+filterGoalType p tp dflags mpc plId uri range jdg =
   case p $ unCType $ jGoal jdg of
-    True  -> tp dflags plId uri range jdg
+    True  -> tp dflags mpc plId uri range jdg
     False -> pure []
 
 
@@ -262,14 +279,20 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp dflags plId uri range jdg =
+filterBindingType p tp dflags mpc plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
    in fmap join $ for (M.toList hy) $ \(occ, CType ty) ->
         case p (unCType g) ty of
-          True  -> tp occ ty dflags plId uri range jdg
+          True  -> tp occ ty dflags mpc plId uri range jdg
           False -> pure []
 
+allMetaprograms
+    :: (T.Text -> TacticProvider)
+    -> TacticProvider
+allMetaprograms f dflags mpc@(MetaprogramCache cache) plId uri range jdg =
+  fmap join $ for (M.keys cache) $ \key -> f key dflags mpc plId uri range jdg
+
 
 data TacticParams = TacticParams
     { file :: Uri -- ^ Uri of the file to fill the hole in
@@ -331,16 +354,20 @@ judgementForHole state nfp range = do
 
 
 
-tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
+tacticCmd :: (Maybe Metaprogram -> OccName -> TacticsM ()) -> CommandFunction TacticParams
+-- TODO(sandy): This is gross; it is reusing var_name as a metaprogram name as well
 tacticCmd tac lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right Null, Nothing) $ do
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
-        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
+        pm  <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
+        mpc <- MaybeT $ runIde state $ use GetMetaprogramCache nfp
+        let mp = M.lookup var_name $ getMetaprogramCache mpc
+
         x <- lift $ timeout 2e8 $
           case runTactic ctx jdg
-                $ tac
+                $ tac mp
                 $ mkVarOcc
                 $ T.unpack var_name of
             Left err ->
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
index 2ea4b8d06c..27d25f028b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -15,6 +15,7 @@ data TacticCommand
   | Homomorphism
   | DestructLambdaCase
   | HomomorphismLambdaCase
+  | RunMetaprogram
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -25,3 +26,5 @@ tacticTitle Destruct var = "Case split on " <> var
 tacticTitle Homomorphism var = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _ = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
+tacticTitle RunMetaprogram mp = "Run metaprogram: " <> mp
+

From d6f4617f2cf9b1f4798ea47ba611703442226b74 Mon Sep 17 00:00:00 2001
From: TOTBWF <reed.mullanix@calabrio.com>
Date: Sun, 18 Oct 2020 11:35:53 -0700
Subject: [PATCH 52/61] Implement tactic parser

---
 haskell-language-server.cabal                 |  3 +
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  2 +-
 .../src/Ide/Plugin/Tactic/Metaprogramming.hs  | 16 ++-
 .../tactics/src/Ide/Plugin/Tactic/Parser.hs   | 99 +++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 28 ++++++
 5 files changed, 145 insertions(+), 3 deletions(-)
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index 29d0392d75..34b98dce14 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -104,6 +104,7 @@ executable haskell-language-server
     Ide.Plugin.Tactic.Machinery
     Ide.Plugin.Tactic.Metaprogramming
     Ide.Plugin.Tactic.Naming
+    Ide.Plugin.Tactic.Parser
     Ide.Plugin.Tactic.Range
     Ide.Plugin.Tactic.Tactics
     Ide.Plugin.Tactic.Types
@@ -145,8 +146,10 @@ executable haskell-language-server
     , haskell-lsp              ^>=0.22
     , hls-plugin-api
     , lens
+    , megaparsec               ^>=7
     , mtl
     , ormolu                   ^>=0.1.2
+    , parser-combinators
     , regex-tdfa
     , retrie                   >=0.1.1.0
     , safe-exceptions
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index cb07774877..bb82e6d561 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -102,7 +102,7 @@ tacticRules = do
     (mtime, Just contents) <- getFileContents nfp
     pure
       $ (Just $ BS.pack $ show mtime ,)
-      $ case parseMetaprogram contents of
+      $ case parseMetaprogram (fromNormalizedFilePath nfp) contents of
           Left err ->
             ( [ (nfp
                 , ShowDiag
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
index 94f4adc35e..970b9e1ef2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -10,6 +10,11 @@ import           Language.Haskell.LSP.Types
 import           System.Directory
 import           System.FilePath ((</>))
 
+import qualified Text.Megaparsec as P
+
+import           Ide.Plugin.Tactic.Parser
+import           Ide.Plugin.Tactic.Types
+
 
 buildCache :: [Metaprogram] -> MetaprogramCache
 buildCache mps = MetaprogramCache $ M.fromList $ do
@@ -31,6 +36,13 @@ getKnownFiles = do
   pure $ fmap toNormalizedFilePath files
 
 
-parseMetaprogram :: T.Text -> Either String Metaprogram
-parseMetaprogram = const $ Left "unimplemented"
+parseMetaprogram :: FilePath -> T.Text -> Either String Metaprogram
+parseMetaprogram fp str = case P.runParser tactics fp str of
+  (Left err) -> Left $ show err
+  (Right tac) -> Right $ Metaprogram
+    { mp_name             = "metaprogram" -- TODO [Reed M. 2020-10-18]
+    , mp_known_by_auto    = False -- TODO [Reed M. 2020-10-18]
+    , mp_show_code_action = False -- TODO [Reed M. 2020-10-18]
+    , mp_program          = tac
+    }
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
new file mode 100644
index 0000000000..93527dfe84
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Ide.Plugin.Tactic.Parser where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Functor
+import           Data.Function
+import           Data.List (foldl')
+import           Data.Text (Text)
+import           Data.Void
+
+import qualified Control.Monad.Combinators.Expr as P
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
+import qualified Text.Megaparsec.Char.Lexer as L
+
+import           Name
+
+import qualified Refinery.Tactic as R
+
+import           Ide.Plugin.Tactic.Auto
+import           Ide.Plugin.Tactic.Tactics
+import           Ide.Plugin.Tactic.Types
+
+type Parser = P.Parsec Void Text
+
+lineComment :: Parser ()
+lineComment = L.skipLineComment "--"
+
+blockComment :: Parser ()
+blockComment = L.skipBlockComment "{-" "-}"
+
+sc :: Parser ()
+sc = L.space P.space1 lineComment blockComment
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme sc
+
+symbol :: Text -> Parser Text
+symbol = L.symbol sc
+
+symbol_ :: Text -> Parser ()
+symbol_ = void . symbol
+
+brackets :: Parser a -> Parser a
+brackets = P.between (symbol "[") (symbol "]")
+
+identifier :: Text -> Parser ()
+identifier i = lexeme (P.string i *> P.notFollowedBy P.alphaNumChar)
+
+-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
+variable :: Parser OccName
+variable = lexeme $ do
+    c <- P.alphaNumChar
+    cs <- P.many (P.alphaNumChar <|> P.char '\'')
+    pure $ mkVarOcc (c:cs)
+
+named :: Text -> TacticsM () -> Parser (TacticsM ())
+named name tac = identifier name $> tac
+
+named' :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
+named' name tac = tac <$> (identifier name *> variable)
+
+keyword :: Text -> Parser ()
+keyword = identifier
+
+tactic :: Parser (TacticsM ())
+tactic = flip P.makeExprParser operators $  P.choice
+    [ named  "assumption" assumption
+    , named' "assume" assume
+    , named  "intros" intros
+    , named' "intro" intro
+    , named' "destruct" destruct
+    , named' "homo" homo
+    , named' "apply" apply
+    , named  "split" split
+    , named  "auto" auto
+    , R.try <$> (keyword "try" *> tactics)
+    ]
+
+multitactic :: Parser (TacticsM () -> TacticsM ())
+multitactic = P.choice
+    [ (flip (R.<@>)) <$> brackets (P.sepBy1 tactic (symbol ","))
+    , (flip (>>)) <$> tactic
+    ]
+
+operators :: [[P.Operator Parser (TacticsM ())]]
+operators =
+    [ [ P.Prefix (symbol "*" $> R.many_) ]
+    , [ P.InfixR (symbol "|" $> (R.<%>) )]
+    ]
+
+tactics :: Parser (TacticsM ())
+tactics = do
+    t <- tactic
+    ts <- P.many ((symbol ";") *> multitactic)
+    pure $ foldl' (&) t ts
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 4fcccbb61b..022b8cb456 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -39,6 +39,7 @@ import           Name (nameOccName, occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
+import           TyCoRep (Type(..))
 import           Type hiding (Var)
 
 
@@ -77,6 +78,33 @@ recursion = tracing "recursion" $ do
         <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
+------------------------------------------------------------------------------
+-- | Introduce a lambda binding using the specified name.
+intro :: OccName -> TacticsM ()
+intro name = rule $ \jdg -> do
+  let g  = jGoal jdg
+  ctx <- ask
+  case unCType g of
+    (FunTy a b) -> do
+        let jdg' = introducing [(name, coerce a)]
+                 $ withNewGoal (CType b) jdg
+        modify $ withIntroducedVals $ mappend $ S.singleton name
+        (tr, sg)
+          <- newSubgoal
+            $ bool
+                id
+                (withPositionMapping
+                 (extremelyStupid__definingFunction ctx) [name])
+                (isTopHole jdg)
+            $ jdg'
+        pure
+            . (rose ("intro {" <> show name <> "}") $ pure tr, )
+            . noLoc
+            . lambda [bvar' name]
+            $ unLoc sg
+    _ -> throwError $ GoalMismatch "intro" g
+
+
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()

From ec1ca1740df1b054a22e57e95488d3092952a3d4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 12:08:58 -0700
Subject: [PATCH 53/61] fix loading metaprograms

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index bb82e6d561..4bd7c291bf 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -18,26 +18,32 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
-import Control.Monad.Error.Class
 import           Control.Arrow
+import           Control.DeepSeq (NFData)
 import           Control.Monad
+import           Control.Monad.Error.Class
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
+import           Data.Binary (Binary)
+import qualified Data.ByteString.Char8 as BS
 import           Data.Coerce
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
+import           Data.Hashable (Hashable)
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
+import qualified Data.Text.IO as T
 import           Data.Traversable
+import           Development.IDE (ShowDiagnostic(ShowDiag))
 import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Service (runAction)
-import           Development.IDE.Core.Shake (defineEarlyCutoff, define, use, useWithStale, IdeState (..))
+import           Development.IDE.Core.Shake (GetModificationTime (..), defineEarlyCutoff, define, use, useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
@@ -51,6 +57,7 @@ import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Metaprogramming
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
@@ -62,13 +69,6 @@ import           Language.Haskell.LSP.Types
 import           OccName
 import           SrcLoc (containsSpan)
 import           System.Timeout
-import Data.Hashable (Hashable)
-import Control.DeepSeq (NFData)
-import Data.Binary (Binary)
-import Ide.Plugin.Tactic.Metaprogramming
-import Development.IDE (getFileContents)
-import qualified Data.ByteString.Char8 as BS
-import Development.IDE (ShowDiagnostic(ShowDiag))
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -99,7 +99,8 @@ type instance RuleResult GetMetaprogramCache = MetaprogramCache
 tacticRules :: Rules ()
 tacticRules = do
   defineEarlyCutoff $ \GetMetaprogram nfp -> do
-    (mtime, Just contents) <- getFileContents nfp
+    mtime <- use GetModificationTime nfp
+    contents <- liftIO $ T.readFile $ fromNormalizedFilePath nfp
     pure
       $ (Just $ BS.pack $ show mtime ,)
       $ case parseMetaprogram (fromNormalizedFilePath nfp) contents of

From c5ff512c7b4466db06d3fb2e4d5649338a446159 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 12:53:55 -0700
Subject: [PATCH 54/61] Parse annotations

---
 .../src/Ide/Plugin/Tactic/Metaprogramming.hs  | 13 ++----
 .../tactics/src/Ide/Plugin/Tactic/Parser.hs   | 46 +++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  5 ++
 3 files changed, 55 insertions(+), 9 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
index 970b9e1ef2..8339159699 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -13,7 +13,7 @@ import           System.FilePath ((</>))
 import qualified Text.Megaparsec as P
 
 import           Ide.Plugin.Tactic.Parser
-import           Ide.Plugin.Tactic.Types
+import Text.Megaparsec (errorBundlePretty)
 
 
 buildCache :: [Metaprogram] -> MetaprogramCache
@@ -37,12 +37,7 @@ getKnownFiles = do
 
 
 parseMetaprogram :: FilePath -> T.Text -> Either String Metaprogram
-parseMetaprogram fp str = case P.runParser tactics fp str of
-  (Left err) -> Left $ show err
-  (Right tac) -> Right $ Metaprogram
-    { mp_name             = "metaprogram" -- TODO [Reed M. 2020-10-18]
-    , mp_known_by_auto    = False -- TODO [Reed M. 2020-10-18]
-    , mp_show_code_action = False -- TODO [Reed M. 2020-10-18]
-    , mp_program          = tac
-    }
+parseMetaprogram fp str = case P.runParser metaprogram fp str of
+  Left err -> trace (errorBundlePretty err) $ Left $ show err
+  Right tac -> Right tac
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
index 93527dfe84..36a0b80032 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
@@ -1,8 +1,13 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Ide.Plugin.Tactic.Parser where
 
+import Data.Generics.Product (field)
+import Control.Lens ((.~))
 import           Control.Applicative
 import           Control.Monad
 import           Data.Functor
@@ -10,6 +15,8 @@ import           Data.Function
 import           Data.List (foldl')
 import           Data.Text (Text)
 import           Data.Void
+import Data.Foldable (asum)
+import qualified Data.Text as T
 
 import qualified Control.Monad.Combinators.Expr as P
 import qualified Text.Megaparsec as P
@@ -57,6 +64,13 @@ variable = lexeme $ do
     cs <- P.many (P.alphaNumChar <|> P.char '\'')
     pure $ mkVarOcc (c:cs)
 
+-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
+name :: Parser Text
+name = lexeme $ do
+    c <- P.alphaNumChar
+    cs <- P.many (P.alphaNumChar <|> P.char '\'' <|> P.char '-')
+    pure $ T.pack (c:cs)
+
 named :: Text -> TacticsM () -> Parser (TacticsM ())
 named name tac = identifier name $> tac
 
@@ -66,6 +80,38 @@ named' name tac = tac <$> (identifier name *> variable)
 keyword :: Text -> Parser ()
 keyword = identifier
 
+annotationHeader :: Text -> Parser ()
+annotationHeader ann = lexeme $ do
+  void $ P.char '@'
+  void $ P.string ann
+
+data Annototation
+   = AnnotationName Text
+   | AnnotationAuto
+   deriving (Eq, Ord, Show)
+
+annotation :: Parser Annototation
+annotation = asum
+  [ do
+      annotationHeader "name"
+      n <- name
+      pure $ AnnotationName n
+  , AnnotationAuto <$ annotationHeader "auto"
+  ]
+
+
+metaprogram :: Parser Metaprogram
+metaprogram = do
+  anns <- P.many $ annotation <* symbol ";"
+  t <- tactics
+  pure $
+    foldr
+      (\case
+        AnnotationName name -> field @"mp_name" .~ name
+        AnnotationAuto      -> field @"mp_known_by_auto" .~ True
+      ) emptyMetaprogram { mp_program  = t } anns
+
+
 tactic :: Parser (TacticsM ())
 tactic = flip P.makeExprParser operators $  P.choice
     [ named  "assumption" assumption
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 736c73fa4c..cfe9d65fb3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
 {-# OPTIONS_GHC -fno-warn-orphans       #-}
@@ -233,6 +234,10 @@ data Metaprogram = Metaprogram
   , mp_show_code_action :: !Bool
   , mp_program          :: !(TacticsM ())
   }
+  deriving stock Generic
+
+emptyMetaprogram :: Metaprogram
+emptyMetaprogram = Metaprogram "" False False (pure ())
 
 instance NFData Metaprogram where
   rnf (!(Metaprogram !_ !_ !_ !_)) = ()

From 232a0dba5e64fc8e51f5e863961a3ac180c5fc25 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 19:07:49 -0700
Subject: [PATCH 55/61] Connect @auto metaprograms to the auto tactic

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 13 ++++----
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  | 25 ++++++++++------
 .../src/Ide/Plugin/Tactic/KnownStrategies.hs  | 30 ++++++++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Parser.hs   |  7 ++---
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  8 ++---
 5 files changed, 50 insertions(+), 33 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 4bd7c291bf..608da8a1b7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -219,8 +219,7 @@ codeActionProvider :: CodeActionProvider
 codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range
-        mpc <- MaybeT $ runIde state $ use GetMetaprogramCache nfp
+        (_, jdg, _, dflags, mpc) <- judgementForHole state nfp range
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
@@ -310,7 +309,7 @@ judgementForHole
     :: IdeState
     -> NormalizedFilePath
     -> Range
-    -> MaybeT IO (Range, Judgement, Context, DynFlags)
+    -> MaybeT IO (Range, Judgement, Context, DynFlags, MetaprogramCache)
 judgementForHole state nfp range = do
   (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
   range' <- liftMaybe $ fromCurrentRange amapping range
@@ -333,9 +332,11 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  mpc <- MaybeT $ runIde state $ use GetMetaprogramCache nfp
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
+              mpc
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
               tcg
@@ -351,6 +352,7 @@ judgementForHole state nfp range = do
            goal
        , ctx
        , dflags
+       , mpc
        )
 
 
@@ -360,11 +362,10 @@ tacticCmd :: (Maybe Metaprogram -> OccName -> TacticsM ()) -> CommandFunction Ta
 tacticCmd tac lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right Null, Nothing) $ do
-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range
+        (range', jdg, ctx, dflags, mpc) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm  <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        mpc <- MaybeT $ runIde state $ use GetMetaprogramCache nfp
-        let mp = M.lookup var_name $ getMetaprogramCache mpc
+        let mp = M.lookup var_name $ unMetaprogramCache mpc
 
         x <- lift $ timeout 2e8 $
           case runTactic ctx jdg
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index 2c8b48227a..055825fc41 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -12,14 +12,17 @@ import OccName
 import TcRnTypes
 
 
-mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
-mkContext locals
-  = Context locals
-  . fmap splitId
-  . (getFunBindId =<<)
-  . fmap unLoc
-  . bagToList
-  . tcg_binds
+mkContext :: MetaprogramCache -> [(OccName, CType)] -> TcGblEnv -> Context
+mkContext mpc locals tcg_env = Context
+  { ctxDefiningFuncs = locals
+  , ctxMetaprogramCache = mpc
+  , ctxModuleFuncs
+      = fmap splitId
+      . (getFunBindId =<<)
+      . fmap unLoc
+      . bagToList
+      $ tcg_binds tcg_env
+  }
 
 
 splitId :: Id -> (OccName, CType)
@@ -35,8 +38,12 @@ getFunBindId _ = []
 
 
 getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
-getCurrentDefinitions = asks $ ctxDefiningFuncs
+getCurrentDefinitions = asks ctxDefiningFuncs
+
 
 getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
 getModuleHypothesis = asks ctxModuleFuncs
 
+getMetaprogramCache :: MonadReader Context m => m MetaprogramCache
+getMetaprogramCache = asks ctxMetaprogramCache
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
index 610740aba3..5c3758ecd6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
@@ -2,19 +2,29 @@
 
 module Ide.Plugin.Tactic.KnownStrategies where
 
-import Control.Monad.Error.Class
-import Ide.Plugin.Tactic.Context (getCurrentDefinitions)
-import Ide.Plugin.Tactic.Tactics
-import Ide.Plugin.Tactic.Types
-import OccName (mkVarOcc)
-import Refinery.Tactic
-import Ide.Plugin.Tactic.Machinery (tracing)
+import           Control.Monad (guard)
+import           Control.Monad.Error.Class
+import qualified Data.Map as M
+import qualified Data.Text as T
+import           Ide.Plugin.Tactic.Context (getMetaprogramCache, getCurrentDefinitions)
+import           Ide.Plugin.Tactic.Machinery (tracing)
+import           Ide.Plugin.Tactic.Tactics
+import           Ide.Plugin.Tactic.Types
+import           OccName (mkVarOcc)
+import           Refinery.Tactic
+
+
+knownMetaprograms :: MetaprogramCache -> [TacticsM ()]
+knownMetaprograms (MetaprogramCache mpc) = do
+  mp <- fmap snd $ M.toList mpc
+  guard $ mp_known_by_auto mp
+  pure $ tracing (T.unpack $ mp_name mp) $ mp_program mp
 
 
 knownStrategies :: TacticsM ()
-knownStrategies = choice
-  [ deriveFmap
-  ]
+knownStrategies = do
+  mpc <- getMetaprogramCache
+  choice $ knownMetaprograms mpc <> [ deriveFmap ]
 
 
 known :: String -> TacticsM () -> TacticsM ()
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
index 36a0b80032..b2b0c6238b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
@@ -27,7 +27,6 @@ import           Name
 
 import qualified Refinery.Tactic as R
 
-import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.Types
 
@@ -92,11 +91,11 @@ data Annototation
 
 annotation :: Parser Annototation
 annotation = asum
-  [ do
+  [ P.try $ do
       annotationHeader "name"
       n <- name
       pure $ AnnotationName n
-  , AnnotationAuto <$ annotationHeader "auto"
+  , P.try $ AnnotationAuto <$ annotationHeader "auto"
   ]
 
 
@@ -122,7 +121,7 @@ tactic = flip P.makeExprParser operators $  P.choice
     , named' "homo" homo
     , named' "apply" apply
     , named  "split" split
-    , named  "auto" auto
+    , named  "auto" (auto' 4)
     , R.try <$> (keyword "try" *> tactics)
     ]
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index cfe9d65fb3..490bd749ce 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -196,12 +196,12 @@ type Trace = Rose String
 ------------------------------------------------------------------------------
 -- | The Reader context of tactics and rules
 data Context = Context
-  { ctxDefiningFuncs :: [(OccName, CType)]
+  { ctxDefiningFuncs :: ![(OccName, CType)]
     -- ^ The functions currently being defined
-  , ctxModuleFuncs :: [(OccName, CType)]
+  , ctxModuleFuncs :: ![(OccName, CType)]
     -- ^ Everything defined in the current module
+  , ctxMetaprogramCache :: !MetaprogramCache
   }
-  deriving stock (Eq, Ord)
 
 
 newtype Rose a = Rose (Tree a)
@@ -248,7 +248,7 @@ instance Show Metaprogram where
 
 
 newtype MetaprogramCache = MetaprogramCache
-  { getMetaprogramCache :: Map Text Metaprogram
+  { unMetaprogramCache :: Map Text Metaprogram
   }
   deriving stock (Show, Generic)
   deriving newtype (Semigroup, Monoid)

From ea77d9cfb34c5dca4b1dc5e5788f8ca634d034ad Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 19:16:21 -0700
Subject: [PATCH 56/61] Auto can use known strategies too

---
 plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
index b2b0c6238b..f872965ed2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
@@ -27,6 +27,7 @@ import           Name
 
 import qualified Refinery.Tactic as R
 
+import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.Types
 
@@ -121,7 +122,7 @@ tactic = flip P.makeExprParser operators $  P.choice
     , named' "homo" homo
     , named' "apply" apply
     , named  "split" split
-    , named  "auto" (auto' 4)
+    , named  "auto" auto
     , R.try <$> (keyword "try" *> tactics)
     ]
 

From d33af4387cb1596974e17e22f3e785f71f5a5458 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 21 Oct 2020 00:45:20 -0700
Subject: [PATCH 57/61] Upgrade megaparsec to 9.0.0

---
 plugins/tactics/hls-tactics-plugin.cabal | 2 +-
 stack-8.10.1.yaml                        | 1 +
 stack-8.10.2.yaml                        | 1 +
 stack-8.6.4.yaml                         | 1 +
 stack-8.6.5.yaml                         | 1 +
 stack-8.8.2.yaml                         | 1 +
 stack-8.8.3.yaml                         | 1 +
 stack-8.8.4.yaml                         | 1 +
 8 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/hls-tactics-plugin.cabal b/plugins/tactics/hls-tactics-plugin.cabal
index 0bd33a82a5..07b6593835 100644
--- a/plugins/tactics/hls-tactics-plugin.cabal
+++ b/plugins/tactics/hls-tactics-plugin.cabal
@@ -74,7 +74,7 @@ library
     , haskell-lsp    ^>=0.22
     , hls-plugin-api
     , lens
-    , megaparsec               ^>=7
+    , megaparsec     ^>=9
     , mtl
     , parser-combinators
     , refinery       ^>=0.3
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index 577041af4a..ddf7cf9715 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -19,6 +19,7 @@ extra-deps:
 - floskell-0.10.4
 - fourmolu-0.2.0.0
 - HsYAML-aeson-0.2.0.0@rev:2
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index 3570c1cdb5..cdf1fd24a0 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -18,6 +18,7 @@ extra-deps:
 - data-tree-print-0.1.0.2
 - floskell-0.10.4
 - fourmolu-0.2.0.0
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - refinery-0.3.0.0
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index e27a62be4f..4f7b6288b9 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -40,6 +40,7 @@ extra-deps:
 - indexed-profunctors-0.1
 - lens-4.18
 - lsp-test-0.11.0.5
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - optics-core-0.2
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 93a47a3472..53a999c677 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -39,6 +39,7 @@ extra-deps:
 - indexed-profunctors-0.1
 - lens-4.18
 - lsp-test-0.11.0.5
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - optics-core-0.2
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index 3b780ed048..64cf89226c 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -36,6 +36,7 @@ extra-deps:
 - HsYAML-aeson-0.2.0.0@rev:2
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index 07e3e6310f..1f381caac3 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -29,6 +29,7 @@ extra-deps:
 - hsimport-0.11.0
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - ormolu-0.1.3.0
 - refinery-0.3.0.0
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 3627d24139..69bca6888f 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -30,6 +30,7 @@ extra-deps:
 - hsimport-0.11.0
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
+- megaparsec-9.0.0
 - monad-dijkstra-0.1.1.2
 - refinery-0.3.0.0
 - retrie-0.1.1.1

From 63d115cce33508672c0c9ceaefb92e21507c2190 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 21 Oct 2020 01:06:57 -0700
Subject: [PATCH 58/61] Properly split fun type

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 12 +++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 33 +++++++++----------
 2 files changed, 25 insertions(+), 20 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 7f89e4c0c9..da47b26b95 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -43,8 +43,16 @@ cloneTyVar t =
 ------------------------------------------------------------------------------
 -- | Is this a function type?
 isFunction :: Type -> Bool
-isFunction (tcSplitFunTys -> ((_:_), _)) = True
-isFunction _ = False
+isFunction (tacticsSplitFunTy -> (_, _, [], _)) = False
+isFunction _ = True
+
+
+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
+tacticsSplitFunTy t
+  = let (vars, theta, t') = tcSplitSigmaTy t
+        (args, res) = tcSplitFunTys t'
+     in (vars, theta, args, res)
+
 
 ------------------------------------------------------------------------------
 -- | Is this an algebraic type?
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index b0f27b484b..5b575ef629 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -83,24 +83,21 @@ intro :: OccName -> TacticsM ()
 intro name = rule $ \jdg -> do
   let g  = jGoal jdg
   ctx <- ask
-  case unCType g of
-    (FunTy a b) -> do
-        let jdg' = introducing [(name, coerce a)]
-                 $ withNewGoal (CType b) jdg
-        modify $ withIntroducedVals $ mappend $ S.singleton name
-        (tr, sg)
-          <- newSubgoal
-            $ bool
-                id
-                (withPositionMapping
-                 (extremelyStupid__definingFunction ctx) [name])
-                (isTopHole jdg)
-            $ jdg'
-        pure
-            . (rose ("intro {" <> show name <> "}") $ pure tr, )
-            . noLoc
-            . lambda [bvar' name]
-            $ unLoc sg
+  case tacticsSplitFunTy $ unCType g of
+    ([], [], (a : as), res) -> do
+      let b = mkFunTys as res
+      let jdg' = introducing [(name, coerce a)]
+               $ withNewGoal (CType b) jdg
+      modify $ withIntroducedVals $ mappend $ S.singleton name
+      (tr, sg)
+        <- newSubgoal
+          -- TODO(sandy): Position mapping doesn't work for a single intro
+          $ jdg'
+      pure
+          . (rose ("intro {" <> show name <> "}") $ pure tr, )
+          . noLoc
+          . lambda [bvar' name]
+          $ unLoc sg
     _ -> throwError $ GoalMismatch "intro" g
 
 

From 3f9668d8e5e08d9d8f3ed03fcaa7e5904555e671 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 21 Oct 2020 01:19:23 -0700
Subject: [PATCH 59/61] CPP for mkVisFunTys in older versions of GHC

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs     | 5 +++++
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index da47b26b95..23d506382e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -53,6 +53,11 @@ tacticsSplitFunTy t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
+#if __GLASGOW_HASKELL__ <= 810
+mkVisFunTys :: [Type] -> Type -> Type
+mkVisFunTys = mkFunTys
+#endif
+
 
 ------------------------------------------------------------------------------
 -- | Is this an algebraic type?
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 5b575ef629..4462be085f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -85,7 +85,7 @@ intro name = rule $ \jdg -> do
   ctx <- ask
   case tacticsSplitFunTy $ unCType g of
     ([], [], (a : as), res) -> do
-      let b = mkFunTys as res
+      let b = mkVisFunTys as res
       let jdg' = introducing [(name, coerce a)]
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.singleton name

From 961640489b9241240b603e9448b24e0781160ac1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 21 Oct 2020 01:27:37 -0700
Subject: [PATCH 60/61] Wrong comparison

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 23d506382e..5fae605de6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -53,7 +53,7 @@ tacticsSplitFunTy t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
-#if __GLASGOW_HASKELL__ <= 810
+#if __GLASGOW_HASKELL__ < 810
 mkVisFunTys :: [Type] -> Type -> Type
 mkVisFunTys = mkFunTys
 #endif

From e79f238f8f63bdd0dd463765ad1b75dfe5c73ea5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 21 Oct 2020 09:36:57 -0700
Subject: [PATCH 61/61] Empty context for quickcheck tests

---
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 4 ++++
 plugins/tactics/test/AutoTupleSpec.hs          | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index ed8100cfec..ed8707c63d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -204,6 +204,10 @@ data Context = Context
   }
 
 
+emptyContext :: Context
+emptyContext = Context mempty mempty mempty
+
+
 newtype Rose a = Rose (Tree a)
   deriving stock (Eq, Functor, Generic)
 
diff --git a/plugins/tactics/test/AutoTupleSpec.hs b/plugins/tactics/test/AutoTupleSpec.hs
index efe37bf09a..89baf7ce0f 100644
--- a/plugins/tactics/test/AutoTupleSpec.hs
+++ b/plugins/tactics/test/AutoTupleSpec.hs
@@ -40,7 +40,7 @@ spec = describe "auto for tuple" $ do
       pure $
           -- We should always be able to find a solution
           runTactic
-            (Context [] [])
+            emptyContext
             (mkFirstJudgement
               (M.singleton (mkVarOcc "x") $ CType in_type)
               True