d4bd8e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Clean up unused imports (#4065)

commitd4bd8e63534886faad116074a43c8cdc382fbabf authorJason Felice <jason.m.felice@gmail.com> dateSat 16 Sep 2017, 13:28 (9 years ago) parentbe8523f

80 files changed+58−531

compare with master

unifiedsplit

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+1−6 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+1−1 src/Idris/Chaser.hs+1−5 src/Idris/Core/Binary.hs−4 src/Idris/Core/CaseTree.hs−3 src/Idris/Core/Constraints.hs+2−4 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+2−7 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+1−2 src/Idris/Directives.hs−1 src/Idris/Elab/AsPat.hs−1 src/Idris/Elab/Clause.hs+2−15 src/Idris/Elab/Data.hs+1−20 src/Idris/Elab/Implementation.hs+2−25 src/Idris/Elab/Interface.hs+1−30 src/Idris/Elab/Provider.hs−27 src/Idris/Elab/Record.hs+1−14 src/Idris/Elab/Rewrite.hs−3 src/Idris/Elab/RunElab.hs+1−3 src/Idris/Elab/Term.hs+4−10 src/Idris/Elab/Transform.hs+1−29 src/Idris/Elab/Type.hs+1−28 src/Idris/Elab/Utils.hs−4 src/Idris/Elab/Value.hs+2−30 src/Idris/ElabDecls.hs+1−26 src/Idris/Erasure.hs−3 src/Idris/ErrReverse.hs−1 src/Idris/Error.hs−7 src/Idris/IdeMode.hs+1−1 src/Idris/IdrisDoc.hs+4−9 src/Idris/Imports.hs−1 src/Idris/Info.hs−1 src/Idris/Output.hs+2−3 src/Idris/Package.hs+1−4 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+3−5 src/Idris/Providers.hs−2 src/Idris/REPL/Parser.hs+1−4 src/Idris/Termination.hs+1−2 src/Idris/Transforms.hs−3 src/Idris/TypeSearch.hs+1−1 src/Util/DynamicLinker.hs+16−9 stack.yaml+3

codegen/idris-codegen-c/Main.hs−3

@@ -1,7 +1,6 @@

11module Main where

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

@@ -10,8 +9,6 @@ import IRTS.Compiler

109

1110import Util.System

1211

13−import Paths_idris

14−

1512import Control.Monad

1613import System.Environment

1714import System.Exit

codegen/idris-codegen-javascript/Main.hs−3

@@ -1,15 +1,12 @@

11module Main where

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

87import IRTS.CodegenJavaScript

98import IRTS.Compiler

109

11−import Paths_idris

12−

1310import System.Environment

1411import System.Exit

1512

codegen/idris-codegen-node/Main.hs−3

@@ -1,15 +1,12 @@

11module Main where

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

87import IRTS.CodegenJavaScript

98import IRTS.Compiler

109

11−import Paths_idris

12−

1310import System.Environment

1411import System.Exit

1512

idris.cabal−1

@@ -226,7 +226,6 @@ Library

226226 , Idris.WhoCalls

227227 , Idris.CmdOptions

228228

229− , IRTS.BCImp

230229 , IRTS.Bytecode

231230 , IRTS.CodegenC

232231 , IRTS.CodegenCommon

main/Main.hs+1−6

@@ -2,9 +2,7 @@ module Main where

33import System.Exit (ExitCode(..), exitSuccess, exitWith)

5−import Control.Monad (unless, when, (>=>))

6−import Data.Foldable (foldrM)

7−import Data.Maybe (fromMaybe)

5+import Control.Monad (unless, when)

97import Idris.AbsSyntax

108import Idris.CmdOptions

@@ -16,9 +14,6 @@ import Idris.Package

1614

1715import Util.System (setupBundledCC)

1816

19−import System.Exit (ExitCode(..), exitWith)

20−import Util.System (setupBundledCC)

21−

2217processShowOptions :: [Opt] -> Idris ()

2318processShowOptions opts = runIO $ do

2419 when (ShowAll `elem` opts) $ showExitIdrisInfo

src/IRTS/BCImp.hsdeleted−23

@@ -1,23 +0,0 @@

1−{-|

2−Module : IRTS.BCImp

3−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)

4−Copyright :

5−License : BSD3

6−Maintainer : The Idris Community.

7−-}

8−module IRTS.BCImp where

9−

10−import Idris.Core.TT

11−import IRTS.Lang

12−import IRTS.Simplified

13−

14−data Reg = RVal | L Int

15−

16−data BC = NOP

17−

18−toBC :: (Name, SDecl) -> (Name, [BC])

19−toBC (n, SFun n' args locs exp)

20− = (n, bc RVal exp)

21−

22−bc :: Reg -> SExp -> [BC]

23−bc = undefined

src/IRTS/Bytecode.hs−1

@@ -23,7 +23,6 @@ module IRTS.Bytecode where

2323

2424import Idris.Core.TT

2525import IRTS.Defunctionalise

26−import IRTS.Lang

2726import IRTS.Simplified

2827

2928import Data.Maybe

src/IRTS/CodegenC.hs−4

@@ -9,12 +9,10 @@ Maintainer : The Idris Community.

1010module IRTS.CodegenC (codegenC) where

1111

12−import Idris.AbsSyntax

1312import Idris.Core.TT

1413import IRTS.Bytecode

1514import IRTS.CodegenCommon

1615import IRTS.Defunctionalise

17−import IRTS.Lang

1816import IRTS.Simplified

1917import IRTS.System

2018

@@ -24,9 +22,7 @@ import Control.Monad

2422import Data.Bits

2523import Data.Char

2624import Data.List (intercalate, nubBy)

27−import Debug.Trace

2825import Numeric

29−import System.Directory

3026import System.Exit

3127import System.FilePath ((<.>), (</>))

3228import System.IO

src/IRTS/Compiler.hs−10

@@ -10,7 +10,6 @@ Maintainer : The Idris Community.

1010module IRTS.Compiler(compile, generate) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.ASTUtils

1514import Idris.Core.CaseTree

1615import Idris.Core.Evaluate

@@ -21,33 +20,24 @@ import Idris.Options

2120import Idris.Output

2221import IRTS.CodegenC

2322import IRTS.CodegenCommon

24−import IRTS.CodegenJavaScript

2523import IRTS.Defunctionalise

2624import IRTS.DumpBC

2725import IRTS.Exports

2826import IRTS.Inliner

29−import IRTS.Lang

3027import IRTS.LangOpts

3128import IRTS.Portable

3229import IRTS.Simplified

3330

3431import Prelude hiding (id, (.))

3532

36−import Control.Applicative

3733import Control.Category

3834import Control.Monad.State

39−import Data.IntSet (IntSet)

40−import qualified Data.IntSet as IS

4135import Data.List

4236import qualified Data.Map as M

43−import Data.Maybe

4437import Data.Ord

4538import qualified Data.Set as S

46−import Debug.Trace

4739import System.Directory

48−import System.Environment

4940import System.Exit

50−import System.FilePath (addTrailingPathSeparator, (</>))

5141import System.IO

5242import System.Process

5343

src/IRTS/Defunctionalise.hs−1

@@ -32,7 +32,6 @@ import Control.Monad

3232import Control.Monad.State

3333import Data.List

3434import Data.Maybe

35−import Debug.Trace

3635

3736data DExp = DV Name

3837 | DApp Bool Name [DExp] -- True = tail call

src/IRTS/DumpBC.hs−1

@@ -9,7 +9,6 @@ module IRTS.DumpBC where

1010import Idris.Core.TT

1111import IRTS.Bytecode

12−import IRTS.Lang

1312import IRTS.Simplified

1413

1514import Data.List

src/IRTS/JavaScript/LangTransforms.hs−5

@@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode

1212 ) where

