diff --git a/plugins/tactics/hls-tactics-plugin.cabal b/plugins/tactics/hls-tactics-plugin.cabal
index 7fecc860c4..07b6593835 100644
--- a/plugins/tactics/hls-tactics-plugin.cabal
+++ b/plugins/tactics/hls-tactics-plugin.cabal
@@ -39,7 +39,9 @@ library
     Ide.Plugin.Tactic.Judgements
     Ide.Plugin.Tactic.KnownStrategies
     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
@@ -54,7 +56,10 @@ library
   build-depends:
     , aeson
     , base           >=4.12 && <5
+    , binary
+    , bytestring
     , containers
+    , deepseq
     , directory
     , extra
     , filepath
@@ -65,10 +70,13 @@ library
     , ghc-exactprint
     , ghc-source-gen
     , ghcide         >=0.1
+    , hashable
     , haskell-lsp    ^>=0.22
     , hls-plugin-api
     , lens
+    , megaparsec     ^>=9
     , mtl
+    , parser-combinators
     , refinery       ^>=0.3
     , retrie         >=0.1.1.0
     , shake          >=0.17.5
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 5750835ef7..bd79ccbf71 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
@@ -17,28 +19,35 @@ module Ide.Plugin.Tactic
   ) where
 
 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 (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)
-import           Development.Shake (Action)
+import           Development.Shake (RuleResult, Rules, Action)
 import           DynFlags (xopt)
 import qualified FastString
 import           GHC.Generics (Generic)
@@ -48,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
@@ -71,15 +81,66 @@ 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 <- use GetModificationTime nfp
+    contents <- liftIO $ T.readFile $ fromNormalizedFilePath nfp
+    pure
+      $ (Just $ BS.pack $ show mtime ,)
+      $ case parseMetaprogram (fromNormalizedFilePath nfp) 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"
 
 ------------------------------------------------------------------------------
 -- | 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]
 
 
 ------------------------------------------------------------------------------
@@ -115,17 +176,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
 
 
 ------------------------------------------------------------------------------
@@ -152,11 +219,12 @@ 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
+        (_, jdg, _, dflags, mpc) <- judgementForHole state nfp range
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
             dflags
+            mpc
             plId
             uri
             range
@@ -173,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])
@@ -188,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 []
 
 
@@ -198,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 []
 
 
@@ -211,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
@@ -235,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
@@ -258,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
@@ -276,20 +352,24 @@ judgementForHole state nfp range = do
            goal
        , ctx
        , dflags
+       , mpc
        )
 
 
 
-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
+        (range', jdg, ctx, dflags, mpc) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
-        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
+        pm  <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
+        let mp = M.lookup var_name $ unMetaprogramCache 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/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 89947e1443..ba1973a531 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 #-}
 {-# LANGUAGE TupleSections    #-}
 {-# LANGUAGE ViewPatterns     #-}
@@ -191,7 +192,6 @@ coerceName :: HasOccName a => a -> RdrNameStr
 coerceName = fromString . occNameString . occName
 
 
-
 ------------------------------------------------------------------------------
 -- | Like 'var', but works over standard GHC 'OccName's.
 var' :: Var a => OccName -> a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index 2c8b48227a..40f0361faf 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,13 @@ 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/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 7f89e4c0c9..5fae605de6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -43,8 +43,21 @@ 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)
+
+#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/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/Metaprogramming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
new file mode 100644
index 0000000000..8339159699
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Metaprogramming.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Ide.Plugin.Tactic.Metaprogramming where
+
+import           Control.Monad.Extra (unlessM)
+import qualified Data.Map as M
+import qualified Data.Text as T
+import           Ide.Plugin.Tactic.Types
+import           Language.Haskell.LSP.Types
+import           System.Directory
+import           System.FilePath ((</>))
+
+import qualified Text.Megaparsec as P
+
+import           Ide.Plugin.Tactic.Parser
+import Text.Megaparsec (errorBundlePretty)
+
+
+buildCache :: [Metaprogram] -> MetaprogramCache
+buildCache mps = MetaprogramCache $ M.fromList $ do
+  mp <- mps
+  pure (mp_name mp, mp)
+
+
+configDir :: IO FilePath
+configDir = do
+  dir <- getXdgDirectory XdgConfig "hls-tactics-plugin"
+  unlessM (doesDirectoryExist dir) $ createDirectory dir
+  pure dir
+
+
+getKnownFiles :: IO [NormalizedFilePath]
+getKnownFiles = do
+  dir    <- configDir
+  files  <- fmap (dir </>) <$> listDirectory dir
+  pure $ fmap toNormalizedFilePath files
+
+
+parseMetaprogram :: FilePath -> T.Text -> Either String Metaprogram
+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
new file mode 100644
index 0000000000..f872965ed2
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Parser.hs
@@ -0,0 +1,145 @@
+{-# 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
+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
+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)
+
+-- 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
+
+named' :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
+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
+  [ P.try $ do
+      annotationHeader "name"
+      n <- name
+      pure $ AnnotationName n
+  , P.try $ 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
+    , 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 f00a1087cb..4462be085f 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)
 
 
@@ -66,7 +67,6 @@ assume name = rule $ \jdg -> do
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-
 recursion :: TacticsM ()
 recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
@@ -77,6 +77,30 @@ 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 tacticsSplitFunTy $ unCType g of
+    ([], [], (a : as), res) -> do
+      let b = mkVisFunTys 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
+
+
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
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
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 4d1b802697..ed8707c63d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,11 +1,14 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE BangPatterns               #-}
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE DeriveAnyClass             #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
 {-# OPTIONS_GHC -fno-warn-orphans       #-}
 
@@ -20,21 +23,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           Control.DeepSeq
+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
 
 
 ------------------------------------------------------------------------------
@@ -119,7 +125,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.
@@ -190,12 +196,16 @@ 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)
+
+
+emptyContext :: Context
+emptyContext = Context mempty mempty mempty
 
 
 newtype Rose a = Rose (Tree a)
@@ -221,6 +231,32 @@ rose a rs = Rose $ Node a $ coerce rs
 
 
 ------------------------------------------------------------------------------
+data Metaprogram = Metaprogram
+  { mp_name             :: !Text
+  , mp_known_by_auto    :: !Bool
+  , mp_show_code_action :: !Bool
+  , mp_program          :: !(TacticsM ())
+  }
+  deriving stock Generic
+
+emptyMetaprogram :: Metaprogram
+emptyMetaprogram = Metaprogram "" False False (pure ())
+
+instance NFData Metaprogram where
+  rnf (!(Metaprogram !_ !_ !_ !_)) = ()
+
+
+instance Show Metaprogram where
+  show = T.unpack . mp_name
+
+
+newtype MetaprogramCache = MetaprogramCache
+  { unMetaprogramCache :: Map Text Metaprogram
+  }
+  deriving stock (Show, Generic)
+  deriving newtype (Semigroup, Monoid)
+  deriving anyclass (NFData)
+
 -- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic'
 data RunTacticResults = RunTacticResults
   { rtr_trace       :: Trace
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
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