692d610 · Idris-dev · git.iko.soy

codegen/idris-codegen-c/Main.hs+7−5

compare with master

unifiedsplit

@@ -1,19 +1,21 @@

1module Main where

2

3−import Idris.Core.TT

4import Idris.AbsSyntax

3import Idris.AbsSyntax

4+import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7−import IRTS.Compiler

8import IRTS.CodegenC

7import IRTS.CodegenC

8+import IRTS.Compiler

9+

10+import Util.System

9

11

12+import Paths_idris

13+

14+import Control.Monad

10import System.Environment

15import System.Environment

11import System.Exit

16import System.Exit

12−import Control.Monad

13

17

14−import Paths_idris

15

18

16−import Util.System

17

19

18data Opts = Opts { inputs :: [FilePath],

20data Opts = Opts { inputs :: [FilePath],

19 interface :: Bool,

21 interface :: Bool,

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

@@ -1,16 +1,17 @@

1module Main where

2

3−import Idris.Core.TT

4import Idris.AbsSyntax

3import Idris.AbsSyntax

4+import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7−import IRTS.Compiler

8import IRTS.CodegenJavaScript

7import IRTS.CodegenJavaScript

8+import IRTS.Compiler

9+

10+import Paths_idris

9

11

10import System.Environment

12import System.Environment

11import System.Exit

13import System.Exit

12

14

13−import Paths_idris

14

15

15data Opts = Opts {

16data Opts = Opts {

16 inputs :: [FilePath]

17 inputs :: [FilePath]

codegen/idris-codegen-node/Main.hs+4−5

@@ -1,18 +1,17 @@

1module Main where

2

3−import Idris.Core.TT

4import Idris.AbsSyntax

3import Idris.AbsSyntax

4+import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7−

8−import IRTS.Compiler

9import IRTS.CodegenJavaScript

7import IRTS.CodegenJavaScript

8+import IRTS.Compiler

9+

10+import Paths_idris

10

11

11import System.Environment

12import System.Environment

12import System.Exit

13import System.Exit

13

14

14−import Paths_idris

15−

16data Opts = Opts { inputs :: [FilePath]

15data Opts = Opts { inputs :: [FilePath]

17 , output :: FilePath

16 , output :: FilePath

18 }

17 }

main/Main.hs+6−6

@@ -1,16 +1,16 @@

1module Main where

2

3−import Control.Monad ( when )

4−import System.Exit ( exitSuccess )

5−

6import Idris.AbsSyntax

3import Idris.AbsSyntax

7−import Idris.Error

8import Idris.CmdOptions

4import Idris.CmdOptions

5+import Idris.Error

9import Idris.Info.Show

6import Idris.Info.Show

10−import Idris.Package

11import Idris.Main

7import Idris.Main

8+import Idris.Package

9+

10+import Util.System (setupBundledCC)

12

11

13−import Util.System ( setupBundledCC )

12+import Control.Monad (when)

13+import System.Exit (exitSuccess)

14

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

16processShowOptions opts = runIO $ do

src/IRTS/BCImp.hs+1−1

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

7-}

8module IRTS.BCImp where

9

10+import Idris.Core.TT

10import IRTS.Lang

11import IRTS.Lang

11import IRTS.Simplified

12import IRTS.Simplified

12−import Idris.Core.TT

13

14data Reg = RVal | L Int

15

src/IRTS/Bytecode.hs+3−2

@@ -21,10 +21,11 @@ returns) are stored.

21module IRTS.Bytecode where

22

23

24+import Idris.Core.TT

25+import IRTS.Defunctionalise

24import IRTS.Lang

26import IRTS.Lang

25import IRTS.Simplified

27import IRTS.Simplified

26−import IRTS.Defunctionalise

28+

27−import Idris.Core.TT

28import Data.Maybe

29import Data.Maybe

29

30

30data Reg = RVal | L Int | T Int | Tmp

31data Reg = RVal | L Int | T Int | Tmp

src/IRTS/CodegenC.hs+11−11

@@ -8,27 +8,27 @@ Maintainer : The Idris Community.

8module IRTS.CodegenC (codegenC) where

9

10import Idris.AbsSyntax

11+import Idris.Core.TT

11import IRTS.Bytecode

12import IRTS.Bytecode

13+import IRTS.CodegenCommon

14+import IRTS.Defunctionalise

12import IRTS.Lang

15import IRTS.Lang

13import IRTS.Simplified

16import IRTS.Simplified

14−import IRTS.Defunctionalise

15import IRTS.System

17import IRTS.System

16−import IRTS.CodegenCommon

18+

17−import Idris.Core.TT

18import Util.System

19import Util.System

19

20

20−import Numeric

21+import Control.Monad

21−import Data.Char

22import Data.Bits

23+import Data.Char

23import Data.List (intercalate, nubBy)

24import Data.List (intercalate, nubBy)

24−import System.Process

25+import Debug.Trace

26+import Numeric

27+import System.Directory

25import System.Exit

28import System.Exit

29+import System.FilePath ((<.>), (</>))

26import System.IO

30import System.IO

27−import System.Directory

31+import System.Process

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

29−import Control.Monad

30−

31−import Debug.Trace

32

33codegenC :: CodeGenerator

34codegenC ci = do codegenC' (simpleDecls ci)

src/IRTS/CodegenCommon.hs+3−3

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

8-}

9module IRTS.CodegenCommon where

10

11−import GHC.Generics (Generic)

12−

13import Idris.Core.TT

11import Idris.Core.TT

14−import IRTS.Simplified

15import IRTS.Defunctionalise

12import IRTS.Defunctionalise

13+import IRTS.Simplified

14+

15+import GHC.Generics (Generic)

16

17data DbgLevel = NONE | DEBUG | TRACE deriving Eq

18data OutputType = Raw | Object | Executable deriving (Eq, Show, Generic)

src/IRTS/CodegenJavaScript.hs+13−16

@@ -5,44 +5,41 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards #-}

9−{-# LANGUAGE OverloadedStrings #-}

8+{-# LANGUAGE OverloadedStrings, PatternGuards #-}

10module IRTS.CodegenJavaScript (codegenJavaScript

9module IRTS.CodegenJavaScript (codegenJavaScript

11 , codegenNode

10 , codegenNode

12 , JSTarget(..)

11 , JSTarget(..)

13 ) where

12 ) where

14

13

15−import IRTS.JavaScript.AST

16−

17import Idris.AbsSyntax hiding (TypeCase)

14import Idris.AbsSyntax hiding (TypeCase)

15+import Idris.Core.TT

18import IRTS.Bytecode

16import IRTS.Bytecode

19−import IRTS.Lang

17+import IRTS.CodegenCommon

18+import IRTS.Defunctionalise

20import IRTS.Exports

19import IRTS.Exports

20+import IRTS.JavaScript.AST

21+import IRTS.Lang

21import IRTS.Simplified

22import IRTS.Simplified

22−import IRTS.Defunctionalise

23−import IRTS.CodegenCommon

24−import Idris.Core.TT

25import IRTS.System

23import IRTS.System

26import Util.System

24import Util.System

27

25

26+import Control.Applicative (pure, (<$>), (<*>))

28import Control.Arrow

27import Control.Arrow

29import Control.Monad (mapM)

28import Control.Monad (mapM)

30−import Control.Applicative ((<$>), (<*>), pure)

31import Control.Monad.RWS hiding (mapM)

29import Control.Monad.RWS hiding (mapM)

32import Control.Monad.State

30import Control.Monad.State

33import Data.Char

31import Data.Char

34−import Numeric

35import Data.List

32import Data.List

33+import qualified Data.Map.Strict as M

36import Data.Maybe

34import Data.Maybe

37−import Data.Word

35+import qualified Data.Text as T

36+import qualified Data.Text.IO as TIO

38import Data.Traversable hiding (mapM)

37import Data.Traversable hiding (mapM)

39−import System.IO

38+import Data.Word

39+import Numeric

40import System.Directory

41import System.FilePath

42−

42+import System.IO

43−import qualified Data.Map.Strict as M

44−import qualified Data.Text as T

45−import qualified Data.Text.IO as TIO

46

43

47

44

48data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

45data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

src/IRTS/Compiler.hs+28−33

@@ -5,55 +5,50 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}

8+{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}

9

10module IRTS.Compiler(compile, generate) where

11

12−import IRTS.Lang

13−import IRTS.LangOpts

14−import IRTS.Defunctionalise

15−import IRTS.Simplified

16−import IRTS.CodegenCommon

17−import IRTS.CodegenC

18−import IRTS.DumpBC

19−import IRTS.CodegenJavaScript

20−import IRTS.Inliner

21−import IRTS.Exports

22−import IRTS.Portable

23−

24import Idris.AbsSyntax

12import Idris.AbsSyntax

25import Idris.AbsSyntaxTree

13import Idris.AbsSyntaxTree

26import Idris.ASTUtils

14import Idris.ASTUtils

15+import Idris.Core.CaseTree

16+import Idris.Core.Evaluate

17+import Idris.Core.TT

27import Idris.Erasure

18import Idris.Erasure

28import Idris.Error

19import Idris.Error

29import Idris.Output

20import Idris.Output

21+import IRTS.CodegenC

22+import IRTS.CodegenCommon

23+import IRTS.CodegenJavaScript

24+import IRTS.Defunctionalise

25+import IRTS.DumpBC

26+import IRTS.Exports

27+import IRTS.Inliner

28+import IRTS.Lang

29+import IRTS.LangOpts

30+import IRTS.Portable

31+import IRTS.Simplified

30

32

31−import Debug.Trace

32−

33−import Idris.Core.TT

34−import Idris.Core.Evaluate

35−import Idris.Core.CaseTree

36−

37−import Control.Category

38import Prelude hiding (id, (.))

33import Prelude hiding (id, (.))

39

34

40import Control.Applicative

35import Control.Applicative

36+import Control.Category

41import Control.Monad.State

37import Control.Monad.State

42−

43−import Data.Maybe

44−import Data.List

45−import Data.Ord

46−import Data.IntSet (IntSet)

38+import Data.IntSet (IntSet)

47−import qualified Data.IntSet as IS

39+import qualified Data.IntSet as IS

40+import Data.List

48−import qualified Data.Map as M

41+import qualified Data.Map as M

42+import Data.Maybe

43+import Data.Ord

49−import qualified Data.Set as S

44+import qualified Data.Set as S

50−

45+import Debug.Trace

51−import System.Process

52−import System.IO

53−import System.Exit

54import System.Directory

46import System.Directory

55import System.Environment

47import System.Environment

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

48+import System.Exit

49+import System.FilePath (addTrailingPathSeparator, (</>))

50+import System.IO

51+import System.Process

57

52

58-- | Compile to simplified forms and return CodegenInfo

53-- | Compile to simplified forms and return CodegenInfo

59compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

54compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

src/IRTS/Defunctionalise.hs+5−5

@@ -24,15 +24,15 @@ module IRTS.Defunctionalise(module IRTS.Defunctionalise

24 , module IRTS.Lang

25 ) where

26

27−import IRTS.Lang

28−import Idris.Core.TT

29import Idris.Core.CaseTree

27import Idris.Core.CaseTree

28+import Idris.Core.TT

29+import IRTS.Lang

30

31−import Debug.Trace

32−import Data.Maybe

33−import Data.List

34import Control.Monad

31import Control.Monad

35import Control.Monad.State

32import Control.Monad.State

33+import Data.List

34+import Data.Maybe

35+import Debug.Trace

36

37data DExp = DV LVar

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

src/IRTS/DumpBC.hs+2−2

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

7-}

8module IRTS.DumpBC where

9

10+import Idris.Core.TT

11+import IRTS.Bytecode

10import IRTS.Lang

12import IRTS.Lang

11import IRTS.Simplified

13import IRTS.Simplified

12−import Idris.Core.TT

13

14

14−import IRTS.Bytecode

15import Data.List

16

17interMap :: [a] -> [b] -> (a -> [b]) -> [b]

src/IRTS/Exports.hs+1−1

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

9module IRTS.Exports(findExports, getExpNames) where

10

11import Idris.AbsSyntax

12−import Idris.Core.TT

13import Idris.Core.CaseTree

12import Idris.Core.CaseTree

14import Idris.Core.Evaluate

13import Idris.Core.Evaluate

14+import Idris.Core.TT

15import Idris.Error

16import IRTS.Lang

17

src/IRTS/Inliner.hs−1

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

8module IRTS.Inliner where

9

10import Idris.Core.TT

11−

12import IRTS.Defunctionalise

11import IRTS.Defunctionalise

13

12

14inline :: DDefs -> DDefs

13inline :: DDefs -> DDefs

src/IRTS/JavaScript/AST.hs+2−4

@@ -5,14 +5,12 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards #-}

9−{-# LANGUAGE OverloadedStrings #-}

8+{-# LANGUAGE OverloadedStrings, PatternGuards #-}

10module IRTS.JavaScript.AST where

9module IRTS.JavaScript.AST where

11

10

12−import Data.Word

13import Data.Char (isDigit)

11import Data.Char (isDigit)

14−

15import qualified Data.Text as T

12import qualified Data.Text as T

13+import Data.Word

16

14

17data JSType = JSIntTy

15data JSType = JSIntTy

18 | JSStringTy

16 | JSStringTy

src/IRTS/Lang.hs+5−6

@@ -5,16 +5,15 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, DeriveFunctor, DeriveGeneric #-}

8+{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards #-}

9

10module IRTS.Lang where

11

12−import Control.Monad.State hiding (lift)

13−import Control.Applicative hiding (Const)

14−

15−import Idris.Core.TT

16import Idris.Core.CaseTree

12import Idris.Core.CaseTree

13+import Idris.Core.TT

17

14

15+import Control.Applicative hiding (Const)

16+import Control.Monad.State hiding (lift)

18import Data.List

17import Data.List

19import Debug.Trace

18import Debug.Trace

20import GHC.Generics (Generic)

19import GHC.Generics (Generic)

@@ -319,7 +318,7 @@ lsubst n new (LCon lv t cn args) = let args' = map (lsubst n new) args in

319 LCon lv t cn args'

318 LCon lv t cn args'

320lsubst n new (LOp op args) = let args' = map (lsubst n new) args in

319lsubst n new (LOp op args) = let args' = map (lsubst n new) args in

321 LOp op args'

320 LOp op args'

322−lsubst n new (LForeign fd rd args)

321+lsubst n new (LForeign fd rd args)

323 = let args' = map (\(d, a) -> (d, lsubst n new a)) args in

322 = let args' = map (\(d, a) -> (d, lsubst n new a)) args in

324 LForeign fd rd args'

323 LForeign fd rd args'

325lsubst n new (LCase t e alts) = let e' = lsubst n new e

324lsubst n new (LCase t e alts) = let e' = lsubst n new e

src/IRTS/LangOpts.hs+6−6

@@ -5,16 +5,16 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, DeriveFunctor #-}

8+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

9

10module IRTS.LangOpts where

11

12−import Control.Monad.State hiding (lift)

13−import Control.Applicative hiding (Const)

14−

15−import IRTS.Lang

16−import Idris.Core.TT

17import Idris.Core.CaseTree

12import Idris.Core.CaseTree

13+import Idris.Core.TT

14+import IRTS.Lang

15+

16+import Control.Applicative hiding (Const)

17+import Control.Monad.State hiding (lift)

18import Data.List

19import Debug.Trace

20

src/IRTS/Portable.hs+3−5

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

8{-# LANGUAGE OverloadedStrings #-}

9module IRTS.Portable (writePortable) where

10

11−import Data.Aeson

12−import qualified Data.ByteString.Lazy as B

13−import qualified Data.Text as T

14−

15import Idris.Core.CaseTree

11import Idris.Core.CaseTree

16import Idris.Core.TT

12import Idris.Core.TT

17−

18import IRTS.Bytecode

13import IRTS.Bytecode

19import IRTS.CodegenCommon

14import IRTS.CodegenCommon

20import IRTS.Defunctionalise

15import IRTS.Defunctionalise

21import IRTS.Lang

16import IRTS.Lang

22import IRTS.Simplified

17import IRTS.Simplified

23

18

19+import Data.Aeson

20+import qualified Data.ByteString.Lazy as B

21+import qualified Data.Text as T

24import System.IO

22import System.IO

25

23

26data CodegenFile = CGFile {

24data CodegenFile = CGFile {

src/IRTS/Simplified.hs+4−4

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

7-}

8module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where

9

10−import IRTS.Defunctionalise

11−import Idris.Core.TT

12import Idris.Core.CaseTree

10import Idris.Core.CaseTree

11+import Idris.Core.TT

13import Idris.Core.Typecheck

12import Idris.Core.Typecheck

14−import Data.Maybe

13+import IRTS.Defunctionalise

15−import Control.Monad.State

16

14

15+import Control.Monad.State

16+import Data.Maybe

17import Debug.Trace

18

19data SExp = SV LVar

src/IRTS/System.hs+8−8

@@ -19,20 +19,20 @@ module IRTS.System( getDataFileName

19 , version

20 ) where

21

22−import Data.List.Split

23−

24−import Control.Applicative ((<$>))

25−import Data.Maybe (fromMaybe)

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

27−import System.Environment

28−

29#ifdef FREESTANDING

22#ifdef FREESTANDING

30−import Target_idris

31import Paths_idris (version)

23import Paths_idris (version)

24+import Target_idris

32#else

25#else

33import Paths_idris

26import Paths_idris

34#endif

27#endif

35

28

29+import Control.Applicative ((<$>))

30+import Data.List.Split

31+import Data.Maybe (fromMaybe)

32+import System.Environment

33+import System.FilePath (addTrailingPathSeparator, (</>))

34+

35+

36getIdrisDataDir :: IO String

37getIdrisDataDir = do

38 envValue <- lookupEnv "TARGET"

src/Idris/ASTUtils.hs+7−6

@@ -44,15 +44,16 @@ module Idris.ASTUtils(

44 , opts_idrisCmdline, repl_definitions

45 ) where

46

47−import Control.Category

47+import Idris.AbsSyntaxTree

48+import Idris.Core.Evaluate

49+import Idris.Core.TT

50+

51+import Prelude hiding (id, (.))

52+

48import Control.Applicative

53import Control.Applicative

54+import Control.Category

49import Control.Monad.State.Class

55import Control.Monad.State.Class

50import Data.Maybe

56import Data.Maybe

51−import Prelude hiding (id, (.))

52−

53−import Idris.Core.TT

54−import Idris.Core.Evaluate

55−import Idris.AbsSyntaxTree

56

57

57data Field rec fld = Field

58data Field rec fld = Field

58 { fget :: rec -> fld

59 { fget :: rec -> fld

src/Idris/AbsSyntax.hs+17−23

@@ -5,53 +5,47 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

8+{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

9− TypeSynonymInstances, PatternGuards #-}

9+ PatternGuards, TypeSynonymInstances #-}

10

11module Idris.AbsSyntax(

12 module Idris.AbsSyntax

13 , module Idris.AbsSyntaxTree

14 ) where

15

16−import Idris.Core.TT

17−import Idris.Core.Evaluate

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

19−import Idris.Core.Typecheck

20import Idris.AbsSyntaxTree

16import Idris.AbsSyntaxTree

21import Idris.Colours

17import Idris.Colours

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

19+import Idris.Core.Evaluate

20+import Idris.Core.TT

21+import Idris.Core.Typecheck

22import Idris.Docstrings

23import Idris.IdeMode hiding (Opt(..))

24import IRTS.CodegenCommon

25−import Util.DynamicLinker

26

25

27−import System.Console.Haskeline

26+import Util.DynamicLinker

28−import System.IO

27+import Util.Pretty

29−import System.Directory (canonicalizePath, doesFileExist)

28+import Util.ScreenSize

29+import Util.System

30

31import Control.Applicative

32import Control.Monad (liftM3)

33import Control.Monad.State

34−

35−import Data.List hiding (insert,union)

36import Data.Char

34import Data.Char

37−import qualified Data.Text as T

38import Data.Either

35import Data.Either

36+import Data.Generics.Uniplate.Data (descend, descendM)

37+import Data.List hiding (insert, union)

39import qualified Data.Map as M

38import qualified Data.Map as M

40import Data.Maybe

39import Data.Maybe

41import qualified Data.Set as S

40import qualified Data.Set as S

41+import qualified Data.Text as T

42import Data.Word (Word)

43−

44−import Data.Generics.Uniplate.Data (descend, descendM)

45−

46import Debug.Trace

43import Debug.Trace

47−

48−import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

49−

50import Network (PortID(PortNumber))

44import Network (PortID(PortNumber))

51−

45+import System.Console.Haskeline

52−import Util.Pretty

46+import System.Directory (canonicalizePath, doesFileExist)

53−import Util.ScreenSize

47+import System.IO

54−import Util.System

48+import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)

55

49

56getContext :: Idris Context

50getContext :: Idris Context

57getContext = do i <- getIState; return (tt_ctxt i)

51getContext = do i <- getIState; return (tt_ctxt i)

src/Idris/AbsSyntaxTree.hs+21−27

@@ -5,54 +5,48 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

8+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,

9+ FlexibleInstances, MultiParamTypeClasses, PatternGuards,

9− DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,

10+ TypeSynonymInstances #-}

10− PatternGuards #-}

11

12module Idris.AbsSyntaxTree where

13

14−import Idris.Core.TT

14+import Idris.Colours

15−import Idris.Core.Evaluate

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

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

16+import Idris.Core.Evaluate

17+import Idris.Core.TT

17import Idris.Core.Typecheck

18import Idris.Core.Typecheck

18import Idris.Docstrings

19import Idris.Docstrings

19−import IRTS.Lang

20import IRTS.CodegenCommon

21−import Util.Pretty

21+import IRTS.Lang

22import Util.DynamicLinker

23−

23+import Util.Pretty

24−import Idris.Colours

25−

26−import System.Console.Haskeline

27−import System.IO

28

24

29import Prelude hiding ((<$>))

25import Prelude hiding ((<$>))

30

26

31import Control.Applicative ((<|>))

27import Control.Applicative ((<|>))

32−

33−import Control.Monad.Trans.State.Strict

34−import Control.Monad.Trans.Except

35import qualified Control.Monad.Trans.Class as Trans (lift)

28import qualified Control.Monad.Trans.Class as Trans (lift)

36−

29+import Control.Monad.Trans.Except

30+import Control.Monad.Trans.State.Strict

31+import Data.Char

37import Data.Data (Data)

32import Data.Data (Data)

33+import Data.Either

34+import Data.Foldable (Foldable)

38import Data.Function (on)

35import Data.Function (on)

39−import Data.Generics.Uniplate.Data (universe, children)

36+import Data.Generics.Uniplate.Data (children, universe)

40import Data.List hiding (group)

37import Data.List hiding (group)

41−import Data.Char

42import qualified Data.Map.Strict as M

38import qualified Data.Map.Strict as M

43−import qualified Data.Text as T

44−import Data.Either

45−import qualified Data.Set as S

46−import Data.Word (Word)

47import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

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

40+import qualified Data.Set as S

41+import qualified Data.Text as T

48import Data.Traversable (Traversable)

42import Data.Traversable (Traversable)

49import Data.Typeable

43import Data.Typeable

50−import Data.Foldable (Foldable)

44+import Data.Word (Word)

51−import GHC.Generics (Generic)

52−import Network.Socket(PortNumber)

53−

54import Debug.Trace

45import Debug.Trace

55−

46+import GHC.Generics (Generic)

47+import Network.Socket (PortNumber)

48+import System.Console.Haskeline

49+import System.IO

56import Text.PrettyPrint.Annotated.Leijen

50import Text.PrettyPrint.Annotated.Leijen

57

51

58data ElabWhat = ETypes | EDefns | EAll

52data ElabWhat = ETypes | EDefns | EAll

src/Idris/Apropos.hs+5−5

@@ -8,12 +8,12 @@ Maintainer : The Idris Community.

8module Idris.Apropos (apropos, aproposModules) where

9

10import Idris.AbsSyntax

11−import Idris.Core.Evaluate (ctxtAlist, Def(..))

11+import Idris.Core.Evaluate (Def(..), ctxtAlist)

12−import Idris.Core.TT (Name(..), Type, TT(..), NameType(..), Binder(..), Const(..),

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

13− lookupCtxtExact, toAlist)

13+ Type, lookupCtxtExact, toAlist)

14−import Idris.Docstrings (Docstring, DocTerm, containsText)

14+import Idris.Docstrings (DocTerm, Docstring, containsText)

15

16−import Data.List (nub, nubBy, intersperse)

16+import Data.List (intersperse, nub, nubBy)

17import qualified Data.Text as T

18

19-- | Find definitions that are relevant to all space-delimited components of

src/Idris/CaseSplit.hs+15−19

@@ -28,34 +28,30 @@ module Idris.CaseSplit(

28 ) where

29

30import Idris.AbsSyntax

31−import Idris.AbsSyntaxTree (Idris, IState, PTerm)

31+import Idris.AbsSyntaxTree (IState, Idris, PTerm)

32−import Idris.ElabDecls

32+import Idris.Core.Evaluate

33+import Idris.Core.TT

34+import Idris.Core.Typecheck

33import Idris.Delaborate

35import Idris.Delaborate

34−import Idris.Parser

36+import Idris.Elab.Term

35−import Idris.Parser.Helpers

37+import Idris.Elab.Value

38+import Idris.ElabDecls

36import Idris.Error

39import Idris.Error

37import Idris.Output

40import Idris.Output

41+import Idris.Parser

42+import Idris.Parser.Helpers

38

43

39−import Idris.Elab.Value

40−import Idris.Elab.Term

41−

42−import Idris.Core.TT

43−import Idris.Core.Typecheck

44−import Idris.Core.Evaluate

45−

46−import Data.Maybe

47−import Data.Char

48−import Data.List (isPrefixOf, isSuffixOf)

49import Control.Monad

44import Control.Monad

50import Control.Monad.State.Strict

45import Control.Monad.State.Strict

51−

46+import Data.Char

47+import Data.List (isPrefixOf, isSuffixOf)

48+import Data.Maybe

49+import Debug.Trace

50+import Text.Parser.Char (anyChar)

52import Text.Parser.Combinators

51import Text.Parser.Combinators

53−import Text.Parser.Char(anyChar)

54−import Text.Trifecta(Result(..), parseString)

52+import Text.Trifecta (Result(..), parseString)

55import Text.Trifecta.Delta

53import Text.Trifecta.Delta

56

54

57−import Debug.Trace

58−

59-- | Given a variable to split, and a term application, return a list

55-- | Given a variable to split, and a term application, return a list

60-- of variable updates, paired with a flag to say whether the given

56-- of variable updates, paired with a flag to say whether the given

61-- update typechecks (False = impossible) if the flag is 'False' the

57-- update typechecks (False = impossible) if the flag is 'False' the

src/Idris/Chaser.hs+8−9

@@ -11,22 +11,21 @@ module Idris.Chaser(

11 , ModuleTree(..)

12 ) where

13

14−import Idris.Core.TT

15−import Idris.Parser

16import Idris.AbsSyntax

14import Idris.AbsSyntax

17−import Idris.Imports

15+import Idris.Core.TT

18−import Idris.Unlit

19import Idris.Error

16import Idris.Error

20import Idris.IBC

17import Idris.IBC

18+import Idris.Imports

19+import Idris.Parser

20+import Idris.Unlit

21

22−import System.FilePath

23−import System.Directory

24−import Data.Time.Clock

25−import Control.Monad.Trans

26import Control.Monad.State

22import Control.Monad.State

23+import Control.Monad.Trans

27import Data.List

24import Data.List

28−

25+import Data.Time.Clock

29import Debug.Trace

26import Debug.Trace

27+import System.Directory

28+import System.FilePath

30import Util.System (readSource, writeSource)

29import Util.System (readSource, writeSource)

31

30

32data ModuleTree = MTree { mod_path :: IFileType,

31data ModuleTree = MTree { mod_path :: IFileType,

src/Idris/CmdOptions.hs+9−12

@@ -13,27 +13,24 @@ module Idris.CmdOptions

13 , getPkgREPL, getPkgTest, getPort, getIBCSubDir

14 ) where

15

16+import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,

17+ getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,

18+ getPort, opt)

16import Idris.AbsSyntaxTree

19import Idris.AbsSyntaxTree

17−import Idris.AbsSyntax (opt, getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc

18− , getPkgREPL, getPkgTest, getPort, getIBCSubDir)

19−-- import Idris.REPL

20import Idris.Info (getIdrisVersion)

21−

21+-- import Idris.REPL

22import IRTS.CodegenCommon

23

24−import Options.Applicative

25−import Options.Applicative.Arrows

26−import Options.Applicative.Types (ReadM(..))

27import Control.Monad.Trans (lift)

24import Control.Monad.Trans (lift)

28−import Control.Monad.Trans.Reader (ask)

29import Control.Monad.Trans.Except (throwE)

25import Control.Monad.Trans.Except (throwE)

26+import Control.Monad.Trans.Reader (ask)

30import Data.Char

27import Data.Char

31import Data.Maybe

28import Data.Maybe

32−

29+import Options.Applicative

33−import Text.ParserCombinators.ReadP hiding (many, option)

30+import Options.Applicative.Arrows

34−

31+import Options.Applicative.Types (ReadM(..))

35import Safe (lastMay)

32import Safe (lastMay)

36−

33+import Text.ParserCombinators.ReadP hiding (many, option)

37import qualified Text.PrettyPrint.ANSI.Leijen as PP

34import qualified Text.PrettyPrint.ANSI.Leijen as PP

38

35

39runArgParser :: IO [Opt]

36runArgParser :: IO [Opt]

src/Idris/Completion.hs+9−11

@@ -7,28 +7,26 @@ Maintainer : The Idris Community.

7-}

8module Idris.Completion (replCompletion, proverCompletion) where

9

10−import Idris.Core.Evaluate (definitions, ctxtAlist)

11−import Idris.Core.TT

12−

13import Idris.AbsSyntax (runIO)

10import Idris.AbsSyntax (runIO)

14import Idris.AbsSyntaxTree

11import Idris.AbsSyntaxTree

12+import Idris.Colours

13+import Idris.Core.Evaluate (ctxtAlist, definitions)

14+import Idris.Core.TT

15import Idris.Help

16import Idris.Imports (installedPackages)

17−import Idris.Colours

17+import Idris.Parser.Expr (TacticArg(..))

18−import Idris.Parser.Helpers(opChars)

19import qualified Idris.Parser.Expr (constants, tactics)

18import qualified Idris.Parser.Expr (constants, tactics)

20−import Idris.Parser.Expr (TacticArg (..))

19+import Idris.Parser.Helpers (opChars)

21import Idris.REPL.Parser (allHelp, setOptions)

20import Idris.REPL.Parser (allHelp, setOptions)

22−import Control.Monad.State.Strict

23

21

22+import Control.Monad.State.Strict

23+import Data.Char (toLower)

24import Data.List

25−import Data.Maybe

26−import Data.Char(toLower)

27import qualified Data.Map.Strict as Map

25import qualified Data.Map.Strict as Map

26+import Data.Maybe

28import qualified Data.Text as T

27import qualified Data.Text as T

29−

30−import System.Console.Haskeline

31import System.Console.ANSI (Color)

28import System.Console.ANSI (Color)

29+import System.Console.Haskeline

32

30

33commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

31commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

34

32

src/Idris/Core/Binary.hs+5−5

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

8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

9module Idris.Core.Binary where

10

11−import Control.Applicative ((<*>), (<$>))

11+import Idris.Core.TT

12−import Control.Monad (liftM2)

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

14

12

13+import Control.Applicative ((<$>), (<*>))

14+import Control.DeepSeq (($!!))

15+import Control.Monad (liftM2)

15import Data.Binary

16import Data.Binary

16−import Data.Vector.Binary

17import qualified Data.Text as T

18import qualified Data.Text.Encoding as E

19−import Idris.Core.TT

19+import Data.Vector.Binary

20

21instance Binary ErrorReportPart where

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

src/Idris/Core/CaseTree.hs+14−14

@@ -18,8 +18,8 @@ allows casing on arbitrary terms, here we choose to maintain the distinction

18in order to allow for better optimisation opportunities.

19

20-}

21−{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances,

21+{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances

22− DeriveGeneric #-}

22+ #-}

23

24module Idris.Core.CaseTree (

25 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo

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

31import Idris.Core.TT

32

33import Control.Applicative hiding (Const)

34−import Control.Monad.State

35import Control.Monad.Reader

34import Control.Monad.Reader

36−import Data.Maybe

35+import Control.Monad.State

37import Data.List hiding (partition)

36import Data.List hiding (partition)

38−import qualified Data.List(partition)

37+import qualified Data.List (partition)

38+import Data.Maybe

39import Debug.Trace

40import GHC.Generics (Generic)

41

@@ -169,9 +169,9 @@ findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where

169 | otherwise = [(n, [])] -- tmp

170 nut ps fn@(App _ f a)

171 | (P _ n _, args) <- unApply fn

172− = if ignoreasserts && n == sUN "assert_total"

172+ = if ignoreasserts && n == sUN "assert_total"

173 then []

174− else if n `elem` ps

174+ else if n `elem` ps

175 then nut ps f ++ nut ps a

176 else [(n, map argNames args)] ++ concatMap (nut ps) args

177 | (P (TCon _ _) n _, _) <- unApply fn = []

@@ -249,7 +249,7 @@ data Phase = CompileTime | RunTime

249-- Work Right to Left

250

251simpleCase :: Bool -> SC -> Bool ->

252− Phase -> FC -> [Int] ->

252+ Phase -> FC -> [Int] ->

253 [(Type, Bool)] -> -- (Argument type, whether it's canonical)

254 [([Name], Term, Term)] ->

255 ErasureInfo ->

@@ -431,12 +431,12 @@ partition xs = error $ "Partition " ++ show xs

431-- The first argument means [(Name, IsInaccessible)].

432

433order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])

434−-- do nothing at compile time: FIXME (EB): Put this in after checking

434+-- do nothing at compile time: FIXME (EB): Put this in after checking

435-- implications for Franck's reflection work... see issue 3233

436−-- order CompileTime ns cs _ = (map fst ns, cs)

436+-- order CompileTime ns cs _ = (map fst ns, cs)

437order _ [] cs cans = ([], cs)

438order _ ns' [] cans = (map fst ns', [])

439−order phase ns' cs cans

439+order phase ns' cs cans

440 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))

441 -- only sort the arguments where there is no clash in

442 -- constructor tags between families, the argument type is canonical,

@@ -444,7 +444,7 @@ order phase ns' cs cans

444 -- clash, because otherwise we can't reliable make the

445 -- case distinction on evaluation

446 (patnames_ord, patnames_rest)

447− = Data.List.partition (noClash . map snd) patnames

447+ = Data.List.partition (noClash . map snd) patnames

448 patnames_ord' = case phase of

449 CompileTime -> patnames_ord

450 -- reversing tends to make better case trees

@@ -460,7 +460,7 @@ order phase ns' cs cans

460 rebuild patnames clause = (map (snd . snd) patnames, snd clause)

461

462 noClash [] = True

463− noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))

463+ noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))

