d4bd8e6 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

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

10

9

11import Util.System

10import Util.System

12

11

13−import Paths_idris

14−

15import Control.Monad

12import Control.Monad

16import System.Environment

13import System.Environment

17import System.Exit

14import System.Exit

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

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

8import IRTS.CodegenJavaScript

7import IRTS.CodegenJavaScript

9import IRTS.Compiler

8import IRTS.Compiler

10

9

11−import Paths_idris

12−

13import System.Environment

10import System.Environment

14import System.Exit

11import System.Exit

15

12

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

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

8import IRTS.CodegenJavaScript

7import IRTS.CodegenJavaScript

9import IRTS.Compiler

8import IRTS.Compiler

10

9

11−import Paths_idris

12−

13import System.Environment

10import System.Environment

14import System.Exit

11import System.Exit

15

12

idris.cabal−1

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

226 , Idris.WhoCalls

227 , Idris.CmdOptions

228

229− , IRTS.BCImp

230 , IRTS.Bytecode

229 , IRTS.Bytecode

231 , IRTS.CodegenC

230 , IRTS.CodegenC

232 , IRTS.CodegenCommon

231 , IRTS.CodegenCommon

main/Main.hs+1−6

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

2

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

4

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

5+import Control.Monad (unless, when)

6−import Data.Foldable (foldrM)

7−import Data.Maybe (fromMaybe)

8

6

9import Idris.AbsSyntax

7import Idris.AbsSyntax

10import Idris.CmdOptions

8import Idris.CmdOptions

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

16

14

17import Util.System (setupBundledCC)

15import Util.System (setupBundledCC)

18

16

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

20−import Util.System (setupBundledCC)

21−

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

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

23processShowOptions opts = runIO $ do

18processShowOptions opts = runIO $ do

24 when (ShowAll `elem` opts) $ showExitIdrisInfo

19 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

23

24import Idris.Core.TT

25import IRTS.Defunctionalise

26−import IRTS.Lang

27import IRTS.Simplified

26import IRTS.Simplified

28

27

29import Data.Maybe

28import Data.Maybe

src/IRTS/CodegenC.hs−4

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

9

10module IRTS.CodegenC (codegenC) where

11

12−import Idris.AbsSyntax

13import Idris.Core.TT

12import Idris.Core.TT

14import IRTS.Bytecode

13import IRTS.Bytecode

15import IRTS.CodegenCommon

14import IRTS.CodegenCommon

16import IRTS.Defunctionalise

15import IRTS.Defunctionalise

17−import IRTS.Lang

18import IRTS.Simplified

16import IRTS.Simplified

19import IRTS.System

17import IRTS.System

20

18

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

24import Data.Bits

22import Data.Bits

25import Data.Char

23import Data.Char

26import Data.List (intercalate, nubBy)

24import Data.List (intercalate, nubBy)

27−import Debug.Trace

28import Numeric

25import Numeric

29−import System.Directory

30import System.Exit

26import System.Exit

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

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

32import System.IO

28import System.IO

src/IRTS/Compiler.hs−10

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

10module IRTS.Compiler(compile, generate) where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.ASTUtils

13import Idris.ASTUtils

15import Idris.Core.CaseTree

14import Idris.Core.CaseTree

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

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

21import Idris.Output

20import Idris.Output

22import IRTS.CodegenC

21import IRTS.CodegenC

23import IRTS.CodegenCommon

22import IRTS.CodegenCommon

24−import IRTS.CodegenJavaScript

25import IRTS.Defunctionalise

23import IRTS.Defunctionalise

26import IRTS.DumpBC

24import IRTS.DumpBC

27import IRTS.Exports

25import IRTS.Exports

28import IRTS.Inliner

26import IRTS.Inliner

29−import IRTS.Lang

30import IRTS.LangOpts

27import IRTS.LangOpts

31import IRTS.Portable

28import IRTS.Portable

32import IRTS.Simplified

29import IRTS.Simplified

33

30

34import Prelude hiding (id, (.))

31import Prelude hiding (id, (.))

35

32

36−import Control.Applicative

37import Control.Category

33import Control.Category

38import Control.Monad.State

34import Control.Monad.State

39−import Data.IntSet (IntSet)

40−import qualified Data.IntSet as IS

41import Data.List

35import Data.List

42import qualified Data.Map as M

36import qualified Data.Map as M

43−import Data.Maybe

44import Data.Ord

37import Data.Ord

45import qualified Data.Set as S

38import qualified Data.Set as S

46−import Debug.Trace

47import System.Directory

39import System.Directory

48−import System.Environment

49import System.Exit

40import System.Exit

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

51import System.IO

41import System.IO

52import System.Process

42import System.Process

53

43

src/IRTS/Defunctionalise.hs−1

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

32import Control.Monad.State

33import Data.List

34import Data.Maybe

35−import Debug.Trace

36

35

37data DExp = DV Name

36data DExp = DV Name

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

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

src/IRTS/DumpBC.hs−1

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

9

10import Idris.Core.TT

11import IRTS.Bytecode

12−import IRTS.Lang

13import IRTS.Simplified

12import IRTS.Simplified

14

13

15import Data.List

14import Data.List

src/IRTS/JavaScript/LangTransforms.hs−5

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

12 ) where

13

14

15−import Control.DeepSeq

16−import Control.Monad.Trans.State

17import Data.List

15import Data.List

18import Data.Map.Strict (Map)

16import Data.Map.Strict (Map)

19import qualified Data.Map.Strict as Map

17import qualified Data.Map.Strict as Map

20import Data.Maybe

18import Data.Maybe

21import Data.Set (Set)

19import Data.Set (Set)

22import qualified Data.Set as Set

20import qualified Data.Set as Set

23−import Data.Text (Text)

24−import qualified Data.Text as T

25import Idris.Core.CaseTree

21import Idris.Core.CaseTree

26import Idris.Core.TT

22import Idris.Core.TT

27import IRTS.Lang

23import IRTS.Lang

28

24

29import Data.Data

25import Data.Data

30import Data.Generics.Uniplate.Data

26import Data.Generics.Uniplate.Data

31−import GHC.Generics (Generic)

32

27

33deriving instance Typeable FDesc

28deriving instance Typeable FDesc

34deriving instance Data FDesc

29deriving instance Data FDesc

src/IRTS/JavaScript/Name.hs−3

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

20 ) where

21

22import Data.Char

23−import Data.List

24−import qualified Data.Map.Strict as Map

25import Data.Text (Text)

23import Data.Text (Text)

26import qualified Data.Text as T

24import qualified Data.Text as T

27import Idris.Core.TT

25import Idris.Core.TT

28−import IRTS.JavaScript.AST

29

26

30jsEscape :: String -> String

27jsEscape :: String -> String

31jsEscape = concatMap jschar

28jsEscape = concatMap jschar

src/IRTS/JavaScript/PrimOp.hs−4

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

16 , jsPrimCoerce

17 ) where

18

19−import Data.Char