1313

1414

15−import Control.DeepSeq

16−import Control.Monad.Trans.State

1715import Data.List

1816import Data.Map.Strict (Map)

1917import qualified Data.Map.Strict as Map

2018import Data.Maybe

2119import Data.Set (Set)

2220import qualified Data.Set as Set

23−import Data.Text (Text)

24−import qualified Data.Text as T

2521import Idris.Core.CaseTree

2622import Idris.Core.TT

2723import IRTS.Lang

2824

2925import Data.Data

3026import Data.Generics.Uniplate.Data

31−import GHC.Generics (Generic)

3227

3328deriving instance Typeable FDesc

3429deriving instance Data FDesc

src/IRTS/JavaScript/Name.hs−3

@@ -20,12 +20,9 @@ module IRTS.JavaScript.Name

2020 ) where

2121

2222import Data.Char

23−import Data.List

24−import qualified Data.Map.Strict as Map

2523import Data.Text (Text)

2624import qualified Data.Text as T

2725import Idris.Core.TT

28−import IRTS.JavaScript.AST

2926

3027jsEscape :: String -> String

3128jsEscape = concatMap jschar

src/IRTS/JavaScript/PrimOp.hs−4

@@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp

1616 , jsPrimCoerce

1717 ) where

1818

19−import Data.Char

20−import Data.List

2119import qualified Data.Map.Strict as Map

22−import Data.Text (Text)

23−import qualified Data.Text as T

2420import Idris.Core.TT

2521import IRTS.JavaScript.AST

2622import IRTS.Lang

src/IRTS/JavaScript/Specialize.hs−3

@@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize

1717 , qualifyN

1818 ) where

1919

20−import Data.Char

21−import Data.List

2220import qualified Data.Map.Strict as Map

23−import Data.Text (Text)

2421import qualified Data.Text as T

2522import Idris.Core.TT

2623import IRTS.JavaScript.AST

src/IRTS/Lang.hs−2

@@ -13,12 +13,10 @@ module IRTS.Lang where

1313import Idris.Core.CaseTree

1414import Idris.Core.TT

1515

16−import Control.Applicative hiding (Const)

1716import Control.Monad.State hiding (lift)

1817import Data.Data (Data)

1918import Data.List

2019import Data.Typeable (Typeable)

21−import Debug.Trace

2220import GHC.Generics (Generic)

2321

2422data Endianness = Native | BE | LE deriving (Show, Eq)

src/IRTS/LangOpts.hs−4

@@ -9,14 +9,10 @@ Maintainer : The Idris Community.

1010module IRTS.LangOpts where

1111

12−import Idris.Core.CaseTree

1312import Idris.Core.TT

1413import IRTS.Lang

1514

16−import Control.Applicative hiding (Const)

1715import Control.Monad.State hiding (lift)

18−import Data.List

19−import Debug.Trace

2016

2117inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]

2218inlineAll lds = let defs = addAlist lds emptyContext in

src/IRTS/Portable.hs−2

@@ -14,12 +14,10 @@ import Idris.Core.TT

1414import IRTS.Bytecode

1515import IRTS.CodegenCommon

1616import IRTS.Defunctionalise

17−import IRTS.Lang

1817import IRTS.Simplified

1918

2019import Data.Aeson

2120import qualified Data.ByteString.Lazy as B

22−import qualified Data.Text as T

2321import System.IO

2422

2523data CodegenFile = CGFile {

src/IRTS/Simplified.hs−3

@@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where

1010

1111import Idris.Core.CaseTree

1212import Idris.Core.TT

13−import Idris.Core.Typecheck

1413import IRTS.Defunctionalise

1514

1615import Control.Monad.State

17−import Data.Maybe

18−import Debug.Trace

1916

2017data SExp = SV LVar

2118 | SApp Bool Name [LVar]

src/Idris/ASTUtils.hs−1

@@ -52,7 +52,6 @@ import Idris.Options

5252

5353import Prelude hiding (id, (.))

5454

55−import Control.Applicative

5655import Control.Category

5756import Control.Monad.State.Class

5857import Data.Maybe

src/Idris/AbsSyntaxTree.hs−1

@@ -46,7 +46,6 @@ import qualified Data.Text as T

4646import Data.Traversable (Traversable)

4747import Data.Typeable

4848import GHC.Generics (Generic)

49−import Network.Socket (PortNumber)

5049

5150

5251data ElabWhat = ETypes | EDefns | EAll

src/Idris/Apropos.hs+1−1

@@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where

1111import Idris.AbsSyntax

1212import Idris.Core.Evaluate (Def(..), ctxtAlist)

1313import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),

14− Type, lookupCtxtExact, toAlist)

14+ Type, toAlist)

1515import Idris.Docstrings (DocTerm, Docstring, containsText)

1616

1717import Data.List (intersperse, nub, nubBy)

src/Idris/Chaser.hs+1−5

@@ -16,19 +16,15 @@ module Idris.Chaser(

1616import Idris.AbsSyntax

1717import Idris.Core.TT

1818import Idris.Error

19−import Idris.IBC

2019import Idris.Imports

2120import Idris.Parser

2221import Idris.Unlit

2322

2423import Control.Monad.State

25−import Control.Monad.Trans

2624import Data.List

2725import Data.Time.Clock

28−import Debug.Trace

2926import System.Directory

30−import System.FilePath

31−import Util.System (readSource, writeSource)

27+import Util.System (readSource)

3228

3329data ModuleTree = MTree { mod_path :: IFileType,

3430 mod_needsRecheck :: Bool,

src/Idris/Core/Binary.hs−4

@@ -13,14 +13,10 @@ module Idris.Core.Binary where

1313import Idris.Core.TT

1414

1515import Control.Applicative ((<$>), (<*>))

16−import Control.DeepSeq (($!!))

1716import Control.Monad (liftM2)

1817import Data.Binary

1918import Data.Binary.Get

2019import Data.Binary.Put

21−import qualified Data.Text as T

22−import qualified Data.Text.Encoding as E

23−import Data.Vector.Binary

2420

2521instance Binary ErrorReportPart where

2622 put (TextPart msg) = do putWord8 0 ; put msg

src/Idris/Core/CaseTree.hs−3

@@ -31,14 +31,11 @@ module Idris.Core.CaseTree (

3131

3232import Idris.Core.TT

3333

34−import Control.Applicative hiding (Const)

3534import Control.Monad.Reader

3635import Control.Monad.State

3736import Data.List hiding (partition)

3837import qualified Data.List (partition)

39−import Data.Maybe

4038import qualified Data.Set as S

41−import Debug.Trace

4239import GHC.Generics (Generic)

4340

4441data CaseDef = CaseDef [Name] !SC [Term]

src/Idris/Core/Constraints.hs+2−4

@@ -8,15 +8,13 @@ Maintainer : The Idris Community.

88-}

99module Idris.Core.Constraints ( ucheck ) where

1010

11−import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),

12− UConstraint(..), UExp(..))