464 && noClash ps

465

466 clashPat (PCon _ _ _ _) (PConst _) = True

@@ -471,7 +471,7 @@ order phase ns' cs cans

471 clashPat _ _ = False

472

473 -- this compares (+isInaccessible, -numberOfCases)

474− moreDistinct xs ys

474+ moreDistinct xs ys

475 = compare (snd . fst . head $ xs, numNames [] (map snd ys))

476 (snd . fst . head $ ys, numNames [] (map snd xs))

477

src/Idris/Core/Constraints.hs+3−3

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

7-}

8module Idris.Core.Constraints ( ucheck ) where

9

10−import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),

11− ConstraintFC(..), Err'(..) )

10+import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),

11+ UConstraint(..), UExp(..))

12

13import Control.Applicative

14import Control.Monad.State.Strict

15−import Data.List ( partition )

15+import Data.List (partition)

16import qualified Data.Map.Strict as M

17import qualified Data.Set as S

18import Debug.Trace

src/Idris/Core/DeepSeq.hs+1−1

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

10

11module Idris.Core.DeepSeq where

12

13−import Idris.Core.TT

14import Idris.Core.CaseTree

13import Idris.Core.CaseTree

15import Idris.Core.Evaluate

14import Idris.Core.Evaluate

15+import Idris.Core.TT

16

17import Control.DeepSeq

18

src/Idris/Core/Elaborate.hs+7−7

@@ -10,20 +10,22 @@ because this gives us a language to build derived tactics out of the

10primitives.

11-}

12

13−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

13+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}

14module Idris.Core.Elaborate (

15 module Idris.Core.Elaborate

16 , module Idris.Core.ProofState

17 ) where

18

19+import Idris.Core.DeepSeq

20+import Idris.Core.Evaluate

19import Idris.Core.ProofState

21import Idris.Core.ProofState

20−import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,

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

21− refocus)

23+ refocus)

22import Idris.Core.TT

24import Idris.Core.TT

23−import Idris.Core.Evaluate

24import Idris.Core.Typecheck

25import Idris.Core.Typecheck

25import Idris.Core.Unify

26import Idris.Core.Unify

26−import Idris.Core.DeepSeq

27+

28+import Util.Pretty hiding (fill)

27

29

28import Control.DeepSeq

30import Control.DeepSeq

29import Control.Monad.State.Strict

31import Control.Monad.State.Strict

@@ -31,8 +33,6 @@ import Data.Char

31import Data.List

33import Data.List

32import Debug.Trace

34import Debug.Trace

33

35

34−import Util.Pretty hiding (fill)

35−

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

37 deriving Show

38

src/Idris/Core/Evaluate.hs+11−11

@@ -5,8 +5,8 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,

8+{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

9− PatternGuards, DeriveGeneric #-}

9+ MultiParamTypeClasses, PatternGuards #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11

12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

@@ -21,22 +21,22 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

21 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

22 mapDefCtxt,

23 lookupTotal, lookupTotalExact, lookupInjectiveExact,

24− lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

24+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

25 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

26 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

27 isUniverse) where

28

29−import Debug.Trace

29+import Idris.Core.CaseTree

30+import Idris.Core.TT

31+

30import Control.Applicative hiding (Const)

32import Control.Applicative hiding (Const)

31−import Control.Monad.State -- not Strict!

33+import Control.Monad.State

32−import qualified Data.Binary as B

33import Data.Binary hiding (get, put)

34import Data.Binary hiding (get, put)

35+import qualified Data.Binary as B

34import Data.Maybe (listToMaybe)

36import Data.Maybe (listToMaybe)

37+import Debug.Trace

35import GHC.Generics (Generic)

38import GHC.Generics (Generic)

36

39

37−import Idris.Core.TT

38−import Idris.Core.CaseTree

39−

40data EvalState = ES { limited :: [(Name, Int)],

41 nexthole :: Int,

42 blocking :: Bool }

@@ -687,7 +687,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

687 caseeq ((x,y):ps) xdef ydef

688 _ -> return False

689

690− sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->

690+ sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->

691 StateT UCs TC Bool

692 sameCase ps x y xargs yargs

693 = case (lookupDef x ctxt, lookupDef y ctxt) of

@@ -697,7 +697,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

697 [CaseOp _ _ _ _ _ yd])

698 -> let (xin, xdef) = cases_compiletime xd

699 (yin, ydef) = cases_compiletime yd in

700− do liftM2 (&&)

700+ do liftM2 (&&)

701 (do ok <- zipWithM (ceq ps)

702 (drop (length xin) xargs)

703 (drop (length yin) yargs)

src/Idris/Core/Execute.hs+13−18

@@ -6,48 +6,43 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8

9−{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}

9+{-# LANGUAGE CPP, ExistentialQuantification, PatternGuards #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11module Idris.Core.Execute (execute) where

12

13import Idris.AbsSyntax

14import Idris.AbsSyntaxTree

15−import IRTS.Lang(FDesc(..), FType(..))

16−

17−import Idris.Primitives(Prim(..), primitives)

18−

19−import Idris.Core.TT

20−import Idris.Core.Evaluate

21import Idris.Core.CaseTree

15import Idris.Core.CaseTree

22−

16+import Idris.Core.Evaluate

17+import Idris.Core.TT

23import Idris.Error

18import Idris.Error

24−

19+import Idris.Primitives (Prim(..), primitives)

25−import Debug.Trace

20+import IRTS.Lang (FDesc(..), FType(..))

26

21

27import Util.DynamicLinker

22import Util.DynamicLinker

28import Util.System

23import Util.System

29

24

30import Control.Applicative hiding (Const)

25import Control.Applicative hiding (Const)

31import Control.Exception

26import Control.Exception

27+import Control.Monad hiding (forM)

32import Control.Monad.Trans

28import Control.Monad.Trans

33−import Control.Monad.Trans.State.Strict

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

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

35−import Control.Monad hiding (forM)

30+import Control.Monad.Trans.State.Strict

36−import Data.Maybe

37import Data.Bits

31import Data.Bits

38−import Data.Traversable (forM)

39−import Data.Time.Clock.POSIX (getPOSIXTime)

40import qualified Data.Map as M

32import qualified Data.Map as M

33+import Data.Maybe

34+import Data.Time.Clock.POSIX (getPOSIXTime)

35+import Data.Traversable (forM)

36+import Debug.Trace

37+import System.IO

41

38

42#ifdef IDRIS_FFI

39#ifdef IDRIS_FFI

43−import Foreign.LibFFI

44import Foreign.C.String

40import Foreign.C.String

41+import Foreign.LibFFI

45import Foreign.Marshal.Alloc (free)

42import Foreign.Marshal.Alloc (free)

46import Foreign.Ptr

43import Foreign.Ptr

47#endif

44#endif

48

45

49−import System.IO

50−

51#ifndef IDRIS_FFI

46#ifndef IDRIS_FFI

52execute :: Term -> Idris Term

47execute :: Term -> Idris Term

53execute tm = fail "libffi not supported, rebuild Idris with -f FFI"

48execute tm = fail "libffi not supported, rebuild Idris with -f FFI"

src/Idris/Core/ProofState.hs+6−6

@@ -10,7 +10,7 @@ proofs, and some high level commands for introducing new theorems,

10evaluation/checking inside the proof system, etc.

11-}

12

13−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

13+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}

