Merge branch 'meta-use-any-term' into cata

Author: isovector

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

@@ -1,10 +1,10 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE TypeFamilies      #-}
 
 {-# LANGUAGE NoMonoLocalBinds  #-}
-{-# LANGUAGE TupleSections #-}
 
 module Wingman.LanguageServer where
 
@@ -17,7 +17,6 @@ import           Control.Monad.State (State, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
-import           Data.Foldable (toList)
 import           Data.Functor ((<&>))
 import           Data.Functor.Identity (runIdentity)
 import qualified Data.HashMap.Strict as Map
@@ -67,7 +66,6 @@ import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
 import           Wingman.Judgements.Theta
-import           Wingman.Machinery (getOccNameType)
 import           Wingman.Metaprogramming.Lexer (ParserContext(..))
 import           Wingman.Range
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
@@ -581,6 +579,10 @@ mkWorkspaceEdits dflags ccs uri pm g = do
    in first (InfrastructureError . T.pack) response
 
 
+------------------------------------------------------------------------------
+-- | Add ExactPrint annotations to every metaprogram in the source tree.
+-- Usually the ExactPrint module can do this for us, but we've enabled
+-- QuasiQuotes, so the round-trip print/parse journey will crash.
 annotateMetaprograms :: Data a => a -> Transform a
 annotateMetaprograms = everywhereM $ mkM $ \case
   L ss (WingmanMetaprogram mp) -> do
@@ -591,6 +593,8 @@ annotateMetaprograms = everywhereM $ mkM $ \case
   (x :: LHsExpr GhcPs) -> pure x
 
 
+------------------------------------------------------------------------------
+-- | Find the source of a tactic metaprogram at the given span.
 getMetaprogramAtSpan
     :: Tracked age SrcSpan
     -> Tracked age TcGblEnv
@@ -603,36 +607,19 @@ getMetaprogramAtSpan (unTrack -> ss)
   . unTrack
 
 
-getOccNameTypes
-    :: Foldable t
-    => IdeState
-    -> NormalizedFilePath
-    -> t OccName
-    -> MaybeT IO (M.Map OccName Type)
-getOccNameTypes state nfp occs = do
-  let stale a = runStaleIde "getOccNameTypes" state nfp a
-
-  TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck
-  TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
-
-  let tcgblenv = tmrTypechecked tcmod
-      modul = extractModule tcgblenv
-      rdrenv = tcg_rdr_env tcgblenv
-  lift $ fmap M.fromList $
-    fmap join $ for (toList occs) $ \occ ->
-      fmap (maybeToList . fmap (occ, )) $
-        getOccNameType (hscEnv hscenv) rdrenv modul occ
-
-
+------------------------------------------------------------------------------
+-- | The metaprogram parser needs the ability to lookup terms from the module
+-- and imports. The 'ParserContext' contains everything we need to find that
+-- stuff.
 getParserState
     :: IdeState
     -> NormalizedFilePath
-   -> Context
+    -> Context
     -> MaybeT IO ParserContext
 getParserState state nfp ctx = do
-  let stale a = runStaleIde "getOccNameTypes" state nfp a
+  let stale a = runStaleIde "getParserState" state nfp a
 
-  TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck
+  TrackedStale (unTrack -> tcmod) _  <- stale TypeCheck
   TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
 
   let tcgblenv = tmrTypechecked tcmod

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

@@ -332,6 +332,8 @@ useNameFromContext f name = do
     Nothing -> throwError $ NotInScope name
 
 
+------------------------------------------------------------------------------
+-- | Find the type of an 'OccName' that is defined in the current module.
 lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
 lookupNameInContext name = do
   ctx <- asks ctxModuleFuncs
@@ -340,6 +342,8 @@ lookupNameInContext name = do
     Nothing      -> empty
 
 
+------------------------------------------------------------------------------
+-- | Build a 'HyInfo' for an imported term.
 createImportedHyInfo :: OccName -> CType -> HyInfo CType
 createImportedHyInfo on ty = HyInfo
   { hi_name = on
@@ -348,6 +352,10 @@ createImportedHyInfo on ty = HyInfo
   }
 
 
+------------------------------------------------------------------------------
+-- | Lookup the type of any 'OccName' that was imported. Necessarily done in
+-- IO, so we only expose this functionality to the parser. Internal Haskell
+-- code that wants to lookup terms should do it via 'KnownThings'.
 getOccNameType
     :: HscEnv
     -> OccEnv [GlobalRdrElt]

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

@@ -20,6 +20,8 @@ import qualified Text.Megaparsec.Char.Lexer as L
 import Wingman.Types (Context)
 
 
+------------------------------------------------------------------------------
+-- | Everything we need in order to call 'Wingman.Machinery.getOccNameType'.
 data ParserContext = ParserContext
   { ps_hscEnv :: HscEnv
   , ps_occEnv :: OccEnv [GlobalRdrElt]

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

@@ -27,15 +27,21 @@ import           Wingman.Types
 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)
 
+
+------------------------------------------------------------------------------
+-- | Like 'unary_occ', but runs directly in the 'Parser' monad.
 unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
 unary_occM name tac = tac =<< (identifier name *> variable)
 
+
 variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
 variadic_occ name tac = tac <$> (identifier name *> P.many variable)
 
+
 oneTactic :: Parser (TacticsM ())
 oneTactic =
   P.choice
@@ -106,6 +112,9 @@ wrapError :: String -> String
 wrapError err = "```\n" <> err <> "\n```\n"
 
 
+------------------------------------------------------------------------------
+-- | Attempt to run a metaprogram tactic, returning the proof state, or the
+-- errors.
 attempt_it
     :: Context
     -> Judgement
@@ -130,6 +139,8 @@ parseMetaprogram
     . P.runParserT tacticProgram "<splice>"
 
 
+------------------------------------------------------------------------------
+-- | Like 'getOccNameType', but runs in the 'Parser' monad.
 getOccTy :: OccName -> Parser Type
 getOccTy occ = do
   ParserContext hscenv rdrenv modul _ <- ask

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

@@ -24,23 +24,23 @@ import qualified Data.Set as S
 import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
+import           GHC.SourceGen ((@@))
 import           GHC.SourceGen.Expr
 import           Name (occNameString, occName)
+import           OccName (mkVarOcc)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import           TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar)
 import           Wingman.CodeGen
 import           Wingman.Context
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Machinery
 import           Wingman.Naming
+import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
 import           Wingman.Types
-import OccName (mkVarOcc)
-import Wingman.StaticPlugin (pattern MetaprogramSyntax)
-import GHC.SourceGen ((@@))
-import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar)
 
 
 ------------------------------------------------------------------------------
@@ -440,6 +440,9 @@ applyByName name = do
       False -> empty
 
 
+------------------------------------------------------------------------------
+-- | Make a function application where the function being applied itself is
+-- a hole.
 applyByType :: Type -> TacticsM ()
 applyByType ty = tracing ("applyByType " <> show ty) $ do
   jdg <- goal
@@ -463,9 +466,14 @@ applyByType ty = tracing ("applyByType " <> show ty) $ do
           <*> fmap (fmap unLoc) ext
 
 
+------------------------------------------------------------------------------
+-- | Make an n-ary function call of the form
+-- @(_ :: forall a b. a -> a -> b) _ _@.
 nary :: Int -> TacticsM ()
-nary n = do
-  applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ mkFunTys (replicate n alphaTy) betaTy
+nary n =
+  applyByType $
+    mkInvForAllTys [alphaTyVar, betaTyVar] $
+      mkFunTys (replicate n alphaTy) betaTy
 
 
 self :: TacticsM ()

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

@@ -153,12 +153,6 @@ instance Show TyCon where
 instance Show ConLike where
   show  = unsafeRender
 
-instance Show (HsBindLR GhcTc GhcTc) where
-  show  = unsafeRender
-
-instance Show (ABExport GhcTc) where
-  show  = unsafeRender
-
 
 ------------------------------------------------------------------------------
 -- | The state that should be shared between subgoals. Extracts move towards

plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs

@@ -28,6 +28,9 @@ spec = do
     metaTest  2 32 "MetaBindAll"
     metaTest  2 13 "MetaTry"
     metaTest  2 74 "MetaChoice"
+    metaTest  5 40 "MetaUseImport"
+    metaTest  6 31 "MetaUseLocal"
+    metaTest 11 11 "MetaUseMethod"
     metaTest  9 38 "MetaCataCollapse"
     metaTest  7 16 "MetaCataCollapseUnary"
 

plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs

@@ -0,0 +1,6 @@
+import Data.Char
+
+
+result :: Char -> Bool
+result = isAlpha
+

plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs

@@ -0,0 +1,6 @@
+import Data.Char
+
+
+result :: Char -> Bool
+result = [wingman| intro c, use isAlpha, assume c |]
+

plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs

@@ -0,0 +1,7 @@
+test :: Int
+test = 0
+
+
+resolve :: Int
+resolve = test
+

plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs

@@ -0,0 +1,7 @@
+test :: Int
+test = 0
+
+
+resolve :: Int
+resolve = [wingman| use test |]
+

plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs

@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+class Test where
+  test :: Int
+
+instance Test where
+  test = 10
+
+
+resolve :: Int
+resolve = test
+

plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs

@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+class Test where
+  test :: Int
+
+instance Test where
+  test = 10
+
+
+resolve :: Int
+resolve = [wingman| use test |]
+