11+import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),

12+ UExp(..))

1313

14−import Control.Applicative

1514import Control.Monad.State.Strict

1615import Data.List (partition)

1716import qualified Data.Map.Strict as M

1817import qualified Data.Set as S

19−import Debug.Trace

2018

2119-- | Check that a list of universe constraints can be satisfied.

2220ucheck :: S.Set ConstraintFC -> TC ()

src/Idris/Core/Elaborate.hs−7

@@ -16,7 +16,6 @@ module Idris.Core.Elaborate (

1616 , module Idris.Core.ProofState

1717 ) where

1818

19−import Idris.Core.DeepSeq

2019import Idris.Core.Evaluate

2120import Idris.Core.ProofState

2221import 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,

2423import Idris.Core.TT

2524import Idris.Core.Typecheck

2625import Idris.Core.Unify

27−import Idris.Core.WHNF

2826

29−import Util.Pretty hiding (fill)

30−

31−import Control.DeepSeq

3227import Control.Monad.State.Strict

33−import Data.Char

3428import Data.List

35−import Debug.Trace

3629

3730data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

3831 deriving Show

src/Idris/Core/Execute.hs−6

@@ -11,7 +11,6 @@ Maintainer : The Idris Community.

1111module Idris.Core.Execute (execute) where

1212

1313import Idris.AbsSyntax

14−import Idris.AbsSyntaxTree

1514import Idris.Core.CaseTree

1615import Idris.Core.Evaluate

1716import Idris.Core.TT

@@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..))

2221import Util.DynamicLinker

2322import Util.System

2423

25−import Control.Applicative hiding (Const)

2624import Control.Exception

27−import Control.Monad hiding (forM)

2825import Control.Monad.Trans

2926import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)

3027import Control.Monad.Trans.State.Strict

31−import Data.Bits

3228import Data.IORef

33−import qualified Data.Map as M

3429import Data.Maybe

3530import Data.Time.Clock.POSIX (getPOSIXTime)

3631import Data.Traversable (forM)

@@ -42,7 +37,6 @@ import System.IO.Unsafe

4237#ifdef IDRIS_FFI

4338import Foreign.C.String

4439import Foreign.LibFFI

45−import Foreign.Marshal.Alloc (free)

4640import Foreign.Ptr

4741#endif

4842

src/Idris/Core/ProofState.hs−2

@@ -28,11 +28,9 @@ import Idris.Core.WHNF

2828

2929import Util.Pretty hiding (fill)

3030

31−import Control.Applicative hiding (empty)

3231import Control.Arrow ((***))

3332import Control.Monad.State.Strict

3433import Data.List

35−import Debug.Trace

3634

3735data ProofState = PS { thname :: Name,

3836 holes :: [Name], -- ^ holes still to be solved

src/Idris/Core/ProofTerm.hs−3

@@ -18,11 +18,8 @@ module Idris.Core.ProofTerm(

1818

1919import Idris.Core.Evaluate

2020import Idris.Core.TT

21−import Idris.Core.Typecheck

2221

2322import Control.Monad.State.Strict

24−import Data.List

25−import Debug.Trace

2623

2724-- | A zipper over terms, in order to efficiently update proof terms.

2825data TermPath = Top

src/Idris/Core/TT.hs+2−7

@@ -60,29 +60,24 @@ import Util.Pretty hiding (Str)

6060-- Work around AMP without CPP

6161import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,

6262 Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),

63− Read(..), Show(..), String, div, error, flip, fst, mod, not,

64− otherwise, read, snd, ($), (&&), (.), (||))

63+ Show(..), String, div, error, fst, mod, not, otherwise, read,

64+ snd, ($), (&&), (.), (||))

6565

6666import Control.Applicative (Alternative, Applicative(..))

6767import qualified Control.Applicative as A (Alternative(..))

6868import Control.DeepSeq (($!!))

6969import Control.Monad.State.Strict

70−import Control.Monad.Trans.Except (Except(..))

7170import Data.Binary hiding (get, put)

72−import qualified Data.Binary as B

7371import Data.Char

7472import Data.Data (Data)

7573import Data.Foldable (Foldable)

7674import Data.List hiding (group, insert)

7775import qualified Data.Map.Strict as Map

7876import Data.Maybe (listToMaybe)

79−import Data.Monoid (mconcat)

8077import Data.Set (Set, fromList, insert, member)

8178import qualified Data.Text as T

8279import Data.Traversable (Traversable)

8380import Data.Typeable (Typeable)

84−import Data.Vector.Unboxed (Vector)

85−import qualified Data.Vector.Unboxed as V

8681import Debug.Trace

8782import Foreign.Storable (sizeOf)

8883import GHC.Generics (Generic)

src/Idris/Core/Typecheck.hs−3

@@ -13,11 +13,8 @@ module Idris.Core.Typecheck where

1313

1414import Idris.Core.Evaluate

1515import Idris.Core.TT

16−import Idris.Core.WHNF

1716

1817import Control.Monad.State

19−import qualified Data.Vector.Unboxed as V (length)

20−import Debug.Trace

2118

2219-- To check conversion, normalise each term wrt the current environment.

2320-- Since we haven't converted everything to de Bruijn indices yet, we'll have to

src/Idris/Core/Unify.hs−2

@@ -22,11 +22,9 @@ module Idris.Core.Unify(

2222import Idris.Core.Evaluate

2323import Idris.Core.TT

2424

25−import Control.Monad

2625import Control.Monad.State.Strict

2726import Data.List

2827import Data.Maybe

29−import Debug.Trace

3028

3129-- terms which need to be injective, with the things we're trying to unify

3230-- at the time

src/Idris/Core/WHNF.hs−3

@@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where

1212

1313import Idris.Core.CaseTree

1414import Idris.Core.Evaluate hiding (quote)

15−import qualified Idris.Core.Evaluate as Evaluate

1615import Idris.Core.TT

1716

18−import Debug.Trace

19−

2017-- | A stack entry consists of a term and the environment it is to be

2118-- evaluated in (i.e. it's a thunk)

2219type StackEntry = (Term, WEnv)

src/Idris/Coverage.hs−3

@@ -16,14 +16,11 @@ import Idris.Core.TT

1616import Idris.Delaborate

1717import Idris.Elab.Utils

1818import Idris.Error

19−import Idris.Output (iWarn, iputStrLn)

2019

2120import Control.Monad.State.Strict

2221import Data.Char

23−import Data.Either

2422import Data.List

2523import Data.Maybe

26−import Debug.Trace

2724

2825-- | Generate a pattern from an 'impossible' LHS.

2926--

src/Idris/DSL.hs−2

@@ -11,12 +11,10 @@ Maintainer : The Idris Community.

1111module Idris.DSL where

1212

1313import Idris.AbsSyntax

14−import Idris.Core.Evaluate

1514import Idris.Core.TT

1615

1716import Control.Monad.State.Strict

1817import Data.Generics.Uniplate.Data (transform)

19−import Debug.Trace

2018

2119debindApp :: SyntaxInfo -> PTerm -> PTerm

2220debindApp syn t = debind (dsl_bind (dsl_info syn)) t

src/Idris/DataOpts.hs−6

@@ -10,14 +10,8 @@ Maintainer : The Idris Community.

1010module Idris.DataOpts(applyOpts) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.Core.TT

1514

16−import Control.Applicative

17−import Data.List

18−import Data.Maybe

19−import Debug.Trace

20−

2115class Optimisable term where

2216 applyOpts :: term -> Idris term

2317

src/Idris/DeepSeq.hs−1

@@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))