14module Idris.Core.ProofState(

15 ProofState(..), newProof, envAtFocus, goalAtFocus

16 , Tactic(..), Goal(..), processTactic, nowElaboratingPS

@@ -18,20 +18,20 @@ module Idris.Core.ProofState(

18 , keepGiven, getProvenance

19 ) where

20

21−import Idris.Core.Typecheck

22import Idris.Core.Evaluate

21import Idris.Core.Evaluate

22+import Idris.Core.ProofTerm

23import Idris.Core.TT

24+import Idris.Core.Typecheck

24import Idris.Core.Unify

25import Idris.Core.Unify

25−import Idris.Core.ProofTerm

26

27−import Control.Monad.State.Strict

27+import Util.Pretty hiding (fill)

28+

28import Control.Applicative hiding (empty)

29import Control.Applicative hiding (empty)

29import Control.Arrow ((***))

30import Control.Arrow ((***))

31+import Control.Monad.State.Strict

30import Data.List

32import Data.List

31import Debug.Trace

33import Debug.Trace

32

34

33−import Util.Pretty hiding (fill)

34−

35data ProofState = PS { thname :: Name,

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

37 usedns :: [Name], -- ^ used names, don't use again

src/Idris/Core/ProofTerm.hs+2−2

@@ -6,7 +6,7 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8

9−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

9+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}

10module Idris.Core.ProofTerm(

11 ProofTerm, Goal(..), mkProofTerm, getProofTerm

12 , resetProofTerm

@@ -16,9 +16,9 @@ module Idris.Core.ProofTerm(

16 , goal, atHole

17 ) where

18

19−import Idris.Core.Typecheck

20import Idris.Core.Evaluate

19import Idris.Core.Evaluate

21import Idris.Core.TT

20import Idris.Core.TT

21+import Idris.Core.Typecheck

22

23import Control.Monad.State.Strict

24import Data.List

src/Idris/Core/TT.hs+24−25

@@ -22,8 +22,8 @@ TT is the core language of Idris. The language has:

22 * We have a simple collection of tactics which we use to elaborate source

23 programs with implicit syntax into fully explicit terms.

24-}

25−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,

25+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,

26− DeriveDataTypeable, DeriveGeneric, PatternGuards #-}

26+ FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-}

27{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

28module Idris.Core.TT(

29 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

@@ -51,40 +51,39 @@ module Idris.Core.TT(

51 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

52 ) where

53

54+import Util.Pretty hiding (Str)

55+

54-- Work around AMP without CPP

56-- Work around AMP without CPP

55−import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,

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

56− Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),

58+ Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),

57− Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, flip,

59+ Read(..), Show(..), String, div, error, flip, fst, mod, not,

58− fst, snd, not, mod, read, otherwise)

60+ otherwise, read, snd, ($), (&&), (.), (||))

59

61

60−import Control.Applicative (Applicative (..), Alternative)

62+import Control.Applicative (Alternative, Applicative(..))

61−import qualified Control.Applicative as A (Alternative (..))

63+import qualified Control.Applicative as A (Alternative(..))

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

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

63import Control.Monad.State.Strict

65import Control.Monad.State.Strict

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

66+import Control.Monad.Trans.Except (Except(..))

65−import Debug.Trace

67+import Data.Binary hiding (get, put)

66−import qualified Data.Map.Strict as Map

68+import qualified Data.Binary as B

67import Data.Char

69import Data.Char

68import Data.Data (Data)

70import Data.Data (Data)

69−import Data.Monoid (mconcat)

71+import Data.Foldable (Foldable)

70−import Numeric (showIntAtBase)

71−import qualified Data.Text as T

72import Data.List hiding (group, insert)

73−import Data.Set(Set, member, fromList, insert)

73+import qualified Data.Map.Strict as Map

74import Data.Maybe (listToMaybe)

75−import Data.Foldable (Foldable)

75+import Data.Monoid (mconcat)

76+import Data.Set (Set, fromList, insert, member)

77+import qualified Data.Text as T

76import Data.Traversable (Traversable)

78import Data.Traversable (Traversable)

77import Data.Typeable (Typeable)

79import Data.Typeable (Typeable)

78import Data.Vector.Unboxed (Vector)

80import Data.Vector.Unboxed (Vector)

79import qualified Data.Vector.Unboxed as V

81import qualified Data.Vector.Unboxed as V

80−import qualified Data.Binary as B

82+import Debug.Trace

81−import Data.Binary hiding (get, put)

82import Foreign.Storable (sizeOf)

83import Foreign.Storable (sizeOf)

83import GHC.Generics (Generic)

84import GHC.Generics (Generic)

84−

85+import Numeric (showIntAtBase)

85−import Numeric.IEEE (IEEE (identicalIEEE))

86+import Numeric.IEEE (IEEE(identicalIEEE))

86−

87−import Util.Pretty hiding (Str)

88

87

89data Option = TTypeInTType

88data Option = TTypeInTType

90 | CheckConv

89 | CheckConv

@@ -941,7 +940,7 @@ instance Sized UExp where

941 size _ = 1

940 size _ = 1

942

941

943instance Show UExp where

942instance Show UExp where

944− show (UVar ns x)

943+ show (UVar ns x)

945 | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]

944 | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]

946 | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

945 | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

947 show (UVal x) = show x

946 show (UVal x) = show x

@@ -1289,7 +1288,7 @@ substTerm old new = st where

1289 st (Bind x b sc) = Bind x (fmap st b) (st sc)

1288 st (Bind x b sc) = Bind x (fmap st b) (st sc)

1290 st t = t

1289 st t = t

1291

1290

1292− eqAlpha as (P _ x _) (P _ y _)

1291+ eqAlpha as (P _ x _) (P _ y _)

1293 = x == y || (x, y) `elem` as || (y, x) `elem` as

1292 = x == y || (x, y) `elem` as || (y, x) `elem` as

1294 eqAlpha as (V x) (V y) = x == y

1293 eqAlpha as (V x) (V y) = x == y

1295 eqAlpha as (Bind x xb xs) (Bind y yb ys)

1294 eqAlpha as (Bind x xb xs) (Bind y yb ys)

@@ -1301,7 +1300,7 @@ substTerm old new = st where

1301 = eqAlpha as xt yt && eqAlpha as xv yv

1300 = eqAlpha as xt yt && eqAlpha as xv yv

1302 eqAlphaB as (Guess xt xv) (Guess yt yv)

1301 eqAlphaB as (Guess xt xv) (Guess yt yv)

1303 = eqAlpha as xt yt && eqAlpha as xv yv

1302 = eqAlpha as xt yt && eqAlpha as xv yv

1304− eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)

1303+ eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)

1305

1304

1306-- | Return number of occurrences of V 0 or bound name i the term

1305-- | Return number of occurrences of V 0 or bound name i the term

1307occurrences :: Eq n => n -> TT n -> Int

1306occurrences :: Eq n => n -> TT n -> Int

src/Idris/Core/Typecheck.hs+7−7

@@ -6,17 +6,17 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8

9−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