20−import Data.List

21import qualified Data.Map.Strict as Map

19import qualified Data.Map.Strict as Map

22−import Data.Text (Text)

23−import qualified Data.Text as T

24import Idris.Core.TT

20import Idris.Core.TT

25import IRTS.JavaScript.AST

21import IRTS.JavaScript.AST

26import IRTS.Lang

22import IRTS.Lang

src/IRTS/JavaScript/Specialize.hs−3

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

17 , qualifyN

18 ) where

19

20−import Data.Char

21−import Data.List

22import qualified Data.Map.Strict as Map

20import qualified Data.Map.Strict as Map

23−import Data.Text (Text)

24import qualified Data.Text as T

21import qualified Data.Text as T

25import Idris.Core.TT

22import Idris.Core.TT

26import IRTS.JavaScript.AST

23import IRTS.JavaScript.AST

src/IRTS/Lang.hs−2

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

13import Idris.Core.CaseTree

14import Idris.Core.TT

15

16−import Control.Applicative hiding (Const)

17import Control.Monad.State hiding (lift)

16import Control.Monad.State hiding (lift)

18import Data.Data (Data)

17import Data.Data (Data)

19import Data.List

18import Data.List

20import Data.Typeable (Typeable)

19import Data.Typeable (Typeable)

21−import Debug.Trace

22import GHC.Generics (Generic)

20import GHC.Generics (Generic)

23

21

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

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

src/IRTS/LangOpts.hs−4

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

9

10module IRTS.LangOpts where

11

12−import Idris.Core.CaseTree

13import Idris.Core.TT

12import Idris.Core.TT

14import IRTS.Lang

13import IRTS.Lang

15

14

16−import Control.Applicative hiding (Const)

17import Control.Monad.State hiding (lift)

15import Control.Monad.State hiding (lift)

18−import Data.List

19−import Debug.Trace

20

16

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

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

22inlineAll lds = let defs = addAlist lds emptyContext in

18inlineAll lds = let defs = addAlist lds emptyContext in

src/IRTS/Portable.hs−2

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

14import IRTS.Bytecode

15import IRTS.CodegenCommon

16import IRTS.Defunctionalise

17−import IRTS.Lang

18import IRTS.Simplified

17import IRTS.Simplified

19

18

20import Data.Aeson

19import Data.Aeson

21import qualified Data.ByteString.Lazy as B

20import qualified Data.ByteString.Lazy as B

22−import qualified Data.Text as T

23import System.IO

21import System.IO

24

22

25data CodegenFile = CGFile {

23data CodegenFile = CGFile {

src/IRTS/Simplified.hs−3

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

10

11import Idris.Core.CaseTree

12import Idris.Core.TT

13−import Idris.Core.Typecheck

14import IRTS.Defunctionalise

13import IRTS.Defunctionalise

15

14

16import Control.Monad.State

15import Control.Monad.State

17−import Data.Maybe

18−import Debug.Trace

19

16

20data SExp = SV LVar

17data SExp = SV LVar

21 | SApp Bool Name [LVar]

18 | SApp Bool Name [LVar]

src/Idris/ASTUtils.hs−1

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

52

53import Prelude hiding (id, (.))

54

55−import Control.Applicative

56import Control.Category

55import Control.Category

57import Control.Monad.State.Class

56import Control.Monad.State.Class

58import Data.Maybe

57import Data.Maybe

src/Idris/AbsSyntaxTree.hs−1

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

46import Data.Traversable (Traversable)

47import Data.Typeable

48import GHC.Generics (Generic)

49−import Network.Socket (PortNumber)

50

49

51

50

52data ElabWhat = ETypes | EDefns | EAll

51data ElabWhat = ETypes | EDefns | EAll

src/Idris/Apropos.hs+1−1

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

11import Idris.AbsSyntax

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

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

14− Type, lookupCtxtExact, toAlist)

14+ Type, toAlist)

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

16

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

src/Idris/Chaser.hs+1−5

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

16import Idris.AbsSyntax

17import Idris.Core.TT

18import Idris.Error

19−import Idris.IBC

20import Idris.Imports

19import Idris.Imports

21import Idris.Parser

20import Idris.Parser

22import Idris.Unlit

21import Idris.Unlit

23

22

24import Control.Monad.State

23import Control.Monad.State

25−import Control.Monad.Trans

26import Data.List

24import Data.List

27import Data.Time.Clock

25import Data.Time.Clock

28−import Debug.Trace

29import System.Directory

26import System.Directory

30−import System.FilePath

31−import Util.System (readSource, writeSource)

27+import Util.System (readSource)

32

28

33data ModuleTree = MTree { mod_path :: IFileType,

29data ModuleTree = MTree { mod_path :: IFileType,

34 mod_needsRecheck :: Bool,

30 mod_needsRecheck :: Bool,

src/Idris/Core/Binary.hs−4

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

13import Idris.Core.TT

14

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

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

17import Control.Monad (liftM2)

16import Control.Monad (liftM2)

18import Data.Binary

17import Data.Binary

19import Data.Binary.Get

18import Data.Binary.Get

20import Data.Binary.Put

19import Data.Binary.Put

21−import qualified Data.Text as T

22−import qualified Data.Text.Encoding as E

23−import Data.Vector.Binary

24

20

25instance Binary ErrorReportPart where

21instance Binary ErrorReportPart where

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

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

src/Idris/Core/CaseTree.hs−3

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

31

32import Idris.Core.TT

33

34−import Control.Applicative hiding (Const)

35import Control.Monad.Reader

34import Control.Monad.Reader

36import Control.Monad.State

35import Control.Monad.State

37import Data.List hiding (partition)

36import Data.List hiding (partition)

38import qualified Data.List (partition)

37import qualified Data.List (partition)

39−import Data.Maybe

40import qualified Data.Set as S

38import qualified Data.Set as S

41−import Debug.Trace

42import GHC.Generics (Generic)

39import GHC.Generics (Generic)

43

40

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

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

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

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

8-}

9module Idris.Core.Constraints ( ucheck ) where

10

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

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

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

12+ UExp(..))

13

14−import Control.Applicative

15import Control.Monad.State.Strict

14import Control.Monad.State.Strict

16import Data.List (partition)

15import Data.List (partition)

17import qualified Data.Map.Strict as M

16import qualified Data.Map.Strict as M

18import qualified Data.Set as S

17import qualified Data.Set as S

19−import Debug.Trace

20

18

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

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

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

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

src/Idris/Core/Elaborate.hs−7

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

16 , module Idris.Core.ProofState

17 ) where

18

19−import Idris.Core.DeepSeq

20import Idris.Core.Evaluate

19import Idris.Core.Evaluate

21import Idris.Core.ProofState

20import Idris.Core.ProofState

22import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,

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

24import Idris.Core.TT

23import Idris.Core.TT

25import Idris.Core.Typecheck

24import Idris.Core.Typecheck

26import Idris.Core.Unify

25import Idris.Core.Unify