2424

2525import Util.DynamicLinker

2626

27−import qualified Cheapskate.Types as CT

2827import Control.DeepSeq

2928import Network.Socket (PortNumber)

3029

src/Idris/Delaborate.hs+1−2

@@ -26,10 +26,9 @@ import Prelude hiding ((<$>))

2626import Control.Applicative (Alternative((<|>)))

2727import Control.Monad.State

2828import Data.Generics.Uniplate.Data (transform)

29−import Data.List (intersperse, nub)

29+import Data.List (nub)

3030import Data.Maybe (mapMaybe)

3131import qualified Data.Text as T

32−import Debug.Trace

3332

3433bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

3534

src/Idris/Directives.hs−1

@@ -8,7 +8,6 @@ Maintainer : The Idris Community.

88module Idris.Directives(directiveAction) where

1010import Idris.AbsSyntax

11−import Idris.ASTUtils

1211import Idris.Core.Evaluate

1312import Idris.Core.TT

1413import Idris.Imports

src/Idris/Elab/AsPat.hs−1

@@ -10,7 +10,6 @@ module Idris.Elab.AsPat(desugarAs) where

1010import Idris.AbsSyntax

1111import Idris.Core.TT

1212

13−import Control.Applicative

1413import Control.Monad.State.Strict

1514import Data.Generics.Uniplate.Data (transformM, universe)

1615

src/Idris/Elab/Clause.hs+2−15

@@ -13,51 +13,38 @@ import Idris.ASTUtils

1313import Idris.Core.CaseTree

1414import Idris.Core.Elaborate hiding (Tactic(..))

1515import Idris.Core.Evaluate

16−import Idris.Core.Execute

1716import Idris.Core.TT

1817import Idris.Core.Typecheck

1918import Idris.Core.WHNF

2019import Idris.Coverage

2120import Idris.DataOpts

22−import Idris.DeepSeq

21+import Idris.DeepSeq ()

2322import Idris.Delaborate

2423import Idris.Docstrings hiding (Unchecked)

25−import Idris.DSL

2624import Idris.Elab.AsPat

2725import Idris.Elab.Term

2826import Idris.Elab.Transform

2927import Idris.Elab.Type

3028import Idris.Elab.Utils

3129import Idris.Error

32−import Idris.Imports

3330import Idris.Inliner

3431import Idris.Options

35−import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)

32+import Idris.Output (iputStrLn, pshow, sendHighlighting)

3633import Idris.PartialEval

37−import Idris.Primitives

38−import Idris.Providers

3934import Idris.Termination

4035import Idris.Transforms

41−import IRTS.Lang

4236

4337import Util.Pretty hiding ((<$>))

44−import Util.Pretty (pretty, text)

4538

4639import Prelude hiding (id, (.))

4740

48−import Control.Applicative hiding (Const)

4941import Control.Category

5042import Control.DeepSeq

5143import Control.Monad

5244import qualified Control.Monad.State.Lazy as LState

5345import Control.Monad.State.Strict as State

54−import Data.Char (isLetter, toLower)

5546import Data.List

56−import Data.List.Split (splitOn)

57−import qualified Data.Map as Map

5847import Data.Maybe

59−import qualified Data.Set as S

60−import qualified Data.Text as T

6148import Data.Word

6249import Debug.Trace

6350import Numeric

src/Idris/Elab/Data.hs+1−20

@@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where

1010

1111import Idris.AbsSyntax

1212import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

1513import Idris.Core.Evaluate

16−import Idris.Core.Execute

1714import Idris.Core.TT

1815import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

2518import Idris.Elab.Rewrite

26−import Idris.Elab.Term

2719import Idris.Elab.Type

2820import Idris.Elab.Utils

2921import Idris.Elab.Value

3022import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

23+import Idris.Output (iWarn, sendHighlighting)

3824

3925import Util.Pretty

4026

4127import Prelude hiding (id, (.))

4228

43−import Control.Applicative hiding (Const)

4429import Control.Category

45−import Control.DeepSeq

4630import Control.Monad

4731import Control.Monad.State.Strict as State

4832import Data.Char (isLetter, toLower)

4933import Data.List

50−import Data.List.Split (splitOn)

5134import qualified Data.Map as Map

5235import Data.Maybe

53−import qualified Data.Set as S

5436import qualified Data.Text as T

55−import Debug.Trace

5637

5738warnLC :: FC -> Name -> Idris ()

5839warnLC fc n

src/Idris/Elab/Implementation.hs+2−25

@@ -9,50 +9,27 @@ Maintainer : The Idris Community.

99module Idris.Elab.Implementation(elabImplementation) where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

1312import Idris.Core.CaseTree

1413import Idris.Core.Elaborate hiding (Tactic(..))

1514import Idris.Core.Evaluate

16−import Idris.Core.Execute

1715import Idris.Core.TT

18−import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

25−import Idris.Elab.Data

2618import Idris.Elab.Term

2719import Idris.Elab.Type

2820import Idris.Elab.Utils

2921import Idris.Error

30−import Idris.Imports

31−import Idris.Inliner

32−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

33−import Idris.PartialEval

34−import Idris.Primitives

35−import Idris.Providers

36−import IRTS.Lang

22+import Idris.Output (iWarn, sendHighlighting)

3723

38−import Util.Pretty (pretty, text)

24+import Util.Pretty (text)

3925

4026import Prelude hiding (id, (.))

4127

42−import Control.Applicative hiding (Const)

4328import Control.Category

44−import Control.DeepSeq

4529import Control.Monad

46−import Control.Monad.State.Strict as State

47−import Data.Char (isLetter, toLower)

4830import Data.List

49−import Data.List.Split (splitOn)

50−import qualified Data.Map as Map

5131import Data.Maybe

52−import qualified Data.Set as S

5332import qualified Data.Text as T

54−import Debug.Trace

55−

5633

5734elabImplementation :: ElabInfo

5835 -> SyntaxInfo

src/Idris/Elab/Interface.hs+1−30

@@ -10,51 +10,22 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Interface(elabInterface) where

1111

1212import Idris.AbsSyntax

13−import Idris.ASTUtils

14−import Idris.Core.CaseTree

15−import Idris.Core.Elaborate hiding (Tactic(..))

1613import Idris.Core.Evaluate

17−import Idris.Core.Execute

1814import Idris.Core.TT

19−import Idris.Core.Typecheck

20−import Idris.Coverage

21−import Idris.DataOpts

22−import Idris.DeepSeq

2315import Idris.Delaborate

2416import Idris.Docstrings

25−import Idris.DSL

2617import Idris.Elab.Data

27−import Idris.Elab.Term

28−import Idris.Elab.Type

2918import Idris.Elab.Utils

3019import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38−

39−import Util.Pretty (pretty, text)

20+import Idris.Output (sendHighlighting)

4021

4122import Prelude hiding (id, (.))

4223

43−import Control.Applicative hiding (Const)

4424import Control.Category

45−import Control.DeepSeq

4625import Control.Monad

47−import Control.Monad.State.Strict as State

48−import Data.Char (isLetter, toLower)

4926import Data.Generics.Uniplate.Data (transform)