9+{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

10 PatternGuards #-}

11

12module Idris.Core.Typecheck where

13

14+import Idris.Core.Evaluate

15+import Idris.Core.TT

16+

14import Control.Monad.State

17import Control.Monad.State

15−import Debug.Trace

16import qualified Data.Vector.Unboxed as V (length)

18import qualified Data.Vector.Unboxed as V (length)

17−

19+import Debug.Trace

18−import Idris.Core.TT

19−import Idris.Core.Evaluate

20

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

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

@@ -83,7 +83,7 @@ recheck_borrowing uniq_check bs tcns ctxt env tm orig

83check :: Context -> Env -> Raw -> TC (Term, Type)

84check ctxt env tm

85 -- Holes allowed, so constraint namespace doesn't matter

86− = evalStateT (check' True [] ctxt env tm) (0, [])

86+ = evalStateT (check' True [] ctxt env tm) (0, [])

87

88check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

89check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top where

@@ -343,7 +343,7 @@ checkUnique borrowed ctxt env tm

343 StateT [(Name, (UniqueUse, Universe))] TC ()

344 chkBinderName env n b

345 = do let rawty = forgetEnv (map fst env) (binderTy b)

346− (_, kind) <- lift $ check ctxt env rawty

346+ (_, kind) <- lift $ check ctxt env rawty

347 case kind of

348 UType UniqueType -> do ns <- get

349 if n `elem` borrowed

src/Idris/Core/Unify.hs+2−2

@@ -19,13 +19,13 @@ module Idris.Core.Unify(

19 , unrecoverable

20 ) where

21

22−import Idris.Core.TT

23import Idris.Core.Evaluate

22import Idris.Core.Evaluate

23+import Idris.Core.TT

24

25import Control.Monad

26import Control.Monad.State.Strict

27−import Data.Maybe

28import Data.List

27import Data.List

28+import Data.Maybe

29import Debug.Trace

30

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

src/Idris/Core/WHNF.hs+1−1

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

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11module Idris.Core.WHNF(whnf, WEnv) where

12

13−import Idris.Core.TT

14import Idris.Core.CaseTree

13import Idris.Core.CaseTree

15import Idris.Core.Evaluate hiding (quote)

14import Idris.Core.Evaluate hiding (quote)

16import qualified Idris.Core.Evaluate as Evaluate

15import qualified Idris.Core.Evaluate as Evaluate

16+import Idris.Core.TT

17

18import Debug.Trace

19

src/Idris/Coverage.hs+7−9

@@ -8,23 +8,21 @@ Maintainer : The Idris Community.

8{-# LANGUAGE PatternGuards #-}

9module Idris.Coverage where

10

11−import Idris.Core.TT

12−import Idris.Core.Evaluate

13−import Idris.Core.CaseTree

14−

15import Idris.AbsSyntax

11import Idris.AbsSyntax

12+import Idris.Core.CaseTree

13+import Idris.Core.Evaluate

14+import Idris.Core.TT

16import Idris.Delaborate

15import Idris.Delaborate

17import Idris.Error

16import Idris.Error

18import Idris.Output (iWarn, iputStrLn)

17import Idris.Output (iWarn, iputStrLn)

19

18

19+import Control.Monad.State.Strict

20import Data.Char

21−import Data.List

22import Data.Either

21import Data.Either

22+import Data.List

23import Data.Maybe

24import Debug.Trace

25

26−import Control.Monad.State.Strict

27−

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

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

29--

27--

30-- We need this to eliminate the pattern clauses which have been

28-- We need this to eliminate the pattern clauses which have been

@@ -213,7 +211,7 @@ genAll i (addPH, args)

213

211

214 -- Merge patterns with placeholders in other patterns, to ensure we've

212 -- Merge patterns with placeholders in other patterns, to ensure we've

215 -- covered all possible generated cases

213 -- covered all possible generated cases

216− -- e.g. if we have (True, _) (False, _) (_, True) (_, False)

214+ -- e.g. if we have (True, _) (False, _) (_, True) (_, False)

217 -- we should merge these to get (True, True), (False, False)

215 -- we should merge these to get (True, True), (False, False)

218 -- (False, True) and (True, False)

216 -- (False, True) and (True, False)

219 mergePHs :: [PTerm] -> [PTerm]

217 mergePHs :: [PTerm] -> [PTerm]

@@ -224,7 +222,7 @@ genAll i (addPH, args)

224

222

225 mergePH :: PTerm -> [PTerm] -> [PTerm]

223 mergePH :: PTerm -> [PTerm] -> [PTerm]

226 mergePH tm [] = []

224 mergePH tm [] = []

227− mergePH tm (x : xs)

225+ mergePH tm (x : xs)

228 | Just merged <- mergePTerm tm x = merged : mergePH tm xs

226 | Just merged <- mergePTerm tm x = merged : mergePH tm xs

229 | otherwise = mergePH tm xs

227 | otherwise = mergePH tm xs

230

228

src/Idris/DSL.hs+2−4

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

10

11module Idris.DSL where

12

13−import Data.Generics.Uniplate.Data (transform)

14−

15import Idris.AbsSyntax

13import Idris.AbsSyntax

16−

17−import Idris.Core.TT

18import Idris.Core.Evaluate

14import Idris.Core.Evaluate

15+import Idris.Core.TT

19

16

20import Control.Monad.State.Strict

17import Control.Monad.State.Strict

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

21import Debug.Trace

19import Debug.Trace

22

20

23debindApp :: SyntaxInfo -> PTerm -> PTerm

21debindApp :: SyntaxInfo -> PTerm -> PTerm

src/Idris/DeepSeq.hs+8−8

@@ -12,20 +12,20 @@ module Idris.DeepSeq(

12 , module Idris.Core.DeepSeq

13 ) where

14

15−import Idris.Core.DeepSeq

16−import Idris.Docstrings

17−import Idris.Core.TT

18import Idris.AbsSyntaxTree

15import Idris.AbsSyntaxTree

19import Idris.Colours

16import Idris.Colours

17+import Idris.Core.DeepSeq

18+import Idris.Core.TT

19+import Idris.Docstrings

20+import qualified Idris.Docstrings as D

21+import IRTS.CodegenCommon (OutputType(..))

20import IRTS.Lang (PrimFn(..))

22import IRTS.Lang (PrimFn(..))

21−import IRTS.CodegenCommon (OutputType (..))

22−import Util.DynamicLinker

23

24−import Control.DeepSeq

24+import Util.DynamicLinker

25−import Network.Socket(PortNumber)

26

25

27import qualified Cheapskate.Types as CT

26import qualified Cheapskate.Types as CT

28−import qualified Idris.Docstrings as D

27+import Control.DeepSeq

28+import Network.Socket (PortNumber)

29

30-- These types don't have Generic instances

31instance NFData CT.Options where

src/Idris/Delaborate.hs+11−12

@@ -13,23 +13,22 @@ module Idris.Delaborate (

13 , pprintDelabTy, pprintErr, resugar

14 ) where

15

16−import Util.Pretty

17−

18import Idris.AbsSyntax

16import Idris.AbsSyntax

19−import Idris.Core.TT

20import Idris.Core.Evaluate

17import Idris.Core.Evaluate

18+import Idris.Core.TT

21−import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

19+import Idris.Docstrings (overview, renderDocTerm, renderDocstring)

22import Idris.ErrReverse

20import Idris.ErrReverse

23

21

22+import Util.Pretty

23+

24import Prelude hiding ((<$>))

25

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

27+import Control.Monad.State

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

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

27−import Data.Maybe (mapMaybe)

28import Data.List (intersperse, nub)

29import Data.List (intersperse, nub)

30+import Data.Maybe (mapMaybe)

29import qualified Data.Text as T

31import qualified Data.Text as T

30−import Control.Applicative (Alternative((<|>)))

31−import Control.Monad.State

32−

33import Debug.Trace

32import Debug.Trace

34

33

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

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

@@ -81,10 +80,10 @@ delabSugared ist tm = resugar ist $ delab ist tm

81

80

82-- | Delaborate a term without resugaring

81-- | Delaborate a term without resugaring

83delab :: IState -> Term -> PTerm

82delab :: IState -> Term -> PTerm

84−delab i tm = delab' i tm False False

83+delab i tm = delab' i tm False False

85

84

86delabMV :: IState -> Term -> PTerm

85delabMV :: IState -> Term -> PTerm

87−delabMV i tm = delab' i tm False True

86+delabMV i tm = delab' i tm False True

88

87

89-- | Delaborate a term directly, leaving case applications as they are.

88-- | Delaborate a term directly, leaving case applications as they are.

90-- We need this for interactive case splitting, where we need access to the

89-- We need this for interactive case splitting, where we need access to the

@@ -112,7 +111,7 @@ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

112delabTy' ist imps tm fullname mvs docases = de [] imps tm

111delabTy' ist imps tm fullname mvs docases = de [] imps tm

113 where

112 where

114 un = fileFC "(val)"

113 un = fileFC "(val)"

115−

114+

116 -- Special case for spotting applications of case functions

115 -- Special case for spotting applications of case functions

117 -- (Normally the scrutinee is let-bound, but hole types get normalised,

116 -- (Normally the scrutinee is let-bound, but hole types get normalised,

118 -- so they could appear in this form. The scrutinee is always added as

117 -- so they could appear in this form. The scrutinee is always added as

@@ -123,7 +122,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

123 | docases

122 | docases

124 , isCaseApp sc

123 , isCaseApp sc

125 , (P _ cOp _, args@(_:_)) <- unApply sc

124 , (P _ cOp _, args@(_:_)) <- unApply sc

126− , Just caseblock <- delabCase env imps (last args) cOp args

125+ , Just caseblock <- delabCase env imps (last args) cOp args

127 = caseblock

126 = caseblock

128

127

129 de env _ (App _ f a) = deFn env f [a]

128 de env _ (App _ f a) = deFn env f [a]

src/Idris/Directives.hs+2−3

@@ -9,11 +9,10 @@ module Idris.Directives(directiveAction) where

9

10import Idris.AbsSyntax

11import Idris.ASTUtils

12−import Idris.Imports

13−import Idris.Output (sendHighlighting)

14−

15import Idris.Core.Evaluate

12import Idris.Core.Evaluate

16import Idris.Core.TT

13import Idris.Core.TT

14+import Idris.Imports

15+import Idris.Output (sendHighlighting)

17

16

18import Util.DynamicLinker

17import Util.DynamicLinker

19

18

src/Idris/Docs.hs+7−6

@@ -5,7 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}

8+{-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10module Idris.Docs (

11 pprintDocs

@@ -15,19 +15,20 @@ module Idris.Docs (

15

16import Idris.AbsSyntax

17import Idris.AbsSyntaxTree

18−import Idris.Delaborate

19−import Idris.Core.TT

20import Idris.Core.Evaluate

18import Idris.Core.Evaluate

19+import Idris.Core.TT

20+import Idris.Delaborate

21−import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)

21+import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,

22+ nullDocstring, overview, renderDocTerm,

23+ renderDocstring)

22

24

23import Util.Pretty

25import Util.Pretty

24

26

25import Prelude hiding ((<$>))

27import Prelude hiding ((<$>))

26

28

27import Control.Arrow (first)

29import Control.Arrow (first)

28−

29−import Data.Maybe

30import Data.List

31+import Data.Maybe

31import qualified Data.Text as T

32import qualified Data.Text as T

32

33

33-- TODO: Only include names with public/export accessibility

34-- TODO: Only include names with public/export accessibility

src/Idris/Docstrings.hs+7−10

@@ -14,24 +14,21 @@ module Idris.Docstrings (

14 , renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring

15 ) where

16

17−import qualified Cheapskate as C

17+import Idris.Core.TT (Err, Name, OutputAnnotation(..), Term, TextFormatting(..))

18−import qualified Cheapskate.Types as CT

19−import Cheapskate.Html (renderDoc)

20

18

21import Util.Pretty

19import Util.Pretty

22

20

23−import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)

24−

25import Prelude hiding ((<$>))

21import Prelude hiding ((<$>))

26

22

27−import qualified Data.Text as T

23+import qualified Cheapskate as C

24+import Cheapskate.Html (renderDoc)

28−import qualified Data.Foldable as F

25+import qualified Cheapskate.Types as CT

29import Data.Foldable (Foldable)

26import Data.Foldable (Foldable)

30−import Data.Traversable (Traversable)

27+import qualified Data.Foldable as F

31import qualified Data.Sequence as S

28import qualified Data.Sequence as S

32−

29+import qualified Data.Text as T

30+import Data.Traversable (Traversable)

33import GHC.Generics (Generic)

31import GHC.Generics (Generic)

34−

35import Text.Blaze.Html (Html)

32import Text.Blaze.Html (Html)

36

33

37-- | The various kinds of code samples that can be embedded in docs

34-- | The various kinds of code samples that can be embedded in docs

src/Idris/Elab/AsPat.hs+1−2

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

7-}

8module Idris.Elab.AsPat(desugarAs) where

9

10−import Idris.Core.TT

11import Idris.AbsSyntax

10import Idris.AbsSyntax

11+import Idris.Core.TT

12

13import Control.Applicative

14import Control.Monad.State.Strict

15−

16import Data.Generics.Uniplate.Data (transformM)

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

17

16

18-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

17-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

src/Idris/Elab/Clause.hs+29−34

@@ -10,58 +10,53 @@ module Idris.Elab.Clause where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13+import Idris.Core.CaseTree

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

15+import Idris.Core.Evaluate

16+import Idris.Core.Execute

17+import Idris.Core.TT

18+import Idris.Core.Typecheck

19+import Idris.Coverage

20+import Idris.DataOpts

21+import Idris.DeepSeq

22+import Idris.Delaborate

23+import Idris.Docstrings hiding (Unchecked)

13import Idris.DSL

24import Idris.DSL

25+import Idris.Elab.AsPat

26+import Idris.Elab.Term

27+import Idris.Elab.Transform

28+import Idris.Elab.Type

29+import Idris.Elab.Utils

14import Idris.Error

30import Idris.Error

15−import Idris.Delaborate

16import Idris.Imports

31import Idris.Imports

17−import Idris.Elab.Term

18−import Idris.Coverage

19−import Idris.DataOpts

20−import Idris.Providers

21−import Idris.Primitives

22import Idris.Inliner

32import Idris.Inliner

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

23import Idris.PartialEval

34import Idris.PartialEval

35+import Idris.Primitives

36+import Idris.Providers

24import Idris.Transforms

37import Idris.Transforms

25−import Idris.DeepSeq

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

27import IRTS.Lang

38import IRTS.Lang

28

39

29−import Idris.Elab.AsPat

30−import Idris.Elab.Type

31−import Idris.Elab.Transform

32−import Idris.Elab.Utils

33−

34−import Idris.Core.TT

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

36−import Idris.Core.Evaluate

37−import Idris.Core.Execute

38−import Idris.Core.Typecheck

39−import Idris.Core.CaseTree

40−

41−import Idris.Docstrings hiding (Unchecked)

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

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

41+import Util.Pretty (pretty, text)

43

42

44import Prelude hiding (id, (.))

43import Prelude hiding (id, (.))

45−import Control.Category

46

44

47import Control.Applicative hiding (Const)

45import Control.Applicative hiding (Const)

46+import Control.Category

48import Control.DeepSeq

47import Control.DeepSeq

49import Control.Monad

48import Control.Monad

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

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

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

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

51+import Data.Char (isLetter, toLower)

52import Data.List

53−import Data.Maybe

53+import Data.List.Split (splitOn)

54−import Data.Word

55−

56−import Debug.Trace

57−

58import qualified Data.Map as Map

54import qualified Data.Map as Map

55+import Data.Maybe

59import qualified Data.Set as S

56import qualified Data.Set as S

60import qualified Data.Text as T

57import qualified Data.Text as T

61−import Data.Char(isLetter, toLower)

58+import Data.Word

62−import Data.List.Split (splitOn)

59+import Debug.Trace

63−

64−import Util.Pretty(pretty, text)

65import Numeric

60import Numeric

66

61

67-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

62-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

@@ -404,7 +399,7 @@ elabPE info fc caller r =

404 let opts = [Specialise ((if pe_simple specdecl

399 let opts = [Specialise ((if pe_simple specdecl

405 then map (\x -> (x, Nothing)) cgns'

400 then map (\x -> (x, Nothing)) cgns'

406 else []) ++

401 else []) ++

407− (n, Just maxred) : specnames ++

402+ (n, Just maxred) : specnames ++

408 concat descs)]

403 concat descs)]

409 logElab 3 $ "Specialising application: " ++ show specapp

404 logElab 3 $ "Specialising application: " ++ show specapp

410 ++ " in " ++ show caller ++

405 ++ " in " ++ show caller ++

@@ -454,7 +449,7 @@ elabPE info fc caller r =

454 i <- getIState

449 i <- getIState

455 let statics = filter (staticFn i) ns

450 let statics = filter (staticFn i) ns

456 return (map (\n -> (n, Nothing)) statics)

451 return (map (\n -> (n, Nothing)) statics)

457−

452+

458 staticFn :: IState -> Name -> Bool

453 staticFn :: IState -> Name -> Bool

459 staticFn i n = case lookupCtxt n (idris_flags i) of

454 staticFn i n = case lookupCtxt n (idris_flags i) of

460 [opts] -> elem StaticFn opts

455 [opts] -> elem StaticFn opts

src/Idris/Elab/Data.hs+26−30

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

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13−import Idris.DSL

13+import Idris.Core.CaseTree

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

14−import Idris.Error

15+import Idris.Core.Evaluate

15−import Idris.Delaborate

16+import Idris.Core.Execute

16−import Idris.Imports

17+import Idris.Core.TT

17−import Idris.Elab.Term

18+import Idris.Core.Typecheck

18import Idris.Coverage

19import Idris.Coverage

19import Idris.DataOpts

20import Idris.DataOpts

20−import Idris.Providers

21−import Idris.Primitives

22−import Idris.Inliner

23−import Idris.PartialEval

24import Idris.DeepSeq

21import Idris.DeepSeq

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

22+import Idris.Delaborate

26−import IRTS.Lang

23+import Idris.Docstrings

27−

24+import Idris.DSL

25+import Idris.Elab.Rewrite

26+import Idris.Elab.Term

28import Idris.Elab.Type

27import Idris.Elab.Type

29import Idris.Elab.Utils

28import Idris.Elab.Utils

30−import Idris.Elab.Rewrite

31import Idris.Elab.Value

29import Idris.Elab.Value

30+import 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

32

38

33−import Idris.Core.TT

39+import Util.Pretty

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

35−import Idris.Core.Evaluate

36−import Idris.Core.Execute

37−import Idris.Core.Typecheck

38−import Idris.Core.CaseTree

39−

40−import Idris.Docstrings

41

40

42import Prelude hiding (id, (.))

41import Prelude hiding (id, (.))

43−import Control.Category

44

42

45import Control.Applicative hiding (Const)

43import Control.Applicative hiding (Const)

44+import Control.Category

46import Control.DeepSeq

45import Control.DeepSeq

47import Control.Monad

46import Control.Monad

48import Control.Monad.State.Strict as State

47import Control.Monad.State.Strict as State

48+import Data.Char (isLetter, toLower)

49import Data.List

50−import Data.Maybe

50+import Data.List.Split (splitOn)

51−import Debug.Trace

52−

53import qualified Data.Map as Map

51import qualified Data.Map as Map

52+import Data.Maybe

54import qualified Data.Set as S

53import qualified Data.Set as S

55import qualified Data.Text as T

54import qualified Data.Text as T

56−import Data.Char(isLetter, toLower)

55+import Debug.Trace

57−import Data.List.Split (splitOn)

58−

59−import Util.Pretty

60

56

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

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

62warnLC fc n

58warnLC fc n

@@ -289,7 +285,7 @@ addParamConstraints fc ps cty cons

289 then ULE avar cvar

285 then ULE avar cvar

290 else ULT avar cvar

286 else ULT avar cvar

291 addConstraints fc (tv, [con])

287 addConstraints fc (tv, [con])

292− addIBC (IBCConstraint fc con)

288+ addIBC (IBCConstraint fc con)

293 _ -> return ()

289 _ -> return ()

294 constraintTy t = return ()

290 constraintTy t = return ()

295

291

src/Idris/Elab/Implementation.hs+24−27

@@ -10,52 +10,49 @@ module Idris.Elab.Implementation(elabImplementation) where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13+import Idris.Core.CaseTree

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

15+import Idris.Core.Evaluate

16+import Idris.Core.Execute

17+import Idris.Core.TT

18+import Idris.Core.Typecheck

19+import Idris.Coverage

20+import Idris.DataOpts

21+import Idris.DeepSeq

22+import Idris.Delaborate

23+import Idris.Docstrings

13import Idris.DSL

24import Idris.DSL

25+import Idris.Elab.Data

26+import Idris.Elab.Term

27+import Idris.Elab.Type

28+import Idris.Elab.Utils

14import Idris.Error

29import Idris.Error

15−import Idris.Delaborate

16import Idris.Imports

30import Idris.Imports

17−import Idris.Coverage

18−import Idris.DataOpts

19−import Idris.Providers

20−import Idris.Primitives

21import Idris.Inliner

31import Idris.Inliner

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

22import Idris.PartialEval

33import Idris.PartialEval

23−import Idris.DeepSeq

34+import Idris.Primitives

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

35+import Idris.Providers

25import IRTS.Lang

36import IRTS.Lang

26

37

27−import Idris.Elab.Type

38+import Util.Pretty (pretty, text)

28−import Idris.Elab.Data

29−import Idris.Elab.Utils

30−import Idris.Elab.Term

31−

32−import Idris.Core.TT

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

34−import Idris.Core.Evaluate

35−import Idris.Core.Execute

36−import Idris.Core.Typecheck

37−import Idris.Core.CaseTree

38−

39−import Idris.Docstrings

40

39

41import Prelude hiding (id, (.))

40import Prelude hiding (id, (.))

42−import Control.Category

43

41

44import Control.Applicative hiding (Const)

42import Control.Applicative hiding (Const)

43+import Control.Category

45import Control.DeepSeq

44import Control.DeepSeq

46import Control.Monad

45import Control.Monad

47import Control.Monad.State.Strict as State

46import Control.Monad.State.Strict as State

47+import Data.Char (isLetter, toLower)

48import Data.List

49−import Data.Maybe

49+import Data.List.Split (splitOn)

50−import Debug.Trace

51−

52import qualified Data.Map as Map

50import qualified Data.Map as Map

51+import Data.Maybe

53import qualified Data.Set as S

52import qualified Data.Set as S

54import qualified Data.Text as T

53import qualified Data.Text as T

55−import Data.Char(isLetter, toLower)

54+import Debug.Trace

56−import Data.List.Split (splitOn)

57

55

58−import Util.Pretty(pretty, text)

59

56

60elabImplementation :: ElabInfo

57elabImplementation :: ElabInfo

61 -> SyntaxInfo

58 -> SyntaxInfo

src/Idris/Elab/Interface.hs+25−28

@@ -11,53 +11,50 @@ module Idris.Elab.Interface(elabInterface) where

11

12import Idris.AbsSyntax

13import Idris.ASTUtils

14+import Idris.Core.CaseTree

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

16+import Idris.Core.Evaluate

17+import Idris.Core.Execute

18+import Idris.Core.TT

19+import Idris.Core.Typecheck

20+import Idris.Coverage

21+import Idris.DataOpts

22+import Idris.DeepSeq

23+import Idris.Delaborate

24+import Idris.Docstrings

14import Idris.DSL

25import Idris.DSL

26+import Idris.Elab.Data

27+import Idris.Elab.Term

28+import Idris.Elab.Type

29+import Idris.Elab.Utils

15import Idris.Error

30import Idris.Error

16−import Idris.Delaborate

17import Idris.Imports

31import Idris.Imports

18−import Idris.Elab.Term

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.Providers

22−import Idris.Primitives

23import Idris.Inliner

32import Idris.Inliner

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

24import Idris.PartialEval

34import Idris.PartialEval

25−import Idris.DeepSeq

35+import Idris.Primitives

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

36+import Idris.Providers

27import IRTS.Lang

37import IRTS.Lang

28

38

29−import Idris.Elab.Type

39+import Util.Pretty (pretty, text)

30−import Idris.Elab.Data

31−import Idris.Elab.Utils

32−

33−import Idris.Core.TT

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

35−import Idris.Core.Evaluate

36−import Idris.Core.Execute

37−import Idris.Core.Typecheck

38−import Idris.Core.CaseTree

39−

40−import Idris.Docstrings

41

40

42import Prelude hiding (id, (.))

41import Prelude hiding (id, (.))

43−import Control.Category

44

42

45import Control.Applicative hiding (Const)

43import Control.Applicative hiding (Const)

44+import Control.Category

46import Control.DeepSeq

45import Control.DeepSeq

47import Control.Monad

46import Control.Monad

48import Control.Monad.State.Strict as State

47import Control.Monad.State.Strict as State

48+import Data.Char (isLetter, toLower)

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

49import Data.List

50import Data.List

50−import Data.Maybe

51+import Data.List.Split (splitOn)

51−import Debug.Trace

52−

53import qualified Data.Map as Map

52import qualified Data.Map as Map

53+import Data.Maybe

54import qualified Data.Set as S

55import qualified Data.Text as T

56−import Data.Char(isLetter, toLower)

56+import Debug.Trace

57−import Data.List.Split (splitOn)

58−import Data.Generics.Uniplate.Data (transform)

59

57

60−import Util.Pretty(pretty, text)

61

58

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

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

63

60

src/Idris/Elab/Provider.hs+25−29

@@ -10,53 +10,49 @@ module Idris.Elab.Provider(elabProvider) where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13+import Idris.Core.CaseTree

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

15+import Idris.Core.Evaluate

16+import Idris.Core.Execute

17+import Idris.Core.TT

18+import Idris.Core.Typecheck

19+import Idris.Coverage

20+import Idris.DataOpts

21+import Idris.DeepSeq

22+import Idris.Delaborate

23+import Idris.Docstrings

13import Idris.DSL

24import Idris.DSL

25+import Idris.Elab.Clause

26+import Idris.Elab.Term

27+import Idris.Elab.Type

28+import Idris.Elab.Utils

29+import Idris.Elab.Value

14import Idris.Error

30import Idris.Error

15−import Idris.Delaborate

16import Idris.Imports

31import Idris.Imports

17−import Idris.Coverage

18−import Idris.DataOpts

19−import Idris.Providers

20−import Idris.Primitives

21import Idris.Inliner

32import Idris.Inliner

33+import Idris.Output (iWarn, iputStrLn, pshow)

22import Idris.PartialEval

34import Idris.PartialEval

23−import Idris.DeepSeq

35+import Idris.Primitives

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

36+import Idris.Providers

25import IRTS.Lang

37import IRTS.Lang

26

38

27−import Idris.Elab.Type

39+import Util.Pretty (pretty, text)

28−import Idris.Elab.Clause

29−import Idris.Elab.Value

30−import Idris.Elab.Utils

31−import Idris.Elab.Term

32−

33−import Idris.Core.TT

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

35−import Idris.Core.Evaluate

36−import Idris.Core.Execute

37−import Idris.Core.Typecheck

38−import Idris.Core.CaseTree

39−

40−import Idris.Docstrings

41

40

42import Prelude hiding (id, (.))

41import Prelude hiding (id, (.))

43−import Control.Category

44

42

45import Control.Applicative hiding (Const)

43import Control.Applicative hiding (Const)

44+import Control.Category

46import Control.DeepSeq

45import Control.DeepSeq

47import Control.Monad

46import Control.Monad

48import Control.Monad.State.Strict as State

47import Control.Monad.State.Strict as State

48+import Data.Char (isLetter, toLower)

49import Data.List

50−import Data.Maybe

50+import Data.List.Split (splitOn)

51−import Debug.Trace

52−

53import qualified Data.Map as Map

51import qualified Data.Map as Map

52+import Data.Maybe

54import qualified Data.Set as S

53import qualified Data.Set as S

55import qualified Data.Text as T

54import qualified Data.Text as T

56−import Data.Char(isLetter, toLower)

55+import Debug.Trace

57−import Data.List.Split (splitOn)

58−

59−import Util.Pretty(pretty, text)

60

56

61-- | Elaborate a type provider

57-- | Elaborate a type provider

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

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

src/Idris/Elab/Quasiquote.hs+1−1

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

7-}

8module Idris.Elab.Quasiquote (extractUnquotes) where

9

10+import Idris.AbsSyntax

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

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

11import Idris.Core.TT

12import Idris.Core.TT

12−import Idris.AbsSyntax

13

14

15extract1 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])

src/Idris/Elab/Record.hs+20−24

@@ -5,39 +5,35 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, ViewPatterns #-}

8+{-# LANGUAGE PatternGuards #-}

9module Idris.Elab.Record(elabRecord) where

10

11import Idris.AbsSyntax

12+import Idris.Core.Evaluate

13+import Idris.Core.TT

14+import Idris.Coverage

15+import Idris.DataOpts

16+import Idris.DeepSeq

17+import Idris.Delaborate

12import Idris.Docstrings

18import Idris.Docstrings

19+import Idris.Elab.Data

20+import Idris.Elab.Data

21+import Idris.Elab.Term

22+import Idris.Elab.Type

23+import Idris.Elab.Utils

13import Idris.Error

24import Idris.Error

14−import Idris.Delaborate

15import Idris.Imports

25import Idris.Imports

16−import Idris.Elab.Term

17−import Idris.Coverage

18−import Idris.DataOpts

19−import Idris.Providers

20−import Idris.Primitives

21import Idris.Inliner

26import Idris.Inliner

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

28+import Idris.Parser.Expr (tryFullExpr)

22import Idris.PartialEval

29import Idris.PartialEval

23−import Idris.DeepSeq

30+import Idris.Primitives

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

31+import Idris.Providers

25import IRTS.Lang

32import IRTS.Lang

26

33

27−import Idris.Parser.Expr (tryFullExpr)

28−

29−import Idris.Elab.Type

30−import Idris.Elab.Data

31−import Idris.Elab.Utils

32−

33−import Idris.Core.TT

34−import Idris.Core.Evaluate

35−

36−import Idris.Elab.Data

37−

38−import Data.Maybe

39−import Data.List

40import Control.Monad

34import Control.Monad

35+import Data.List

36+import Data.Maybe

41

37

42-- | Elaborate a record declaration

38-- | Elaborate a record declaration

43elabRecord :: ElabInfo

39elabRecord :: ElabInfo

@@ -271,7 +267,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

271

267

272 -- | Elaborate the projection functions.

268 -- | Elaborate the projection functions.

273 elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

269 elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

274− elabProj cn paramnames fs

270+ elabProj cn paramnames fs

275 = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

271 = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

276 elab = \(n, n', p, t, doc, i) ->

272 elab = \(n, n', p, t, doc, i) ->

277 -- Use projections in types

273 -- Use projections in types

@@ -283,7 +279,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

283

279

284 -- | Elaborate the update functions.

280 -- | Elaborate the update functions.

285 elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

281 elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

286− elabUp cn paramnames fs

282+ elabUp cn paramnames fs

287 = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

283 = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

288 elab = \(n, n', p, t, doc, i) -> elabUpdate info n paramnames n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

284 elab = \(n, n', p, t, doc, i) -> elabUpdate info n paramnames n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

289 in mapM_ elab fs

285 in mapM_ elab fs

src/Idris/Elab/Rewrite.hs+4−5

@@ -5,23 +5,22 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, ViewPatterns #-}

8+{-# LANGUAGE PatternGuards #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

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

11

12import Idris.AbsSyntax

13import Idris.AbsSyntaxTree

14−import Idris.Delaborate

15−import Idris.Error

16−import Idris.Core.TT

17import Idris.Core.Elaborate

14import Idris.Core.Elaborate

18import Idris.Core.Evaluate

15import Idris.Core.Evaluate

16+import Idris.Core.TT

17+import Idris.Delaborate

19import Idris.Docstrings

18import Idris.Docstrings

19+import Idris.Error

20

21import Control.Monad

22import Control.Monad.State.Strict

23import Data.List

24−

25import Debug.Trace

24import Debug.Trace

26

25

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

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

src/Idris/Elab/RunElab.hs+5−8

@@ -7,19 +7,16 @@ Maintainer : The Idris Community.

7-}

8module Idris.Elab.RunElab (elabRunElab) where

9

10−import Idris.Elab.Term

11−import Idris.Elab.Value (elabVal)

12−

13import Idris.AbsSyntax

10import Idris.AbsSyntax

14−import Idris.Error

15−

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

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

17import Idris.Core.Evaluate

12import Idris.Core.Evaluate

18import Idris.Core.Execute

13import Idris.Core.Execute

19import Idris.Core.TT

14import Idris.Core.TT

20import Idris.Core.Typecheck

15import Idris.Core.Typecheck

21−

16+import Idris.Elab.Term

17+import Idris.Elab.Value (elabVal)

18+import Idris.Error

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

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

23

20

24elabScriptTy :: Type

21elabScriptTy :: Type

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

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

src/Idris/Elab/Term.hs+18−18

@@ -11,26 +11,27 @@ module Idris.Elab.Term where

11

12import Idris.AbsSyntax

13import Idris.AbsSyntaxTree

14−import Idris.DSL

15−import Idris.Delaborate

16−import Idris.Error

17−import Idris.ProofSearch

18−import Idris.Output (pshow)

19−

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

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

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

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

22−import Idris.Core.TT

23import Idris.Core.Evaluate

16import Idris.Core.Evaluate

24−import Idris.Core.Unify

25import Idris.Core.ProofTerm (getProofTerm)

17import Idris.Core.ProofTerm (getProofTerm)

18+import Idris.Core.TT

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

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

20+import Idris.Core.Unify

27import Idris.Core.WHNF (whnf)

21import Idris.Core.WHNF (whnf)

28−import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, recoverableCoverage, validCoverageCase)

22+import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses,

23+ recoverableCoverage, validCoverageCase)

29−import Idris.ErrReverse (errReverse)

24+import Idris.Delaborate

25+import Idris.DSL

30import Idris.Elab.Quasiquote (extractUnquotes)

26import Idris.Elab.Quasiquote (extractUnquotes)

31−import Idris.Elab.Utils

32import Idris.Elab.Rewrite

27import Idris.Elab.Rewrite

28+import Idris.Elab.Utils

29+import Idris.Error

30+import Idris.ErrReverse (errReverse)

31+import Idris.Output (pshow)

32+import Idris.ProofSearch

33import Idris.Reflection

34+

34import qualified Util.Pretty as U

35import qualified Util.Pretty as U

35

36

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

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

@@ -39,10 +40,9 @@ import Control.Monad.State.Strict

39import Data.Foldable (for_)

40import Data.Foldable (for_)

40import Data.List

41import Data.List

41import qualified Data.Map as M

42import qualified Data.Map as M

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

43+import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)

43import qualified Data.Set as S

44import qualified Data.Set as S

44import qualified Data.Text as T

45import qualified Data.Text as T

45−

46import Debug.Trace

47

48data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

@@ -878,7 +878,7 @@ elab ist info emode opts fn tm

878 ns <- apply (Var f) (map isph args)

879-- trace ("ns is " ++ show ns) $ return ()

880 -- mark any interface arguments as injective

881−-- when (not pattern) $

881+-- when (not pattern) $

882 mapM_ checkIfInjective (map snd ns)

883 unifyProblems -- try again with the new information,

884 -- to help with disambiguation

@@ -916,7 +916,7 @@ elab ist info emode opts fn tm

916 ivs' <- get_implementations

917 -- Attempt to resolve any interfaces which have 'complete' types,

918 -- i.e. no holes in them

919− when (not pattern || (e_inarg ina && not tcgen)) $

919+ when (not pattern || (e_inarg ina && not tcgen)) $

920 mapM_ (\n -> do focus n

921 g <- goal

922 env <- get_env

@@ -969,7 +969,7 @@ elab ist info emode opts fn tm

969 ulog <- getUnifyLog

970 probs <- get_probs

971 inj <- get_inj

972− traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj

972+ traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj

973 ++ "\nProblems: " ++ qshow probs) $

974 unifyProblems

975 probs <- get_probs

@@ -1421,7 +1421,7 @@ elab ist info emode opts fn tm

1421 insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1422 insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1423 insertLazy ina (PCoerced t) = return t

1424− -- Don't add a delay to top level pattern variables, since they

1424+ -- Don't add a delay to top level pattern variables, since they

1425 -- can be forced on the rhs if needed

1426 insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t

1427 insertLazy ina t =

src/Idris/Elab/Transform.hs+22−26

@@ -10,50 +10,46 @@ module Idris.Elab.Transform where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13+import Idris.Core.CaseTree

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

15+import Idris.Core.Evaluate

16+import Idris.Core.Execute

17+import Idris.Core.TT

18+import Idris.Core.Typecheck

19+import Idris.Coverage

20+import Idris.DataOpts

21+import Idris.DeepSeq

22+import Idris.Delaborate

23+import Idris.Docstrings

13import Idris.DSL

24import Idris.DSL

25+import Idris.Elab.Term

26+import Idris.Elab.Utils

14import Idris.Error

27import Idris.Error

15−import Idris.Delaborate

16import Idris.Imports

28import Idris.Imports

17−import Idris.Coverage

18−import Idris.DataOpts

19−import Idris.Providers

20−import Idris.Primitives

21import Idris.Inliner

29import Idris.Inliner

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

22import Idris.PartialEval

31import Idris.PartialEval

23−import Idris.DeepSeq

32+import Idris.Primitives

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

33+import Idris.Providers

25import IRTS.Lang

34import IRTS.Lang

26

35

27−import Idris.Elab.Utils

36+import Util.Pretty (pretty, text)

28−import Idris.Elab.Term

29−

30−import Idris.Core.TT

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

32−import Idris.Core.Evaluate

33−import Idris.Core.Execute

34−import Idris.Core.Typecheck

35−import Idris.Core.CaseTree

36−

37−import Idris.Docstrings

38

37

39import Prelude hiding (id, (.))

38import Prelude hiding (id, (.))

40−import Control.Category

41

39

42import Control.Applicative hiding (Const)

40import Control.Applicative hiding (Const)

41+import Control.Category

43import Control.DeepSeq

42import Control.DeepSeq

44import Control.Monad

43import Control.Monad

45import Control.Monad.State.Strict as State

44import Control.Monad.State.Strict as State

45+import Data.Char (isLetter, toLower)

46import Data.List

47−import Data.Maybe

47+import Data.List.Split (splitOn)

48−import Debug.Trace

49−

50import qualified Data.Map as Map

48import qualified Data.Map as Map

49+import Data.Maybe

51import qualified Data.Set as S

50import qualified Data.Set as S

52import qualified Data.Text as T

51import qualified Data.Text as T

53−import Data.Char(isLetter, toLower)

52+import Debug.Trace

54−import Data.List.Split (splitOn)

55−

56−import Util.Pretty(pretty, text)

57

53

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

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

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

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

src/Idris/Elab/Type.hs+24−29

@@ -13,53 +13,48 @@ module Idris.Elab.Type (

13

14import Idris.AbsSyntax

15import Idris.ASTUtils

16+import Idris.Core.CaseTree

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

18+import Idris.Core.Evaluate

19+import Idris.Core.Execute

20+import Idris.Core.TT

21+import Idris.Core.Typecheck

22+import Idris.Coverage

23+import Idris.DataOpts

24+import Idris.DeepSeq

25+import Idris.Delaborate

26+import Idris.Docstrings (Docstring)

16import Idris.DSL

27import Idris.DSL

28+import Idris.Elab.Term

29+import Idris.Elab.Utils

30+import Idris.Elab.Value

17import Idris.Error

31import Idris.Error

18−import Idris.Delaborate

19import Idris.Imports

32import Idris.Imports

20−import Idris.Elab.Term

21−import Idris.Coverage

22−import Idris.DataOpts

23−import Idris.Providers

24−import Idris.Primitives

25import Idris.Inliner

33import Idris.Inliner

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

26import Idris.PartialEval

35import Idris.PartialEval

27−import Idris.DeepSeq

36+import Idris.Primitives

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

37+import Idris.Providers

29import IRTS.Lang

38import IRTS.Lang

30

39

31−import Idris.Elab.Utils

40+import Util.Pretty (pretty, text)

32−import Idris.Elab.Value

33−

34−import Idris.Core.TT

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

36−import Idris.Core.Evaluate

37−import Idris.Core.Execute

38−import Idris.Core.Typecheck

39−import Idris.Core.CaseTree

40−

41−import Idris.Docstrings (Docstring)

42

41

43import Prelude hiding (id, (.))

42import Prelude hiding (id, (.))

44−import Control.Category

45

43

46import Control.Applicative hiding (Const)

44import Control.Applicative hiding (Const)

45+import Control.Category

47import Control.DeepSeq

46import Control.DeepSeq

48import Control.Monad

47import Control.Monad

49import Control.Monad.State.Strict as State

48import Control.Monad.State.Strict as State

49+import Data.Char (isLetter, toLower)

50import Data.List

51−import Data.Maybe

51+import Data.List.Split (splitOn)

52−import Debug.Trace

53−

54−import qualified Data.Traversable as Traversable

55−

56import qualified Data.Map as Map

52import qualified Data.Map as Map

53+import Data.Maybe

57import qualified Data.Set as S

54import qualified Data.Set as S

58import qualified Data.Text as T

55import qualified Data.Text as T

59−import Data.Char(isLetter, toLower)

56+import qualified Data.Traversable as Traversable

60−import Data.List.Split (splitOn)

57+import Debug.Trace

61−

62−import Util.Pretty(pretty, text)

63

58

64buildType :: ElabInfo

59buildType :: ElabInfo

65 -> SyntaxInfo

60 -> SyntaxInfo

src/Idris/Elab/Utils.hs+9−12

@@ -9,35 +9,32 @@ Maintainer : The Idris Community.

9module Idris.Elab.Utils where

10

11import Idris.AbsSyntax

12−import Idris.Error

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

13+import Idris.Core.Evaluate

14+import Idris.Core.TT

15+import Idris.Core.Typecheck

13import Idris.DeepSeq

16import Idris.DeepSeq

14import Idris.Delaborate

17import Idris.Delaborate

15import Idris.Docstrings

18import Idris.Docstrings

19+import Idris.Error

16import Idris.Output

20import Idris.Output

17

21

18−import Idris.Core.TT

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

20−import Idris.Core.Evaluate

21−import Idris.Core.Typecheck

22−

23import Util.Pretty

22import Util.Pretty

24

23

25import Control.Applicative hiding (Const)

24import Control.Applicative hiding (Const)

26−import Control.Monad.State

27import Control.Monad

25import Control.Monad

26+import Control.Monad.State

28import Data.List

27import Data.List

28+import qualified Data.Map as Map

29import Data.Maybe

30import qualified Data.Traversable as Traversable

31−

32import Debug.Trace

31import Debug.Trace

33

32

34−import qualified Data.Map as Map

35−

36recheckC = recheckC_borrowing False True []

33recheckC = recheckC_borrowing False True []

37

34

38recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

35recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

39 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

36 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

40−

37+

41 ctxt <- getContext

38 ctxt <- getContext

42 t' <- case safeForget t of

39 t' <- case safeForget t of

43 Just ft -> return ft

40 Just ft -> return ft

@@ -47,7 +44,7 @@ recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

47 OK x -> return x

44 OK x -> return x

48 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

45 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

49 tit <- typeInType

46 tit <- typeInType

50− when (not tit && addConstrs) $

47+ when (not tit && addConstrs) $

51 do addConstraints fc cs

48 do addConstraints fc cs

52 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

49 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

53 mapM_ (checkDeprecated fc) (allTTNames tm)

50 mapM_ (checkDeprecated fc) (allTTNames tm)

src/Idris/Elab/Value.hs+23−27

@@ -14,51 +14,47 @@ module Idris.Elab.Value(

14

15import Idris.AbsSyntax

16import Idris.ASTUtils

17+import Idris.Core.CaseTree

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

19+import Idris.Core.Evaluate hiding (Unchecked)

20+import Idris.Core.Execute

21+import Idris.Core.TT

22+import Idris.Core.Typecheck

23+import Idris.Coverage

24+import Idris.DataOpts

25+import Idris.DeepSeq

26+import Idris.Delaborate

27+import Idris.Docstrings

17import Idris.DSL

28import Idris.DSL

29+import Idris.Elab.Term

30+import Idris.Elab.Utils

18import Idris.Error

31import Idris.Error

19−import Idris.Delaborate

20import Idris.Imports

32import Idris.Imports

21−import Idris.Coverage

22−import Idris.DataOpts

23−import Idris.Providers

24−import Idris.Primitives

25import Idris.Inliner

33import Idris.Inliner

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

26import Idris.PartialEval

35import Idris.PartialEval

27−import Idris.DeepSeq

36+import Idris.Primitives

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

37+import Idris.Providers

29import IRTS.Lang

38import IRTS.Lang

30

39

31−import Idris.Elab.Utils

40+import Util.Pretty (pretty, text)

32−import Idris.Elab.Term

33−

34−import Idris.Core.TT

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

36−import Idris.Core.Evaluate hiding (Unchecked)

37−import Idris.Core.Execute

38−import Idris.Core.Typecheck

39−import Idris.Core.CaseTree

40−

41−import Idris.Docstrings

42

41

43import Prelude hiding (id, (.))

42import Prelude hiding (id, (.))

44−import Control.Category

45

43

46import Control.Applicative hiding (Const)

44import Control.Applicative hiding (Const)

45+import Control.Category

47import Control.DeepSeq

46import Control.DeepSeq

48import Control.Monad

47import Control.Monad

49import Control.Monad.State.Strict as State

48import Control.Monad.State.Strict as State

49+import Data.Char (isLetter, toLower)

50import Data.List

51−import Data.Maybe

51+import Data.List.Split (splitOn)

52−import qualified Data.Traversable as Traversable

53−import Debug.Trace

54−

55import qualified Data.Map as Map

52import qualified Data.Map as Map

53+import Data.Maybe

56import qualified Data.Set as S

54import qualified Data.Set as S

57import qualified Data.Text as T

55import qualified Data.Text as T

58−import Data.Char(isLetter, toLower)

56+import qualified Data.Traversable as Traversable

59−import Data.List.Split (splitOn)

57+import Debug.Trace

60−

61−import Util.Pretty(pretty, text)

62

58

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

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

64-- happen if elaborating as a pattern clause)

60-- happen if elaborating as a pattern clause)

src/Idris/ElabDecls.hs+31−36

@@ -6,69 +6,64 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8

9−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

9+{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

10 PatternGuards #-}

11

12module Idris.ElabDecls where

13

14import Idris.AbsSyntax

15import Idris.ASTUtils

16−import Idris.DSL

16+import Idris.Core.CaseTree

17−import Idris.Error

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

18−import Idris.Delaborate

18+import Idris.Core.Evaluate

19−import Idris.Directives

19+import Idris.Core.Execute

20−import Idris.Imports

20+import Idris.Core.TT

21−import Idris.Elab.Term

21+import Idris.Core.Typecheck

22import Idris.Coverage

23import Idris.DataOpts

24−import Idris.Providers

25−import Idris.Primitives

26−import Idris.Inliner

27−import Idris.PartialEval

28import Idris.DeepSeq

24import Idris.DeepSeq

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

25+import Idris.Delaborate

26+import Idris.Directives

27+import Idris.Docstrings hiding (Unchecked)

30−import IRTS.Lang

28+import Idris.DSL

31−

32−import Idris.Elab.Utils

33−import Idris.Elab.Type

34import Idris.Elab.Clause

29import Idris.Elab.Clause

35import Idris.Elab.Data

30import Idris.Elab.Data

36−import Idris.Elab.Record

37−import Idris.Elab.Interface

38import Idris.Elab.Implementation

31import Idris.Elab.Implementation

32+import Idris.Elab.Interface

39import Idris.Elab.Provider

33import Idris.Elab.Provider

34+import Idris.Elab.Record

40import Idris.Elab.RunElab

35import Idris.Elab.RunElab

36+import Idris.Elab.Term

41import Idris.Elab.Transform

37import Idris.Elab.Transform

38+import Idris.Elab.Type

39+import Idris.Elab.Utils

42import Idris.Elab.Value

40import Idris.Elab.Value

41+import Idris.Error

42+import Idris.Imports

43+import Idris.Inliner

44+import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

45+import Idris.PartialEval

46+import Idris.Primitives

47+import Idris.Providers

48+import IRTS.Lang

43

49

44−import Idris.Core.TT

50+import Util.Pretty (pretty, text)

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

46−import Idris.Core.Evaluate

47−import Idris.Core.Execute

48−import Idris.Core.Typecheck

49−import Idris.Core.CaseTree

50−

51−import Idris.Docstrings hiding (Unchecked)

52

51

53import Prelude hiding (id, (.))

52import Prelude hiding (id, (.))

54−import Control.Category

55

53

56import Control.Applicative hiding (Const)

54import Control.Applicative hiding (Const)

55+import Control.Category

57import Control.DeepSeq

56import Control.DeepSeq

58import Control.Monad

57import Control.Monad

59import Control.Monad.State.Strict as State

58import Control.Monad.State.Strict as State

59+import Data.Char (isLetter, toLower)

60import Data.List

61−import Data.Maybe

61+import Data.List.Split (splitOn)

62−import Debug.Trace

63−

64import qualified Data.Map as Map

62import qualified Data.Map as Map

63+import Data.Maybe

65import qualified Data.Set as S

64import qualified Data.Set as S

66import qualified Data.Text as T

65import qualified Data.Text as T

67−import Data.Char(isLetter, toLower)

66+import Debug.Trace

68−import Data.List.Split (splitOn)

69−

70−import Util.Pretty(pretty, text)

71−

72

67

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

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

74recinfo :: FC -> ElabInfo

69recinfo :: FC -> ElabInfo

@@ -87,7 +82,7 @@ elabPrims :: Idris ()

87elabPrims = do i <- getIState

82elabPrims = do i <- getIState

88 let cs_in = idris_constraints i

83 let cs_in = idris_constraints i

89 let mkdec opt decl docs argdocs =

84 let mkdec opt decl docs argdocs =

90− PData docs argdocs defaultSyntax (fileFC "builtin")

85+ PData docs argdocs defaultSyntax (fileFC "builtin")

91 opt decl

86 opt decl

92 elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

87 elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

93 -- We don't want the constraints generated by 'Infer' since

88 -- We don't want the constraints generated by 'Infer' since

src/Idris/Erasure.hs+13−14

@@ -12,32 +12,31 @@ module Idris.Erasure (performUsageAnalysis, mkFieldName) where

12import Idris.AbsSyntax

13import Idris.ASTUtils

14import Idris.Core.CaseTree

15−import Idris.Core.TT

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

17−import Idris.Primitives

16+import Idris.Core.TT

18import Idris.Error

17import Idris.Error

18+import Idris.Primitives

19

20−import Debug.Trace

21−import System.IO.Unsafe

22−

23−import Control.Category

24import Prelude hiding (id, (.))

20import Prelude hiding (id, (.))

25

21

26−import Control.Arrow

27import Control.Applicative

22import Control.Applicative

23+import Control.Arrow

24+import Control.Category

28import Control.Monad.State

25import Control.Monad.State

29−import Data.Maybe

26+import Data.IntMap (IntMap)

30−import Data.List

31−import qualified Data.Set as S

32−import qualified Data.IntSet as IS

33−import qualified Data.Map as M

34import qualified Data.IntMap as IM

27import qualified Data.IntMap as IM

35−import Data.Set (Set)

36import Data.IntSet (IntSet)

28import Data.IntSet (IntSet)

29+import qualified Data.IntSet as IS

30+import Data.List

37import Data.Map (Map)

31import Data.Map (Map)

38−import Data.IntMap (IntMap)

32+import qualified Data.Map as M

33+import Data.Maybe

34+import Data.Set (Set)

35+import qualified Data.Set as S

39import Data.Text (pack)

36import Data.Text (pack)

40import qualified Data.Text as T

37import qualified Data.Text as T

38+import Debug.Trace

39+import System.IO.Unsafe

41

40

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

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

43-- positions.

42-- positions.

src/Idris/Error.hs+10−10

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

10

11module Idris.Error where

12

13−import Prelude hiding (catch)

14import Idris.AbsSyntax

13import Idris.AbsSyntax

15−import Idris.Delaborate

14+import Idris.Core.Constraints

16−

17import Idris.Core.Evaluate (ctxtAlist)

15import Idris.Core.Evaluate (ctxtAlist)

18import Idris.Core.TT

16import Idris.Core.TT

19import Idris.Core.Typecheck

17import Idris.Core.Typecheck

20−import Idris.Core.Constraints

18+import Idris.Delaborate

21import Idris.Output

19import Idris.Output

22

20

23−import System.Console.Haskeline

21+import Prelude hiding (catch)

24−import System.Console.Haskeline.MonadException

22+

25import Control.Monad (when)

23import Control.Monad (when)

26import Control.Monad.State.Strict

24import Control.Monad.State.Strict

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

28import Data.Char

25import Data.Char

26+import qualified Data.Foldable as Foldable

29import Data.List (intercalate, isPrefixOf)

27import Data.List (intercalate, isPrefixOf)

30−import qualified Data.Text as T

31import qualified Data.Set as S

28import qualified Data.Set as S

32−import Data.Typeable

29+import qualified Data.Text as T

33import qualified Data.Traversable as Traversable

30import qualified Data.Traversable as Traversable

34−import qualified Data.Foldable as Foldable

31+import Data.Typeable

32+import System.Console.Haskeline

33+import System.Console.Haskeline.MonadException

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

35

36iucheck :: Idris ()

37iucheck = do tit <- typeInType

src/Idris/IBC.hs+17−19

@@ -12,41 +12,39 @@ module Idris.IBC (loadIBC, loadPkgIndex,

12 writeIBC, writePkgIndex,

13 hasValidIBCVersion, IBCPhase(..)) where

14

15−import Idris.Core.Evaluate

15+import Idris.AbsSyntax

16−import Idris.Core.TT

17import Idris.Core.Binary

16import Idris.Core.Binary

18import Idris.Core.CaseTree

17import Idris.Core.CaseTree

19−import Idris.AbsSyntax

18+import Idris.Core.Evaluate

20−import Idris.Imports

19+import Idris.Core.TT

21−import Idris.Error

22import Idris.DeepSeq

20import Idris.DeepSeq

23import Idris.Delaborate

21import Idris.Delaborate

24−import qualified Idris.Docstrings as D

25import Idris.Docstrings (Docstring)

22import Idris.Docstrings (Docstring)

23+import qualified Idris.Docstrings as D

24+import Idris.Error

25+import Idris.Imports

26import Idris.Output

27import IRTS.System (getIdrisLibDir)

28+

28import Paths_idris

29import Paths_idris

29

30

30import qualified Cheapskate.Types as CT

31import qualified Cheapskate.Types as CT

31−

32+import Codec.Archive.Zip

33+import Control.DeepSeq

34+import Control.Monad

35+import Control.Monad.State.Strict hiding (get, put)

36+import qualified Control.Monad.State.Strict as ST

32import Data.Binary

37import Data.Binary

38+import Data.ByteString.Lazy as B hiding (elem, length, map)

33import Data.Functor

39import Data.Functor

34−import Data.Vector.Binary

35import Data.List as L

40import Data.List as L

36import Data.Maybe (catMaybes)

41import Data.Maybe (catMaybes)

37−import Data.ByteString.Lazy as B hiding (length, elem, map)

38−import qualified Data.Text as T

39import qualified Data.Set as S

42import qualified Data.Set as S

40−

41−import Control.Monad

42−import Control.DeepSeq

43−import Control.Monad.State.Strict hiding (get, put)

44−import qualified Control.Monad.State.Strict as ST

43+import qualified Data.Text as T

45−import System.FilePath

44+import Data.Vector.Binary

46−import System.Directory

47−import Codec.Archive.Zip

48−

49import Debug.Trace

45import Debug.Trace

46+import System.Directory

47+import System.FilePath

50

48

51ibcVersion :: Word16

49ibcVersion :: Word16

52ibcVersion = 149

50ibcVersion = 149

src/Idris/IdeMode.hs+9−10

@@ -11,23 +11,22 @@ 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 Text.Printf

14+import Idris.Core.Binary

15−import Numeric

15+import Idris.Core.TT

16−import Data.List

16+

17−import Data.Maybe (isJust)

17+import Control.Applicative hiding (Const)

18import qualified Data.Binary as Binary

19import qualified Data.ByteString.Base64 as Base64

20import qualified Data.ByteString.Lazy as Lazy

21import qualified Data.ByteString.UTF8 as UTF8

22+import Data.List

23+import Data.Maybe (isJust)

22import qualified Data.Text as T

24import qualified Data.Text as T

25+import Numeric

26+import System.IO

27+import Text.Printf

23import Text.Trifecta hiding (Err)

28import Text.Trifecta hiding (Err)

24import Text.Trifecta.Delta

29import Text.Trifecta.Delta

25−import System.IO

26−

27−import Idris.Core.TT

28−import Idris.Core.Binary

29−

30−import Control.Applicative hiding (Const)

31

30

32getNChar :: Handle -> Int -> String -> IO (String)

31getNChar :: Handle -> Int -> String -> IO (String)

33getNChar _ 0 s = return (reverse s)

32getNChar _ 0 s = return (reverse s)

src/Idris/IdrisDoc.hs+17−24

@@ -5,57 +5,50 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards #-}

9−{-# LANGUAGE OverloadedStrings #-}

8+{-# LANGUAGE OverloadedStrings, PatternGuards #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11module Idris.IdrisDoc (generateDocs) where

10module Idris.IdrisDoc (generateDocs) where

12

11

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

14− TextFormatting (..), txt, str, nsroot, constIsType, toAlist)

15−import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,

16− Accessibility (..), isDConName, isFnName,

17− isTConName)

18−import Idris.Parser.Helpers (opChars)

19import Idris.AbsSyntax

12import 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)

20import Idris.Docs

18import Idris.Docs

21import Idris.Docstrings (nullDocstring)

19import Idris.Docstrings (nullDocstring)

22import qualified Idris.Docstrings as Docstrings

20import qualified Idris.Docstrings as Docstrings

23−

21+import Idris.Parser.Helpers (opChars)

24import IRTS.System (getDataFileName)

22import IRTS.System (getDataFileName)

25

23

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

24import Control.Applicative ((<|>))

27import Control.Monad (forM_)

25import Control.Monad (forM_)

28import Control.Monad.Trans.Except

26import Control.Monad.Trans.Except

29import Control.Monad.Trans.State.Strict

27import Control.Monad.Trans.State.Strict

30−

31−import Data.Maybe

32−

33import qualified Data.ByteString as BS

28import qualified Data.ByteString as BS

34import qualified Data.ByteString.Lazy as BS2

29import qualified Data.ByteString.Lazy as BS2

35−import qualified Data.Text.Encoding as E

36import qualified Data.List as L

30import qualified Data.List as L

37import qualified Data.List.Split as LS

31import qualified Data.List.Split as LS

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

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

33+import Data.Maybe

39import Data.Monoid (mempty)

34import Data.Monoid (mempty)

40import qualified Data.Ord (compare)

35import qualified Data.Ord (compare)

41import qualified Data.Set as S

36import qualified Data.Set as S

42import qualified Data.Text as T

37import qualified Data.Text as T

43−

38+import qualified Data.Text.Encoding as E

39+import System.Directory

40+import System.FilePath

44import System.IO

41import System.IO

45import System.IO.Error

42import System.IO.Error

46−import System.FilePath

43+import Text.Blaze (contents, toValue)

47−import System.Directory

44+import qualified Text.Blaze.Html.Renderer.String as R

48−

45+import Text.Blaze.Html.Renderer.Utf8 (renderHtml)

49−import Text.PrettyPrint.Annotated.Leijen (displayDecorated, renderCompact)

50−

51−import Text.Blaze (toValue, contents)

52−import Text.Blaze.Internal (MarkupM (Empty))

53−import Text.Blaze.Html5 ((!), toHtml, preEscapedToHtml)

46+import Text.Blaze.Html5 (preEscapedToHtml, toHtml, (!))

54import qualified Text.Blaze.Html5 as H

47import qualified Text.Blaze.Html5 as H

55import Text.Blaze.Html5.Attributes as A

48import Text.Blaze.Html5.Attributes as A

56−import Text.Blaze.Html.Renderer.Utf8 (renderHtml)

49+import Text.Blaze.Internal (MarkupM(Empty))

57−import qualified Text.Blaze.Html.Renderer.String as R

58import Text.Blaze.Renderer.String (renderMarkup)

50import Text.Blaze.Renderer.String (renderMarkup)

51+import Text.PrettyPrint.Annotated.Leijen (displayDecorated, renderCompact)

59

52

60-- ---------------------------------------------------------------- [ Public ]

53-- ---------------------------------------------------------------- [ Public ]

61

54

src/Idris/Imports.hs+5−8

@@ -10,19 +10,16 @@ module Idris.Imports(

10 , ibcPathNoFallback, installedPackages, pkgIndex

11 ) where

12

13−import Control.Applicative ((<$>))

14−import Data.List (isSuffixOf)

15−

16import Idris.AbsSyntax

13import Idris.AbsSyntax

17−import Idris.Error

18−

19import Idris.Core.TT

14import Idris.Core.TT

20−

15+import Idris.Error

21import IRTS.System (getIdrisLibDir)

16import IRTS.System (getIdrisLibDir)

22

17

23−import System.FilePath

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

24−import System.Directory

25import Control.Monad.State.Strict

19import Control.Monad.State.Strict

20+import Data.List (isSuffixOf)

21+import System.Directory

22+import System.FilePath

26

23

27data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

24data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

28 deriving (Show, Eq)

25 deriving (Show, Eq)

src/Idris/Info.hs+5−8

@@ -24,19 +24,16 @@ module Idris.Info

24 , getIdrisLoggingCategories

25 ) where

26

27−import System.FilePath

28−import System.Directory

29−import Data.Version

30−

31−import Idris.Imports (installedPackages)

32import Idris.AbsSyntax (loggingCatsStr)

27import Idris.AbsSyntax (loggingCatsStr)

33−

28+import Idris.Imports (installedPackages)

34import qualified IRTS.System as S

29import qualified IRTS.System as S

35

30

36−import Version_idris (gitHash)

37−

38import Paths_idris

31import Paths_idris

32+import Version_idris (gitHash)

39

33

34+import Data.Version

35+import System.Directory

36+import System.FilePath

40getIdrisDataDir :: IO String

37getIdrisDataDir :: IO String

41getIdrisDataDir = S.getIdrisDataDir

38getIdrisDataDir = S.getIdrisDataDir

42

39

src/Idris/Info/Show.hs+2−2

@@ -1,9 +1,9 @@

1module Idris.Info.Show where

2

3−import System.Exit

4−

5import Idris.Info

3import Idris.Info

6

4

5+import System.Exit

6+

7showIdrisCRTSDir :: IO ()

8showIdrisCRTSDir = do

9 ldir <- getIdrisCRTSDir

src/Idris/Inliner.hs+1−1

@@ -9,8 +9,8 @@ Maintainer : The Idris Community.

9

10module Idris.Inliner(inlineDef, inlineTerm) where

11

12−import Idris.Core.TT

13import Idris.AbsSyntax

12import Idris.AbsSyntax

13+import Idris.Core.TT

14

15inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

16inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

src/Idris/Interactive.hs+11−12

@@ -14,30 +14,29 @@ module Idris.Interactive(

14 , makeLemma

15 ) where

16

17−import Idris.Core.TT

18−import Idris.Core.Evaluate

19−import Idris.CaseSplit

20import Idris.AbsSyntax

17import Idris.AbsSyntax

18+import Idris.CaseSplit

19+import Idris.Core.Evaluate

20+import Idris.Core.TT

21+import Idris.Delaborate

22+import Idris.Elab.Term

23+import Idris.Elab.Value

21import Idris.ElabDecls

24import Idris.ElabDecls

22import Idris.Error

25import Idris.Error

23import Idris.ErrReverse

26import Idris.ErrReverse

24−import Idris.Delaborate

25−import Idris.Output

26import Idris.IdeMode hiding (IdeModeCommand(..))

27import Idris.IdeMode hiding (IdeModeCommand(..))

27−import Idris.Elab.Value

28+import Idris.Output

28−import Idris.Elab.Term

29

30import Util.Pretty

31import Util.System

32

33−import System.FilePath

34−import System.Directory

35−import System.IO

36import Data.Char

33import Data.Char

37−import Data.Maybe (fromMaybe)

38import Data.List (isSuffixOf)

34import Data.List (isSuffixOf)

39−

35+import Data.Maybe (fromMaybe)

40import Debug.Trace

36import Debug.Trace

37+import System.Directory

38+import System.FilePath

39+import System.IO

41

40

42caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

41caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

43caseSplitAt fn updatefile l n

42caseSplitAt fn updatefile l n

src/Idris/Main.hs+20−27

@@ -13,46 +13,39 @@ module Idris.Main

13 ) where

14

15import Idris.AbsSyntax

16−import Idris.ModeCommon

16+import Idris.Core.Execute (execute)

17+import Idris.Core.TT

18+import Idris.Elab.Term

17−import Idris.REPL.Parser

19+import Idris.Elab.Value

20+import Idris.ElabDecls

18import Idris.Error

21import Idris.Error

19import Idris.IBC

22import Idris.IBC

20−import Idris.Parser hiding (indent)

23+import Idris.Info

24+import Idris.ModeCommon

21import Idris.Output

25import Idris.Output

22−

23−import Idris.REPL.Commands

26+import Idris.Parser hiding (indent)

24import Idris.REPL

27import Idris.REPL

25−

26−import Idris.ElabDecls

28+import Idris.REPL.Commands

27−import Idris.Elab.Value

28−import Idris.Elab.Term

29+import Idris.REPL.Parser

29−import Idris.Info

30+import IRTS.CodegenCommon

30

31

31import Util.System

32import Util.System

32

33

33−import Idris.Core.Execute (execute)

34+import Prelude hiding (id, (.), (<$>))

34−import Idris.Core.TT

35−

36−import IRTS.CodegenCommon

37

35

38import Control.Category

36import Control.Category

39−import Prelude hiding ((<$>), (.), id)

37+import Control.DeepSeq

40−

41−import Text.Trifecta.Result(Result(..), ErrInfo(..))

42−

43−import System.Console.Haskeline as H

44−import System.FilePath

45−import System.Exit

46−import System.Directory

47−import System.IO

48import Control.Monad

38import Control.Monad

39+import Control.Monad.Trans (lift)

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

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

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

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

51−import Control.Monad.Trans ( lift )

52import Data.Maybe

42import Data.Maybe

53−import Control.DeepSeq

43+import System.Console.Haskeline as H

54−

44+import System.Directory

55−

45+import System.Exit

46+import System.FilePath

47+import System.IO

48+import Text.Trifecta.Result (ErrInfo(..), Result(..))

56

49

57-- | How to run Idris programs.

50-- | How to run Idris programs.

58runMain :: Idris () -> IO ()

51runMain :: Idris () -> IO ()

src/Idris/ModeCommon.hs+11−14

@@ -6,32 +6,29 @@ Maintainer : The Idris Community.

6-}

