Tactic metaprogramming

ghcide/session-loader/Development/IDE/Session.hs

@@ -90,7 +90,7 @@ import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
 import           Maybes                               (MaybeT (runMaybeT))
-import           GHC.LanguageExtensions               (Extension(EmptyCase))
+import           GHC.LanguageExtensions               (Extension(EmptyCase, QuasiQuotes))
 
 -- | Bump this version number when making changes to the format of the data stored in hiedb
 hiedbDataVersion :: String
@@ -774,13 +774,16 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           disableOptimisation $
           allowEmptyCaseButWithWarning $
           setUpTypedHoles $
+          enableQuasiQuotes $
           makeDynFlagsAbsolute compRoot dflags'
     -- initPackages parses the -package flags and
     -- sets up the visibility for each component.
     -- Throws if a -package flag cannot be satisfied.
     (final_df, _) <- liftIO $ wrapPackageSetupException $ initPackages dflags''
     return (final_df, targets)
 
+enableQuasiQuotes :: DynFlags -> DynFlags
+enableQuasiQuotes = flip xopt_set QuasiQuotes
 
 -- | Wingman wants to support destructing of empty cases, but these are a parse
 -- error by default. So we want to enable 'EmptyCase', but then that leads to

ghcide/src/Development/IDE/Core/Compile.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE CPP        #-}
 {-# LANGUAGE GADTs      #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
 #include "ghc-api-version.h"
 
 -- | Based on https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/API.
@@ -31,6 +32,7 @@ module Development.IDE.Core.Compile
   , setupFinderCache
   , getDocsBatch
   , lookupName
+  , pattern WingmanMetaprogram
   ) where
 
 import           Development.IDE.Core.Preprocessor
@@ -122,6 +124,7 @@ import           Data.Unique
 import           GHC.Fingerprint
 import qualified Language.LSP.Server               as LSP
 import qualified Language.LSP.Types                as LSP
+import Generics.SYB hiding (orElse)
 
 -- | Given a string buffer, return the string (after preprocessing) and the 'ParsedModule'.
 parseModule
@@ -208,6 +211,36 @@ captureSplices dflags k = do
             pure $ f aw'
 
 
+wingmanMetaprogrammingPlugin :: StaticPlugin
+wingmanMetaprogrammingPlugin =
+    StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []
+  where
+    worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule
+    worker _ _ pm = pure $ pm { hpm_module = addWingmanMetaprogrammingSyntax $ hpm_module pm }
+
+
+pattern WingmanMetaprogram :: FastString -> HsExpr p
+pattern WingmanMetaprogram mp
+  <- HsSCC _ (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
+      (L _ ( HsVar _ _))
+
+mkWingmanMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
+mkWingmanMetaprogram ss mp =
+  HsSCC noExt (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
+    $ L ss
+    $ HsVar noExt
+    $ L ss
+    $ mkRdrUnqual
+    $ mkVarOcc "_"
+
+
+addWingmanMetaprogrammingSyntax :: Data a => a -> a
+addWingmanMetaprogrammingSyntax =
+  everywhere $ mkT $ \case
+    L ss (HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)) ->
+      L ss $ mkWingmanMetaprogram ss mp
+    (x :: LHsExpr GhcPs) -> x
+
 tcRnModule :: HscEnv -> [Linkable] -> ParsedModule -> IO TcModuleResult
 tcRnModule hsc_env keep_lbls pmod = do
   let ms = pm_mod_summary pmod
@@ -817,7 +850,13 @@ parseFileContents
        -> ExceptT [FileDiagnostic] IO ([FileDiagnostic], ParsedModule)
 parseFileContents env customPreprocessor filename ms = do
    let loc  = mkRealSrcLoc (mkFastString filename) 1 1
-       dflags = ms_hspp_opts ms
+       dflags' = ms_hspp_opts ms
+       dflags =
+         dflags'
+            { staticPlugins =
+                staticPlugins dflags' <> [wingmanMetaprogrammingPlugin]
+            }
+
        contents = fromJust $ ms_hspp_buf ms
    case unP Parser.parseModule (mkPState dflags contents loc) of
 #if MIN_GHC_API_VERSION(8,10,0)

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

@@ -45,6 +45,8 @@ library
     Wingman.LanguageServer
     Wingman.LanguageServer.TacticProviders
     Wingman.Machinery
+    Wingman.Metaprogramming.Lexer
+    Wingman.Metaprogramming.Parser
     Wingman.Naming
     Wingman.Plugin
     Wingman.Range
@@ -86,6 +88,8 @@ library
     , transformers
     , unordered-containers
     , hyphenation
+    , megaparsec ^>=9
+    , parser-combinators
 
   default-language:   Haskell2010
   default-extensions:

plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

@@ -42,7 +42,7 @@ import           Development.IDE.Graph (Action, RuleResult, Rules, action)
 import           Development.IDE.Graph.Classes (Typeable, Binary, Hashable, NFData)
 import qualified FastString
 import           GHC.Generics (Generic)
-import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO, unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
@@ -62,6 +62,10 @@ import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
+import Generics.SYB hiding (Generic)
+import Development.IDE.Core.Compile (pattern WingmanMetaprogram)
+import Data.Foldable (for_)
+import Wingman.Metaprogramming.Parser (attempt_it)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -178,6 +182,10 @@ getIdeDynflags state nfp = do
   msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps
   pure $ ms_hspp_opts $ msrModSummary msr
 
+getAllMetaprograms :: Data a => a -> [String]
+getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
+  WingmanMetaprogram fs -> [ unpackFS fs ]
+  (_ :: HsExpr GhcTc)  -> mempty
 
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
@@ -199,6 +207,7 @@ judgementForHole state nfp range cfg = do
       binds <- stale GetBindings
       tcg <- fmap (fmap tmrTypechecked)
            $ stale TypeCheck
+
       hscenv <- stale GhcSessionDeps
 
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
@@ -212,6 +221,10 @@ judgementForHole state nfp range cfg = do
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
 
+      let mps = getAllMetaprograms $ tcg_binds $ untrackedStaleValue tcg
+      for_ mps $ \prog ->
+        liftIO $ putStrLn $ either id show $ attempt_it ctx jdg prog
+
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 

plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs

@@ -7,6 +7,7 @@ module Wingman.LanguageServer.TacticProviders
   , tcCommandId
   , TacticParams (..)
   , TacticProviderData (..)
+  , useNameFromHypothesis
   ) where
 
 import           Control.Monad

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs

