[WIP] Metaprogramming interface to tactics

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

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -1,12 +1,14 @@
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE DerivingStrategies  #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE PatternSynonyms     #-}
 {-# 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,19 +256,19 @@ 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 []
 
 
 ------------------------------------------------------------------------------
 -- | 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 ->

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

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
+

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?