7module Idris.ModeCommon where

8

9−

10import Idris.AbsSyntax

9import Idris.AbsSyntax

10+import Idris.Chaser

11+import Idris.Core.TT

12+import Idris.Delaborate

11import Idris.Erasure

13import Idris.Erasure

12import Idris.Error

14import Idris.Error

13import Idris.IBC

15import Idris.IBC

14−import Idris.Delaborate

15−import Idris.Parser hiding (indent)

16−import Idris.Chaser

17import Idris.Imports

16import Idris.Imports

18−import Idris.Output

19import Idris.Info

17import Idris.Info

20−import Idris.Core.TT

18+import Idris.Output

21−

19+import Idris.Parser hiding (indent)

22import IRTS.Exports

20import IRTS.Exports

23

21

24−import Control.Category

25−import Prelude hiding ((<$>), (.), id)

22+import Prelude hiding (id, (.), (<$>))

26

23

27−import System.Directory

24+import Control.Category

25+import Control.DeepSeq

28import Control.Monad

26import Control.Monad

29import Control.Monad.Trans.State.Strict (get)

27import Control.Monad.Trans.State.Strict (get)

30−import Network.Socket (PortNumber)

31−import Data.Maybe

32import Data.List hiding (group)

28import Data.List hiding (group)

33−import Control.DeepSeq