27−import Idris.Core.WHNF

28

26

29−import Util.Pretty hiding (fill)

30−

31−import Control.DeepSeq

32import Control.Monad.State.Strict

27import Control.Monad.State.Strict

33−import Data.Char

34import Data.List

28import Data.List

35−import Debug.Trace

36

29

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

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

38 deriving Show

31 deriving Show

src/Idris/Core/Execute.hs−6

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

11module Idris.Core.Execute (execute) where

12

13import Idris.AbsSyntax

14−import Idris.AbsSyntaxTree

15import Idris.Core.CaseTree

14import Idris.Core.CaseTree

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

17import Idris.Core.TT

16import Idris.Core.TT

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

22import Util.DynamicLinker

21import Util.DynamicLinker

23import Util.System

22import Util.System

24

23

25−import Control.Applicative hiding (Const)

26import Control.Exception

24import Control.Exception

27−import Control.Monad hiding (forM)

28import Control.Monad.Trans

25import Control.Monad.Trans

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

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

30import Control.Monad.Trans.State.Strict

27import Control.Monad.Trans.State.Strict

31−import Data.Bits

32import Data.IORef

28import Data.IORef

33−import qualified Data.Map as M

34import Data.Maybe

29import Data.Maybe

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

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

36import Data.Traversable (forM)

31import Data.Traversable (forM)

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

42#ifdef IDRIS_FFI

37#ifdef IDRIS_FFI

43import Foreign.C.String

38import Foreign.C.String

44import Foreign.LibFFI

39import Foreign.LibFFI

45−import Foreign.Marshal.Alloc (free)

46import Foreign.Ptr

40import Foreign.Ptr

47#endif

41#endif

48

42

src/Idris/Core/ProofState.hs−2

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

28

29import Util.Pretty hiding (fill)

30

31−import Control.Applicative hiding (empty)

32import Control.Arrow ((***))

31import Control.Arrow ((***))

33import Control.Monad.State.Strict

32import Control.Monad.State.Strict

34import Data.List

33import Data.List

35−import Debug.Trace

36

34