5027import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

5328import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

57−

5829

5930data MArgTy = IA Name | EA Name | CA deriving Show

6031

src/Idris/Elab/Provider.hs−27

@@ -9,51 +9,24 @@ Maintainer : The Idris Community.

99module Idris.Elab.Provider(elabProvider) where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

1512import Idris.Core.Evaluate

1613import Idris.Core.Execute

1714import Idris.Core.TT

1815import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

2518import Idris.Elab.Clause

2619import Idris.Elab.Term

2720import Idris.Elab.Type

28−import Idris.Elab.Utils

2921import Idris.Elab.Value

3022import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

3323import Idris.Options

34−import Idris.Output (iWarn, iputStrLn, pshow)

35−import Idris.PartialEval

36−import Idris.Primitives

3724import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

4125

4226import Prelude hiding (id, (.))

4327

44−import Control.Applicative hiding (Const)

4528import Control.Category

46−import Control.DeepSeq

4729import Control.Monad

48−import Control.Monad.State.Strict as State

49−import Data.Char (isLetter, toLower)

50−import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53−import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

5730

5831-- | Elaborate a type provider

5932elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()

src/Idris/Elab/Record.hs+1−14

@@ -11,25 +11,12 @@ module Idris.Elab.Record(elabRecord) where

1111import Idris.AbsSyntax

1212import Idris.Core.Evaluate

1313import Idris.Core.TT

14−import Idris.Coverage

15−import Idris.DataOpts

16−import Idris.DeepSeq

1714import Idris.Delaborate

1815import Idris.Docstrings

1916import Idris.Elab.Data

20−import Idris.Elab.Data

21−import Idris.Elab.Term

22−import Idris.Elab.Type

23−import Idris.Elab.Utils

2417import Idris.Error

25−import Idris.Imports

26−import Idris.Inliner

27−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

18+import Idris.Output (sendHighlighting)

2819import Idris.Parser.Expr (tryFullExpr)

29−import Idris.PartialEval

30−import Idris.Primitives

31−import Idris.Providers

32−import IRTS.Lang

3320

3421import Control.Monad

3522import Data.List

src/Idris/Elab/Rewrite.hs−3

@@ -10,7 +10,6 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.Core.Elaborate

1514import Idris.Core.Evaluate

1615import Idris.Core.TT

@@ -20,8 +19,6 @@ import Idris.Error

2019

2120import Control.Monad

2221import Control.Monad.State.Strict

23−import Data.List

24−import Debug.Trace

2522

2623elabRewrite :: (PTerm -> ElabD ()) -> IState ->

2724 FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

src/Idris/Elab/RunElab.hs+1−3

@@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where

1010import Idris.AbsSyntax

1111import Idris.Core.Elaborate hiding (Tactic(..))

12−import Idris.Core.Evaluate

13−import Idris.Core.Execute

1412import Idris.Core.TT

1513import Idris.Core.Typecheck

1614import Idris.Elab.Term

1715import Idris.Elab.Value (elabVal)

1816import Idris.Error

19−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

17+import Idris.Output (sendHighlighting)

2018

2119elabScriptTy :: Type

2220elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)

src/Idris/Elab/Term.hs+4−10

@@ -10,40 +10,34 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Term where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14−import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)

13+import Idris.Core.CaseTree (SC'(STerm), findCalls)

1514import Idris.Core.Elaborate hiding (Tactic(..))

1615import Idris.Core.Evaluate

1716import Idris.Core.ProofTerm (getProofTerm)

1817import Idris.Core.TT

1918import Idris.Core.Typecheck (check, converts, isType, recheck)

2019import Idris.Core.Unify

21−import Idris.Core.WHNF (whnf, whnfArgs)

22−import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

20+import Idris.Core.WHNF (whnf)

21+import Idris.Coverage (genClauses, recoverableCoverage)

2322import Idris.Delaborate

24−import Idris.DSL

2523import Idris.Elab.Quasiquote (extractUnquotes)

2624import Idris.Elab.Rewrite

2725import Idris.Elab.Utils

2826import Idris.Error

2927import Idris.ErrReverse (errReverse)

3028import Idris.Options

31−import Idris.Output (pshow)

3229import Idris.ProofSearch

3330import Idris.Reflection

3431import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

3532

36−import qualified Util.Pretty as U

37−

3833import Control.Applicative ((<$>))

3934import Control.Monad

4035import Control.Monad.State.Strict

4136import Data.Foldable (for_)

4237import Data.List

4338import qualified Data.Map as M

44−import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)

39+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

4540import qualified Data.Set as S

46−import qualified Data.Text as T

4741import Debug.Trace

4842

4943data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS

src/Idris/Elab/Transform.hs+1−29

@@ -9,47 +9,19 @@ Maintainer : The Idris Community.

99module Idris.Elab.Transform where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

1412import Idris.Core.Elaborate hiding (Tactic(..))

15−import Idris.Core.Evaluate

16−import Idris.Core.Execute

1713import Idris.Core.TT

1814import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22−import Idris.Delaborate

23−import Idris.Docstrings

24−import Idris.DSL

2515import Idris.Elab.Term

2616import Idris.Elab.Utils

2717import Idris.Error

28−import Idris.Imports

29−import Idris.Inliner

30−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

31−import Idris.PartialEval

32−import Idris.Primitives

33−import Idris.Providers

34−import IRTS.Lang

35−

36−import Util.Pretty (pretty, text)

18+import Idris.Output (sendHighlighting)

3719

3820import Prelude hiding (id, (.))

3921

40−import Control.Applicative hiding (Const)

4122import Control.Category

42−import Control.DeepSeq

4323import Control.Monad

4424import Control.Monad.State.Strict as State

45−import Data.Char (isLetter, toLower)

46−import Data.List

47−import Data.List.Split (splitOn)

48−import qualified Data.Map as Map

49−import Data.Maybe

50−import qualified Data.Set as S

51−import qualified Data.Text as T

52−import Debug.Trace

5325

5426elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

5527elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

src/Idris/Elab/Type.hs+1−28