29+import Data.Maybe

34−

30+import Network.Socket (PortNumber)

31+import System.Directory

35

32

36defaultPort :: PortNumber

33defaultPort :: PortNumber

37defaultPort = fromIntegral 4294

34defaultPort = fromIntegral 4294

src/Idris/Output.hs+9−12

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

10

11module Idris.Output where

12

13−import Idris.Core.TT

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

15−

16import Idris.AbsSyntax

13import Idris.AbsSyntax

17−import Idris.Colours (hStartColourise, hEndColourise)

14+import Idris.Colours (hEndColourise, hStartColourise)

15+import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)

16+import Idris.Core.TT

18import Idris.Delaborate

17import Idris.Delaborate

19import Idris.Docstrings

18import Idris.Docstrings

20import Idris.IdeMode

19import Idris.IdeMode

@@ -23,18 +22,16 @@ import Util.Pretty

23import Util.ScreenSize (getScreenWidth)

22import Util.ScreenSize (getScreenWidth)

24import Util.System (isATTY)

23import Util.System (isATTY)

25

24

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

27−

28−import System.Console.Haskeline.MonadException

29− (MonadException (controlIO), RunIO (RunIO))

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

31−import System.FilePath (replaceExtension)

32−

33import Prelude hiding ((<$>))

25import Prelude hiding ((<$>))

34

26

27+import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

35import Data.Char (isAlpha)

28import Data.Char (isAlpha)

36−import Data.List (nub, intersperse)

29+import Data.List (intersperse, nub)

37import Data.Maybe (fromMaybe)

30import Data.Maybe (fromMaybe)

31+import System.Console.Haskeline.MonadException (MonadException(controlIO),

32+ RunIO(RunIO))

33+import System.FilePath (replaceExtension)

34+import System.IO (Handle, hPutStr, hPutStrLn, stdout)

38

35

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

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

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

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

src/Idris/Package.hs+25−29

@@ -8,42 +8,38 @@ Maintainer : The Idris Community.

8{-# LANGUAGE CPP #-}

9module Idris.Package where

10

11−import System.Process

12−import System.Directory

13−import System.Exit

14−import System.IO

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

16− takeDirectory, normalise, addExtension, hasExtension)

17−import System.Directory (createDirectoryIfMissing, copyFile)

18−

19−import Util.System

20−

21−import Control.Monad

22−import Control.Monad.Trans.State.Strict (execStateT)

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

24−

25−import Data.List

26−import Data.List.Split(splitOn)

27−import Data.Maybe(fromMaybe)

28−import Data.Either(partitionEithers)

29−

30−import Idris.Core.TT

31−import Idris.REPL

32−import Idris.Parser (loadModule)

33−import Idris.Output (pshow)

34import Idris.AbsSyntax

11import Idris.AbsSyntax

35−import Idris.IdrisDoc

12+import Idris.Core.TT

13+import Idris.Error (ifail)

36import Idris.IBC

14import Idris.IBC

37−import Idris.Output

15+import Idris.IdrisDoc

38import Idris.Imports

16import Idris.Imports

39−import Idris.Error (ifail)

17+import Idris.Main (idris, idrisMain)

40−import Idris.Main (idrisMain, idris)

18+import Idris.Output (pshow)

41−

19+import Idris.Output

42import Idris.Package.Common

20import Idris.Package.Common

43import Idris.Package.Parser

21import Idris.Package.Parser

44−

22+import Idris.Parser (loadModule)

23+import Idris.REPL

45import IRTS.System

24import IRTS.System

46

25

26+import Util.System

27+

28+import Control.Monad

29+import Control.Monad.Trans.Except (runExceptT)

30+import Control.Monad.Trans.State.Strict (execStateT)

31+import Data.Either (partitionEithers)

32+import Data.List

33+import Data.List.Split (splitOn)

34+import Data.Maybe (fromMaybe)

35+import System.Directory

36+import System.Directory (copyFile, createDirectoryIfMissing)

37+import System.Exit

38+import System.FilePath (addExtension, addTrailingPathSeparator, hasExtension,

39+ normalise, takeDirectory, takeFileName, (</>))

40+import System.IO

41+import System.Process

42+

47-- To build a package:

43-- To build a package:

48-- * read the package description

44-- * read the package description

49-- * check all the library dependencies exist

45-- * check all the library dependencies exist

src/Idris/Package/Common.hs+1−2

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

6-}

7module Idris.Package.Common where

8

9−import Idris.Core.TT (Name)

10−

11import Idris.AbsSyntaxTree (Opt(..))

9import Idris.AbsSyntaxTree (Opt(..))

10+import Idris.Core.TT (Name)

12

11

13-- | Description of an Idris package.

12-- | Description of an Idris package.

14data PkgDesc = PkgDesc {

13data PkgDesc = PkgDesc {

src/Idris/Package/Parser.hs+11−11

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

11#endif

12module Idris.Package.Parser where

13

14−import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)

15−import qualified Text.PrettyPrint.ANSI.Leijen as PP

16−import Idris.Core.TT

17−import Idris.REPL

18import Idris.AbsSyntaxTree

14import Idris.AbsSyntaxTree

19−import Idris.Parser.Helpers hiding (stringLiteral)

20import Idris.CmdOptions

15import Idris.CmdOptions

21−

16+import Idris.Core.TT

22import Idris.Package.Common

17import Idris.Package.Common

18+import Idris.Parser.Helpers hiding (stringLiteral)

19+import Idris.REPL

20+

21+import Util.System

23

22

24−import Control.Monad.State.Strict

25import Control.Applicative

23import Control.Applicative

26−import System.FilePath (takeFileName, isValid)

24+import Control.Monad.State.Strict

27−import Data.Maybe (isNothing, fromJust)

28import Data.List (union)

25import Data.List (union)

29−

26+import Data.Maybe (fromJust, isNothing)

30−import Util.System

27+import System.FilePath (isValid, takeFileName)

28+import qualified Text.PrettyPrint.ANSI.Leijen as PP

29+import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,

30+ whiteSpace)

31

32type PParser = StateT PkgDesc IdrisInnerParser

33

src/Idris/Parser.hs+37−45

@@ -5,7 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

8+{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}