37data ProofState = PS { thname :: Name,

35data ProofState = PS { thname :: Name,

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

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

src/Idris/Core/ProofTerm.hs−3

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

18

19import Idris.Core.Evaluate

20import Idris.Core.TT

21−import Idris.Core.Typecheck

22

21

23import Control.Monad.State.Strict

22import Control.Monad.State.Strict

24−import Data.List

25−import Debug.Trace

26

23

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

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

28data TermPath = Top

25data TermPath = Top

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

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

60-- Work around AMP without CPP

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

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

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

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

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

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

65

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

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

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

69import Control.Monad.State.Strict

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

71import Data.Binary hiding (get, put)

70import Data.Binary hiding (get, put)

72−import qualified Data.Binary as B

73import Data.Char

71import Data.Char

74import Data.Data (Data)

72import Data.Data (Data)

75import Data.Foldable (Foldable)

73import Data.Foldable (Foldable)

76import Data.List hiding (group, insert)

74import Data.List hiding (group, insert)

77import qualified Data.Map.Strict as Map

75import qualified Data.Map.Strict as Map

78import Data.Maybe (listToMaybe)

76import Data.Maybe (listToMaybe)

79−import Data.Monoid (mconcat)

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

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

81import qualified Data.Text as T

78import qualified Data.Text as T

82import Data.Traversable (Traversable)

79import Data.Traversable (Traversable)

83import Data.Typeable (Typeable)

80import Data.Typeable (Typeable)

84−import Data.Vector.Unboxed (Vector)

85−import qualified Data.Vector.Unboxed as V

86import Debug.Trace

81import Debug.Trace

87import Foreign.Storable (sizeOf)

82import Foreign.Storable (sizeOf)

88import GHC.Generics (Generic)

83import GHC.Generics (Generic)

src/Idris/Core/Typecheck.hs−3

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

13

14import Idris.Core.Evaluate

15import Idris.Core.TT

16−import Idris.Core.WHNF

17

16

18import Control.Monad.State

17import Control.Monad.State

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

20−import Debug.Trace

21

18

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

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

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

20-- 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(

22import Idris.Core.Evaluate

23import Idris.Core.TT

24

25−import Control.Monad

26import Control.Monad.State.Strict

25import Control.Monad.State.Strict

27import Data.List

26import Data.List

28import Data.Maybe

27import Data.Maybe

29−import Debug.Trace

30

28

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

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

32-- at the time

30-- at the time

src/Idris/Core/WHNF.hs−3

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

12

13import Idris.Core.CaseTree

14import Idris.Core.Evaluate hiding (quote)

15−import qualified Idris.Core.Evaluate as Evaluate

16import Idris.Core.TT

15import Idris.Core.TT

17

16

18−import Debug.Trace

19−

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

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

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

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

22type StackEntry = (Term, WEnv)

19type StackEntry = (Term, WEnv)

src/Idris/Coverage.hs−3

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

16import Idris.Delaborate

17import Idris.Elab.Utils

18import Idris.Error

19−import Idris.Output (iWarn, iputStrLn)

20

19

21import Control.Monad.State.Strict

20import Control.Monad.State.Strict

22import Data.Char

21import Data.Char

23−import Data.Either

24import Data.List

22import Data.List

25import Data.Maybe

23import Data.Maybe

26−import Debug.Trace

27

24

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

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

29--

26--

src/Idris/DSL.hs−2

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

11module Idris.DSL where

12

13import Idris.AbsSyntax

14−import Idris.Core.Evaluate

15import Idris.Core.TT

14import Idris.Core.TT

16

15

17import Control.Monad.State.Strict

16import Control.Monad.State.Strict

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

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

19−import Debug.Trace

20

18

21debindApp :: SyntaxInfo -> PTerm -> PTerm

19debindApp :: SyntaxInfo -> PTerm -> PTerm

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

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

src/Idris/DataOpts.hs−6

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

10module Idris.DataOpts(applyOpts) where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.Core.TT

13import Idris.Core.TT

15

14

16−import Control.Applicative

17−import Data.List

18−import Data.Maybe

19−import Debug.Trace

20−

21class Optimisable term where

15class Optimisable term where

22 applyOpts :: term -> Idris term

16 applyOpts :: term -> Idris term

23

17

src/Idris/DeepSeq.hs−1

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

24

25import Util.DynamicLinker

26

27−import qualified Cheapskate.Types as CT

28import Control.DeepSeq

27import Control.DeepSeq

29import Network.Socket (PortNumber)

28import Network.Socket (PortNumber)

30

29

src/Idris/Delaborate.hs+1−2

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

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

27import Control.Monad.State

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

29−import Data.List (intersperse, nub)

29+import Data.List (nub)

30import Data.Maybe (mapMaybe)

31import qualified Data.Text as T

32−import Debug.Trace

33

32

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

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

35

34

src/Idris/Directives.hs−1

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

8module Idris.Directives(directiveAction) where

9

10import Idris.AbsSyntax

11−import Idris.ASTUtils

12import Idris.Core.Evaluate

11import Idris.Core.Evaluate

13import Idris.Core.TT

12import Idris.Core.TT

14import Idris.Imports

13import Idris.Imports

src/Idris/Elab/AsPat.hs−1

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

10import Idris.AbsSyntax

11import Idris.Core.TT

12

13−import Control.Applicative

14import Control.Monad.State.Strict

13import Control.Monad.State.Strict

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

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

16

15

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

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

13import Idris.Core.CaseTree

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

15import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

16import Idris.Core.TT

18import Idris.Core.Typecheck

17import Idris.Core.Typecheck

19import Idris.Core.WHNF

18import Idris.Core.WHNF

20import Idris.Coverage

19import Idris.Coverage

21import Idris.DataOpts

20import Idris.DataOpts

22−import Idris.DeepSeq

21+import Idris.DeepSeq ()

23import Idris.Delaborate

22import Idris.Delaborate

24import Idris.Docstrings hiding (Unchecked)

23import Idris.Docstrings hiding (Unchecked)

25−import Idris.DSL

26import Idris.Elab.AsPat

24import Idris.Elab.AsPat

27import Idris.Elab.Term

25import Idris.Elab.Term

28import Idris.Elab.Transform

26import Idris.Elab.Transform

29import Idris.Elab.Type

27import Idris.Elab.Type

30import Idris.Elab.Utils

28import Idris.Elab.Utils

31import Idris.Error

29import Idris.Error

32−import Idris.Imports

33import Idris.Inliner

30import Idris.Inliner

34import Idris.Options

31import Idris.Options

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

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

36import Idris.PartialEval

33import Idris.PartialEval

37−import Idris.Primitives

38−import Idris.Providers

39import Idris.Termination

34import Idris.Termination

40import Idris.Transforms

35import Idris.Transforms

41−import IRTS.Lang

42

36

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

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

44−import Util.Pretty (pretty, text)

45

38

46import Prelude hiding (id, (.))

39import Prelude hiding (id, (.))

47

40

48−import Control.Applicative hiding (Const)

49import Control.Category

41import Control.Category

50import Control.DeepSeq

42import Control.DeepSeq

51import Control.Monad

43import Control.Monad

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

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

53import Control.Monad.State.Strict as State

45import Control.Monad.State.Strict as State

54−import Data.Char (isLetter, toLower)

55import Data.List

46import Data.List

56−import Data.List.Split (splitOn)

57−import qualified Data.Map as Map

58import Data.Maybe

47import Data.Maybe

59−import qualified Data.Set as S

60−import qualified Data.Text as T

61import Data.Word

48import Data.Word

62import Debug.Trace

49import Debug.Trace

63import Numeric

50import Numeric

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

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

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13−import Idris.Core.CaseTree

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

15import Idris.Core.Evaluate

13import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

14import Idris.Core.TT

18import Idris.Core.Typecheck

15import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25import Idris.Elab.Rewrite

18import Idris.Elab.Rewrite

26−import Idris.Elab.Term

27import Idris.Elab.Type

19import Idris.Elab.Type

28import Idris.Elab.Utils

20import Idris.Elab.Utils

29import Idris.Elab.Value

21import Idris.Elab.Value

30import Idris.Error

22import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

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

23+import Idris.Output (iWarn, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38

24

39import Util.Pretty

25import Util.Pretty

40

26

41import Prelude hiding (id, (.))

27import Prelude hiding (id, (.))

42

28

43−import Control.Applicative hiding (Const)

44import Control.Category

29import Control.Category

45−import Control.DeepSeq

46import Control.Monad

30import Control.Monad

47import Control.Monad.State.Strict as State

31import Control.Monad.State.Strict as State

48import Data.Char (isLetter, toLower)

32import Data.Char (isLetter, toLower)

49import Data.List

33import Data.List

50−import Data.List.Split (splitOn)

51import qualified Data.Map as Map

34import qualified Data.Map as Map

52import Data.Maybe

35import Data.Maybe

53−import qualified Data.Set as S

54import qualified Data.Text as T

36import qualified Data.Text as T

55−import Debug.Trace

56

37

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

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

58warnLC fc n

39warnLC fc n

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

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

9module Idris.Elab.Implementation(elabImplementation) where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13import Idris.Core.CaseTree

12import Idris.Core.CaseTree

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

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

15import Idris.Core.Evaluate

14import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

15import Idris.Core.TT

18−import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25−import Idris.Elab.Data

26import Idris.Elab.Term

18import Idris.Elab.Term

27import Idris.Elab.Type

19import Idris.Elab.Type

28import Idris.Elab.Utils

20import Idris.Elab.Utils

29import Idris.Error

21import Idris.Error

30−import Idris.Imports

31−import Idris.Inliner

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

22+import Idris.Output (iWarn, sendHighlighting)

33−import Idris.PartialEval

34−import Idris.Primitives

35−import Idris.Providers

36−import IRTS.Lang

37

23

38−import Util.Pretty (pretty, text)

24+import Util.Pretty (text)

39

25

40import Prelude hiding (id, (.))

26import Prelude hiding (id, (.))

41

27

42−import Control.Applicative hiding (Const)

43import Control.Category

28import Control.Category

44−import Control.DeepSeq

45import Control.Monad

29import Control.Monad

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

47−import Data.Char (isLetter, toLower)

48import Data.List

30import Data.List

49−import Data.List.Split (splitOn)

50−import qualified Data.Map as Map

51import Data.Maybe

31import Data.Maybe

52−import qualified Data.Set as S

53import qualified Data.Text as T

32import qualified Data.Text as T

54−import Debug.Trace

55−

56

33

57elabImplementation :: ElabInfo

34elabImplementation :: ElabInfo

58 -> SyntaxInfo

35 -> SyntaxInfo

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

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

10module Idris.Elab.Interface(elabInterface) where

11

12import Idris.AbsSyntax

13−import Idris.ASTUtils

14−import Idris.Core.CaseTree

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

16import Idris.Core.Evaluate

13import Idris.Core.Evaluate

17−import Idris.Core.Execute

18import Idris.Core.TT

14import Idris.Core.TT

19−import Idris.Core.Typecheck

20−import Idris.Coverage

21−import Idris.DataOpts

22−import Idris.DeepSeq

23import Idris.Delaborate

15import Idris.Delaborate

24import Idris.Docstrings

16import Idris.Docstrings

25−import Idris.DSL

26import Idris.Elab.Data

17import Idris.Elab.Data

27−import Idris.Elab.Term

28−import Idris.Elab.Type

29import Idris.Elab.Utils

18import Idris.Elab.Utils

30import Idris.Error

19import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

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

20+import Idris.Output (sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38−

39−import Util.Pretty (pretty, text)

40

21

41import Prelude hiding (id, (.))

22import Prelude hiding (id, (.))

42

23

43−import Control.Applicative hiding (Const)

44import Control.Category

24import Control.Category

45−import Control.DeepSeq

46import Control.Monad

25import Control.Monad

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

48−import Data.Char (isLetter, toLower)

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

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

50import Data.List

27import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53import Data.Maybe

28import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

57−

58

29

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

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

60

31

src/Idris/Elab/Provider.hs−27

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

9module Idris.Elab.Provider(elabProvider) where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

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

15import Idris.Core.Evaluate

12import Idris.Core.Evaluate

16import Idris.Core.Execute

13import Idris.Core.Execute

17import Idris.Core.TT

14import Idris.Core.TT

18import Idris.Core.Typecheck

15import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25import Idris.Elab.Clause

18import Idris.Elab.Clause

26import Idris.Elab.Term

19import Idris.Elab.Term

27import Idris.Elab.Type

20import Idris.Elab.Type

28−import Idris.Elab.Utils

29import Idris.Elab.Value

21import Idris.Elab.Value

30import Idris.Error

22import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33import Idris.Options

23import Idris.Options

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

35−import Idris.PartialEval

36−import Idris.Primitives

37import Idris.Providers

24import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

41

25

42import Prelude hiding (id, (.))

26import Prelude hiding (id, (.))

43

27

44−import Control.Applicative hiding (Const)

45import Control.Category

28import Control.Category

46−import Control.DeepSeq

47import Control.Monad

29import 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

57

30

58-- | Elaborate a type provider

31-- | Elaborate a type provider

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

32elabProvider :: 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

11import Idris.AbsSyntax

12import Idris.Core.Evaluate

13import Idris.Core.TT

14−import Idris.Coverage

15−import Idris.DataOpts

16−import Idris.DeepSeq

17import Idris.Delaborate

14import Idris.Delaborate

18import Idris.Docstrings

15import Idris.Docstrings

19import Idris.Elab.Data

16import Idris.Elab.Data

20−import Idris.Elab.Data

21−import Idris.Elab.Term

22−import Idris.Elab.Type

23−import Idris.Elab.Utils

24import Idris.Error

17import Idris.Error

25−import Idris.Imports

26−import Idris.Inliner

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

18+import Idris.Output (sendHighlighting)

28import Idris.Parser.Expr (tryFullExpr)

19import Idris.Parser.Expr (tryFullExpr)

29−import Idris.PartialEval

30−import Idris.Primitives

31−import Idris.Providers

32−import IRTS.Lang

33

20

34import Control.Monad

21import Control.Monad

35import Data.List

22import Data.List

src/Idris/Elab/Rewrite.hs−3

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

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

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.Core.Elaborate

13import Idris.Core.Elaborate

15import Idris.Core.Evaluate

14import Idris.Core.Evaluate

16import Idris.Core.TT

15import Idris.Core.TT

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

20

19

21import Control.Monad

20import Control.Monad

22import Control.Monad.State.Strict

21import Control.Monad.State.Strict

23−import Data.List

24−import Debug.Trace

25

22

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

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

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

24 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

9

10import Idris.AbsSyntax

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

12−import Idris.Core.Evaluate

13−import Idris.Core.Execute

14import Idris.Core.TT

12import Idris.Core.TT

15import Idris.Core.Typecheck

13import Idris.Core.Typecheck

16import Idris.Elab.Term

14import Idris.Elab.Term

17import Idris.Elab.Value (elabVal)

15import Idris.Elab.Value (elabVal)

18import Idris.Error

16import Idris.Error

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

17+import Idris.Output (sendHighlighting)

20

18

21elabScriptTy :: Type

19elabScriptTy :: Type

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

20elabScriptTy = 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.

10module Idris.Elab.Term where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

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

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

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

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

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

17import Idris.Core.ProofTerm (getProofTerm)

16import Idris.Core.ProofTerm (getProofTerm)

18import Idris.Core.TT

17import Idris.Core.TT

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

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

20import Idris.Core.Unify

19import Idris.Core.Unify

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

20+import Idris.Core.WHNF (whnf)

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

21+import Idris.Coverage (genClauses, recoverableCoverage)

23import Idris.Delaborate

22import Idris.Delaborate

24−import Idris.DSL

25import Idris.Elab.Quasiquote (extractUnquotes)

23import Idris.Elab.Quasiquote (extractUnquotes)

26import Idris.Elab.Rewrite

24import Idris.Elab.Rewrite

27import Idris.Elab.Utils

25import Idris.Elab.Utils

28import Idris.Error

26import Idris.Error

29import Idris.ErrReverse (errReverse)

27import Idris.ErrReverse (errReverse)

30import Idris.Options

28import Idris.Options

31−import Idris.Output (pshow)

32import Idris.ProofSearch

29import Idris.ProofSearch

33import Idris.Reflection

30import Idris.Reflection

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

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

35

32

36−import qualified Util.Pretty as U

37−

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

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

39import Control.Monad

34import Control.Monad

40import Control.Monad.State.Strict

35import Control.Monad.State.Strict

41import Data.Foldable (for_)

36import Data.Foldable (for_)

42import Data.List

37import Data.List

43import qualified Data.Map as M

38import qualified Data.Map as M

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

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

45import qualified Data.Set as S

40import qualified Data.Set as S

46−import qualified Data.Text as T

47import Debug.Trace

41import Debug.Trace

48

42

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

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

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

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

9module Idris.Elab.Transform where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

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

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

15−import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

13import Idris.Core.TT

18import Idris.Core.Typecheck

14import 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

25import Idris.Elab.Term

15import Idris.Elab.Term

26import Idris.Elab.Utils

16import Idris.Elab.Utils

27import Idris.Error

17import Idris.Error

28−import Idris.Imports

29−import Idris.Inliner

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

18+import Idris.Output (sendHighlighting)

31−import Idris.PartialEval

32−import Idris.Primitives

33−import Idris.Providers

34−import IRTS.Lang

35−

36−import Util.Pretty (pretty, text)

37

19

38import Prelude hiding (id, (.))

20import Prelude hiding (id, (.))

39

21

40−import Control.Applicative hiding (Const)

41import Control.Category

22import Control.Category

42−import Control.DeepSeq

43import Control.Monad

23import Control.Monad

44import Control.Monad.State.Strict as State

24import 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

53

25

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

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

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

27elabTransform 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 (

13

14import Idris.AbsSyntax

15import Idris.ASTUtils

16−import Idris.Core.CaseTree

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

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

18import Idris.Core.Evaluate

17import Idris.Core.Evaluate

19−import Idris.Core.Execute

20import Idris.Core.TT

18import Idris.Core.TT

21−import Idris.Core.Typecheck

22import Idris.Core.WHNF

19import Idris.Core.WHNF

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

27import Idris.Docstrings (Docstring)

20import Idris.Docstrings (Docstring)

28−import Idris.DSL

29import Idris.Elab.Term

21import Idris.Elab.Term

30import Idris.Elab.Utils

22import Idris.Elab.Utils

31import Idris.Elab.Value

23import Idris.Elab.Value

32import Idris.Error

24import Idris.Error

33−import Idris.Imports

34−import Idris.Inliner

35import Idris.Options

25import Idris.Options

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

26+import Idris.Output (sendHighlighting)

37−import Idris.PartialEval

38−import Idris.Primitives

39−import Idris.Providers

40−import IRTS.Lang

41−

42−import Util.Pretty (pretty, text)

43

27

44import Prelude hiding (id, (.))

28import Prelude hiding (id, (.))

45

29

46−import Control.Applicative hiding (Const)

47import Control.Category

30import Control.Category

48−import Control.DeepSeq

49import Control.Monad

31import 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

56import qualified Data.Set as S

32import qualified Data.Set as S

57−import qualified Data.Text as T

58−import qualified Data.Traversable as Traversable

59−import Debug.Trace

60

33

61buildType :: ElabInfo

34buildType :: ElabInfo

62 -> SyntaxInfo

35 -> SyntaxInfo

src/Idris/Elab/Utils.hs−4

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

14import Idris.Core.TT

15import Idris.Core.Typecheck

16import Idris.Core.WHNF

17−import Idris.DeepSeq

18import Idris.Delaborate

17import Idris.Delaborate

19import Idris.Docstrings

18import Idris.Docstrings

20import Idris.Error

19import Idris.Error

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

22

21

23import Util.Pretty

22import Util.Pretty

24

23

25−import Control.Applicative hiding (Const)

26import Control.Monad

24import Control.Monad

27import Control.Monad.State

25import Control.Monad.State

28import Data.List

26import Data.List

29import qualified Data.Map as Map

27import qualified Data.Map as Map

30import Data.Maybe

28import Data.Maybe

31−import qualified Data.Traversable as Traversable

32−import Debug.Trace

33

29

34recheckC = recheckC_borrowing False True []

30recheckC = recheckC_borrowing False True []

35

31

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

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

13 ) where

14

15import Idris.AbsSyntax

16−import Idris.ASTUtils

17−import Idris.Core.CaseTree

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

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

19import Idris.Core.Evaluate hiding (Unchecked)

17import Idris.Core.Evaluate hiding (Unchecked)

20−import Idris.Core.Execute

21import Idris.Core.TT

18import Idris.Core.TT

22−import Idris.Core.Typecheck

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

27import Idris.Docstrings

19import Idris.Docstrings

28−import Idris.DSL

29import Idris.Elab.Term

20import Idris.Elab.Term

30import Idris.Elab.Utils

21import Idris.Elab.Utils

31import Idris.Error

22import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

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

23+import Idris.Output (sendHighlighting)

35−import Idris.PartialEval

36−import Idris.Primitives

37−import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

41

24

42import Prelude hiding (id, (.))

25import Prelude hiding (id, (.))

43

26

44−import Control.Applicative hiding (Const)

45import Control.Category

27import Control.Category

46−import Control.DeepSeq

47−import Control.Monad

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

49−import Data.Char (isLetter, toLower)

28+import Data.Char (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

56import qualified Data.Traversable as Traversable

29import qualified Data.Traversable as Traversable

57−import Debug.Trace

58

30

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

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

60-- happen if elaborating as a pattern clause)

32-- happen if elaborating as a pattern clause)

src/Idris/ElabDecls.hs+1−26

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

12module Idris.ElabDecls where

13

14import Idris.AbsSyntax

15−import Idris.ASTUtils

16−import Idris.Core.CaseTree

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

18import Idris.Core.Evaluate

15import Idris.Core.Evaluate

19−import Idris.Core.Execute

20import Idris.Core.TT

16import Idris.Core.TT

21−import Idris.Core.Typecheck

22−import Idris.Coverage

23−import Idris.DataOpts

24−import Idris.DeepSeq

25−import Idris.Delaborate

26import Idris.Directives

17import Idris.Directives

27import Idris.Docstrings hiding (Unchecked)

18import Idris.Docstrings hiding (Unchecked)

28−import Idris.DSL

29import Idris.Elab.Clause

19import Idris.Elab.Clause

30import Idris.Elab.Data

20import Idris.Elab.Data

31import Idris.Elab.Implementation

21import Idris.Elab.Implementation

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

36import Idris.Elab.Term

26import Idris.Elab.Term

37import Idris.Elab.Transform

27import Idris.Elab.Transform

38import Idris.Elab.Type

28import Idris.Elab.Type

39−import Idris.Elab.Utils

40import Idris.Elab.Value

29import Idris.Elab.Value

41import Idris.Error

30import Idris.Error

42−import Idris.Imports

43−import Idris.Inliner

44import Idris.Options

31import Idris.Options

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

32+import Idris.Output (sendHighlighting)

46−import Idris.PartialEval

47import Idris.Primitives

33import Idris.Primitives

48−import Idris.Providers

49import Idris.Termination

34import Idris.Termination

50import IRTS.Lang

35import IRTS.Lang

51

36

52−import Util.Pretty (pretty, text)

53−

54import Prelude hiding (id, (.))

37import Prelude hiding (id, (.))

55

38

56−import Control.Applicative hiding (Const)

57import Control.Category

39import Control.Category

58−import Control.DeepSeq

59import Control.Monad

40import Control.Monad

60import Control.Monad.State.Strict as State

41import 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

65import Data.Maybe

42import Data.Maybe

66−import qualified Data.Set as S

67import qualified Data.Text as T

43import qualified Data.Text as T

68−import Debug.Trace

69

44

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

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

71recinfo :: FC -> ElabInfo

46recinfo :: FC -> ElabInfo

src/Idris/Erasure.hs−3

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

20

21import Prelude hiding (id, (.))

22

23−import Control.Applicative

24import Control.Arrow

23import Control.Arrow

25import Control.Category

24import Control.Category

26import Control.Monad.State

25import Control.Monad.State

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

36import qualified Data.Set as S

35import qualified Data.Set as S

37import Data.Text (pack)

36import Data.Text (pack)

38import qualified Data.Text as T

37import qualified Data.Text as T

39−import Debug.Trace

40−import System.IO.Unsafe

41

38

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

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

43-- positions.

40-- positions.

src/Idris/ErrReverse.hs−1

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

15import Util.Pretty

16

17import Data.List

18−import Debug.Trace

19

18

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

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

21-- so that errors will be more readable,

20-- so that errors will be more readable,

src/Idris/Error.hs−7

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

14import Idris.Core.Constraints

15import Idris.Core.Evaluate (ctxtAlist)

16import Idris.Core.TT

17−import Idris.Core.Typecheck

18import Idris.Delaborate

17import Idris.Delaborate

19import Idris.Output

18import Idris.Output

20

19

21import Prelude hiding (catch)

20import Prelude hiding (catch)

22

21

23import Control.Monad (when)

22import Control.Monad (when)

24−import Control.Monad.State.Strict

25−import Data.Char

26import qualified Data.Foldable as Foldable

23import qualified Data.Foldable as Foldable

27import Data.List (intercalate, isPrefixOf)

24import Data.List (intercalate, isPrefixOf)

28import qualified Data.Set as S

25import qualified Data.Set as S

29import qualified Data.Text as T

26import 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

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

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

35

28

36iucheck :: Idris ()

29iucheck :: Idris ()

src/Idris/IdeMode.hs+1−1

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

11

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

13

14−import Idris.Core.Binary

14+import Idris.Core.Binary ()

15import Idris.Core.TT

16

17import Control.Applicative hiding (Const)

src/Idris/IdrisDoc.hs+4−9

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

10module Idris.IdrisDoc (generateDocs) where

11

12import Idris.AbsSyntax

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

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

14− isFnName, isTConName, lookupDefAcc)

14+ isTConName, lookupDefAcc)

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

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

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

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

17− toAlist, txt)

18import Idris.Docs

17import Idris.Docs

19import Idris.Docstrings (nullDocstring)

18import Idris.Docstrings (nullDocstring)

20import qualified Idris.Docstrings as Docstrings

19import qualified Idris.Docstrings as Docstrings

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

26import Control.Monad (forM_)

25import Control.Monad (forM_)

27import Control.Monad.Trans.Except

26import Control.Monad.Trans.Except

28import Control.Monad.Trans.State.Strict

27import Control.Monad.Trans.State.Strict

29−import qualified Data.ByteString as BS

30import qualified Data.ByteString.Lazy as BS2

28import qualified Data.ByteString.Lazy as BS2

31import qualified Data.List as L

29import qualified Data.List as L

32−import qualified Data.List.Split as LS

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

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

34import Data.Maybe

31import Data.Maybe

35import Data.Monoid (mempty)

32import Data.Monoid (mempty)

36−import qualified Data.Ord (compare)

37import qualified Data.Set as S

33import qualified Data.Set as S

38import qualified Data.Text as T

34import qualified Data.Text as T

39−import qualified Data.Text.Encoding as E

40import System.Directory

35import System.Directory

41import System.FilePath

36import System.FilePath

42import System.IO

37import System.IO

src/Idris/Imports.hs−1

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

13import Idris.AbsSyntax

14import Idris.Core.TT

15import Idris.Error

16−import Idris.Output

17import IRTS.System (getIdrisLibDir)

16import IRTS.System (getIdrisLibDir)

18

17

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

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

src/Idris/Info.hs−1

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

29import Idris.Options (loggingCatsStr)

30import qualified IRTS.System as S

31

32−import Paths_idris

33import Version_idris (gitHash)

32import Version_idris (gitHash)

34

33

35import Data.Version

34import Data.Version

src/Idris/Output.hs+2−3

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

13

14import Idris.AbsSyntax

15import Idris.Colours (hEndColourise, hStartColourise)

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

16+import Idris.Core.Evaluate (normaliseAll)

17import Idris.Core.TT

18import Idris.Delaborate

19import Idris.Docstrings

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

27import Prelude hiding ((<$>))

28

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

30−import Data.Char (isAlpha)

31import Data.List (intersperse, nub)

30import Data.List (intersperse, nub)

32import Data.Maybe (fromMaybe)

31import Data.Maybe (fromMaybe)

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

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

34 RunIO(RunIO))