@@ -13,50 +13,23 @@ module Idris.Elab.Type (

1313

1414import Idris.AbsSyntax

1515import Idris.ASTUtils

16−import Idris.Core.CaseTree

1716import Idris.Core.Elaborate hiding (Tactic(..))

1817import Idris.Core.Evaluate

19−import Idris.Core.Execute

2018import Idris.Core.TT

21−import Idris.Core.Typecheck

2219import Idris.Core.WHNF

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

2720import Idris.Docstrings (Docstring)

28−import Idris.DSL

2921import Idris.Elab.Term

3022import Idris.Elab.Utils

3123import Idris.Elab.Value

3224import Idris.Error

33−import Idris.Imports

34−import Idris.Inliner

3525import Idris.Options

36−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

37−import Idris.PartialEval

38−import Idris.Primitives

39−import Idris.Providers

40−import IRTS.Lang

41−

42−import Util.Pretty (pretty, text)

26+import Idris.Output (sendHighlighting)

4327

4428import Prelude hiding (id, (.))

4529

46−import Control.Applicative hiding (Const)

4730import Control.Category

48−import Control.DeepSeq

4931import Control.Monad

50−import Control.Monad.State.Strict as State

51−import Data.Char (isLetter, toLower)

52−import Data.List

53−import Data.List.Split (splitOn)

54−import qualified Data.Map as Map

55−import Data.Maybe

5632import qualified Data.Set as S

57−import qualified Data.Text as T

58−import qualified Data.Traversable as Traversable

59−import Debug.Trace

6033

6134buildType :: ElabInfo

6235 -> SyntaxInfo

src/Idris/Elab/Utils.hs−4

@@ -14,7 +14,6 @@ import Idris.Core.Evaluate

1414import Idris.Core.TT

1515import Idris.Core.Typecheck

1616import Idris.Core.WHNF

17−import Idris.DeepSeq

1817import Idris.Delaborate

1918import Idris.Docstrings

2019import Idris.Error

@@ -22,14 +21,11 @@ import Idris.Output

2221

2322import Util.Pretty

2423

25−import Control.Applicative hiding (Const)

2624import Control.Monad

2725import Control.Monad.State

2826import Data.List

2927import qualified Data.Map as Map

3028import Data.Maybe

31−import qualified Data.Traversable as Traversable

32−import Debug.Trace

3329

3430recheckC = recheckC_borrowing False True []

3531

src/Idris/Elab/Value.hs+2−30

@@ -13,48 +13,20 @@ module Idris.Elab.Value(

1313 ) where

1414

1515import Idris.AbsSyntax

16−import Idris.ASTUtils

17−import Idris.Core.CaseTree

1816import Idris.Core.Elaborate hiding (Tactic(..))

1917import Idris.Core.Evaluate hiding (Unchecked)

20−import Idris.Core.Execute

2118import Idris.Core.TT

22−import Idris.Core.Typecheck

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

2719import Idris.Docstrings

28−import Idris.DSL

2920import Idris.Elab.Term

3021import Idris.Elab.Utils

3122import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

34−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

35−import Idris.PartialEval

36−import Idris.Primitives

37−import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

23+import Idris.Output (sendHighlighting)

4124

4225import Prelude hiding (id, (.))

4326

44−import Control.Applicative hiding (Const)

4527import Control.Category

46−import Control.DeepSeq

47−import Control.Monad

48−import Control.Monad.State.Strict as State

49−import Data.Char (isLetter, toLower)

50−import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53−import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

28+import Data.Char (toLower)

5629import qualified Data.Traversable as Traversable

57−import Debug.Trace

5830

5931-- | Elaborate a value, returning any new bindings created (this will only

6032-- happen if elaborating as a pattern clause)

src/Idris/ElabDecls.hs+1−26

@@ -12,20 +12,10 @@ Maintainer : The Idris Community.

1212module Idris.ElabDecls where

1313

1414import Idris.AbsSyntax

15−import Idris.ASTUtils

16−import Idris.Core.CaseTree

17−import Idris.Core.Elaborate hiding (Tactic(..))

1815import Idris.Core.Evaluate

19−import Idris.Core.Execute

2016import Idris.Core.TT

21−import Idris.Core.Typecheck

22−import Idris.Coverage

23−import Idris.DataOpts

24−import Idris.DeepSeq

25−import Idris.Delaborate

2617import Idris.Directives

2718import Idris.Docstrings hiding (Unchecked)

28−import Idris.DSL

2919import Idris.Elab.Clause

3020import Idris.Elab.Data

3121import Idris.Elab.Implementation

@@ -36,36 +26,21 @@ import Idris.Elab.RunElab

3626import Idris.Elab.Term

3727import Idris.Elab.Transform

3828import Idris.Elab.Type

39−import Idris.Elab.Utils

4029import Idris.Elab.Value

4130import Idris.Error

42−import Idris.Imports

43−import Idris.Inliner

4431import Idris.Options

45−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

46−import Idris.PartialEval

32+import Idris.Output (sendHighlighting)

4733import Idris.Primitives

48−import Idris.Providers

4934import Idris.Termination

5035import IRTS.Lang

5136

52−import Util.Pretty (pretty, text)

53−

5437import Prelude hiding (id, (.))

5538

56−import Control.Applicative hiding (Const)

5739import Control.Category

58−import Control.DeepSeq

5940import Control.Monad

6041import Control.Monad.State.Strict as State

61−import Data.Char (isLetter, toLower)

62−import Data.List

63−import Data.List.Split (splitOn)

64−import qualified Data.Map as Map

6542import Data.Maybe

66−import qualified Data.Set as S

6743import qualified Data.Text as T

68−import Debug.Trace

6944

7045-- | Top level elaborator info, supporting recursive elaboration

7146recinfo :: FC -> ElabInfo

src/Idris/Erasure.hs−3

@@ -20,7 +20,6 @@ import Idris.Primitives

2020

2121import Prelude hiding (id, (.))

2222

23−import Control.Applicative

2423import Control.Arrow

2524import Control.Category

2625import Control.Monad.State

@@ -36,8 +35,6 @@ import Data.Set (Set)

3635import qualified Data.Set as S

3736import Data.Text (pack)

3837import qualified Data.Text as T

39−import Debug.Trace

40−import System.IO.Unsafe

4138

4239-- | UseMap maps names to the set of used (reachable) argument

4340-- positions.

src/Idris/ErrReverse.hs−1

@@ -15,7 +15,6 @@ import Idris.Core.TT

1515import Util.Pretty

1616

1717import Data.List

18−import Debug.Trace

1918

2019-- | For display purposes, apply any 'error reversal' transformations

2120-- so that errors will be more readable,

src/Idris/Error.hs−7

@@ -14,23 +14,16 @@ import Idris.AbsSyntax

1414import Idris.Core.Constraints

1515import Idris.Core.Evaluate (ctxtAlist)

1616import Idris.Core.TT

17−import Idris.Core.Typecheck

1817import Idris.Delaborate

1918import Idris.Output

2019

2120import Prelude hiding (catch)

2221

2322import Control.Monad (when)

24−import Control.Monad.State.Strict

25−import Data.Char

2623import qualified Data.Foldable as Foldable

2724import Data.List (intercalate, isPrefixOf)

2825import qualified Data.Set as S

2926import qualified Data.Text as T

30−import qualified Data.Traversable as Traversable

31−import Data.Typeable

32−import System.Console.Haskeline

33−import System.Console.Haskeline.MonadException

3427import System.IO.Error (ioeGetErrorString, isUserError)

3528

3629iucheck :: Idris ()

src/Idris/IdeMode.hs+1−1

@@ -11,7 +11,7 @@ Maintainer : The Idris Community.

1111

1212module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where

1313

14−import Idris.Core.Binary

14+import Idris.Core.Binary ()

1515import Idris.Core.TT

1616

1717import Control.Applicative hiding (Const)

src/Idris/IdrisDoc.hs+4−9

@@ -10,11 +10,10 @@ Maintainer : The Idris Community.

1010module Idris.IdrisDoc (generateDocs) where

1111

1212import Idris.AbsSyntax

13−import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,

14− isFnName, isTConName, lookupDefAcc)

15−import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),

16− TextFormatting(..), constIsType, nsroot, sUN, str,

17− toAlist, txt)

13+import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,

14+ isTConName, lookupDefAcc)

15+import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),

16+ constIsType, nsroot, sUN, str, toAlist, txt)

1817import Idris.Docs

1918import Idris.Docstrings (nullDocstring)

2019import qualified Idris.Docstrings as Docstrings

@@ -26,17 +25,13 @@ import Control.Applicative ((<|>))