9{-# OPTIONS_GHC -O0 #-}

10module Idris.Parser(module Idris.Parser,

11 module Idris.Parser.Expr,

@@ -13,74 +13,66 @@ module Idris.Parser(module Idris.Parser,

13 module Idris.Parser.Helpers,

14 module Idris.Parser.Ops) where

15

16−import Prelude hiding (pi)

17−

18−import qualified System.Directory as Dir (makeAbsolute)

19−

20−import Text.Trifecta.Delta

21−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

22−import Text.Parser.LookAhead

23−import Text.Parser.Expression

24−import qualified Text.Parser.Token as Tok

25−import qualified Text.Parser.Char as Chr

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

27−

28−import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

29−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

30−

31import Idris.AbsSyntax hiding (namespace, params)

16import Idris.AbsSyntax hiding (namespace, params)

32−import Idris.DSL

17+import Idris.Core.Evaluate

18+import Idris.Core.TT

33−import Idris.Imports

19+import Idris.Coverage

34import Idris.Delaborate

20import Idris.Delaborate

35−import Idris.Error

21+import Idris.Docstrings hiding (Unchecked)

36−import Idris.Elab.Value

22+import Idris.DSL

37import Idris.Elab.Term

23import Idris.Elab.Term

24+import Idris.Elab.Value

38import Idris.ElabDecls

25import Idris.ElabDecls

39−import Idris.Coverage

26+import Idris.Error

40import Idris.IBC

27import Idris.IBC

41−import Idris.Unlit

28+import Idris.Imports

42−import Idris.Providers

43import Idris.Output

29import Idris.Output

44−

30+import Idris.Parser.Data

31+import Idris.Parser.Expr

45import Idris.Parser.Helpers

32import Idris.Parser.Helpers

46import Idris.Parser.Ops

33import Idris.Parser.Ops

47−import Idris.Parser.Expr

34+import Idris.Providers

48−import Idris.Parser.Data

35+import Idris.Unlit

49−

50−import Idris.Docstrings hiding (Unchecked)

51−

52−import Paths_idris

53

36

54import Util.DynamicLinker

37import Util.DynamicLinker

55−import Util.System (readSource, writeSource)

56import qualified Util.Pretty as P

38import qualified Util.Pretty as P

39+import Util.System (readSource, writeSource)

57

40

58−import Idris.Core.TT

41+import Paths_idris

59−import Idris.Core.Evaluate

42+

43+import Prelude hiding (pi)

60

44

61import Control.Applicative hiding (Const)

45import Control.Applicative hiding (Const)

62import Control.Monad

46import Control.Monad

63import Control.Monad.State.Strict

47import Control.Monad.State.Strict

64−

65−import Data.Function

66−import Data.Maybe

67−import qualified Data.List.Split as Spl

48+import qualified Data.ByteString.UTF8 as UTF8

68−import Data.List

69−import Data.Monoid

70import Data.Char

49import Data.Char

71−import Data.Ord

72import Data.Foldable (asum)

50import Data.Foldable (asum)

51+import Data.Function

73import Data.Generics.Uniplate.Data (descendM)

52import Data.Generics.Uniplate.Data (descendM)

74−import qualified Data.Map as M

75import qualified Data.HashSet as HS

53import qualified Data.HashSet as HS

54+import Data.List

76−import qualified Data.Text as T

55+import qualified Data.List.Split as Spl

77−import qualified Data.ByteString.UTF8 as UTF8

56+import qualified Data.Map as M

57+import Data.Maybe

58+import Data.Monoid

59+import Data.Ord

78import qualified Data.Set as S

60import qualified Data.Set as S

79−

61+import qualified Data.Text as T

80import Debug.Trace

62import Debug.Trace

81−

63+import qualified System.Directory as Dir (makeAbsolute)

82import System.FilePath

64import System.FilePath

83import System.IO

65import System.IO

66+import qualified Text.Parser.Char as Chr

67+import Text.Parser.Expression

68+import Text.Parser.LookAhead

69+import qualified Text.Parser.Token as Tok

70+import qualified Text.Parser.Token.Highlight as Hi

71+import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

72+import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

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

74+ stringLiteral, symbol, whiteSpace)

75+import Text.Trifecta.Delta

84

76

85{-

77{-

86@

78@

src/Idris/Parser/Data.hs+21−27

@@ -5,46 +5,40 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

8+{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}

9module Idris.Parser.Data where

10

11−import Prelude hiding (pi)

12−

13−import Text.Trifecta.Delta

14−import Text.Trifecta hiding ( span, stringLiteral, charLiteral, natural

15− , symbol, char, string, whiteSpace, Err)

16−

17−import Text.Parser.LookAhead

18−import Text.Parser.Expression

19−import qualified Text.Parser.Token as Tok

20−import qualified Text.Parser.Char as Chr

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

22−

23import Idris.AbsSyntax

11import Idris.AbsSyntax

12+import Idris.Core.Evaluate

13+import Idris.Core.TT

14+import Idris.Docstrings

15+import Idris.DSL

16+import Idris.Parser.Expr

24import Idris.Parser.Helpers

17import Idris.Parser.Helpers

25import Idris.Parser.Ops

18import Idris.Parser.Ops

26−import Idris.Parser.Expr

27−import Idris.DSL

28

19

29−import Idris.Core.TT

20+import Prelude hiding (pi)

30−import Idris.Core.Evaluate

31−

32−import Idris.Docstrings

33

21

34import Control.Applicative

22import Control.Applicative

35import Control.Monad

23import Control.Monad

36import Control.Monad.State.Strict

24import Control.Monad.State.Strict

37−

38−import Data.Maybe

39−import qualified Data.List.Split as Spl

25+import qualified Data.ByteString.UTF8 as UTF8

40−import Data.List

41−import Data.Monoid

42−import Data.Char

26+import Data.Char

43import qualified Data.HashSet as HS

27import qualified Data.HashSet as HS

28+import Data.List

29+import qualified Data.List.Split as Spl

30+import Data.Maybe

31+import Data.Monoid

44import qualified Data.Text as T

32import qualified Data.Text as T

45−import qualified Data.ByteString.UTF8 as UTF8

46−

47import Debug.Trace

33import Debug.Trace

34+import qualified Text.Parser.Char as Chr

35+import 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

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

40+ stringLiteral, symbol, whiteSpace)

41+import Text.Trifecta.Delta

48

42

49{- | Parses a record type declaration

43{- | Parses a record type declaration

50Record ::=

44Record ::=

src/Idris/Parser/Expr.hs+6−10

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

9{-# LANGUAGE PatternGuards, TupleSections #-}

10module Idris.Parser.Expr where

11

12+import Idris.AbsSyntax

13+import Idris.Parser.Helpers

14+import Idris.Parser.Ops

15+import Idris.DSL

16+import Idris.Core.TT

17+

12import Prelude hiding (pi)

18import Prelude hiding (pi)

13

19

14import Text.Trifecta.Delta

20import Text.Trifecta.Delta

@@ -18,18 +24,9 @@ import Text.Parser.Expression

18import qualified Text.Parser.Token as Tok

24import qualified Text.Parser.Token as Tok

19import qualified Text.Parser.Char as Chr

25import qualified Text.Parser.Char as Chr

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

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

21−

22−import Idris.AbsSyntax

23−import Idris.Parser.Helpers

24−import Idris.Parser.Ops

25−import Idris.DSL

26−

27−import Idris.Core.TT

28−

29import Control.Applicative

27import Control.Applicative

30import Control.Monad

28import Control.Monad

31import Control.Monad.State.Strict

29import Control.Monad.State.Strict

32−

33import Data.Function (on)

30import Data.Function (on)

34import Data.Maybe

31import Data.Maybe

35import qualified Data.List.Split as Spl

32import qualified Data.List.Split as Spl

@@ -39,7 +36,6 @@ import Data.Char

39import qualified Data.HashSet as HS

36import qualified Data.HashSet as HS

40import qualified Data.Text as T

37import qualified Data.Text as T

41import qualified Data.ByteString.UTF8 as UTF8

38import qualified Data.ByteString.UTF8 as UTF8

42−

43import Debug.Trace

39import Debug.Trace

44

40

45-- | Allow implicit type declarations

41-- | Allow implicit type declarations

src/Idris/Parser/Helpers.hs+20−24

@@ -5,50 +5,46 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds #-}

8+{-# LANGUAGE CPP, ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,

9−{-# LANGUAGE PatternGuards, StandaloneDeriving #-}

9+ StandaloneDeriving #-}

10#if !(MIN_VERSION_base(4,8,0))

11{-# LANGUAGE OverlappingInstances #-}

12#endif

13module Idris.Parser.Helpers where

14

15−import Prelude hiding (pi)

16−

17−import Text.Trifecta.Delta

18−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

19−import Text.Parser.LookAhead

20−import Text.Parser.Expression

21−import qualified Text.Parser.Token as Tok

22−import qualified Text.Parser.Char as Chr

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

24−

25import Idris.AbsSyntax

15import Idris.AbsSyntax

26−

27−import Idris.Core.TT

28import Idris.Core.Evaluate

16import Idris.Core.Evaluate

17+import Idris.Core.TT

29import Idris.Delaborate (pprintErr)

18import Idris.Delaborate (pprintErr)

30import Idris.Docstrings

19import Idris.Docstrings

31import Idris.Output (iWarn)

20import Idris.Output (iWarn)

32

21

33import qualified Util.Pretty as Pretty (text)

22import qualified Util.Pretty as Pretty (text)

34

23

24+import Prelude hiding (pi)

25+

35import Control.Applicative

26import Control.Applicative

36import Control.Monad

27import Control.Monad

37import Control.Monad.State.Strict

28import Control.Monad.State.Strict

38−

39−import Data.Maybe

40−import qualified Data.List.Split as Spl

29+import qualified Data.ByteString.UTF8 as UTF8

41−import Data.List

42−import Data.Monoid

43import Data.Char

30import Data.Char

44−import qualified Data.Map as M

45import qualified Data.HashSet as HS

31import qualified Data.HashSet as HS

32+import Data.List

33+import qualified Data.List.Split as Spl

34+import qualified Data.Map as M

35+import Data.Maybe

36+import Data.Monoid

46import qualified Data.Text as T

37import qualified Data.Text as T

47−import qualified Data.ByteString.UTF8 as UTF8

48−

49−import System.FilePath

50−

51import Debug.Trace

38import Debug.Trace

39+import System.FilePath

40+import qualified Text.Parser.Char as Chr

41+import Text.Parser.Expression

42+import Text.Parser.LookAhead

43+import qualified Text.Parser.Token as Tok

44+import qualified Text.Parser.Token.Highlight as Hi

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

46+ stringLiteral, symbol, whiteSpace)

47+import Text.Trifecta.Delta

52

48

53-- | Idris parser with state used during parsing

49-- | Idris parser with state used during parsing

54type IdrisParser = StateT IState IdrisInnerParser

50type IdrisParser = StateT IState IdrisInnerParser

src/Idris/Parser/Ops.hs+16−19

@@ -5,38 +5,35 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

8+{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}

9module Idris.Parser.Ops where

10

11−import Prelude hiding (pi)

12−

13−import Text.Trifecta.Delta

14−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

15−import Text.Parser.LookAhead

16−import Text.Parser.Expression

17−import qualified Text.Parser.Token as Tok

18−import qualified Text.Parser.Char as Chr

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

20−

21import Idris.AbsSyntax

11import Idris.AbsSyntax

12+import Idris.Core.TT

22import Idris.Parser.Helpers

13import Idris.Parser.Helpers

23

14

24−import Idris.Core.TT

15+import Prelude hiding (pi)

25

16

26import Control.Applicative

17import Control.Applicative

27import Control.Monad

18import Control.Monad

28import Control.Monad.State.Strict

19import Control.Monad.State.Strict

29−

30−import Data.Maybe

31−import qualified Data.List.Split as Spl

20+import qualified Data.ByteString.UTF8 as UTF8

32−import Data.List

33−import Data.Monoid

34import Data.Char

21import Data.Char

35import qualified Data.HashSet as HS

22import qualified Data.HashSet as HS

23+import Data.List

24+import qualified Data.List.Split as Spl

25+import Data.Maybe

26+import Data.Monoid

36import qualified Data.Text as T

27import qualified Data.Text as T

37−import qualified Data.ByteString.UTF8 as UTF8

38−

39import Debug.Trace

28import Debug.Trace

29+import qualified Text.Parser.Char as Chr

30+import Text.Parser.Expression

31+import Text.Parser.LookAhead

32+import qualified Text.Parser.Token as Tok

33+import qualified Text.Parser.Token.Highlight as Hi

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

35+ stringLiteral, symbol, whiteSpace)

36+import Text.Trifecta.Delta

40

37

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

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

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

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

src/Idris/PartialEval.hs+3−4

@@ -14,14 +14,13 @@ module Idris.PartialEval(

14 ) where

15

16import Idris.AbsSyntax

17−import Idris.Delaborate

18−

19−import Idris.Core.TT

20import Idris.Core.CaseTree

17import Idris.Core.CaseTree

21import Idris.Core.Evaluate

18import Idris.Core.Evaluate

19+import Idris.Core.TT

20+import Idris.Delaborate

22

21

23−import Control.Monad.State

24import Control.Applicative

22import Control.Applicative

23+import Control.Monad.State

25import Data.Maybe

24import Data.Maybe

26import Debug.Trace

25import Debug.Trace

27

26

src/Idris/Primitives.hs+5−7

@@ -5,23 +5,21 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}

8+{-# LANGUAGE PatternGuards, RankNTypes, ScopedTypeVariables #-}

9

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

11

12import Idris.AbsSyntax

13−

13+import Idris.Core.Evaluate

14+import Idris.Core.TT

14import IRTS.Lang

15import IRTS.Lang

15

16

16−import Idris.Core.TT

17−import Idris.Core.Evaluate

18import Data.Bits

17import Data.Bits

19−import Data.Word

20−import Data.Int

21import Data.Char

18import Data.Char

22import Data.Function (on)

19import Data.Function (on)

20+import Data.Int

23import qualified Data.Vector.Unboxed as V

21import qualified Data.Vector.Unboxed as V

24−

22+import Data.Word

25import Debug.Trace

23import Debug.Trace

26

24

27data Prim = Prim { p_name :: Name,

25data Prim = Prim { p_name :: Name,

src/Idris/ProofSearch.hs+5−6

@@ -15,22 +15,21 @@ module Idris.ProofSearch(

15 , resolveTC

16 ) where

17

18+import Idris.AbsSyntax

19+import Idris.Core.CaseTree

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

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

19−import Idris.Core.TT

20−import Idris.Core.Unify

21import Idris.Core.Evaluate

22−import Idris.Core.CaseTree

22+import Idris.Core.TT

23import Idris.Core.Typecheck

24−

25−import Idris.AbsSyntax

24+import Idris.Core.Unify

26import Idris.Delaborate

25import Idris.Delaborate

27import Idris.Error

26import Idris.Error

28

27

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

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

30import Control.Monad

29import Control.Monad

31import Control.Monad.State.Strict

30import Control.Monad.State.Strict

32−import qualified Data.Set as S

33import Data.List

31import Data.List

32+import qualified Data.Set as S

34import Debug.Trace

33import Debug.Trace

35

34

36-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

35-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

src/Idris/Prover.hs+20−24

@@ -10,45 +10,41 @@ module Idris.Prover (prover, showProof, showRunElab) where

10

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

13−import Prelude (Eq(..), Show(..),

14− Bool(..), Either(..), Maybe(..), String,

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

15− (.), ($), (++), (||), (&&),

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

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

17− length, lines, map, not, null, repeat, reverse, tail, zip)

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

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

18

17

18+import Idris.AbsSyntax

19+import Idris.AbsSyntaxTree

20+import Idris.Completion

21+import Idris.Core.CaseTree

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

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

20−import Idris.Core.TT

21import Idris.Core.Evaluate

23import Idris.Core.Evaluate

22−import Idris.Core.CaseTree

24+import Idris.Core.TT

23import Idris.Core.Typecheck

25import Idris.Core.Typecheck

24−

26+import Idris.DataOpts

27+import Idris.Delaborate

28+import Idris.Docs (getDocs, pprintConstDocs, pprintDocs)

29+import Idris.Elab.Term

25import Idris.Elab.Utils

30import Idris.Elab.Utils

26import Idris.Elab.Value

31import Idris.Elab.Value

27−import Idris.Elab.Term

28−

29−import Idris.AbsSyntax

30−import Idris.AbsSyntaxTree

31−import Idris.Delaborate

32−import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)

33import Idris.ElabDecls

32import Idris.ElabDecls

34−import Idris.Parser hiding (params)

35import Idris.Error

33import Idris.Error

36−import Idris.DataOpts

37−import Idris.Completion

38import qualified Idris.IdeMode as IdeMode

34import qualified Idris.IdeMode as IdeMode

39import Idris.Output

35import Idris.Output

36+import Idris.Parser hiding (params)

40import Idris.TypeSearch (searchByType)

37import Idris.TypeSearch (searchByType)

41

38

42−import Text.Trifecta.Result(Result(..), ErrInfo(..))

39+import Util.Pretty

43

40

44−import System.IO (Handle, stdin, stdout, hPutStrLn)

45−import System.Console.Haskeline

46−import System.Console.Haskeline.History

47−import Control.Monad.State.Strict

48import Control.DeepSeq

41import Control.DeepSeq

49−

42+import Control.Monad.State.Strict

50−import Util.Pretty

51import Debug.Trace

43import Debug.Trace

44+import System.Console.Haskeline

45+import System.Console.Haskeline.History

46+import System.IO (Handle, hPutStrLn, stdin, stdout)

47+import Text.Trifecta.Result (ErrInfo(..), Result(..))

52

48

53-- | Launch the proof shell

49-- | Launch the proof shell

54prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

50prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

src/Idris/Providers.hs+3−3

@@ -5,17 +5,17 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, DeriveFunctor #-}

8+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

9module Idris.Providers (

10 providerTy

11 , getProvided

12 , Provided(..)

13 ) where

14

15−import Idris.Core.TT

16−import Idris.Core.Evaluate

17import Idris.AbsSyntax

15import Idris.AbsSyntax

18import Idris.AbsSyntaxTree

16import Idris.AbsSyntaxTree

17+import Idris.Core.Evaluate

18+import Idris.Core.TT

19import Idris.Error

20

21-- | Wrap a type provider in the type of type providers

src/Idris/REPL.hs+56−69

@@ -4,8 +4,8 @@ Description : Entry Point for the Idris REPL and CLI.

4License : BSD3

5Maintainer : The Idris Community.

6-}

7−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

7+{-# LANGUAGE CPP, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

8− PatternGuards, CPP #-}

8+ PatternGuards #-}

9module Idris.REPL

10 ( idemodeStart

11 , startServer

@@ -17,97 +17,84 @@ module Idris.REPL

17 ) where

18

19import Idris.AbsSyntax

20−import Idris.ASTUtils

21import Idris.Apropos (apropos, aproposModules)

20import Idris.Apropos (apropos, aproposModules)

22−import Idris.REPL.Parser

21+import Idris.ASTUtils

22+import Idris.Colours hiding (colourise)

23+import Idris.Completion

24+import Idris.Core.Constraints

25+import Idris.Core.Evaluate

26+import Idris.Core.Execute (execute)

27+import Idris.Core.TT

28+import Idris.Core.Unify

29+import Idris.Core.WHNF

30+import Idris.Coverage

31+import Idris.Delaborate

32+import Idris.Docs hiding (Doc)

33+import Idris.Docstrings (overview, renderDocTerm, renderDocstring)

34+import Idris.Elab.Clause

35+import Idris.Elab.Term

36+import Idris.Elab.Value

37+import Idris.ElabDecls

23import Idris.Error

38import Idris.Error

24−import Idris.IBC

25import Idris.ErrReverse

39import Idris.ErrReverse

26−import Idris.Delaborate

27−import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

28import Idris.Help

40import Idris.Help

29−import Idris.IdrisDoc

41+import Idris.IBC

30−import Idris.Prover

31−import Idris.Parser hiding (indent)

32−import Idris.Coverage

33−import Idris.Docs hiding (Doc)

34−import Idris.Completion

35import qualified Idris.IdeMode as IdeMode

42import qualified Idris.IdeMode as IdeMode

36−import Idris.Colours hiding (colourise)

43+import Idris.IdrisDoc

44+import Idris.Info

37import Idris.Inliner

45import Idris.Inliner

38−import Idris.Output

39import Idris.Interactive

46import Idris.Interactive

40−import Idris.WhoCalls

47+import Idris.ModeCommon

41−import Idris.TypeSearch (searchByType)

48+import Idris.Output

42−

49+import Idris.Parser hiding (indent)

50+import Idris.Prover

43import Idris.REPL.Browse (namesInNS, namespacesInNS)

51import Idris.REPL.Browse (namesInNS, namespacesInNS)

44import Idris.REPL.Commands

52import Idris.REPL.Commands

53+import Idris.REPL.Parser

54+import Idris.TypeSearch (searchByType)

55+import Idris.WhoCalls

56+import IRTS.Compiler

45

57

46−import Idris.ElabDecls

47−import Idris.Elab.Clause

48−import Idris.Elab.Value

49−import Idris.Elab.Term

50−import Idris.ModeCommon

51−import Idris.Info

52−

53−import Version_idris (gitHash)

54−import Util.System

55import Util.DynamicLinker

58import Util.DynamicLinker

56import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

59import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

57import Util.Pretty hiding ((</>))

60import Util.Pretty hiding ((</>))

61+import Util.System

58

62

59−import Idris.Core.Evaluate

63+import Version_idris (gitHash)

60−import Idris.Core.Execute (execute)

61−import Idris.Core.TT

62−import Idris.Core.Unify

63−import Idris.Core.WHNF

64−import Idris.Core.Constraints

65

64

66−import IRTS.Compiler

65+import Prelude hiding (id, (.), (<$>))

67

66

68import Control.Category

67import Control.Category

68+import Control.Concurrent

69+import Control.Concurrent.Async (race)

70+import Control.Concurrent.MVar

71+import Control.DeepSeq

69import qualified Control.Exception as X

72import qualified Control.Exception as X

70−import Prelude hiding ((<$>), (.), id)

71−import Data.List.Split (splitOn)

72−import qualified Data.Text as T

73−

74−import Text.Trifecta.Result(Result(..), ErrInfo(..))

75−

76−import System.Console.Haskeline as H

77−import System.FilePath

78− ( (</>)

79− , (<.>)

80− , splitExtension

81− , addExtension

82− , dropExtension

83− , takeExtension

84− , takeDirectory

85− )

86−import System.Exit

87−import System.Environment

88−import System.Process

89−import System.Directory

90−import System.IO

91import Control.Monad

73import Control.Monad

74+import Control.Monad.Trans (lift)

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

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

93−import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )

76+import Control.Monad.Trans.State.Strict (StateT, evalStateT, execStateT, get,

94−import Control.Monad.Trans ( lift )

77+ put)

95−import Control.Concurrent.MVar

96−import Network

97−import Control.Concurrent

98−import Data.Maybe

99−import Data.List hiding (group)

100import Data.Char

78import Data.Char

79+import Data.Either (partitionEithers)

80+import Data.List hiding (group)

81+import Data.List.Split (splitOn)

82+import Data.Maybe

101import qualified Data.Set as S

83import qualified Data.Set as S

84+import qualified Data.Text as T

102import Data.Version

85import Data.Version

103−import Data.Either (partitionEithers)

86+import Network

104−import Control.DeepSeq

87+import System.Console.Haskeline as H

105−

88+import System.Directory

106−import Control.Concurrent.Async (race)

89+import System.Environment

90+import System.Exit

91+import System.FilePath (addExtension, dropExtension, splitExtension,

92+ takeDirectory, takeExtension, (<.>), (</>))

107−import System.FSNotify (withManager, watchDir)

93+import System.FSNotify (watchDir, withManager)

108import System.FSNotify.Devel (allEvents, doAllEvents)

94import System.FSNotify.Devel (allEvents, doAllEvents)

109−

95+import System.IO

110−

96+import System.Process

97+import Text.Trifecta.Result (ErrInfo(..), Result(..))

111

98

112-- | Run the REPL

99-- | Run the REPL

113repl :: IState -- ^ The initial state

100repl :: IState -- ^ The initial state

src/Idris/REPL/Browse.hs+6−7

@@ -10,18 +10,17 @@ Maintainer : The Idris Community.

10

11module Idris.REPL.Browse (namespacesInNS, namesInNS) where

12

13−import Control.Monad (filterM)

13+import Idris.AbsSyntax (getContext)

14+import Idris.AbsSyntaxTree (Idris)

15+import Idris.Core.Evaluate (Accessibility(Hidden, Private), ctxtAlist,

16+ lookupDefAccExact)

17+import Idris.Core.TT (Name(..))

14

18

19+import Control.Monad (filterM)

15import Data.List (isSuffixOf, nub)

20import Data.List (isSuffixOf, nub)

16import Data.Maybe (mapMaybe)

21import Data.Maybe (mapMaybe)

17import qualified Data.Text as T (unpack)

22import qualified Data.Text as T (unpack)

18

23

19−import Idris.Core.Evaluate (ctxtAlist, Accessibility(Private, Hidden), lookupDefAccExact)

20−import Idris.Core.TT (Name(..))

21−

22−import Idris.AbsSyntaxTree (Idris)

23−import Idris.AbsSyntax (getContext)

24−

25-- | Find the sub-namespaces of a given namespace. The components

24-- | Find the sub-namespaces of a given namespace. The components

26-- should be in display order rather than the order that they are in

25-- should be in display order rather than the order that they are in

27-- inside of NS constructors.

26-- inside of NS constructors.

src/Idris/REPL/Commands.hs+2−2

@@ -1,8 +1,8 @@

1module Idris.REPL.Commands where

2

3−import Idris.Core.TT

4−import Idris.Colours

5import Idris.AbsSyntaxTree

3import Idris.AbsSyntaxTree

4+import Idris.Colours

5+import Idris.Core.TT

6

7-- | REPL commands

8data Command = Quit

src/Idris/REPL/Parser.hs+38−42

@@ -11,31 +11,27 @@ module Idris.REPL.Parser (

11 , setOptions

12 ) where

13

14−import System.FilePath ((</>))

15−import System.Console.ANSI (Color(..))

16−

17−import Idris.Colours

18import Idris.AbsSyntax

14import Idris.AbsSyntax

15+import Idris.Colours

19import Idris.Core.TT

16import Idris.Core.TT

20import Idris.Help

17import Idris.Help

21import qualified Idris.Parser as P

18import qualified Idris.Parser as P

22−

23import Idris.REPL.Commands

19import Idris.REPL.Commands

24

20

25import Control.Applicative

21import Control.Applicative

26import Control.Monad.State.Strict

22import Control.Monad.State.Strict

27−

23+import qualified Data.ByteString.UTF8 as UTF8

24+import Data.Char (isSpace, toLower)

25+import Data.List

26+import Data.List.Split (splitOn)

27+import Debug.Trace

28+import System.Console.ANSI (Color(..))

29+import System.FilePath ((</>))

30+import Text.Parser.Char (anyChar, oneOf)

28import Text.Parser.Combinators

31import Text.Parser.Combinators

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

30−import Text.Trifecta(Result, parseString)

32+import Text.Trifecta (Result, parseString)

31import Text.Trifecta.Delta

33import Text.Trifecta.Delta

32

34

33−import Debug.Trace

34−import Data.List

35−import Data.List.Split(splitOn)

36−import Data.Char(isSpace, toLower)

37−import qualified Data.ByteString.UTF8 as UTF8

38−

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

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

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

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

41 where trim = f . f

37 where trim = f . f

@@ -214,8 +210,8 @@ cmd xs = try $ do

214noArgs :: Command -> String -> P.IdrisParser (Either String Command)

210noArgs :: Command -> String -> P.IdrisParser (Either String Command)

215noArgs cmd name = do

211noArgs cmd name = do

216 let emptyArgs = do

212 let emptyArgs = do

217− eof

213+ eof

218− return (Right cmd)

214+ return (Right cmd)

219

215

220 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

216 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

221

217

@@ -229,17 +225,17 @@ eval = do

229exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

225exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

230exprArg cmd name = do

226exprArg cmd name = do

231 let noArg = do

227 let noArg = do

232− eof

228+ eof

233− return $ Left ("Usage is :" ++ name ++ " <expression>")

229+ return $ Left ("Usage is :" ++ name ++ " <expression>")

234

230

235 let justOperator = do

231 let justOperator = do

236− (op, fc) <- P.operatorFC

232+ (op, fc) <- P.operatorFC

237− eof

233+ eof

238− return $ Right $ cmd (PRef fc [] (sUN op))

234+ return $ Right $ cmd (PRef fc [] (sUN op))

239

235

240 let properArg = do

236 let properArg = do

241− t <- P.fullExpr defaultSyntax

237+ t <- P.fullExpr defaultSyntax

242− return $ Right (cmd t)

238+ return $ Right (cmd t)

243 try noArg <|> try justOperator <|> properArg

239 try noArg <|> try justOperator <|> properArg

244

240

245

241

@@ -279,10 +275,10 @@ optArg cmd name = do

279 return $ Left ("Usage is :" ++ name ++ " <option>")

275 return $ Left ("Usage is :" ++ name ++ " <option>")

280

276

281 let oneArg = do

277 let oneArg = do

282− o <- pOption

278+ o <- pOption

283− P.whiteSpace

279+ P.whiteSpace

284− eof

280+ eof

285− return (Right (cmd o))

281+ return (Right (cmd o))

286

282

287 let failure = return $ Left "Unrecognized setting"

283 let failure = return $ Left "Unrecognized setting"

288

284

@@ -304,14 +300,14 @@ proofArg cmd name = do

304cmd_doc :: String -> P.IdrisParser (Either String Command)

300cmd_doc :: String -> P.IdrisParser (Either String Command)

305cmd_doc name = do

301cmd_doc name = do

306 let constant = do

302 let constant = do

307− c <- fmap fst P.constant

303+ c <- fmap fst P.constant

308− eof

304+ eof

309− return $ Right (DocStr (Right c) FullDocs)

305+ return $ Right (DocStr (Right c) FullDocs)

310

306

311 let pType = do

307 let pType = do

312− P.reserved "Type"

308+ P.reserved "Type"

313− eof

309+ eof

314− return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

310+ return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

315

311

316 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

312 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

317

313

@@ -380,17 +376,17 @@ cmd_compile name = do

380 bytecodeCodegen <|> viaCodegen

376 bytecodeCodegen <|> viaCodegen

381

377

382 let hasOneArg = do

378 let hasOneArg = do

383− i <- get

379+ i <- get

384− f <- fst <$> P.identifier

380+ f <- fst <$> P.identifier

385− eof

381+ eof

386− return $ Right (Compile defaultCodegen f)

382+ return $ Right (Compile defaultCodegen f)

387

383

388 let hasTwoArgs = do

384 let hasTwoArgs = do

389− i <- get

385+ i <- get

390− codegen <- codegenOption

386+ codegen <- codegenOption

391− f <- fst <$> P.identifier

387+ f <- fst <$> P.identifier

392− eof

388+ eof

393− return $ Right (Compile codegen f)

389+ return $ Right (Compile codegen f)

394

390

395 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

391 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

396 try hasTwoArgs <|> try hasOneArg <|> failure

392 try hasTwoArgs <|> try hasOneArg <|> failure

src/Idris/Reflection.hs+15−15

@@ -6,31 +6,31 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8

9−{-# LANGUAGE PatternGuards, CPP #-}

9+{-# LANGUAGE CPP, PatternGuards #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

11module Idris.Reflection where

12

13−#if __GLASGOW_HASKELL__ < 710

14−import Control.Applicative ((<$>), (<*>), pure)

15−import Prelude hiding (mapM)

16−import Data.Traversable (mapM)

17−#endif

18−import Control.Monad (liftM, liftM2, liftM4)

19−import Control.Monad.State.Strict (lift)

20−import Data.Maybe (catMaybes)

21−import Data.List ((\\), findIndex)

22−import qualified Data.Text as T

23−

24import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

13import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

25 movelast, runElab, solve)

14 movelast, runElab, solve)

26−import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

15+import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact,

16+ lookupTyExact)

27import Idris.Core.TT

17import Idris.Core.TT

28

18

29−import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),

19+import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatypes, idris_implicits, idris_patdefs, tt_ctxt),

30− PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

20+ PArg, PArg'(..), PTactic, PTactic'(..), PTerm(..),

31 initEState, pairCon, pairTy)

21 initEState, pairCon, pairTy)

32import Idris.Delaborate (delab)

22import Idris.Delaborate (delab)

33

23

24+#if __GLASGOW_HASKELL__ < 710

25+import Control.Applicative (pure, (<$>), (<*>))

26+import Data.Traversable (mapM)

27+import Prelude hiding (mapM)

28+#endif

29+import Control.Monad (liftM, liftM2, liftM4)

30+import Control.Monad.State.Strict (lift)

31+import Data.List (findIndex, (\\))

32+import Data.Maybe (catMaybes)

33+import qualified Data.Text as T

34

35data RErasure = RErased | RNotErased deriving Show

36

src/Idris/TypeSearch.hs+31−28

@@ -13,38 +13,41 @@ module Idris.TypeSearch (

13 , defaultScoreFunction

14 ) where

15

16−import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))

