Remove unused imports

Author: nvarner

agda-language-server.cabal

@@ -106,7 +106,7 @@ library
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Werror=incomplete-patterns -Wunused-local-binds -Wunused-pattern-binds -Wunused-do-bind -Wunused-foralls -Wunused-imports -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Wsimplifiable-class-constraints -fno-warn-orphans -Werror
   build-depends:
       Agda
     , aeson
@@ -153,7 +153,7 @@ executable als
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Werror=incomplete-patterns -Wunused-local-binds -Wunused-pattern-binds -Wunused-do-bind -Wunused-foralls -Wunused-imports -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Wsimplifiable-class-constraints -fno-warn-orphans -Werror -rtsopts
   build-depends:
       Agda
     , aeson
@@ -268,7 +268,7 @@ test-suite als-test
       OverloadedStrings
       PatternSynonyms
       TypeOperators
-  ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans
+  ghc-options: -Wincomplete-patterns -Werror=incomplete-patterns -Wunused-local-binds -Wunused-pattern-binds -Wunused-do-bind -Wunused-foralls -Wunused-imports -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Wsimplifiable-class-constraints -fno-warn-orphans -Werror -rtsopts
   build-depends:
       Agda
     , aeson

app/Main.hs

@@ -5,12 +5,10 @@ import Control.Monad (when)
 import Options
 import Server (run)
 -- import Simple (run)
-import System.Console.GetOpt
 import System.Directory (doesDirectoryExist)
 import System.Environment
 import System.FilePath ((</>))
 import System.IO
-import Text.Read (readMaybe)
 
 #if MIN_VERSION_Agda(2,8,0)
 import Agda.Setup (setup)

package.yaml

@@ -51,6 +51,10 @@ when:
 - condition: "arch(wasm32)"
   dependencies:
     - unix >= 2.8.0.0 && < 2.9
+- condition: "!arch(wasm32)"
+  ghc-options:
+  - -threaded
+  - -with-rtsopts=-N
 
 dependencies:
   - base >= 4.7 && < 5
@@ -78,48 +82,33 @@ default-extensions:
 - PatternSynonyms
 - TypeOperators
 
+ghc-options:
+- -Wincomplete-patterns
+- -Werror=incomplete-patterns
+- -Wunused-local-binds
+- -Wunused-pattern-binds
+- -Wunused-do-bind
+- -Wunused-foralls
+- -Wunused-imports
+- -Wwarnings-deprecations
+- -Wwrong-do-bind
+- -Wmissing-fields
+- -Wmissing-methods
+- -Wmissing-pattern-synonym-signatures
+- -Wmissing-signatures
+- -Wsimplifiable-class-constraints
+- -fno-warn-orphans
+- -Werror
+
 library:
   source-dirs: src
-  ghc-options:
-  - -Wincomplete-patterns
-  - -Wunused-do-bind
-  - -Wunused-foralls
-  - -Wwarnings-deprecations
-  - -Wwrong-do-bind
-  - -Wmissing-fields
-  - -Wmissing-methods
-  - -Wmissing-pattern-synonym-signatures
-  - -Wmissing-signatures
-  - -Werror=incomplete-patterns
-  - -fno-warn-orphans
-  when:
-  - condition: "!arch(wasm32)"
-    ghc-options:
-    - -threaded
-    - -with-rtsopts=-N
 
 executables:
   als:
-    main:                Main.hs
-    source-dirs:         app
+    main: Main.hs
+    source-dirs: app
     ghc-options:
-    - -Wincomplete-patterns
-    - -Wunused-do-bind
-    - -Wunused-foralls
-    - -Wwarnings-deprecations
-    - -Wwrong-do-bind
-    - -Wmissing-fields
-    - -Wmissing-methods
-    - -Wmissing-pattern-synonym-signatures
-    - -Wmissing-signatures
     - -rtsopts
-    - -Werror=incomplete-patterns
-    - -fno-warn-orphans
-    when:
-    - condition: "!arch(wasm32)"
-      ghc-options:
-      - -threaded
-      - -with-rtsopts=-N
     dependencies:
     - agda-language-server
 
@@ -129,39 +118,11 @@ tests:
     source-dirs:
       - test
       - src
+    ghc-options:
+      - -rtsopts
     dependencies:
       - lsp-test
       - tasty
       - tasty-hunit
       - tasty-golden
       - tasty-quickcheck