2625import Control.Monad (forM_)

2726import Control.Monad.Trans.Except

2827import Control.Monad.Trans.State.Strict

29−import qualified Data.ByteString as BS

3028import qualified Data.ByteString.Lazy as BS2

3129import qualified Data.List as L

32−import qualified Data.List.Split as LS

3330import qualified Data.Map as M hiding ((!))

3431import Data.Maybe

3532import Data.Monoid (mempty)

36−import qualified Data.Ord (compare)

3733import qualified Data.Set as S

3834import qualified Data.Text as T

39−import qualified Data.Text.Encoding as E

4035import System.Directory

4136import System.FilePath

4237import System.IO

src/Idris/Imports.hs−1

@@ -13,7 +13,6 @@ module Idris.Imports(

1313import Idris.AbsSyntax

1414import Idris.Core.TT

1515import Idris.Error

16−import Idris.Output

1716import IRTS.System (getIdrisLibDir)

1817

1918import Control.Applicative ((<$>))

src/Idris/Info.hs−1

@@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)

2929import Idris.Options (loggingCatsStr)

3030import qualified IRTS.System as S

3131

32−import Paths_idris

3332import Version_idris (gitHash)

3433

3534import Data.Version

src/Idris/Output.hs+2−3

@@ -13,7 +13,7 @@ module Idris.Output where

1313

1414import Idris.AbsSyntax

1515import Idris.Colours (hEndColourise, hStartColourise)

16−import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)

16+import Idris.Core.Evaluate (normaliseAll)

1717import Idris.Core.TT

1818import Idris.Delaborate

1919import Idris.Docstrings

@@ -27,13 +27,12 @@ import Util.System (isATTY)

2727import Prelude hiding ((<$>))

2828

2929import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

30−import Data.Char (isAlpha)

3130import Data.List (intersperse, nub)

3231import Data.Maybe (fromMaybe)

3332import System.Console.Haskeline.MonadException (MonadException(controlIO),

3433 RunIO(RunIO))

3534import System.FilePath (replaceExtension)

36−import System.IO (Handle, hPutStr, hPutStrLn, stdout)

35+import System.IO (Handle, hPutStr, hPutStrLn)

3736

3837instance MonadException m => MonadException (ExceptT Err m) where

3938 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

src/Idris/Package.hs+1−4

@@ -12,7 +12,7 @@ import System.Directory

1212import System.Directory (copyFile, createDirectoryIfMissing)

1313import System.Exit

1414import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,

15− hasExtension, normalise, takeDirectory, takeExtension,

15+ hasExtension, takeDirectory, takeExtension,

1616 takeFileName, (</>))

1717import System.IO

1818import System.Process

@@ -23,10 +23,8 @@ import Control.Monad

2323import Control.Monad.Trans.Except (runExceptT)

2424import Control.Monad.Trans.State.Strict (execStateT)

2525import Data.Either (partitionEithers)

26−import Data.Either (partitionEithers)

2726import Data.List

2827import Data.List.Split (splitOn)

29−import Data.Maybe (fromMaybe)

3028

3129import Idris.AbsSyntax

3230import Idris.Core.TT

@@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)

3836import Idris.Options

3937import Idris.Output

4038import Idris.Parser (loadModule)

41−import Idris.REPL

4239

4340import Idris.Package.Common

4441import Idris.Package.Parser

src/Idris/Package/Parser.hs−6

@@ -8,19 +8,13 @@ Maintainer : The Idris Community.

88{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}

99module Idris.Package.Parser where

1010

11−import Idris.AbsSyntaxTree

1211import Idris.CmdOptions

13−import Idris.Core.TT

1412import Idris.Package.Common

1513import Idris.Parser.Helpers hiding (stringLiteral)

16−import Idris.REPL

17−

18−import Util.System

1914

2015import Control.Applicative

2116import Control.Monad.State.Strict

2217import Data.List (union)

23−import Data.Maybe (fromJust, isNothing)

2418import System.Directory (doesFileExist)

2519import System.Exit

2620import System.FilePath (isValid, takeExtension, takeFileName)

src/Idris/Parser/Data.hs−15

@@ -12,7 +12,6 @@ import Idris.AbsSyntax

1212import Idris.Core.Evaluate

1313import Idris.Core.TT

1414import Idris.Docstrings

15−import Idris.DSL

1615import Idris.Options

1716import Idris.Parser.Expr

1817import Idris.Parser.Helpers

@@ -21,25 +20,11 @@ import Idris.Parser.Ops

2120import Prelude hiding (pi)

2221

2322import Control.Applicative

24−import Control.Monad

2523import Control.Monad.State.Strict

26−import qualified Data.ByteString.UTF8 as UTF8

27−import Data.Char

28−import qualified Data.HashSet as HS

2924import Data.List

30−import qualified Data.List.Split as Spl

3125import Data.Maybe

32−import Data.Monoid

33−import qualified Data.Text as T

34−import Debug.Trace

35−import qualified Text.Parser.Char as Chr

36−import Text.Parser.Expression

37−import Text.Parser.LookAhead

38−import qualified Text.Parser.Token as Tok

39−import qualified Text.Parser.Token.Highlight as Hi

4026import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

4127 stringLiteral, symbol, whiteSpace)

42−import Text.Trifecta.Delta

4328

4429{- | Parses a record type declaration

4530Record ::=

src/Idris/Parser/Expr.hs−12

@@ -21,24 +21,12 @@ import Prelude hiding (pi)

2121import Control.Applicative

2222import Control.Monad

2323import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25−import Data.Char

2624import Data.Function (on)

27−import qualified Data.HashSet as HS

2825import Data.List

29−import qualified Data.List.Split as Spl

3026import Data.Maybe

31−import Data.Monoid

32−import qualified Data.Text as T

33−import Debug.Trace

34−import qualified Text.Parser.Char as Chr

3527import Text.Parser.Expression

36−import Text.Parser.LookAhead

37−import qualified Text.Parser.Token as Tok

38−import qualified Text.Parser.Token.Highlight as Hi

3928import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

4029 stringLiteral, symbol, whiteSpace)

41−import Text.Trifecta.Delta

4230

4331-- | Allow implicit type declarations

4432allowImp :: SyntaxInfo -> SyntaxInfo

src/Idris/Parser/Helpers.hs−6

@@ -18,8 +18,6 @@ import Idris.Docstrings

1818import Idris.Options

1919import Idris.Output (iWarn)

2020

21−import qualified Util.Pretty as Pretty (text)

22−

2321import Prelude hiding (pi)

2422

2523import Control.Applicative

@@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8

2927import Data.Char

3028import qualified Data.HashSet as HS

3129import Data.List

32−import qualified Data.List.Split as Spl

3330import qualified Data.Map as M

3431import Data.Maybe

35−import Data.Monoid

3632import qualified Data.Text as T

37−import Debug.Trace

3833import System.FilePath

3934import qualified Text.Parser.Char as Chr

40−import Text.Parser.Expression

4135import Text.Parser.LookAhead

4236import qualified Text.Parser.Token as Tok

4337import qualified Text.Parser.Token.Highlight as Hi

src/Idris/Parser/Ops.hs−13

@@ -18,23 +18,10 @@ import Prelude hiding (pi)

1818import Control.Applicative

1919import Control.Monad

2020import Control.Monad.State.Strict

21−import qualified Data.ByteString.UTF8 as UTF8