17−import Control.Arrow (first, second, (&&&), (***))

18−import Control.Monad (when, guard)

19−

20−import Data.List (find, partition, (\\))

21−import Data.Map (Map)

22−import qualified Data.Map as M

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

24−import Data.Monoid (Monoid (mempty, mappend))

25−import Data.Ord (comparing)

26−import qualified Data.PriorityQueue.FingerTree as Q

27−import Data.Set (Set)

28−import qualified Data.Set as S

29−import qualified Data.Text as T (pack, isPrefixOf)

30−import Data.Traversable (traverse)

31−

32−import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

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

33−import Idris.AbsSyntaxTree (interface_implementations, InterfaceInfo, defaultSyntax, eqTy, Idris

17+ logLvl, putIState)

34− , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode),

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

35− implicitAllowed, OutputMode(..), PTerm, toplevel)

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

20+ defaultSyntax, eqTy, implicitAllowed,

21+ interface_implementations, toplevel)

36−import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

22+import Idris.Core.Evaluate (Context(definitions), Def(CaseOp, Function, TyDecl),

23+ normaliseC)

37−import Idris.Core.TT hiding (score)

24+import Idris.Core.TT hiding (score)

38−import Idris.Core.Unify (match_unify)

25+import Idris.Core.Unify (match_unify)

39−import Idris.Delaborate (delabTy)

26+import Idris.Delaborate (delabTy)

40−import Idris.Docstrings (noDocs, overview)

27+import Idris.Docstrings (noDocs, overview)

41−import Idris.Elab.Type (elabType)

28+import Idris.Elab.Type (elabType)

42−import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)

43import Idris.IBC

29import Idris.IBC

30+import Idris.Output (iPrintResult, iRenderError, iRenderOutput, iRenderResult,

31+ iputStrLn, prettyDocumentedIst)

32+

33+import Util.Pretty (Doc, annotate, char, text, vsep, (<>))

44

34

45import Prelude hiding (pred)

35import Prelude hiding (pred)

46

36

47−import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

37+import Control.Applicative (Applicative(..), (<$>), (<*>), (<|>))

38+import Control.Arrow (first, second, (&&&), (***))

39+import Control.Monad (guard, when)

40+import Data.List (find, partition, (\\))

41+import Data.Map (Map)

42+import qualified Data.Map as M

43+import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe, maybeToList)

44+import Data.Monoid (Monoid(mappend, mempty))

45+import Data.Ord (comparing)

46+import qualified Data.PriorityQueue.FingerTree as Q

47+import Data.Set (Set)

48+import qualified Data.Set as S

49+import qualified Data.Text as T (isPrefixOf, pack)

50+import Data.Traversable (traverse)

48

51

49searchByType :: [String] -> PTerm -> Idris ()

52searchByType :: [String] -> PTerm -> Idris ()

50searchByType pkgs pterm = do

53searchByType pkgs pterm = do

src/Idris/Unlit.hs+1

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

8module Idris.Unlit(unlit) where

9

10import Idris.Core.TT

11+

11import Data.Char

12import Data.Char

12

13

13unlit :: FilePath -> String -> TC String

14unlit :: FilePath -> String -> TC String

src/Idris/WhoCalls.hs−2

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

8module Idris.WhoCalls (whoCalls, callsWho) where

9

10import Idris.AbsSyntax

11−

12import Idris.Core.CaseTree

11import Idris.Core.CaseTree

13import Idris.Core.Evaluate

12import Idris.Core.Evaluate

14import Idris.Core.TT

13import Idris.Core.TT

15

14

16import Data.List (nub)

15import Data.List (nub)

17

16

18−

19occurs :: Name -> Term -> Bool

17occurs :: Name -> Term -> Bool

20occurs n (P Bound _ _) = False

18occurs n (P Bound _ _) = False

21occurs n (P _ n' _) = n == n'

19occurs n (P _ n' _) = n == n'

src/Util/DynamicLinker.hs+7−7

@@ -5,7 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE ExistentialQuantification, CPP, ScopedTypeVariables #-}

8+{-# LANGUAGE CPP, ExistentialQuantification, ScopedTypeVariables #-}

9module Util.DynamicLinker ( ForeignFun(..)

10 , DynamicLib(..)

11 , tryLoadLib

@@ -14,21 +14,21 @@ module Util.DynamicLinker ( ForeignFun(..)

14

15#ifdef IDRIS_FFI

16import Foreign.LibFFI

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

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

18import System.Directory

19#ifndef mingw32_HOST_OS

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

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

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

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

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

23import Data.Maybe (catMaybes)

24−import System.Posix.DynamicLinker

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

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

25+import System.Posix.DynamicLinker

26import Text.Regex.TDFA

27#else

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

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

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

29import System.Win32.DLL

30import System.Win32.DLL

30import System.Win32.Types

31import System.Win32.Types

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

32type DL = HMODULE

33#endif

34

src/Util/Net.hs+2−2

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

7-}

8module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where

9

10+import Control.Exception (bracketOnError)

10import Network hiding (socketPort)

11import Network hiding (socketPort)

11−import Network.Socket hiding (sClose)

12import Network.BSD (getProtocolNumber)

13−import Control.Exception (bracketOnError)

13+import Network.Socket hiding (sClose)

14

15-- Copied from upstream impl of listenOn

16-- bound to localhost interface instead of iNADDR_ANY

src/Util/System.hs+7−12

@@ -22,25 +22,20 @@ import Control.Exception as CE

22import Control.Monad (when)

23import qualified Data.Text as T

24import qualified Data.Text.IO as TIO

25−

26import Foreign.C

25import Foreign.C

27−

28−import System.Directory (getTemporaryDirectory

26+import System.Directory (createDirectoryIfMissing, getTemporaryDirectory,

29− , removeFile

27+ removeDirectoryRecursive, removeFile)

30− , removeDirectoryRecursive

31− , createDirectoryIfMissing

32− )

33−import System.FilePath ((</>), normalise)

28+import System.FilePath (normalise, (</>))

34−import System.IO

35import System.Info

29import System.Info

30+import System.IO

36import System.IO.Error

31import System.IO.Error

37

32

38#ifdef FREESTANDING

33#ifdef FREESTANDING

39−import Tools_idris

40import Data.List (intercalate)

34import Data.List (intercalate)

41−import System.FilePath (isAbsolute, dropFileName, searchPathSeparator)

42import System.Directory (doesDirectoryExist)

35import System.Directory (doesDirectoryExist)

43−import System.Environment (getEnv, setEnv, getExecutablePath)

36+import System.Environment (getEnv, getExecutablePath, setEnv)

37+import System.FilePath (dropFileName, isAbsolute, searchPathSeparator)

38+import Tools_idris

44#endif

39#endif

45

40

46catchIO :: IO a -> (IOError -> IO a) -> IO a

41catchIO :: IO a -> (IOError -> IO a) -> IO a

test/TestRun.hs+10−11

@@ -1,27 +1,26 @@

1module Main where

2

3+import TestData

4+

3import Control.Monad

5import Control.Monad

4import Data.Char (isLetter)

6import Data.Char (isLetter)

5−import Data.Typeable

6−import Data.Proxy

7−import Data.List

8import qualified Data.IntMap as IMap

7import qualified Data.IntMap as IMap

9−

8+import Data.List

9+import Data.Proxy

10+import Data.Typeable

11+import Options.Applicative

10import System.Directory

12import System.Directory

11import System.Environment

13import System.Environment

12import System.Exit

14import System.Exit

13−import System.Process

15+import System.FilePath ((</>))

14import System.Info

16import System.Info

15import System.IO

17import System.IO

16−import System.FilePath ((</>))

18+import System.Process

17−import Options.Applicative

18import Test.Tasty

19import Test.Tasty

19import Test.Tasty.Golden

20import Test.Tasty.Golden

20−import Test.Tasty.Runners

21−import Test.Tasty.Options

22import Test.Tasty.Ingredients.Rerun

21import Test.Tasty.Ingredients.Rerun

23−

22+import Test.Tasty.Options

24−import TestData

23+import Test.Tasty.Runners

25

24

26--------------------------------------------------------------------- [ Config ]

25--------------------------------------------------------------------- [ Config ]

27

26