33 RunIO(RunIO))

35import System.FilePath (replaceExtension)

34import System.FilePath (replaceExtension)

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

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

37

36

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

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

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

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

src/Idris/Package.hs+1−4

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

12import System.Directory (copyFile, createDirectoryIfMissing)

13import System.Exit

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

15− hasExtension, normalise, takeDirectory, takeExtension,

15+ hasExtension, takeDirectory, takeExtension,

16 takeFileName, (</>))

17import System.IO

18import System.Process

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

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

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

25import Data.Either (partitionEithers)

26−import Data.Either (partitionEithers)

27import Data.List

26import Data.List

28import Data.List.Split (splitOn)

27import Data.List.Split (splitOn)

29−import Data.Maybe (fromMaybe)

30

28

31import Idris.AbsSyntax

29import Idris.AbsSyntax

32import Idris.Core.TT

30import Idris.Core.TT

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

38import Idris.Options

36import Idris.Options

39import Idris.Output

37import Idris.Output

40import Idris.Parser (loadModule)

38import Idris.Parser (loadModule)

41−import Idris.REPL

42

39

43import Idris.Package.Common

40import Idris.Package.Common

44import Idris.Package.Parser

41import Idris.Package.Parser

src/Idris/Package/Parser.hs−6

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

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

9module Idris.Package.Parser where

