Cleanup and haddock

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

@@ -3,6 +3,7 @@
 module Wingman.Machinery where
 
 import           Class (Class (classTyVars))
+import           Control.Applicative (empty)
 import           Control.Lens ((<>~))
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
@@ -22,7 +23,9 @@ import           Data.Monoid (getSum)
 import           Data.Ord (Down (..), comparing)
 import           Data.Set (Set)
 import qualified Data.Set as S
+import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
+import           GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv)
 import           OccName (HasOccName (occName), OccEnv)
 import           Refinery.ProofState
 import           Refinery.Tactic
@@ -33,9 +36,6 @@ import           Unify
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
-import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv)
-import Development.IDE.Core.Compile (lookupName)
-import Control.Applicative (empty)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -328,6 +328,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
@@ -336,6 +338,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
@@ -344,6 +348,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
@@ -104,6 +110,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
@@ -128,6 +137,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,7 +466,12 @@ 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
 

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