22−import Data.Char

23−import qualified Data.HashSet as HS

2421import Data.List

25−import qualified Data.List.Split as Spl

26−import Data.Maybe

27−import Data.Monoid

28−import qualified Data.Text as T

29−import Debug.Trace

30−import qualified Text.Parser.Char as Chr

3122import Text.Parser.Expression

32−import Text.Parser.LookAhead

33−import qualified Text.Parser.Token as Tok

34−import qualified Text.Parser.Token.Highlight as Hi

3523import Text.Trifecta hiding (char, charLiteral, natural, span, string,

3624 stringLiteral, symbol, whiteSpace)

37−import Text.Trifecta.Delta

3825

3926-- | Creates table for fixity declarations to build expression parser

4027-- using pre-build and user-defined operator/fixity declarations

src/Idris/PartialEval.hs−3

@@ -19,10 +19,7 @@ import Idris.Core.Evaluate

1919import Idris.Core.TT

2020import Idris.Delaborate

2121

22−import Control.Applicative

2322import Control.Monad.State

24−import Data.Maybe

25−import Debug.Trace

2623

2724-- | Data type representing binding-time annotations for partial evaluation of arguments

2825data PEArgType = ImplicitS Name -- ^ Implicit static argument

src/Idris/Primitives.hs−3

@@ -9,7 +9,6 @@ Maintainer : The Idris Community.

1010module Idris.Primitives(primitives, Prim(..)) where

1111

12−import Idris.AbsSyntax

1312import Idris.Core.Evaluate

1413import Idris.Core.TT

1514import IRTS.Lang

@@ -18,9 +17,7 @@ import Data.Bits

1817import Data.Char

1918import Data.Function (on)

2019import Data.Int

21−import qualified Data.Vector.Unboxed as V

2220import Data.Word

23−import Debug.Trace

2421

2522data Prim = Prim { p_name :: Name,

2623 p_type :: Type,

src/Idris/ProofSearch.hs−3

@@ -16,14 +16,11 @@ module Idris.ProofSearch(

1616 ) where

1717

1818import Idris.AbsSyntax

19−import Idris.Core.CaseTree

2019import Idris.Core.Elaborate hiding (Tactic(..))

2120import Idris.Core.Evaluate

2221import Idris.Core.TT

23−import Idris.Core.Typecheck

2422import Idris.Core.Unify

2523import Idris.Delaborate

26−import Idris.Error

2724

2825import Control.Applicative ((<$>))

2926import Control.Monad

src/Idris/Prover.hs+3−5

@@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where

1111-- Hack for GHC 7.10 and earlier compat without CPP or warnings

1212-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

1313import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,

14− concatMap, elem, error, flip, foldl, foldr, fst, id, init,

15− length, lines, map, not, null, repeat, reverse, tail, zip, ($),

16− (&&), (++), (.), (||))

14+ concatMap, elem, error, foldl, foldr, fst, id, init, length,

15+ lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),

16+ (++), (.), (||))

1717

1818import Idris.AbsSyntax

19−import Idris.AbsSyntaxTree

2019import Idris.Completion

2120import Idris.Core.CaseTree

2221import Idris.Core.Elaborate hiding (Tactic(..))

@@ -41,7 +40,6 @@ import Util.Pretty

4140

4241import Control.DeepSeq

4342import Control.Monad.State.Strict

44−import Debug.Trace

4543import System.Console.Haskeline

4644import System.Console.Haskeline.History

4745import System.IO (Handle, hPutStrLn, stdin, stdout)

src/Idris/Providers.hs−2

@@ -13,8 +13,6 @@ module Idris.Providers (

1313 ) where

1414

1515import Idris.AbsSyntax

16−import Idris.AbsSyntaxTree

17−import Idris.Core.Evaluate

1816import Idris.Core.TT

1917import Idris.Error

2018

src/Idris/REPL/Parser.hs+1−4

@@ -21,17 +21,14 @@ import Idris.REPL.Commands

2121

2222import Control.Applicative

2323import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

2524import Data.Char (isSpace, toLower)

2625import Data.List

2726import Data.List.Split (splitOn)

28−import Debug.Trace

2927import System.Console.ANSI (Color(..))

3028import System.FilePath ((</>))

3129import Text.Parser.Char (anyChar, oneOf)

3230import Text.Parser.Combinators

33−import Text.Trifecta (Result, parseString)

34−import Text.Trifecta.Delta

31+import Text.Trifecta (Result)

3532

3633parseCmd :: IState -> String -> String -> Result (Either String Command)

3734parseCmd i inputname = P.runparser pCmd i inputname . trim

src/Idris/Termination.hs+1−2

@@ -15,10 +15,9 @@ import Idris.Core.TT

1515import Idris.Delaborate

1616import Idris.Error

1717import Idris.Options

18−import Idris.Output (iWarn, iputStrLn)

18+import Idris.Output (iWarn)

1919

2020import Control.Monad.State.Strict

21−import Data.Char

2221import Data.Either

2322import Data.List

2423import Data.Maybe

src/Idris/Transforms.hs−3

@@ -16,11 +16,8 @@ module Idris.Transforms(

1616 ) where

1717

1818import Idris.AbsSyntax

19−import Idris.Core.CaseTree

2019import Idris.Core.TT

2120

22−import Debug.Trace

23−

2421transformPats :: IState -> [Either Term (Term, Term)] ->

2522 [Either Term (Term, Term)]

2623transformPats ist ps = map tClause ps where

src/Idris/TypeSearch.hs+1−1

@@ -14,7 +14,7 @@ module Idris.TypeSearch (

1414 ) where

1515

1616import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,

17− logLvl, putIState)

17+ putIState)

1818import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

1919 Idris, InterfaceInfo, OutputMode(..), PTerm,

2020 defaultSyntax, eqTy, implicitAllowed,

src/Util/DynamicLinker.hs+16−9

@@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)

1313 ) where

1414

1515#ifdef IDRIS_FFI

16−import Foreign.LibFFI

17−import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)

1816import System.Directory

19−#ifndef mingw32_HOST_OS

17+#ifdef mingw32_HOST_OS

18+import qualified Control.Exception as Exception (IOException, catch)

19+import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr)

20+import System.FilePath.Windows ((</>))

21+import System.Win32.DLL

22+import System.Win32.Types

23+#else

2024import Control.Exception (IOException, throwIO, try)

21−import Data.Array (Array, bounds, inRange, (!))

25+import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)

26+#ifdef linux_HOST_OS

27+import Data.Array (bounds, inRange, (!))

2228import Data.Functor ((<$>))

2329import Data.Maybe (catMaybes)

30+#else

31+import Data.Array (bounds, (!))

32+#endif

2433import System.FilePath.Posix ((</>))

2534import System.Posix.DynamicLinker

2635import Text.Regex.TDFA

27−#else

28−import qualified Control.Exception as Exception (IOException, catch)

29−import System.FilePath.Windows ((</>))

30−import System.Win32.DLL

31−import System.Win32.Types

36+#endif

37+

38+#ifdef mingw32_HOST_OS

3239type DL = HMODULE

3340#endif

3441

stack.yaml+3

@@ -9,6 +9,9 @@ flags:

99 FFI: true

1010 GMP: true

1111

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

1215extra-deps:

1316 - binary-0.8.5.1

1417 - cheapskate-0.1.1