10

11−import Idris.AbsSyntaxTree

12import Idris.CmdOptions

11import Idris.CmdOptions

13−import Idris.Core.TT

14import Idris.Package.Common

12import Idris.Package.Common

15import Idris.Parser.Helpers hiding (stringLiteral)

13import Idris.Parser.Helpers hiding (stringLiteral)

16−import Idris.REPL

17−

18−import Util.System

19

14

20import Control.Applicative

15import Control.Applicative

21import Control.Monad.State.Strict

16import Control.Monad.State.Strict

22import Data.List (union)

17import Data.List (union)

23−import Data.Maybe (fromJust, isNothing)

24import System.Directory (doesFileExist)

18import System.Directory (doesFileExist)

25import System.Exit

19import System.Exit

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

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

src/Idris/Parser/Data.hs−15

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

12import Idris.Core.Evaluate

13import Idris.Core.TT

14import Idris.Docstrings

15−import Idris.DSL

16import Idris.Options

15import Idris.Options

17import Idris.Parser.Expr

16import Idris.Parser.Expr

18import Idris.Parser.Helpers

17import Idris.Parser.Helpers

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

21import Prelude hiding (pi)

20import Prelude hiding (pi)

22

21

23import Control.Applicative

22import Control.Applicative

24−import Control.Monad