-
-    ghc-options:
-      - -Wincomplete-patterns
-      - -Wunused-do-bind
-      - -Wunused-foralls
-      - -Wwarnings-deprecations
-      - -Wwrong-do-bind
-      - -Wmissing-fields
-      - -Wmissing-methods
-      - -Wmissing-pattern-synonym-signatures
-      - -Wmissing-signatures
-      - -rtsopts
-      - -Werror=incomplete-patterns
-      - -fno-warn-orphans
-    when:
-    - condition: "!arch(wasm32)"
-      ghc-options:
-      - -threaded
-      - -with-rtsopts=-N
-
-# tests:
-#   als-test:
-#     main:                Spec.hs
-#     source-dirs:         test
-#     ghc-options:
-#     - -threaded
-#     - -rtsopts
-#     - -with-rtsopts=-N
-#     dependencies:
-#     - agda-language-server

src/Agda.hs

@@ -24,7 +24,7 @@ import           Agda.Interaction.Base          ( Command
                                                 , CommandM
 #endif
                                                 , CommandState(optionsOnReload)
-                                                , IOTCM
+                                                
                                                 , initCommandState
                                                 , parseIOTCM
                                                 )
@@ -61,7 +61,6 @@ import           Agda.TypeChecking.Monad.Base   ( TCM )
 import qualified Agda.TypeChecking.Monad.Benchmark
                                                as Bench
 import           Agda.TypeChecking.Monad.State  ( setInteractionOutputCallback )
-import           Agda.Utils.FileName            ( absolute )
 import           Agda.Utils.Impossible          ( CatchImpossible
                                                   ( catchImpossible
                                                   )
@@ -82,18 +81,16 @@ import           Data.Aeson                     ( FromJSON
                                                 , fromJSON
                                                 )
 import qualified Data.Aeson                    as JSON
-import           Data.Maybe                     ( listToMaybe )
 import           Data.Text                      ( pack )
 import           GHC.Generics                   ( Generic )
-import           Language.LSP.Server            ( getConfig )
 import           Monad
 import           Options                        ( Config(configRawAgdaOptions)
                                                 , Options(optRawAgdaOptions, optRawResponses)
                                                 , versionNumber
                                                 )
 
 import qualified Agda.IR                       as IR
-import           Agda.Interaction.JSON          ( encode, encodeTCM )
+import           Agda.Interaction.JSON          ( encodeTCM )
 import           Agda.Interaction.JSONTop       ()
 
 getAgdaVersion :: String

src/Agda/Convert.hs

@@ -13,7 +13,6 @@ import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..),
 import qualified Agda.Interaction.Highlighting.Range as Highlighting
 #if MIN_VERSION_Agda(2,8,0)
 import Agda.Interaction.Command (localStateCommandM)
-import Agda.TypeChecking.Monad.Base (topLevelModuleFilePath)
 #else
 import Agda.Interaction.InteractionTop (localStateCommandM)
 #endif
@@ -26,37 +25,42 @@ import Agda.Syntax.Abstract.Pretty (prettyATop)
 import Agda.Syntax.Common
 import Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal (alwaysUnblock)
-import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
-import Agda.Syntax.Scope.Base
-import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError)
+import Agda.Syntax.Position (noRange)
+import Agda.TypeChecking.Errors (explainWhyInScope)
 import Agda.TypeChecking.Monad hiding (Function)
-import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
 import Agda.TypeChecking.Pretty (prettyTCM)
 import qualified Agda.TypeChecking.Pretty as TCP
-import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
+#if MIN_VERSION_Agda(2,7,0)
+#else
 import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors (..))
+#endif
+import Agda.TypeChecking.Pretty.Warning (filterTCWarnings)
 import Agda.Utils.FileName (filePath)
 import Agda.Utils.Function (applyWhen)
 import Agda.Utils.IO.TempFile (writeToTempFile)
+#if MIN_VERSION_Agda(2,8,0)
+#else
 import Agda.Utils.Impossible (__IMPOSSIBLE__)
+#endif
 import Agda.Utils.Maybe (catMaybes)
 import Agda.Utils.Null (empty)
 import Agda.Utils.RangeMap (IsBasicRangeMap (toList))
-import Agda.Utils.String (delimiter)
 import Agda.Utils.Time (CPUTime)
 import Agda.VersionCommit (versionWithCommitInfo)
 import Control.Monad
 import Control.Monad.State hiding (state)
 import qualified Data.Aeson as JSON
 import qualified Data.ByteString.Lazy.Char8 as BS8
 import qualified Data.List as List
+#if MIN_VERSION_Agda(2,8,0)
+#else
 import qualified Data.Map as Map
+#endif
 import Data.String (IsString)
 import Render (Block (..), Inlines, Render (..), renderATop)
 import qualified Render
 
 import Agda.Syntax.Common.Pretty hiding (render)