@@ -0,0 +1,67 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
+
+module Wingman.Metaprogramming.Lexer where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Text (Text)
+import qualified Data.Text as T
+import           Data.Void
+import           Name
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
+import qualified Text.Megaparsec.Char.Lexer as L
+
+
+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
+
+ichar :: Parser Char
+ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\''
+
+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 "]")
+
+braces :: Parser a -> Parser a
+braces = P.between (symbol "{") (symbol "}")
+
+identifier :: Text -> Parser ()
+identifier i = lexeme (P.string i *> P.notFollowedBy ichar)
+
+-- 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 ichar
+    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 (ichar <|> P.char '-')
+    pure $ T.pack (c:cs)
+
+keyword :: Text -> Parser ()
+keyword = identifier
+

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

@@ -0,0 +1,83 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
+
+module Wingman.Metaprogramming.Parser where
+
+import qualified Control.Monad.Combinators.Expr as P
+import           Data.Functor
+import           Development.IDE.GHC.Compat (alphaTyVars, LHsExpr, GhcPs)
+import           GhcPlugins (mkTyVarTy)
+import qualified Refinery.Tactic as R
+import qualified Text.Megaparsec as P
+import           Wingman.Auto
+import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Lexer
+import           Wingman.Tactics
+import           Wingman.Types
+import qualified Data.Text as T
+
+
+nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
+nullary name tac = identifier name $> tac
+
+unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
+unary_occ name tac = tac <$> (identifier name *> variable)
+
+variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
+variadic_occ name tac = tac <$> (identifier name *> P.many variable)
+
+
+tactic :: Parser (TacticsM ())
+tactic = flip P.makeExprParser operators $  P.choice
+    [ braces tactic
+    , nullary   "assumption" assumption
+    , unary_occ "assume" assume
+    , variadic_occ   "intros" $ \case
+        []    -> intros
+        names -> intros' $ Just names
+    , nullary   "destruct_all" destructAll
+    , unary_occ "destruct" $ useNameFromHypothesis destruct
+    , unary_occ "homo" $ useNameFromHypothesis homo
+    , unary_occ "apply" $ useNameFromHypothesis apply
+    , unary_occ "split" userSplit
+    , nullary   "obvious" obvious
+    , nullary   "auto" auto
+    , R.try <$> (keyword "try" *> tactic)
+    ]
+
+bindOne :: TacticsM a -> TacticsM a -> TacticsM a
+bindOne t t1 = t R.<@> [t1]
+
+operators :: [[P.Operator Parser (TacticsM ())]]
+operators =
+    [ [ P.Prefix (symbol "*" $> R.many_) ]
+    , [ P.InfixR (symbol "|" $> (R.<%>) )]
+    , [ P.InfixL (symbol ";" $> (>>))
+      , P.InfixL (symbol "," $> bindOne)
+      ]
+    ]
+
+
+skolems :: [Type]
+skolems = fmap mkTyVarTy alphaTyVars
+
+a_skolem, b_skolem, c_skolem :: Type
+(a_skolem : b_skolem : c_skolem : _) = skolems
+
+
+attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs)
+attempt_it ctx jdg program =
+  case P.runParser (sc *> tactic <* P.eof) "<splice>" (T.pack program) of
+    Left peb -> Left $ P.errorBundlePretty peb
+    Right tt -> do
+      case runTactic
+             ctx
+             jdg
+             tt
+        of
+          Left tes -> Left $ show tes
+          Right rtr -> Right $ rtr_extract rtr
+

plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

@@ -10,6 +10,7 @@ import           Control.Monad (unless)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader (ask))
 import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
@@ -93,17 +94,26 @@ restrictPositionForApplication f app = do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = rule $ \jdg -> do
+intros = intros' Nothing
+
+------------------------------------------------------------------------------
+-- | Introduce a lambda binding every variable.
+intros'
+    :: Maybe [OccName]  -- ^ When 'Nothing', generate a new name for every
+                        -- variable. Otherwise, only bind the variables named.
+    -> TacticsM ()
+intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   ctx <- ask
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
-      let vs = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
-      let top_hole = isTopHole ctx jdg
+      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
+          num_args = length vs
+          top_hole = isTopHole ctx jdg
           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
           jdg' = introduce hy'
-               $ withNewGoal (CType b) jdg
+               $ withNewGoal (CType $ mkFunTys (drop num_args as) b) jdg
       ext <- newSubgoal jdg'
       pure $
         ext
@@ -255,6 +265,12 @@ splitSingle = tracing "splitSingle" $ do
       splitDataCon dc
     _ -> throwError $ GoalMismatch "splitSingle" g
 
+------------------------------------------------------------------------------
+-- | Like 'split', but prunes any data constructors which have holes.
+obvious :: TacticsM ()
+obvious = tracing "obvious" $ do
+  pruning split $ bool (Just NoProgress) Nothing . null
+
 
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
@@ -402,4 +418,3 @@ applyByName name = do
       True  -> apply hi
       False -> empty
 
-