25import Control.Monad.State.Strict

23import Control.Monad.State.Strict

26−import qualified Data.ByteString.UTF8 as UTF8

27−import Data.Char

28−import qualified Data.HashSet as HS

29import Data.List

24import Data.List

30−import qualified Data.List.Split as Spl

31import Data.Maybe

25import 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

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

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

41 stringLiteral, symbol, whiteSpace)

27 stringLiteral, symbol, whiteSpace)

42−import Text.Trifecta.Delta

43

28

44{- | Parses a record type declaration

29{- | Parses a record type declaration

45Record ::=

30Record ::=

src/Idris/Parser/Expr.hs−12

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

21import Control.Applicative

22import Control.Monad

23import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25−import Data.Char

26import Data.Function (on)

24import Data.Function (on)

27−import qualified Data.HashSet as HS

28import Data.List

25import Data.List

29−import qualified Data.List.Split as Spl

30import Data.Maybe

26import 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

35import Text.Parser.Expression

27import 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

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

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

40 stringLiteral, symbol, whiteSpace)

29 stringLiteral, symbol, whiteSpace)

41−import Text.Trifecta.Delta

42

30

43-- | Allow implicit type declarations

31-- | Allow implicit type declarations

44allowImp :: SyntaxInfo -> SyntaxInfo

