From d4bd8e63534886faad116074a43c8cdc382fbabf Mon Sep 17 00:00:00 2001 From: Jason Felice Date: Sat, 16 Sep 2017 13:28:47 -0400 Subject: [PATCH] Clean up unused imports (#4065) --- codegen/idris-codegen-c/Main.hs | 3 --- codegen/idris-codegen-javascript/Main.hs | 3 --- codegen/idris-codegen-node/Main.hs | 3 --- idris.cabal | 1 - main/Main.hs | 7 +----- src/IRTS/BCImp.hs | 23 ----------------- src/IRTS/Bytecode.hs | 1 - src/IRTS/CodegenC.hs | 4 --- src/IRTS/Compiler.hs | 10 -------- src/IRTS/Defunctionalise.hs | 1 - src/IRTS/DumpBC.hs | 1 - src/IRTS/JavaScript/LangTransforms.hs | 5 ---- src/IRTS/JavaScript/Name.hs | 3 --- src/IRTS/JavaScript/PrimOp.hs | 4 --- src/IRTS/JavaScript/Specialize.hs | 3 --- src/IRTS/Lang.hs | 2 -- src/IRTS/LangOpts.hs | 4 --- src/IRTS/Portable.hs | 2 -- src/IRTS/Simplified.hs | 3 --- src/Idris/ASTUtils.hs | 1 - src/Idris/AbsSyntaxTree.hs | 1 - src/Idris/Apropos.hs | 2 +- src/Idris/Chaser.hs | 6 +---- src/Idris/Core/Binary.hs | 4 --- src/Idris/Core/CaseTree.hs | 3 --- src/Idris/Core/Constraints.hs | 6 ++--- src/Idris/Core/Elaborate.hs | 7 ------ src/Idris/Core/Execute.hs | 6 ----- src/Idris/Core/ProofState.hs | 2 -- src/Idris/Core/ProofTerm.hs | 3 --- src/Idris/Core/TT.hs | 9 ++----- src/Idris/Core/Typecheck.hs | 3 --- src/Idris/Core/Unify.hs | 2 -- src/Idris/Core/WHNF.hs | 3 --- src/Idris/Coverage.hs | 3 --- src/Idris/DSL.hs | 2 -- src/Idris/DataOpts.hs | 6 ----- src/Idris/DeepSeq.hs | 1 - src/Idris/Delaborate.hs | 3 +-- src/Idris/Directives.hs | 1 - src/Idris/Elab/AsPat.hs | 1 - src/Idris/Elab/Clause.hs | 17 ++----------- src/Idris/Elab/Data.hs | 21 +--------------- src/Idris/Elab/Implementation.hs | 27 ++------------------ src/Idris/Elab/Interface.hs | 31 +---------------------- src/Idris/Elab/Provider.hs | 27 -------------------- src/Idris/Elab/Record.hs | 15 +---------- src/Idris/Elab/Rewrite.hs | 3 --- src/Idris/Elab/RunElab.hs | 4 +-- src/Idris/Elab/Term.hs | 14 +++-------- src/Idris/Elab/Transform.hs | 30 +--------------------- src/Idris/Elab/Type.hs | 29 +-------------------- src/Idris/Elab/Utils.hs | 4 --- src/Idris/Elab/Value.hs | 32 ++---------------------- src/Idris/ElabDecls.hs | 27 +------------------- src/Idris/Erasure.hs | 3 --- src/Idris/ErrReverse.hs | 1 - src/Idris/Error.hs | 7 ------ src/Idris/IdeMode.hs | 2 +- src/Idris/IdrisDoc.hs | 13 +++------- src/Idris/Imports.hs | 1 - src/Idris/Info.hs | 1 - src/Idris/Output.hs | 5 ++-- src/Idris/Package.hs | 5 +--- src/Idris/Package/Parser.hs | 6 ----- src/Idris/Parser/Data.hs | 15 ----------- src/Idris/Parser/Expr.hs | 12 --------- src/Idris/Parser/Helpers.hs | 6 ----- src/Idris/Parser/Ops.hs | 13 ---------- src/Idris/PartialEval.hs | 3 --- src/Idris/Primitives.hs | 3 --- src/Idris/ProofSearch.hs | 3 --- src/Idris/Prover.hs | 8 +++--- src/Idris/Providers.hs | 2 -- src/Idris/REPL/Parser.hs | 5 +--- src/Idris/Termination.hs | 3 +-- src/Idris/Transforms.hs | 3 --- src/Idris/TypeSearch.hs | 2 +- src/Util/DynamicLinker.hs | 29 +++++++++++++-------- stack.yaml | 3 +++ 80 files changed, 60 insertions(+), 533 deletions(-) delete mode 100644 src/IRTS/BCImp.hs diff --git a/codegen/idris-codegen-c/Main.hs b/codegen/idris-codegen-c/Main.hs index a525d355d..594ea0d62 100644 --- a/codegen/idris-codegen-c/Main.hs +++ b/codegen/idris-codegen-c/Main.hs @@ -1,7 +1,6 @@ module Main where import Idris.AbsSyntax -import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options @@ -10,8 +9,6 @@ import IRTS.Compiler import Util.System -import Paths_idris - import Control.Monad import System.Environment import System.Exit diff --git a/codegen/idris-codegen-javascript/Main.hs b/codegen/idris-codegen-javascript/Main.hs index 1d13a2612..e8728fcc6 100644 --- a/codegen/idris-codegen-javascript/Main.hs +++ b/codegen/idris-codegen-javascript/Main.hs @@ -1,15 +1,12 @@ module Main where import Idris.AbsSyntax -import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options import IRTS.CodegenJavaScript import IRTS.Compiler -import Paths_idris - import System.Environment import System.Exit diff --git a/codegen/idris-codegen-node/Main.hs b/codegen/idris-codegen-node/Main.hs index 3300f0fb7..b61e0e025 100644 --- a/codegen/idris-codegen-node/Main.hs +++ b/codegen/idris-codegen-node/Main.hs @@ -1,15 +1,12 @@ module Main where import Idris.AbsSyntax -import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options import IRTS.CodegenJavaScript import IRTS.Compiler -import Paths_idris - import System.Environment import System.Exit diff --git a/idris.cabal b/idris.cabal index d880d2bfd..52e2bc291 100644 --- a/idris.cabal +++ b/idris.cabal @@ -226,7 +226,6 @@ Library , Idris.WhoCalls , Idris.CmdOptions - , IRTS.BCImp , IRTS.Bytecode , IRTS.CodegenC , IRTS.CodegenCommon diff --git a/main/Main.hs b/main/Main.hs index 26ea7032b..a90e2d3fc 100644 --- a/main/Main.hs +++ b/main/Main.hs @@ -2,9 +2,7 @@ module Main where import System.Exit (ExitCode(..), exitSuccess, exitWith) -import Control.Monad (unless, when, (>=>)) -import Data.Foldable (foldrM) -import Data.Maybe (fromMaybe) +import Control.Monad (unless, when) import Idris.AbsSyntax import Idris.CmdOptions @@ -16,9 +14,6 @@ import Idris.Package import Util.System (setupBundledCC) -import System.Exit (ExitCode(..), exitWith) -import Util.System (setupBundledCC) - processShowOptions :: [Opt] -> Idris () processShowOptions opts = runIO $ do when (ShowAll `elem` opts) $ showExitIdrisInfo diff --git a/src/IRTS/BCImp.hs b/src/IRTS/BCImp.hs deleted file mode 100644 index 5bcf5857e..000000000 --- a/src/IRTS/BCImp.hs +++ /dev/null @@ -1,23 +0,0 @@ -{-| -Module : IRTS.BCImp -Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC) -Copyright : -License : BSD3 -Maintainer : The Idris Community. --} -module IRTS.BCImp where - -import Idris.Core.TT -import IRTS.Lang -import IRTS.Simplified - -data Reg = RVal | L Int - -data BC = NOP - -toBC :: (Name, SDecl) -> (Name, [BC]) -toBC (n, SFun n' args locs exp) - = (n, bc RVal exp) - -bc :: Reg -> SExp -> [BC] -bc = undefined diff --git a/src/IRTS/Bytecode.hs b/src/IRTS/Bytecode.hs index 24b9c97dc..fb27096b9 100644 --- a/src/IRTS/Bytecode.hs +++ b/src/IRTS/Bytecode.hs @@ -23,7 +23,6 @@ module IRTS.Bytecode where import Idris.Core.TT import IRTS.Defunctionalise -import IRTS.Lang import IRTS.Simplified import Data.Maybe diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs index 9aa9ac63e..a7c2aeaa3 100644 --- a/src/IRTS/CodegenC.hs +++ b/src/IRTS/CodegenC.hs @@ -9,12 +9,10 @@ Maintainer : The Idris Community. module IRTS.CodegenC (codegenC) where -import Idris.AbsSyntax import Idris.Core.TT import IRTS.Bytecode import IRTS.CodegenCommon import IRTS.Defunctionalise -import IRTS.Lang import IRTS.Simplified import IRTS.System @@ -24,9 +22,7 @@ import Control.Monad import Data.Bits import Data.Char import Data.List (intercalate, nubBy) -import Debug.Trace import Numeric -import System.Directory import System.Exit import System.FilePath ((<.>), ()) import System.IO diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs index 0af967bbd..09c7aca5c 100644 --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -10,7 +10,6 @@ Maintainer : The Idris Community. module IRTS.Compiler(compile, generate) where import Idris.AbsSyntax -import Idris.AbsSyntaxTree import Idris.ASTUtils import Idris.Core.CaseTree import Idris.Core.Evaluate @@ -21,33 +20,24 @@ import Idris.Options import Idris.Output import IRTS.CodegenC import IRTS.CodegenCommon -import IRTS.CodegenJavaScript import IRTS.Defunctionalise import IRTS.DumpBC import IRTS.Exports import IRTS.Inliner -import IRTS.Lang import IRTS.LangOpts import IRTS.Portable import IRTS.Simplified import Prelude hiding (id, (.)) -import Control.Applicative import Control.Category import Control.Monad.State -import Data.IntSet (IntSet) -import qualified Data.IntSet as IS import Data.List import qualified Data.Map as M -import Data.Maybe import Data.Ord import qualified Data.Set as S -import Debug.Trace import System.Directory -import System.Environment import System.Exit -import System.FilePath (addTrailingPathSeparator, ()) import System.IO import System.Process diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs index 7994cf2b0..500ad08b6 100644 --- a/src/IRTS/Defunctionalise.hs +++ b/src/IRTS/Defunctionalise.hs @@ -32,7 +32,6 @@ import Control.Monad import Control.Monad.State import Data.List import Data.Maybe -import Debug.Trace data DExp = DV Name | DApp Bool Name [DExp] -- True = tail call diff --git a/src/IRTS/DumpBC.hs b/src/IRTS/DumpBC.hs index 43f00761b..bcad069aa 100644 --- a/src/IRTS/DumpBC.hs +++ b/src/IRTS/DumpBC.hs @@ -9,7 +9,6 @@ module IRTS.DumpBC where import Idris.Core.TT import IRTS.Bytecode -import IRTS.Lang import IRTS.Simplified import Data.List diff --git a/src/IRTS/JavaScript/LangTransforms.hs b/src/IRTS/JavaScript/LangTransforms.hs index 61c66cab4..7560bbd0e 100644 --- a/src/IRTS/JavaScript/LangTransforms.hs +++ b/src/IRTS/JavaScript/LangTransforms.hs @@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode ) where -import Control.DeepSeq -import Control.Monad.Trans.State import Data.List import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe import Data.Set (Set) import qualified Data.Set as Set -import Data.Text (Text) -import qualified Data.Text as T import Idris.Core.CaseTree import Idris.Core.TT import IRTS.Lang import Data.Data import Data.Generics.Uniplate.Data -import GHC.Generics (Generic) deriving instance Typeable FDesc deriving instance Data FDesc diff --git a/src/IRTS/JavaScript/Name.hs b/src/IRTS/JavaScript/Name.hs index 175a58874..546197e1f 100644 --- a/src/IRTS/JavaScript/Name.hs +++ b/src/IRTS/JavaScript/Name.hs @@ -20,12 +20,9 @@ module IRTS.JavaScript.Name ) where import Data.Char -import Data.List -import qualified Data.Map.Strict as Map import Data.Text (Text) import qualified Data.Text as T import Idris.Core.TT -import IRTS.JavaScript.AST jsEscape :: String -> String jsEscape = concatMap jschar diff --git a/src/IRTS/JavaScript/PrimOp.hs b/src/IRTS/JavaScript/PrimOp.hs index 0e11a6429..668f9bd34 100644 --- a/src/IRTS/JavaScript/PrimOp.hs +++ b/src/IRTS/JavaScript/PrimOp.hs @@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp , jsPrimCoerce ) where -import Data.Char -import Data.List import qualified Data.Map.Strict as Map -import Data.Text (Text) -import qualified Data.Text as T import Idris.Core.TT import IRTS.JavaScript.AST import IRTS.Lang diff --git a/src/IRTS/JavaScript/Specialize.hs b/src/IRTS/JavaScript/Specialize.hs index 2cf4e1275..910836bbe 100644 --- a/src/IRTS/JavaScript/Specialize.hs +++ b/src/IRTS/JavaScript/Specialize.hs @@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize , qualifyN ) where -import Data.Char -import Data.List import qualified Data.Map.Strict as Map -import Data.Text (Text) import qualified Data.Text as T import Idris.Core.TT import IRTS.JavaScript.AST diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs index 7384bf6bb..94487b342 100644 --- a/src/IRTS/Lang.hs +++ b/src/IRTS/Lang.hs @@ -13,12 +13,10 @@ module IRTS.Lang where import Idris.Core.CaseTree import Idris.Core.TT -import Control.Applicative hiding (Const) import Control.Monad.State hiding (lift) import Data.Data (Data) import Data.List import Data.Typeable (Typeable) -import Debug.Trace import GHC.Generics (Generic) data Endianness = Native | BE | LE deriving (Show, Eq) diff --git a/src/IRTS/LangOpts.hs b/src/IRTS/LangOpts.hs index 11be92877..90df9add0 100644 --- a/src/IRTS/LangOpts.hs +++ b/src/IRTS/LangOpts.hs @@ -9,14 +9,10 @@ Maintainer : The Idris Community. module IRTS.LangOpts where -import Idris.Core.CaseTree import Idris.Core.TT import IRTS.Lang -import Control.Applicative hiding (Const) import Control.Monad.State hiding (lift) -import Data.List -import Debug.Trace inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)] inlineAll lds = let defs = addAlist lds emptyContext in diff --git a/src/IRTS/Portable.hs b/src/IRTS/Portable.hs index 7840acf2e..7114d7d32 100644 --- a/src/IRTS/Portable.hs +++ b/src/IRTS/Portable.hs @@ -14,12 +14,10 @@ import Idris.Core.TT import IRTS.Bytecode import IRTS.CodegenCommon import IRTS.Defunctionalise -import IRTS.Lang import IRTS.Simplified import Data.Aeson import qualified Data.ByteString.Lazy as B -import qualified Data.Text as T import System.IO data CodegenFile = CGFile { diff --git a/src/IRTS/Simplified.hs b/src/IRTS/Simplified.hs index cb2573ed8..8a66bb461 100644 --- a/src/IRTS/Simplified.hs +++ b/src/IRTS/Simplified.hs @@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where import Idris.Core.CaseTree import Idris.Core.TT -import Idris.Core.Typecheck import IRTS.Defunctionalise import Control.Monad.State -import Data.Maybe -import Debug.Trace data SExp = SV LVar | SApp Bool Name [LVar] diff --git a/src/Idris/ASTUtils.hs b/src/Idris/ASTUtils.hs index dff453293..4e15d3f9e 100644 --- a/src/Idris/ASTUtils.hs +++ b/src/Idris/ASTUtils.hs @@ -52,7 +52,6 @@ import Idris.Options import Prelude hiding (id, (.)) -import Control.Applicative import Control.Category import Control.Monad.State.Class import Data.Maybe diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index c81159cbd..a4b10ec6b 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -46,7 +46,6 @@ import qualified Data.Text as T import Data.Traversable (Traversable) import Data.Typeable import GHC.Generics (Generic) -import Network.Socket (PortNumber) data ElabWhat = ETypes | EDefns | EAll diff --git a/src/Idris/Apropos.hs b/src/Idris/Apropos.hs index 51d9a1d39..e22e33228 100644 --- a/src/Idris/Apropos.hs +++ b/src/Idris/Apropos.hs @@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where import Idris.AbsSyntax import Idris.Core.Evaluate (Def(..), ctxtAlist) import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..), - Type, lookupCtxtExact, toAlist) + Type, toAlist) import Idris.Docstrings (DocTerm, Docstring, containsText) import Data.List (intersperse, nub, nubBy) diff --git a/src/Idris/Chaser.hs b/src/Idris/Chaser.hs index 7c7592add..49cc280e8 100644 --- a/src/Idris/Chaser.hs +++ b/src/Idris/Chaser.hs @@ -16,19 +16,15 @@ module Idris.Chaser( import Idris.AbsSyntax import Idris.Core.TT import Idris.Error -import Idris.IBC import Idris.Imports import Idris.Parser import Idris.Unlit import Control.Monad.State -import Control.Monad.Trans import Data.List import Data.Time.Clock -import Debug.Trace import System.Directory -import System.FilePath -import Util.System (readSource, writeSource) +import Util.System (readSource) data ModuleTree = MTree { mod_path :: IFileType, mod_needsRecheck :: Bool, diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs index 9c36ab8ec..e7ff10d94 100644 --- a/src/Idris/Core/Binary.hs +++ b/src/Idris/Core/Binary.hs @@ -13,14 +13,10 @@ module Idris.Core.Binary where import Idris.Core.TT import Control.Applicative ((<$>), (<*>)) -import Control.DeepSeq (($!!)) import Control.Monad (liftM2) import Data.Binary import Data.Binary.Get import Data.Binary.Put -import qualified Data.Text as T -import qualified Data.Text.Encoding as E -import Data.Vector.Binary instance Binary ErrorReportPart where put (TextPart msg) = do putWord8 0 ; put msg diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs index 45e7af535..67bd9860d 100644 --- a/src/Idris/Core/CaseTree.hs +++ b/src/Idris/Core/CaseTree.hs @@ -31,14 +31,11 @@ module Idris.Core.CaseTree ( import Idris.Core.TT -import Control.Applicative hiding (Const) import Control.Monad.Reader import Control.Monad.State import Data.List hiding (partition) import qualified Data.List (partition) -import Data.Maybe import qualified Data.Set as S -import Debug.Trace import GHC.Generics (Generic) data CaseDef = CaseDef [Name] !SC [Term] diff --git a/src/Idris/Core/Constraints.hs b/src/Idris/Core/Constraints.hs index bbb56286d..44d8a2ffe 100644 --- a/src/Idris/Core/Constraints.hs +++ b/src/Idris/Core/Constraints.hs @@ -8,15 +8,13 @@ Maintainer : The Idris Community. -} module Idris.Core.Constraints ( ucheck ) where -import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..), - UConstraint(..), UExp(..)) +import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..), + UExp(..)) -import Control.Applicative import Control.Monad.State.Strict import Data.List (partition) import qualified Data.Map.Strict as M import qualified Data.Set as S -import Debug.Trace -- | Check that a list of universe constraints can be satisfied. ucheck :: S.Set ConstraintFC -> TC () diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs index c2a9cecdd..282722bd7 100644 --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -16,7 +16,6 @@ module Idris.Core.Elaborate ( , module Idris.Core.ProofState ) where -import Idris.Core.DeepSeq import Idris.Core.Evaluate import Idris.Core.ProofState import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm, @@ -24,15 +23,9 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm, import Idris.Core.TT import Idris.Core.Typecheck import Idris.Core.Unify -import Idris.Core.WHNF -import Util.Pretty hiding (fill) - -import Control.DeepSeq import Control.Monad.State.Strict -import Data.Char import Data.List -import Debug.Trace data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux)) deriving Show diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs index ff1757ba9..29dcf19be 100644 --- a/src/Idris/Core/Execute.hs +++ b/src/Idris/Core/Execute.hs @@ -11,7 +11,6 @@ Maintainer : The Idris Community. module Idris.Core.Execute (execute) where import Idris.AbsSyntax -import Idris.AbsSyntaxTree import Idris.Core.CaseTree import Idris.Core.Evaluate import Idris.Core.TT @@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..)) import Util.DynamicLinker import Util.System -import Control.Applicative hiding (Const) import Control.Exception -import Control.Monad hiding (forM) import Control.Monad.Trans import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE) import Control.Monad.Trans.State.Strict -import Data.Bits import Data.IORef -import qualified Data.Map as M import Data.Maybe import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Traversable (forM) @@ -42,7 +37,6 @@ import System.IO.Unsafe #ifdef IDRIS_FFI import Foreign.C.String import Foreign.LibFFI -import Foreign.Marshal.Alloc (free) import Foreign.Ptr #endif diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs index 05d225a7c..4ea2f4e4b 100644 --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -28,11 +28,9 @@ import Idris.Core.WHNF import Util.Pretty hiding (fill) -import Control.Applicative hiding (empty) import Control.Arrow ((***)) import Control.Monad.State.Strict import Data.List -import Debug.Trace data ProofState = PS { thname :: Name, holes :: [Name], -- ^ holes still to be solved diff --git a/src/Idris/Core/ProofTerm.hs b/src/Idris/Core/ProofTerm.hs index 6f9aa3223..fbfc72f3d 100644 --- a/src/Idris/Core/ProofTerm.hs +++ b/src/Idris/Core/ProofTerm.hs @@ -18,11 +18,8 @@ module Idris.Core.ProofTerm( import Idris.Core.Evaluate import Idris.Core.TT -import Idris.Core.Typecheck import Control.Monad.State.Strict -import Data.List -import Debug.Trace -- | A zipper over terms, in order to efficiently update proof terms. data TermPath = Top diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs index 2451259e2..b13817938 100644 --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -60,29 +60,24 @@ import Util.Pretty hiding (Str) -- Work around AMP without CPP import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int, Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..), - Read(..), Show(..), String, div, error, flip, fst, mod, not, - otherwise, read, snd, ($), (&&), (.), (||)) + Show(..), String, div, error, fst, mod, not, otherwise, read, + snd, ($), (&&), (.), (||)) import Control.Applicative (Alternative, Applicative(..)) import qualified Control.Applicative as A (Alternative(..)) import Control.DeepSeq (($!!)) import Control.Monad.State.Strict -import Control.Monad.Trans.Except (Except(..)) import Data.Binary hiding (get, put) -import qualified Data.Binary as B import Data.Char import Data.Data (Data) import Data.Foldable (Foldable) import Data.List hiding (group, insert) import qualified Data.Map.Strict as Map import Data.Maybe (listToMaybe) -import Data.Monoid (mconcat) import Data.Set (Set, fromList, insert, member) import qualified Data.Text as T import Data.Traversable (Traversable) import Data.Typeable (Typeable) -import Data.Vector.Unboxed (Vector) -import qualified Data.Vector.Unboxed as V import Debug.Trace import Foreign.Storable (sizeOf) import GHC.Generics (Generic) diff --git a/src/Idris/Core/Typecheck.hs b/src/Idris/Core/Typecheck.hs index 2555e76e7..40b33e55d 100644 --- a/src/Idris/Core/Typecheck.hs +++ b/src/Idris/Core/Typecheck.hs @@ -13,11 +13,8 @@ module Idris.Core.Typecheck where import Idris.Core.Evaluate import Idris.Core.TT -import Idris.Core.WHNF import Control.Monad.State -import qualified Data.Vector.Unboxed as V (length) -import Debug.Trace -- To check conversion, normalise each term wrt the current environment. -- Since we haven't converted everything to de Bruijn indices yet, we'll have to diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs index bb029e3d0..89f1ca225 100644 --- a/src/Idris/Core/Unify.hs +++ b/src/Idris/Core/Unify.hs @@ -22,11 +22,9 @@ module Idris.Core.Unify( import Idris.Core.Evaluate import Idris.Core.TT -import Control.Monad import Control.Monad.State.Strict import Data.List import Data.Maybe -import Debug.Trace -- terms which need to be injective, with the things we're trying to unify -- at the time diff --git a/src/Idris/Core/WHNF.hs b/src/Idris/Core/WHNF.hs index 0a5fc8220..059ccfa16 100644 --- a/src/Idris/Core/WHNF.hs +++ b/src/Idris/Core/WHNF.hs @@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where import Idris.Core.CaseTree import Idris.Core.Evaluate hiding (quote) -import qualified Idris.Core.Evaluate as Evaluate import Idris.Core.TT -import Debug.Trace - -- | A stack entry consists of a term and the environment it is to be -- evaluated in (i.e. it's a thunk) type StackEntry = (Term, WEnv) diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs index e42c1606c..b17eb4a35 100644 --- a/src/Idris/Coverage.hs +++ b/src/Idris/Coverage.hs @@ -16,14 +16,11 @@ import Idris.Core.TT import Idris.Delaborate import Idris.Elab.Utils import Idris.Error -import Idris.Output (iWarn, iputStrLn) import Control.Monad.State.Strict import Data.Char -import Data.Either import Data.List import Data.Maybe -import Debug.Trace -- | Generate a pattern from an 'impossible' LHS. -- diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs index 81ebea564..5b25b7217 100644 --- a/src/Idris/DSL.hs +++ b/src/Idris/DSL.hs @@ -11,12 +11,10 @@ Maintainer : The Idris Community. module Idris.DSL where import Idris.AbsSyntax -import Idris.Core.Evaluate import Idris.Core.TT import Control.Monad.State.Strict import Data.Generics.Uniplate.Data (transform) -import Debug.Trace debindApp :: SyntaxInfo -> PTerm -> PTerm debindApp syn t = debind (dsl_bind (dsl_info syn)) t diff --git a/src/Idris/DataOpts.hs b/src/Idris/DataOpts.hs index 6fe17fd6c..e11458779 100644 --- a/src/Idris/DataOpts.hs +++ b/src/Idris/DataOpts.hs @@ -10,14 +10,8 @@ Maintainer : The Idris Community. module Idris.DataOpts(applyOpts) where import Idris.AbsSyntax -import Idris.AbsSyntaxTree import Idris.Core.TT -import Control.Applicative -import Data.List -import Data.Maybe -import Debug.Trace - class Optimisable term where applyOpts :: term -> Idris term diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs index e7ccafbd7..08a3ada7d 100644 --- a/src/Idris/DeepSeq.hs +++ b/src/Idris/DeepSeq.hs @@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..)) import Util.DynamicLinker -import qualified Cheapskate.Types as CT import Control.DeepSeq import Network.Socket (PortNumber) diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs index 2a8426e1f..4f8f3a36a 100644 --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -26,10 +26,9 @@ import Prelude hiding ((<$>)) import Control.Applicative (Alternative((<|>))) import Control.Monad.State import Data.Generics.Uniplate.Data (transform) -import Data.List (intersperse, nub) +import Data.List (nub) import Data.Maybe (mapMaybe) import qualified Data.Text as T -import Debug.Trace bugaddr = "https://github.com/idris-lang/Idris-dev/issues" diff --git a/src/Idris/Directives.hs b/src/Idris/Directives.hs index 4f95bf645..e1f4a02da 100644 --- a/src/Idris/Directives.hs +++ b/src/Idris/Directives.hs @@ -8,7 +8,6 @@ Maintainer : The Idris Community. module Idris.Directives(directiveAction) where import Idris.AbsSyntax -import Idris.ASTUtils import Idris.Core.Evaluate import Idris.Core.TT import Idris.Imports diff --git a/src/Idris/Elab/AsPat.hs b/src/Idris/Elab/AsPat.hs index eb85f54e3..e44e50b0c 100644 --- a/src/Idris/Elab/AsPat.hs +++ b/src/Idris/Elab/AsPat.hs @@ -10,7 +10,6 @@ module Idris.Elab.AsPat(desugarAs) where import Idris.AbsSyntax import Idris.Core.TT -import Control.Applicative import Control.Monad.State.Strict import Data.Generics.Uniplate.Data (transformM, universe) diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index 2d6f53790..8a74e3824 100644 --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -13,51 +13,38 @@ import Idris.ASTUtils import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT import Idris.Core.Typecheck import Idris.Core.WHNF import Idris.Coverage import Idris.DataOpts -import Idris.DeepSeq +import Idris.DeepSeq () import Idris.Delaborate import Idris.Docstrings hiding (Unchecked) -import Idris.DSL import Idris.Elab.AsPat import Idris.Elab.Term import Idris.Elab.Transform import Idris.Elab.Type import Idris.Elab.Utils import Idris.Error -import Idris.Imports import Idris.Inliner import Idris.Options -import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting) +import Idris.Output (iputStrLn, pshow, sendHighlighting) import Idris.PartialEval -import Idris.Primitives -import Idris.Providers import Idris.Termination import Idris.Transforms -import IRTS.Lang import Util.Pretty hiding ((<$>)) -import Util.Pretty (pretty, text) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category import Control.DeepSeq import Control.Monad import qualified Control.Monad.State.Lazy as LState import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map import Data.Maybe -import qualified Data.Set as S -import qualified Data.Text as T import Data.Word import Debug.Trace import Numeric diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs index 539171fb3..f0faef72c 100644 --- a/src/Idris/Elab/Data.hs +++ b/src/Idris/Elab/Data.hs @@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where import Idris.AbsSyntax import Idris.ASTUtils -import Idris.Core.CaseTree -import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings -import Idris.DSL import Idris.Elab.Rewrite -import Idris.Elab.Term import Idris.Elab.Type import Idris.Elab.Utils import Idris.Elab.Value import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang +import Idris.Output (iWarn, sendHighlighting) import Util.Pretty import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad import Control.Monad.State.Strict as State import Data.Char (isLetter, toLower) import Data.List -import Data.List.Split (splitOn) import qualified Data.Map as Map import Data.Maybe -import qualified Data.Set as S import qualified Data.Text as T -import Debug.Trace warnLC :: FC -> Name -> Idris () warnLC fc n diff --git a/src/Idris/Elab/Implementation.hs b/src/Idris/Elab/Implementation.hs index 1a1862c98..5b4683635 100644 --- a/src/Idris/Elab/Implementation.hs +++ b/src/Idris/Elab/Implementation.hs @@ -9,50 +9,27 @@ Maintainer : The Idris Community. module Idris.Elab.Implementation(elabImplementation) where import Idris.AbsSyntax -import Idris.ASTUtils import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT -import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings -import Idris.DSL -import Idris.Elab.Data import Idris.Elab.Term import Idris.Elab.Type import Idris.Elab.Utils import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang +import Idris.Output (iWarn, sendHighlighting) -import Util.Pretty (pretty, text) +import Util.Pretty (text) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map import Data.Maybe -import qualified Data.Set as S import qualified Data.Text as T -import Debug.Trace - elabImplementation :: ElabInfo -> SyntaxInfo diff --git a/src/Idris/Elab/Interface.hs b/src/Idris/Elab/Interface.hs index f08041122..96b274307 100644 --- a/src/Idris/Elab/Interface.hs +++ b/src/Idris/Elab/Interface.hs @@ -10,51 +10,22 @@ Maintainer : The Idris Community. module Idris.Elab.Interface(elabInterface) where import Idris.AbsSyntax -import Idris.ASTUtils -import Idris.Core.CaseTree -import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT -import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings -import Idris.DSL import Idris.Elab.Data -import Idris.Elab.Term -import Idris.Elab.Type import Idris.Elab.Utils import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang - -import Util.Pretty (pretty, text) +import Idris.Output (sendHighlighting) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) import Data.Generics.Uniplate.Data (transform) import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map import Data.Maybe -import qualified Data.Set as S -import qualified Data.Text as T -import Debug.Trace - data MArgTy = IA Name | EA Name | CA deriving Show diff --git a/src/Idris/Elab/Provider.hs b/src/Idris/Elab/Provider.hs index 5acabad3f..05c15568b 100644 --- a/src/Idris/Elab/Provider.hs +++ b/src/Idris/Elab/Provider.hs @@ -9,51 +9,24 @@ Maintainer : The Idris Community. module Idris.Elab.Provider(elabProvider) where import Idris.AbsSyntax -import Idris.ASTUtils -import Idris.Core.CaseTree -import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.Execute import Idris.Core.TT import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings -import Idris.DSL import Idris.Elab.Clause import Idris.Elab.Term import Idris.Elab.Type -import Idris.Elab.Utils import Idris.Elab.Value import Idris.Error -import Idris.Imports -import Idris.Inliner import Idris.Options -import Idris.Output (iWarn, iputStrLn, pshow) -import Idris.PartialEval -import Idris.Primitives import Idris.Providers -import IRTS.Lang - -import Util.Pretty (pretty, text) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) -import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Set as S -import qualified Data.Text as T -import Debug.Trace -- | Elaborate a type provider elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris () diff --git a/src/Idris/Elab/Record.hs b/src/Idris/Elab/Record.hs index 7a2c28121..cf0d5bc61 100644 --- a/src/Idris/Elab/Record.hs +++ b/src/Idris/Elab/Record.hs @@ -11,25 +11,12 @@ module Idris.Elab.Record(elabRecord) where import Idris.AbsSyntax import Idris.Core.Evaluate import Idris.Core.TT -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings import Idris.Elab.Data -import Idris.Elab.Data -import Idris.Elab.Term -import Idris.Elab.Type -import Idris.Elab.Utils import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) +import Idris.Output (sendHighlighting) import Idris.Parser.Expr (tryFullExpr) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang import Control.Monad import Data.List diff --git a/src/Idris/Elab/Rewrite.hs b/src/Idris/Elab/Rewrite.hs index 372739ec6..6cc0a9c04 100644 --- a/src/Idris/Elab/Rewrite.hs +++ b/src/Idris/Elab/Rewrite.hs @@ -10,7 +10,6 @@ Maintainer : The Idris Community. module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where import Idris.AbsSyntax -import Idris.AbsSyntaxTree import Idris.Core.Elaborate import Idris.Core.Evaluate import Idris.Core.TT @@ -20,8 +19,6 @@ import Idris.Error import Control.Monad import Control.Monad.State.Strict -import Data.List -import Debug.Trace elabRewrite :: (PTerm -> ElabD ()) -> IState -> FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD () diff --git a/src/Idris/Elab/RunElab.hs b/src/Idris/Elab/RunElab.hs index c5342943c..876da02bb 100644 --- a/src/Idris/Elab/RunElab.hs +++ b/src/Idris/Elab/RunElab.hs @@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where import Idris.AbsSyntax import Idris.Core.Elaborate hiding (Tactic(..)) -import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT import Idris.Core.Typecheck import Idris.Elab.Term import Idris.Elab.Value (elabVal) import Idris.Error -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) +import Idris.Output (sendHighlighting) elabScriptTy :: Type elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased) diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs index 0e2e4a0df..bb43d63bf 100644 --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -10,40 +10,34 @@ Maintainer : The Idris Community. module Idris.Elab.Term where import Idris.AbsSyntax -import Idris.AbsSyntaxTree -import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs) +import Idris.Core.CaseTree (SC'(STerm), findCalls) import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.ProofTerm (getProofTerm) import Idris.Core.TT import Idris.Core.Typecheck (check, converts, isType, recheck) import Idris.Core.Unify -import Idris.Core.WHNF (whnf, whnfArgs) -import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase) +import Idris.Core.WHNF (whnf) +import Idris.Coverage (genClauses, recoverableCoverage) import Idris.Delaborate -import Idris.DSL import Idris.Elab.Quasiquote (extractUnquotes) import Idris.Elab.Rewrite import Idris.Elab.Utils import Idris.Error import Idris.ErrReverse (errReverse) import Idris.Options -import Idris.Output (pshow) import Idris.ProofSearch import Idris.Reflection import Idris.Termination (buildSCG, checkDeclTotality, checkPositive) -import qualified Util.Pretty as U - import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.Foldable (for_) import Data.List import qualified Data.Map as M -import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList) +import Data.Maybe (fromMaybe, mapMaybe, maybeToList) import qualified Data.Set as S -import qualified Data.Text as T import Debug.Trace data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs index c49f38641..c35e08593 100644 --- a/src/Idris/Elab/Transform.hs +++ b/src/Idris/Elab/Transform.hs @@ -9,47 +9,19 @@ Maintainer : The Idris Community. module Idris.Elab.Transform where import Idris.AbsSyntax -import Idris.ASTUtils -import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) -import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq -import Idris.Delaborate -import Idris.Docstrings -import Idris.DSL import Idris.Elab.Term import Idris.Elab.Utils import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang - -import Util.Pretty (pretty, text) +import Idris.Output (sendHighlighting) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) -import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Set as S -import qualified Data.Text as T -import Debug.Trace elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term) elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs index b43a1918c..64bea8e28 100644 --- a/src/Idris/Elab/Type.hs +++ b/src/Idris/Elab/Type.hs @@ -13,50 +13,23 @@ module Idris.Elab.Type ( import Idris.AbsSyntax import Idris.ASTUtils -import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT -import Idris.Core.Typecheck import Idris.Core.WHNF -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq -import Idris.Delaborate import Idris.Docstrings (Docstring) -import Idris.DSL import Idris.Elab.Term import Idris.Elab.Utils import Idris.Elab.Value import Idris.Error -import Idris.Imports -import Idris.Inliner import Idris.Options -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang - -import Util.Pretty (pretty, text) +import Idris.Output (sendHighlighting) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) -import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map -import Data.Maybe import qualified Data.Set as S -import qualified Data.Text as T -import qualified Data.Traversable as Traversable -import Debug.Trace buildType :: ElabInfo -> SyntaxInfo diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs index 6e6803f62..dcaf9a495 100644 --- a/src/Idris/Elab/Utils.hs +++ b/src/Idris/Elab/Utils.hs @@ -14,7 +14,6 @@ import Idris.Core.Evaluate import Idris.Core.TT import Idris.Core.Typecheck import Idris.Core.WHNF -import Idris.DeepSeq import Idris.Delaborate import Idris.Docstrings import Idris.Error @@ -22,14 +21,11 @@ import Idris.Output import Util.Pretty -import Control.Applicative hiding (Const) import Control.Monad import Control.Monad.State import Data.List import qualified Data.Map as Map import Data.Maybe -import qualified Data.Traversable as Traversable -import Debug.Trace recheckC = recheckC_borrowing False True [] diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs index 84efcbae2..41c8f7084 100644 --- a/src/Idris/Elab/Value.hs +++ b/src/Idris/Elab/Value.hs @@ -13,48 +13,20 @@ module Idris.Elab.Value( ) where import Idris.AbsSyntax -import Idris.ASTUtils -import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate hiding (Unchecked) -import Idris.Core.Execute import Idris.Core.TT -import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq -import Idris.Delaborate import Idris.Docstrings -import Idris.DSL import Idris.Elab.Term import Idris.Elab.Utils import Idris.Error -import Idris.Imports -import Idris.Inliner -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval -import Idris.Primitives -import Idris.Providers -import IRTS.Lang - -import Util.Pretty (pretty, text) +import Idris.Output (sendHighlighting) import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq -import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) -import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Set as S -import qualified Data.Text as T +import Data.Char (toLower) import qualified Data.Traversable as Traversable -import Debug.Trace -- | Elaborate a value, returning any new bindings created (this will only -- happen if elaborating as a pattern clause) diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index 0d631ab6c..03656546d 100644 --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -12,20 +12,10 @@ Maintainer : The Idris Community. module Idris.ElabDecls where import Idris.AbsSyntax -import Idris.ASTUtils -import Idris.Core.CaseTree -import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate -import Idris.Core.Execute import Idris.Core.TT -import Idris.Core.Typecheck -import Idris.Coverage -import Idris.DataOpts -import Idris.DeepSeq -import Idris.Delaborate import Idris.Directives import Idris.Docstrings hiding (Unchecked) -import Idris.DSL import Idris.Elab.Clause import Idris.Elab.Data import Idris.Elab.Implementation @@ -36,36 +26,21 @@ import Idris.Elab.RunElab import Idris.Elab.Term import Idris.Elab.Transform import Idris.Elab.Type -import Idris.Elab.Utils import Idris.Elab.Value import Idris.Error -import Idris.Imports -import Idris.Inliner import Idris.Options -import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting) -import Idris.PartialEval +import Idris.Output (sendHighlighting) import Idris.Primitives -import Idris.Providers import Idris.Termination import IRTS.Lang -import Util.Pretty (pretty, text) - import Prelude hiding (id, (.)) -import Control.Applicative hiding (Const) import Control.Category -import Control.DeepSeq import Control.Monad import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) -import Data.List -import Data.List.Split (splitOn) -import qualified Data.Map as Map import Data.Maybe -import qualified Data.Set as S import qualified Data.Text as T -import Debug.Trace -- | Top level elaborator info, supporting recursive elaboration recinfo :: FC -> ElabInfo diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs index 51c74d452..7429889df 100644 --- a/src/Idris/Erasure.hs +++ b/src/Idris/Erasure.hs @@ -20,7 +20,6 @@ import Idris.Primitives import Prelude hiding (id, (.)) -import Control.Applicative import Control.Arrow import Control.Category import Control.Monad.State @@ -36,8 +35,6 @@ import Data.Set (Set) import qualified Data.Set as S import Data.Text (pack) import qualified Data.Text as T -import Debug.Trace -import System.IO.Unsafe -- | UseMap maps names to the set of used (reachable) argument -- positions. diff --git a/src/Idris/ErrReverse.hs b/src/Idris/ErrReverse.hs index 8d72e7cba..698ca596d 100644 --- a/src/Idris/ErrReverse.hs +++ b/src/Idris/ErrReverse.hs @@ -15,7 +15,6 @@ import Idris.Core.TT import Util.Pretty import Data.List -import Debug.Trace -- | For display purposes, apply any 'error reversal' transformations -- so that errors will be more readable, diff --git a/src/Idris/Error.hs b/src/Idris/Error.hs index e44af6eab..c31ecaa06 100644 --- a/src/Idris/Error.hs +++ b/src/Idris/Error.hs @@ -14,23 +14,16 @@ import Idris.AbsSyntax import Idris.Core.Constraints import Idris.Core.Evaluate (ctxtAlist) import Idris.Core.TT -import Idris.Core.Typecheck import Idris.Delaborate import Idris.Output import Prelude hiding (catch) import Control.Monad (when) -import Control.Monad.State.Strict -import Data.Char import qualified Data.Foldable as Foldable import Data.List (intercalate, isPrefixOf) import qualified Data.Set as S import qualified Data.Text as T -import qualified Data.Traversable as Traversable -import Data.Typeable -import System.Console.Haskeline -import System.Console.Haskeline.MonadException import System.IO.Error (ioeGetErrorString, isUserError) iucheck :: Idris () diff --git a/src/Idris/IdeMode.hs b/src/Idris/IdeMode.hs index ce3422ff9..a14bcaf1f 100644 --- a/src/Idris/IdeMode.hs +++ b/src/Idris/IdeMode.hs @@ -11,7 +11,7 @@ Maintainer : The Idris Community. module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where -import Idris.Core.Binary +import Idris.Core.Binary () import Idris.Core.TT import Control.Applicative hiding (Const) diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs index f74ef41e9..eb370f47c 100644 --- a/src/Idris/IdrisDoc.hs +++ b/src/Idris/IdrisDoc.hs @@ -10,11 +10,10 @@ Maintainer : The Idris Community. module Idris.IdrisDoc (generateDocs) where import Idris.AbsSyntax -import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName, - isFnName, isTConName, lookupDefAcc) -import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..), - TextFormatting(..), constIsType, nsroot, sUN, str, - toAlist, txt) +import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName, + isTConName, lookupDefAcc) +import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..), + constIsType, nsroot, sUN, str, toAlist, txt) import Idris.Docs import Idris.Docstrings (nullDocstring) import qualified Idris.Docstrings as Docstrings @@ -26,17 +25,13 @@ import Control.Applicative ((<|>)) import Control.Monad (forM_) import Control.Monad.Trans.Except import Control.Monad.Trans.State.Strict -import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as BS2 import qualified Data.List as L -import qualified Data.List.Split as LS import qualified Data.Map as M hiding ((!)) import Data.Maybe import Data.Monoid (mempty) -import qualified Data.Ord (compare) import qualified Data.Set as S import qualified Data.Text as T -import qualified Data.Text.Encoding as E import System.Directory import System.FilePath import System.IO diff --git a/src/Idris/Imports.hs b/src/Idris/Imports.hs index 3f1e4c084..b082f6c3b 100644 --- a/src/Idris/Imports.hs +++ b/src/Idris/Imports.hs @@ -13,7 +13,6 @@ module Idris.Imports( import Idris.AbsSyntax import Idris.Core.TT import Idris.Error -import Idris.Output import IRTS.System (getIdrisLibDir) import Control.Applicative ((<$>)) diff --git a/src/Idris/Info.hs b/src/Idris/Info.hs index 0d380a6ba..089c62c6e 100644 --- a/src/Idris/Info.hs +++ b/src/Idris/Info.hs @@ -29,7 +29,6 @@ import Idris.Imports (installedPackages) import Idris.Options (loggingCatsStr) import qualified IRTS.System as S -import Paths_idris import Version_idris (gitHash) import Data.Version diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs index 46550c719..e80028e3c 100644 --- a/src/Idris/Output.hs +++ b/src/Idris/Output.hs @@ -13,7 +13,7 @@ module Idris.Output where import Idris.AbsSyntax import Idris.Colours (hEndColourise, hStartColourise) -import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll) +import Idris.Core.Evaluate (normaliseAll) import Idris.Core.TT import Idris.Delaborate import Idris.Docstrings @@ -27,13 +27,12 @@ import Util.System (isATTY) import Prelude hiding ((<$>)) import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT) -import Data.Char (isAlpha) import Data.List (intersperse, nub) import Data.Maybe (fromMaybe) import System.Console.Haskeline.MonadException (MonadException(controlIO), RunIO(RunIO)) import System.FilePath (replaceExtension) -import System.IO (Handle, hPutStr, hPutStrLn, stdout) +import System.IO (Handle, hPutStr, hPutStrLn) instance MonadException m => MonadException (ExceptT Err m) where controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs index f7708ae95..85fa3dd63 100644 --- a/src/Idris/Package.hs +++ b/src/Idris/Package.hs @@ -12,7 +12,7 @@ import System.Directory import System.Directory (copyFile, createDirectoryIfMissing) import System.Exit import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension, - hasExtension, normalise, takeDirectory, takeExtension, + hasExtension, takeDirectory, takeExtension, takeFileName, ()) import System.IO import System.Process @@ -23,10 +23,8 @@ import Control.Monad import Control.Monad.Trans.Except (runExceptT) import Control.Monad.Trans.State.Strict (execStateT) import Data.Either (partitionEithers) -import Data.Either (partitionEithers) import Data.List import Data.List.Split (splitOn) -import Data.Maybe (fromMaybe) import Idris.AbsSyntax import Idris.Core.TT @@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain) import Idris.Options import Idris.Output import Idris.Parser (loadModule) -import Idris.REPL import Idris.Package.Common import Idris.Package.Parser diff --git a/src/Idris/Package/Parser.hs b/src/Idris/Package/Parser.hs index 102ec6aba..5da1465e7 100644 --- a/src/Idris/Package/Parser.hs +++ b/src/Idris/Package/Parser.hs @@ -8,19 +8,13 @@ Maintainer : The Idris Community. {-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-} module Idris.Package.Parser where -import Idris.AbsSyntaxTree import Idris.CmdOptions -import Idris.Core.TT import Idris.Package.Common import Idris.Parser.Helpers hiding (stringLiteral) -import Idris.REPL - -import Util.System import Control.Applicative import Control.Monad.State.Strict import Data.List (union) -import Data.Maybe (fromJust, isNothing) import System.Directory (doesFileExist) import System.Exit import System.FilePath (isValid, takeExtension, takeFileName) diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs index d15c7653a..38538eb7f 100644 --- a/src/Idris/Parser/Data.hs +++ b/src/Idris/Parser/Data.hs @@ -12,7 +12,6 @@ import Idris.AbsSyntax import Idris.Core.Evaluate import Idris.Core.TT import Idris.Docstrings -import Idris.DSL import Idris.Options import Idris.Parser.Expr import Idris.Parser.Helpers @@ -21,25 +20,11 @@ import Idris.Parser.Ops import Prelude hiding (pi) import Control.Applicative -import Control.Monad import Control.Monad.State.Strict -import qualified Data.ByteString.UTF8 as UTF8 -import Data.Char -import qualified Data.HashSet as HS import Data.List -import qualified Data.List.Split as Spl import Data.Maybe -import Data.Monoid -import qualified Data.Text as T -import Debug.Trace -import qualified Text.Parser.Char as Chr -import Text.Parser.Expression -import Text.Parser.LookAhead -import qualified Text.Parser.Token as Tok -import qualified Text.Parser.Token.Highlight as Hi import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string, stringLiteral, symbol, whiteSpace) -import Text.Trifecta.Delta {- | Parses a record type declaration Record ::= diff --git a/src/Idris/Parser/Expr.hs b/src/Idris/Parser/Expr.hs index 134f63915..eb3eff09d 100644 --- a/src/Idris/Parser/Expr.hs +++ b/src/Idris/Parser/Expr.hs @@ -21,24 +21,12 @@ import Prelude hiding (pi) import Control.Applicative import Control.Monad import Control.Monad.State.Strict -import qualified Data.ByteString.UTF8 as UTF8 -import Data.Char import Data.Function (on) -import qualified Data.HashSet as HS import Data.List -import qualified Data.List.Split as Spl import Data.Maybe -import Data.Monoid -import qualified Data.Text as T -import Debug.Trace -import qualified Text.Parser.Char as Chr import Text.Parser.Expression -import Text.Parser.LookAhead -import qualified Text.Parser.Token as Tok -import qualified Text.Parser.Token.Highlight as Hi import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string, stringLiteral, symbol, whiteSpace) -import Text.Trifecta.Delta -- | Allow implicit type declarations allowImp :: SyntaxInfo -> SyntaxInfo diff --git a/src/Idris/Parser/Helpers.hs b/src/Idris/Parser/Helpers.hs index 35b281df8..eeac0d342 100644 --- a/src/Idris/Parser/Helpers.hs +++ b/src/Idris/Parser/Helpers.hs @@ -18,8 +18,6 @@ import Idris.Docstrings import Idris.Options import Idris.Output (iWarn) -import qualified Util.Pretty as Pretty (text) - import Prelude hiding (pi) import Control.Applicative @@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8 import Data.Char import qualified Data.HashSet as HS import Data.List -import qualified Data.List.Split as Spl import qualified Data.Map as M import Data.Maybe -import Data.Monoid import qualified Data.Text as T -import Debug.Trace import System.FilePath import qualified Text.Parser.Char as Chr -import Text.Parser.Expression import Text.Parser.LookAhead import qualified Text.Parser.Token as Tok import qualified Text.Parser.Token.Highlight as Hi diff --git a/src/Idris/Parser/Ops.hs b/src/Idris/Parser/Ops.hs index b26835652..39e5bb132 100644 --- a/src/Idris/Parser/Ops.hs +++ b/src/Idris/Parser/Ops.hs @@ -18,23 +18,10 @@ import Prelude hiding (pi) import Control.Applicative import Control.Monad import Control.Monad.State.Strict -import qualified Data.ByteString.UTF8 as UTF8 -import Data.Char -import qualified Data.HashSet as HS import Data.List -import qualified Data.List.Split as Spl -import Data.Maybe -import Data.Monoid -import qualified Data.Text as T -import Debug.Trace -import qualified Text.Parser.Char as Chr import Text.Parser.Expression -import Text.Parser.LookAhead -import qualified Text.Parser.Token as Tok -import qualified Text.Parser.Token.Highlight as Hi import Text.Trifecta hiding (char, charLiteral, natural, span, string, stringLiteral, symbol, whiteSpace) -import Text.Trifecta.Delta -- | Creates table for fixity declarations to build expression parser -- using pre-build and user-defined operator/fixity declarations diff --git a/src/Idris/PartialEval.hs b/src/Idris/PartialEval.hs index a1376aa96..d0c23a9a1 100644 --- a/src/Idris/PartialEval.hs +++ b/src/Idris/PartialEval.hs @@ -19,10 +19,7 @@ import Idris.Core.Evaluate import Idris.Core.TT import Idris.Delaborate -import Control.Applicative import Control.Monad.State -import Data.Maybe -import Debug.Trace -- | Data type representing binding-time annotations for partial evaluation of arguments data PEArgType = ImplicitS Name -- ^ Implicit static argument diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs index 882cd7149..477f52fb6 100644 --- a/src/Idris/Primitives.hs +++ b/src/Idris/Primitives.hs @@ -9,7 +9,6 @@ Maintainer : The Idris Community. module Idris.Primitives(primitives, Prim(..)) where -import Idris.AbsSyntax import Idris.Core.Evaluate import Idris.Core.TT import IRTS.Lang @@ -18,9 +17,7 @@ import Data.Bits import Data.Char import Data.Function (on) import Data.Int -import qualified Data.Vector.Unboxed as V import Data.Word -import Debug.Trace data Prim = Prim { p_name :: Name, p_type :: Type, diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs index 06973adf9..e1a6204ff 100644 --- a/src/Idris/ProofSearch.hs +++ b/src/Idris/ProofSearch.hs @@ -16,14 +16,11 @@ module Idris.ProofSearch( ) where import Idris.AbsSyntax -import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.TT -import Idris.Core.Typecheck import Idris.Core.Unify import Idris.Delaborate -import Idris.Error import Control.Applicative ((<$>)) import Control.Monad diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs index 3d1569354..db0548f6b 100644 --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where -- Hack for GHC 7.10 and earlier compat without CPP or warnings -- This exludes (<$>) as fmap, because wl-pprint uses it for newline import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String, - concatMap, elem, error, flip, foldl, foldr, fst, id, init, - length, lines, map, not, null, repeat, reverse, tail, zip, ($), - (&&), (++), (.), (||)) + concatMap, elem, error, foldl, foldr, fst, id, init, length, + lines, map, not, null, repeat, reverse, tail, zip, ($), (&&), + (++), (.), (||)) import Idris.AbsSyntax -import Idris.AbsSyntaxTree import Idris.Completion import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) @@ -41,7 +40,6 @@ import Util.Pretty import Control.DeepSeq import Control.Monad.State.Strict -import Debug.Trace import System.Console.Haskeline import System.Console.Haskeline.History import System.IO (Handle, hPutStrLn, stdin, stdout) diff --git a/src/Idris/Providers.hs b/src/Idris/Providers.hs index cc77e14e5..965491824 100644 --- a/src/Idris/Providers.hs +++ b/src/Idris/Providers.hs @@ -13,8 +13,6 @@ module Idris.Providers ( ) where import Idris.AbsSyntax -import Idris.AbsSyntaxTree -import Idris.Core.Evaluate import Idris.Core.TT import Idris.Error diff --git a/src/Idris/REPL/Parser.hs b/src/Idris/REPL/Parser.hs index 77b21bcef..cdfcde7f8 100644 --- a/src/Idris/REPL/Parser.hs +++ b/src/Idris/REPL/Parser.hs @@ -21,17 +21,14 @@ import Idris.REPL.Commands import Control.Applicative import Control.Monad.State.Strict -import qualified Data.ByteString.UTF8 as UTF8 import Data.Char (isSpace, toLower) import Data.List import Data.List.Split (splitOn) -import Debug.Trace import System.Console.ANSI (Color(..)) import System.FilePath (()) import Text.Parser.Char (anyChar, oneOf) import Text.Parser.Combinators -import Text.Trifecta (Result, parseString) -import Text.Trifecta.Delta +import Text.Trifecta (Result) parseCmd :: IState -> String -> String -> Result (Either String Command) parseCmd i inputname = P.runparser pCmd i inputname . trim diff --git a/src/Idris/Termination.hs b/src/Idris/Termination.hs index faecb04d8..a57e961ea 100644 --- a/src/Idris/Termination.hs +++ b/src/Idris/Termination.hs @@ -15,10 +15,9 @@ import Idris.Core.TT import Idris.Delaborate import Idris.Error import Idris.Options -import Idris.Output (iWarn, iputStrLn) +import Idris.Output (iWarn) import Control.Monad.State.Strict -import Data.Char import Data.Either import Data.List import Data.Maybe diff --git a/src/Idris/Transforms.hs b/src/Idris/Transforms.hs index 6c7532a62..c372fc1bd 100644 --- a/src/Idris/Transforms.hs +++ b/src/Idris/Transforms.hs @@ -16,11 +16,8 @@ module Idris.Transforms( ) where import Idris.AbsSyntax -import Idris.Core.CaseTree import Idris.Core.TT -import Debug.Trace - transformPats :: IState -> [Either Term (Term, Term)] -> [Either Term (Term, Term)] transformPats ist ps = map tClause ps where diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs index cfa72f4a9..99a00741e 100644 --- a/src/Idris/TypeSearch.hs +++ b/src/Idris/TypeSearch.hs @@ -14,7 +14,7 @@ module Idris.TypeSearch ( ) where import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit, - logLvl, putIState) + putIState) import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt), Idris, InterfaceInfo, OutputMode(..), PTerm, defaultSyntax, eqTy, implicitAllowed, diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs index 1119a97e5..08db317e9 100644 --- a/src/Util/DynamicLinker.hs +++ b/src/Util/DynamicLinker.hs @@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..) ) where #ifdef IDRIS_FFI -import Foreign.LibFFI -import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr) import System.Directory -#ifndef mingw32_HOST_OS -import Control.Exception (IOException, throwIO, try) -import Data.Array (Array, bounds, inRange, (!)) -import Data.Functor ((<$>)) -import Data.Maybe (catMaybes) -import System.FilePath.Posix (()) -import System.Posix.DynamicLinker -import Text.Regex.TDFA -#else +#ifdef mingw32_HOST_OS import qualified Control.Exception as Exception (IOException, catch) +import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr) import System.FilePath.Windows (()) import System.Win32.DLL import System.Win32.Types +#else +import Control.Exception (IOException, throwIO, try) +import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr) +#ifdef linux_HOST_OS +import Data.Array (bounds, inRange, (!)) +import Data.Functor ((<$>)) +import Data.Maybe (catMaybes) +#else +import Data.Array (bounds, (!)) +#endif +import System.FilePath.Posix (()) +import System.Posix.DynamicLinker +import Text.Regex.TDFA +#endif + +#ifdef mingw32_HOST_OS type DL = HMODULE #endif diff --git a/stack.yaml b/stack.yaml index 2c59b993e..459786f2d 100644 --- a/stack.yaml +++ b/stack.yaml @@ -9,6 +9,9 @@ flags: FFI: true GMP: true +ghc-options: + idris: -fwarn-unused-imports -fwarn-unused-binds + extra-deps: - binary-0.8.5.1 - cheapskate-0.1.1