-import qualified Prettyprinter
 
 responseAbbr :: (IsString a) => Response -> a
 responseAbbr res = case res of

src/Agda/Interaction/Imports/More.hs

@@ -4,30 +4,29 @@ module Agda.Interaction.Imports.More
   ( setOptionsFromSourcePragmas,
     checkModuleName',
     runPMDropWarnings,
+    srcFilePath,
     moduleName,
     runPM,
     beginningOfFile,
   )
 where
 
 import Agda.Interaction.FindFile (
-    SourceFile (SourceFile),
     checkModuleName,
 #if MIN_VERSION_Agda(2,8,0)
+    SourceFile,
     rootNameModule,
 #else
+    SourceFile (SourceFile),
     moduleName,
 #endif
   )
-import Agda.Interaction.Imports (Source (..))
 import qualified Agda.Interaction.Imports as Imp
 import Agda.Interaction.Library (OptionsPragma (..), _libPragmas)
 import Agda.Interaction.Library.More ()
 import Agda.Syntax.Common (TopLevelModuleName')
 import qualified Agda.Syntax.Concrete as C
 import Agda.Syntax.Parser (
-    moduleParser,
-    parseFile,
 #if MIN_VERSION_Agda(2,8,0)
     parse,
     moduleNameParser,
@@ -38,35 +37,28 @@ import Agda.Syntax.Parser (
   )
 import Agda.Syntax.Position
   ( Range,
-    Range' (Range),
-    RangeFile,
     getRange,
-    intervalToRange,
-    mkRangeFile,
-    posToRange,
-    posToRange',
-    startPos,
 #if MIN_VERSION_Agda(2,8,0)
     beginningOfFile,
     rangeFromAbsolutePath,
+#else
+    RangeFile,
+    posToRange,
+    startPos,
 #endif
   )
+#if MIN_VERSION_Agda(2,8,0)
 import Agda.Syntax.TopLevelModuleName (
     TopLevelModuleName,
     RawTopLevelModuleName (..),
-#if MIN_VERSION_Agda(2,8,0)
     rawTopLevelModuleNameForModule,
-#endif
   )
-import Agda.Syntax.Common.Pretty (Pretty, pretty, text, prettyAssign, (<+>))
+#endif
+import Agda.Syntax.Common.Pretty (Pretty, pretty, text, (<+>))
 import Agda.TypeChecking.Monad
-  ( Interface,
-    TCM,
+  ( TCM,
     setCurrentRange,
     setOptionsFromPragma,
-    setTCLens,
-    stPragmaOptions,
-    useTC,
 #if MIN_VERSION_Agda(2,7,0)
     checkAndSetOptionsFromPragma,
 #endif
@@ -76,17 +68,15 @@ import Agda.TypeChecking.Monad
 #endif
   )
 import qualified Agda.TypeChecking.Monad as TCM
-import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 #if MIN_VERSION_Agda(2,8,0)
+import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 #else
 import Agda.TypeChecking.Warnings (runPM)
 #endif
 import Agda.Utils.FileName (AbsolutePath)
-import Agda.Utils.Monad (bracket_)
 #if MIN_VERSION_Agda(2,8,0)
 import qualified Data.Text as T
 #endif
-import qualified Data.Text.Lazy as TL
 import Control.Monad.Error.Class (
 #if MIN_VERSION_Agda(2,8,0)
     catchError,
@@ -98,13 +88,6 @@ import Control.Monad.Error.Class (
 import Agda.Utils.Singleton (singleton)
 #endif
 
-srcFilePath :: SourceFile -> TCM AbsolutePath
-#if MIN_VERSION_Agda(2,8,0)
-srcFilePath = TCM.srcFilePath
-#else
-srcFilePath (SourceFile f) = return f
-#endif
-
 #if MIN_VERSION_Agda(2,8,0)
 -- beginningOfFile was generalized in Agda 2.8.0 to support the features we
 -- need, so we just import it
@@ -124,6 +107,14 @@ runPMDropWarnings m = do
     Right a -> return a
 #endif
 
+#if MIN_VERSION_Agda(2,8,0)
+srcFilePath :: (TCM.MonadFileId m) => SourceFile -> m AbsolutePath
+srcFilePath = TCM.srcFilePath
+#else
+srcFilePath :: (Monad m) => SourceFile -> m AbsolutePath
+srcFilePath (SourceFile path) = return path
+#endif
+
 -- Unexported Agda functions
 
 srcDefaultPragmas :: Imp.Source -> [OptionsPragma]