32allowImp :: SyntaxInfo -> SyntaxInfo

src/Idris/Parser/Helpers.hs−6

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

18import Idris.Options

19import Idris.Output (iWarn)

20

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

22−

23import Prelude hiding (pi)

21import Prelude hiding (pi)

24

22

25import Control.Applicative

23import Control.Applicative

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

29import Data.Char

27import Data.Char

30import qualified Data.HashSet as HS

28import qualified Data.HashSet as HS

31import Data.List

29import Data.List

32−import qualified Data.List.Split as Spl

33import qualified Data.Map as M

30import qualified Data.Map as M

34import Data.Maybe

31import Data.Maybe

35−import Data.Monoid

36import qualified Data.Text as T

32import qualified Data.Text as T

37−import Debug.Trace

38import System.FilePath

33import System.FilePath

39import qualified Text.Parser.Char as Chr

34import qualified Text.Parser.Char as Chr

40−import Text.Parser.Expression

41import Text.Parser.LookAhead

35import Text.Parser.LookAhead

42import qualified Text.Parser.Token as Tok

36import qualified Text.Parser.Token as Tok

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

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

src/Idris/Parser/Ops.hs−13

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

18import Control.Applicative

19import Control.Monad

20import Control.Monad.State.Strict

21−import qualified Data.ByteString.UTF8 as UTF8

22−import Data.Char

23−import qualified Data.HashSet as HS

24import Data.List

21import 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

31import Text.Parser.Expression

22import 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

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

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

36 stringLiteral, symbol, whiteSpace)

24 stringLiteral, symbol, whiteSpace)

37−import Text.Trifecta.Delta

38

25

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

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

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

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

src/Idris/PartialEval.hs−3

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

19import Idris.Core.TT

20import Idris.Delaborate

21

22−import Control.Applicative

23import Control.Monad.State

22import Control.Monad.State

24−import Data.Maybe

25−import Debug.Trace

26

23

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

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

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

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

src/Idris/Primitives.hs−3

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

9

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

11

12−import Idris.AbsSyntax

13import Idris.Core.Evaluate

12import Idris.Core.Evaluate

14import Idris.Core.TT

13import Idris.Core.TT

15import IRTS.Lang

14import IRTS.Lang

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

18import Data.Char

17import Data.Char

19import Data.Function (on)

18import Data.Function (on)

20import Data.Int

19import Data.Int

21−import qualified Data.Vector.Unboxed as V

22import Data.Word

20import Data.Word

23−import Debug.Trace

24

21

25data Prim = Prim { p_name :: Name,

22data Prim = Prim { p_name :: Name,

26 p_type :: Type,

23 p_type :: Type,

src/Idris/ProofSearch.hs−3

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

16 ) where

17

18import Idris.AbsSyntax

19−import Idris.Core.CaseTree

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

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

21import Idris.Core.Evaluate

20import Idris.Core.Evaluate

22import Idris.Core.TT

21import Idris.Core.TT

23−import Idris.Core.Typecheck

24import Idris.Core.Unify

22import Idris.Core.Unify

25import Idris.Delaborate

23import Idris.Delaborate

26−import Idris.Error

27

24

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

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

29import Control.Monad

26import Control.Monad

src/Idris/Prover.hs+3−5

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

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

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

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

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

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

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

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

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

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

17

18import Idris.AbsSyntax

19−import Idris.AbsSyntaxTree

20import Idris.Completion

19import Idris.Completion

21import Idris.Core.CaseTree

20import Idris.Core.CaseTree

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

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

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

41

40

42import Control.DeepSeq

41import Control.DeepSeq

43import Control.Monad.State.Strict

42import Control.Monad.State.Strict

44−import Debug.Trace

45import System.Console.Haskeline

43import System.Console.Haskeline

46import System.Console.Haskeline.History

44import System.Console.Haskeline.History

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

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

src/Idris/Providers.hs−2

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

13 ) where

14

15import Idris.AbsSyntax

16−import Idris.AbsSyntaxTree

17−import Idris.Core.Evaluate

18import Idris.Core.TT

16import Idris.Core.TT

19import Idris.Error

17import Idris.Error

20

18

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

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

21

22import Control.Applicative

23import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25import Data.Char (isSpace, toLower)

24import Data.Char (isSpace, toLower)

26import Data.List

25import Data.List

27import Data.List.Split (splitOn)

26import Data.List.Split (splitOn)

28−import Debug.Trace

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

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

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

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

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

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

32import Text.Parser.Combinators

30import Text.Parser.Combinators

33−import Text.Trifecta (Result, parseString)

31+import Text.Trifecta (Result)

34−import Text.Trifecta.Delta

35

32

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

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

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

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

src/Idris/Termination.hs+1−2

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

15import Idris.Delaborate

16import Idris.Error

17import Idris.Options

18−import Idris.Output (iWarn, iputStrLn)

18+import Idris.Output (iWarn)

19

20import Control.Monad.State.Strict

21−import Data.Char

22import Data.Either

21import Data.Either

23import Data.List

22import Data.List

24import Data.Maybe

23import Data.Maybe

src/Idris/Transforms.hs−3

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

16 ) where

17

18import Idris.AbsSyntax

19−import Idris.Core.CaseTree

20import Idris.Core.TT

19import Idris.Core.TT

21

20

22−import Debug.Trace

23−

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

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

25 [Either Term (Term, Term)]

22 [Either Term (Term, Term)]

26transformPats ist ps = map tClause ps where

23transformPats ist ps = map tClause ps where

src/Idris/TypeSearch.hs+1−1

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

14 ) where

15

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

17− logLvl, putIState)

17+ putIState)

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

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

20 defaultSyntax, eqTy, implicitAllowed,

src/Util/DynamicLinker.hs+16−9

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

13 ) where

14

15#ifdef IDRIS_FFI

16−import Foreign.LibFFI

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

18import System.Directory

16import 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

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

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

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

26+#ifdef linux_HOST_OS

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

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

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

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

23import Data.Maybe (catMaybes)

29import Data.Maybe (catMaybes)

30+#else

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

32+#endif

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

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

25import System.Posix.DynamicLinker

34import System.Posix.DynamicLinker

26import Text.Regex.TDFA

35import Text.Regex.TDFA

27−#else

36+#endif

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

37+

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

38+#ifdef mingw32_HOST_OS

30−import System.Win32.DLL

31−import System.Win32.Types

32type DL = HMODULE

39type DL = HMODULE

33#endif

40#endif

34

41

stack.yaml+3

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

9 FFI: true

10 GMP: true

11

12+ghc-options:

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

14+

12extra-deps:

15extra-deps:

13 - binary-0.8.5.1

16 - binary-0.8.5.1

14 - cheapskate-0.1.1

17 - cheapskate-0.1.1