1e044ff · Idris-dev · git.iko.soy

codegen/idris-codegen-c/Main.hs+1

compare with master

unifiedsplit

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

4import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7+import Idris.Options

7import IRTS.CodegenC

8import IRTS.CodegenC

8import IRTS.Compiler

9import IRTS.Compiler

9

10

codegen/idris-codegen-javascript/Main.hs+1

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

4import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7+import Idris.Options

7import IRTS.CodegenJavaScript

8import IRTS.CodegenJavaScript

8import IRTS.Compiler

9import IRTS.Compiler

9

10

codegen/idris-codegen-node/Main.hs+1

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

4import Idris.Core.TT

5import Idris.ElabDecls

6import Idris.Main

7+import Idris.Options

7import IRTS.CodegenJavaScript

8import IRTS.CodegenJavaScript

8import IRTS.Compiler

9import IRTS.Compiler

9

10

idris.cabal+1

@@ -196,6 +196,7 @@ Library

196 , Idris.Output

197 , Idris.Main

198 , Idris.ModeCommon

199+ , Idris.Options

199 , Idris.Parser

200 , Idris.Parser

200 , Idris.Parser.Helpers

201 , Idris.Parser.Helpers

201 , Idris.Parser.Ops

202 , Idris.Parser.Ops

main/Main.hs+1

@@ -11,6 +11,7 @@ import Idris.CmdOptions

11import Idris.Error

12import Idris.Info.Show

13import Idris.Main

14+import Idris.Options

14import Idris.Package

15import Idris.Package

15

16

16import Util.System (setupBundledCC)

17import Util.System (setupBundledCC)

src/IRTS/Compiler.hs+1

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

17import Idris.Core.TT

18import Idris.Erasure

19import Idris.Error

20+import Idris.Options

20import Idris.Output

21import Idris.Output

21import IRTS.CodegenC

22import IRTS.CodegenC

22import IRTS.CodegenCommon

23import IRTS.CodegenCommon

src/Idris/ASTUtils.hs+1

@@ -48,6 +48,7 @@ module Idris.ASTUtils(

48import Idris.AbsSyntaxTree

49import Idris.Core.Evaluate

50import Idris.Core.TT

51+import Idris.Options

51

52

52import Prelude hiding (id, (.))

53import Prelude hiding (id, (.))

53

54

src/Idris/AbsSyntax.hs+2−123

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

19import Idris.Core.TT

20import Idris.Docstrings

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

22+import Idris.Options

22import IRTS.CodegenCommon

23import IRTS.CodegenCommon

23

24

24import System.Directory (canonicalizePath, doesFileExist)

25import System.Directory (canonicalizePath, doesFileExist)

@@ -2602,126 +2603,4 @@ mkUniqueNames env shadows tm

2602

2603

2603 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2604 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2604

2605

2605−getFile :: Opt -> Maybe String

2606+

2606−getFile (Filename s) = Just s

2607−getFile _ = Nothing

2608−

2609−getBC :: Opt -> Maybe String

2610−getBC (BCAsm s) = Just s

2611−getBC _ = Nothing

2612−

2613−getOutput :: Opt -> Maybe String

2614−getOutput (Output s) = Just s

2615−getOutput _ = Nothing

2616−

2617−getIBCSubDir :: Opt -> Maybe String

2618−getIBCSubDir (IBCSubDir s) = Just s

2619−getIBCSubDir _ = Nothing

2620−

2621−getImportDir :: Opt -> Maybe String

2622−getImportDir (ImportDir s) = Just s

2623−getImportDir _ = Nothing

2624−

2625−getSourceDir :: Opt -> Maybe String

2626−getSourceDir (SourceDir s) = Just s

2627−getSourceDir _ = Nothing

2628−

2629−getPkgDir :: Opt -> Maybe String

2630−getPkgDir (Pkg s) = Just s

2631−getPkgDir _ = Nothing

2632−

2633−getPkg :: Opt -> Maybe (Bool, String)

2634−getPkg (PkgBuild s) = Just (False, s)

2635−getPkg (PkgInstall s) = Just (True, s)

2636−getPkg _ = Nothing

2637−

2638−getPkgClean :: Opt -> Maybe String

2639−getPkgClean (PkgClean s) = Just s

2640−getPkgClean _ = Nothing

2641−

2642−getPkgREPL :: Opt -> Maybe String

2643−getPkgREPL (PkgREPL s) = Just s

2644−getPkgREPL _ = Nothing

2645−

2646−getPkgCheck :: Opt -> Maybe String

2647−getPkgCheck (PkgCheck s) = Just s

2648−getPkgCheck _ = Nothing

2649−

2650−-- | Returns None if given an Opt which is not PkgMkDoc

2651−-- Otherwise returns Just x, where x is the contents of PkgMkDoc

2652−getPkgMkDoc :: Opt -- ^ Opt to extract

2653− -> Maybe (Bool, String) -- ^ Result

2654−getPkgMkDoc (PkgDocBuild str) = Just (False,str)

2655−getPkgMkDoc (PkgDocInstall str) = Just (True,str)

2656−getPkgMkDoc _ = Nothing

2657−

2658−getPkgTest :: Opt -- ^ the option to extract

2659− -> Maybe String -- ^ the package file to test

2660−getPkgTest (PkgTest f) = Just f

2661−getPkgTest _ = Nothing

2662−

2663−getCodegen :: Opt -> Maybe Codegen

2664−getCodegen (UseCodegen x) = Just x

2665−getCodegen _ = Nothing

2666−

2667−getCodegenArgs :: Opt -> Maybe String

2668−getCodegenArgs (CodegenArgs args) = Just args

2669−getCodegenArgs _ = Nothing

2670−

2671−getConsoleWidth :: Opt -> Maybe ConsoleWidth

2672−getConsoleWidth (UseConsoleWidth x) = Just x

2673−getConsoleWidth _ = Nothing

2674−

2675−getExecScript :: Opt -> Maybe String

2676−getExecScript (InterpretScript expr) = Just expr

2677−getExecScript _ = Nothing

2678−

2679−getPkgIndex :: Opt -> Maybe FilePath

2680−getPkgIndex (PkgIndex file) = Just file

2681−getPkgIndex _ = Nothing

2682−

2683−getEvalExpr :: Opt -> Maybe String

2684−getEvalExpr (EvalExpr expr) = Just expr

2685−getEvalExpr _ = Nothing

2686−

2687−getOutputTy :: Opt -> Maybe OutputType

2688−getOutputTy (OutputTy t) = Just t

2689−getOutputTy _ = Nothing

2690−

2691−getLanguageExt :: Opt -> Maybe LanguageExt

2692−getLanguageExt (Extension e) = Just e

2693−getLanguageExt _ = Nothing

2694−

2695−getTriple :: Opt -> Maybe String

2696−getTriple (TargetTriple x) = Just x

2697−getTriple _ = Nothing

2698−

2699−getCPU :: Opt -> Maybe String

2700−getCPU (TargetCPU x) = Just x

2701−getCPU _ = Nothing

2702−

2703−getOptLevel :: Opt -> Maybe Int

2704−getOptLevel (OptLevel x) = Just x

2705−getOptLevel _ = Nothing

2706−

2707−getOptimisation :: Opt -> Maybe (Bool,Optimisation)

2708−getOptimisation (AddOpt p) = Just (True, p)

2709−getOptimisation (RemoveOpt p) = Just (False, p)

2710−getOptimisation _ = Nothing

2711−

2712−getColour :: Opt -> Maybe Bool

2713−getColour (ColourREPL b) = Just b

2714−getColour _ = Nothing

2715−

2716−getClient :: Opt -> Maybe String

2717−getClient (Client x) = Just x

2718−getClient _ = Nothing

2719−

2720−-- Get the first valid port

2721−getPort :: [Opt] -> Maybe REPLPort

2722−getPort [] = Nothing

2723−getPort (Port p : _ ) = Just p

2724−getPort (_ : xs) = getPort xs

2725−

2726−opt :: (Opt -> Maybe a) -> [Opt] -> [a]

2727−opt = mapMaybe

src/Idris/AbsSyntaxTree.hs+3−133

@@ -14,6 +14,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))

14import Idris.Core.Evaluate

15import Idris.Core.TT

16import Idris.Docstrings

17+import Idris.Options

17import IRTS.CodegenCommon

18import IRTS.CodegenCommon

18import IRTS.Lang

19import IRTS.Lang

19import Util.DynamicLinker

20import Util.DynamicLinker

@@ -146,8 +147,7 @@ data PPOption = PPOption {

146 , ppopt_depth :: Maybe Int

147 , ppopt_depth :: Maybe Int

147 } deriving (Show)

148 } deriving (Show)

148

149

149−data Optimisation = PETransform -- ^ partial eval and associated transforms

150+

150− deriving (Show, Eq, Generic)

151

152defaultOptimise :: [Optimisation]

153defaultOptimise = []

@@ -183,21 +183,12 @@ ppOption opt = PPOption {

183ppOptionIst :: IState -> PPOption

184ppOptionIst = ppOption . idris_options

185

186−data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

187− | DSLNotation | ElabReflection | FCReflection

188− | LinearTypes

189− deriving (Show, Eq, Read, Ord, Generic)

190

186

191-- | The output mode in use

187-- | The output mode in use

192data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

188data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

193 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

189 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

194 deriving Show

190 deriving Show

195

191

196−-- | How wide is the console?

197−data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

198− | ColsWide Int -- ^ Manually specified - must be positive

199− | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

200− deriving (Show, Eq, Generic)

201

192

202-- | If a function has no totality annotation, what do we assume?

193-- | If a function has no totality annotation, what do we assume?

203data DefaultTotality = DefaultCheckingTotal -- ^ Total

194data DefaultTotality = DefaultCheckingTotal -- ^ Total

@@ -434,53 +425,7 @@ throwError = Trans.lift . throwE

434

425

435-- Commands in the REPL

426-- Commands in the REPL

436

427

437−data Codegen = Via IRFormat String

438− | Bytecode

439− deriving (Show, Eq, Generic)

440

428

441−data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)

442−

443−data HowMuchDocs = FullDocs | OverviewDocs

444−

445−data OutputFmt = HTMLOutput | LaTeXOutput

446−

447−-- | Recognised logging categories for the Idris compiler.

448−--

449−-- @TODO add in sub categories.

450−data LogCat = IParse

451− | IElab

452− | ICodeGen

453− | IErasure

454− | ICoverage

455− | IIBC

456− deriving (Show, Eq, Ord, Generic)

457−

458−strLogCat :: LogCat -> String

459−strLogCat IParse = "parser"

460−strLogCat IElab = "elab"

461−strLogCat ICodeGen = "codegen"

462−strLogCat IErasure = "erasure"

463−strLogCat ICoverage = "coverage"

464−strLogCat IIBC = "ibc"

465−

466−codegenCats :: [LogCat]

467−codegenCats = [ICodeGen]

468−

469−parserCats :: [LogCat]

470−parserCats = [IParse]

471−

472−elabCats :: [LogCat]

473−elabCats = [IElab]

474−

475−loggingCatsStr :: String

476−loggingCatsStr = unlines

477− [ (strLogCat IParse)

478− , (strLogCat IElab)

479− , (strLogCat ICodeGen)

480− , (strLogCat IErasure)

481− , (strLogCat ICoverage)

482− , (strLogCat IIBC)

483− ]

484

429

485

430

486data ElabShellCmd = EQED

431data ElabShellCmd = EQED

@@ -494,83 +439,8 @@ data ElabShellCmd = EQED

494 | EDocStr (Either Name Const)

439 | EDocStr (Either Name Const)

495 deriving (Show, Eq)

440 deriving (Show, Eq)

496

441

497−data Opt = Filename String

498− | Quiet

499− | NoBanner

500− | ColourREPL Bool

501− | Idemode

502− | IdemodeSocket

503− | IndentWith Int

504− | IndentClause Int

505− | ShowAll

506− | ShowLibs

507− | ShowLibDir

508− | ShowDocDir

509− | ShowIncs

510− | ShowPkgs

511− | ShowLoggingCats

512− | NoBasePkgs

513− | NoPrelude

514− | NoBuiltins -- only for the really primitive stuff!

515− | NoREPL

516− | OLogging Int

517− | OLogCats [LogCat]

518− | Output String

519− | Interface

520− | TypeCase

521− | TypeInType

522− | DefaultTotal

523− | DefaultPartial

524− | WarnPartial

525− | WarnReach

526− | AuditIPkg

527− | EvalTypes

528− | NoCoverage

529− | ErrContext

530− | ShowImpl

531− | Verbose Int

532− | Port REPLPort -- ^ REPL TCP port

533− | IBCSubDir String

534− | ImportDir String

535− | SourceDir String

536− | PkgBuild String

537− | PkgInstall String

538− | PkgClean String

539− | PkgCheck String

540− | PkgREPL String

541− | PkgDocBuild String -- IdrisDoc

542− | PkgDocInstall String

543− | PkgTest String

544− | PkgIndex FilePath

545− | WarnOnly

546− | Pkg String

547− | BCAsm String

548− | DumpDefun String

549− | DumpCases String

550− | UseCodegen Codegen

551− | CodegenArgs String

552− | OutputTy OutputType

553− | Extension LanguageExt

554− | InterpretScript String

555− | EvalExpr String

556− | TargetTriple String

557− | TargetCPU String

558− | OptLevel Int

559− | AddOpt Optimisation

560− | RemoveOpt Optimisation

561− | Client String

562− | ShowOrigErr

563− | AutoWidth -- ^ Automatically adjust terminal width

564− | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

565− | UseConsoleWidth ConsoleWidth

566− | DumpHighlights

567− | DesugarNats

568− | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

569− | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

570− deriving (Show, Eq, Generic)

571

442

572−data REPLPort = DontListen | ListenPort PortNumber

443+

573− deriving (Eq, Generic, Show)

574

444

575-- Parsed declarations

445-- Parsed declarations

576

446

src/Idris/CmdOptions.hs+1−4

@@ -16,11 +16,8 @@ module Idris.CmdOptions

16 , getPkgREPL, getPkgTest, getPort, getIBCSubDir

17 ) where

18

19−import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,

20− getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,

21− getPort, opt)

22−import Idris.AbsSyntaxTree

23import Idris.Info (getIdrisVersion)

19import Idris.Info (getIdrisVersion)

20+import Idris.Options

24import IRTS.CodegenCommon

21import IRTS.CodegenCommon

25

22

26import Control.Monad.Trans (lift)

23import Control.Monad.Trans (lift)

src/Idris/DeepSeq.hs+1

@@ -18,6 +18,7 @@ import Idris.Core.DeepSeq

18import Idris.Core.TT

19import Idris.Docstrings

20import qualified Idris.Docstrings as D

21+import Idris.Options

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

22import IRTS.CodegenCommon (OutputType(..))

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

23import IRTS.Lang (PrimFn(..))

23

24

src/Idris/Docs.hs+2−1

@@ -15,7 +15,7 @@ module Idris.Docs (

15 , FunDoc, FunDoc'(..), Docs, Docs'(..)

16 ) where

17

18−import Idris.AbsSyntax (FixDecl(..), Fixity, HowMuchDocs(..), IState(..), Idris,

18+import Idris.AbsSyntax (FixDecl(..), Fixity, IState(..), Idris,

19 InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),

20 PTerm(..), Plicity(..), RecordInfo(..), basename,

21 getIState, modDocName, ppOptionIst, pprintPTerm,

@@ -26,6 +26,7 @@ import Idris.Delaborate

26import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,

27 nullDocstring, overview, renderDocTerm,

28 renderDocstring)

29+import Idris.Options (HowMuchDocs(..))

29

30

30import Util.Pretty

31import Util.Pretty

31

32

src/Idris/Elab/Clause.hs+1

@@ -31,6 +31,7 @@ import Idris.Elab.Utils

31import Idris.Error

32import Idris.Imports

33import Idris.Inliner

34+import Idris.Options

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

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

35import Idris.PartialEval

36import Idris.PartialEval

36import Idris.Primitives

37import Idris.Primitives

src/Idris/Elab/Provider.hs+1

@@ -30,6 +30,7 @@ import Idris.Elab.Value

30import Idris.Error

31import Idris.Imports

32import Idris.Inliner

33+import Idris.Options

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

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

34import Idris.PartialEval

35import Idris.PartialEval

35import Idris.Primitives

36import Idris.Primitives

src/Idris/Elab/Term.hs+1

@@ -27,6 +27,7 @@ import Idris.Elab.Rewrite

27import Idris.Elab.Utils

28import Idris.Error

29import Idris.ErrReverse (errReverse)

30+import Idris.Options

30import Idris.Output (pshow)

31import Idris.Output (pshow)

31import Idris.ProofSearch

32import Idris.ProofSearch

32import Idris.Reflection

33import Idris.Reflection

src/Idris/Elab/Type.hs+1

@@ -32,6 +32,7 @@ import Idris.Elab.Value

32import Idris.Error

33import Idris.Imports

34import Idris.Inliner

35+import Idris.Options

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

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

36import Idris.PartialEval

37import Idris.PartialEval

37import Idris.Primitives

38import Idris.Primitives

src/Idris/ElabDecls.hs+1

@@ -41,6 +41,7 @@ import Idris.Elab.Value

41import Idris.Error

42import Idris.Imports

43import Idris.Inliner

44+import Idris.Options

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

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

45import Idris.PartialEval

46import Idris.PartialEval

46import Idris.Primitives

47import Idris.Primitives

src/Idris/Erasure.hs+1

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

15import Idris.Core.Evaluate

16import Idris.Core.TT

17import Idris.Error

18+import Idris.Options

18import Idris.Primitives

19import Idris.Primitives

19

20

20import Prelude hiding (id, (.))

21import Prelude hiding (id, (.))

src/Idris/IBC.hs+1

@@ -23,6 +23,7 @@ import Idris.Docstrings (Docstring)

23import qualified Idris.Docstrings as D

24import Idris.Error

25import Idris.Imports

26+import Idris.Options

26import Idris.Output

27import Idris.Output

27import IRTS.System (getIdrisLibDir)

28import IRTS.System (getIdrisLibDir)

28

29

src/Idris/IdrisDoc.hs+1

@@ -18,6 +18,7 @@ import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),

18import Idris.Docs

19import Idris.Docstrings (nullDocstring)

20import qualified Idris.Docstrings as Docstrings

21+import Idris.Options

21import Idris.Parser.Helpers (opChars)

22import Idris.Parser.Helpers (opChars)

22import IRTS.System (getIdrisDataFileByName)

23import IRTS.System (getIdrisDataFileByName)

23

24

src/Idris/Info.hs+1−1

@@ -25,8 +25,8 @@ module Idris.Info

25 , getIdrisDataFileByName

26 ) where

27

28−import Idris.AbsSyntax (loggingCatsStr)

29import Idris.Imports (installedPackages)

28import Idris.Imports (installedPackages)

29+import Idris.Options (loggingCatsStr)

30import qualified IRTS.System as S

31

32import Paths_idris

src/Idris/Main.hs+1

@@ -22,6 +22,7 @@ import Idris.Error

22import Idris.IBC

23import Idris.Info

24import Idris.ModeCommon

25+import Idris.Options

25import Idris.Output

26import Idris.Output

26import Idris.Parser hiding (indent)

27import Idris.Parser hiding (indent)

27import Idris.REPL

28import Idris.REPL

src/Idris/ModeCommon.hs+1

@@ -15,6 +15,7 @@ import Idris.Error

15import Idris.IBC

16import Idris.Imports

17import Idris.Info

18+import Idris.Options

18import Idris.Output

19import Idris.Output

19import Idris.Parser hiding (indent)

20import Idris.Parser hiding (indent)

20import IRTS.Exports

21import IRTS.Exports

src/Idris/Options.hsnew file+283

@@ -0,0 +1,283 @@

1+{-|

2+Module : Idris.Options

3+Description : Compiler options for Idris.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

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

9+

10+module Idris.Options where

11+

12+import Data.Maybe

13+import GHC.Generics (Generic)

14+import IRTS.CodegenCommon (OutputType)

15+import Network.Socket (PortNumber)

16+

17+data Opt = Filename String

18+ | Quiet

19+ | NoBanner

20+ | ColourREPL Bool

21+ | Idemode

22+ | IdemodeSocket

23+ | IndentWith Int

24+ | IndentClause Int

25+ | ShowAll

26+ | ShowLibs

27+ | ShowLibDir

28+ | ShowDocDir

29+ | ShowIncs

30+ | ShowPkgs

31+ | ShowLoggingCats

32+ | NoBasePkgs

33+ | NoPrelude

34+ | NoBuiltins -- only for the really primitive stuff!

35+ | NoREPL

36+ | OLogging Int

37+ | OLogCats [LogCat]

38+ | Output String

39+ | Interface

40+ | TypeCase

41+ | TypeInType

42+ | DefaultTotal

43+ | DefaultPartial

44+ | WarnPartial

45+ | WarnReach

46+ | AuditIPkg

47+ | EvalTypes

48+ | NoCoverage

49+ | ErrContext

50+ | ShowImpl

51+ | Verbose Int

52+ | Port REPLPort -- ^ REPL TCP port

53+ | IBCSubDir String

54+ | ImportDir String

55+ | SourceDir String

56+ | PkgBuild String

57+ | PkgInstall String

58+ | PkgClean String

59+ | PkgCheck String

60+ | PkgREPL String

61+ | PkgDocBuild String -- IdrisDoc

62+ | PkgDocInstall String

63+ | PkgTest String

64+ | PkgIndex FilePath

65+ | WarnOnly

66+ | Pkg String

67+ | BCAsm String

68+ | DumpDefun String

69+ | DumpCases String

70+ | UseCodegen Codegen

71+ | CodegenArgs String

72+ | OutputTy OutputType

73+ | Extension LanguageExt

74+ | InterpretScript String

75+ | EvalExpr String

76+ | TargetTriple String

77+ | TargetCPU String

78+ | OptLevel Int

79+ | AddOpt Optimisation

80+ | RemoveOpt Optimisation

81+ | Client String

82+ | ShowOrigErr

83+ | AutoWidth -- ^ Automatically adjust terminal width

84+ | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

85+ | UseConsoleWidth ConsoleWidth

86+ | DumpHighlights

87+ | DesugarNats

88+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

89+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

90+ deriving (Show, Eq, Generic)

91+

92+

93+data REPLPort = DontListen | ListenPort PortNumber

94+ deriving (Eq, Generic, Show)

95+

96+

97+data Codegen = Via IRFormat String

98+ | Bytecode

99+ deriving (Show, Eq, Generic)

100+

101+

102+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

103+ | DSLNotation | ElabReflection | FCReflection

104+ | LinearTypes

105+ deriving (Show, Eq, Read, Ord, Generic)

106+

107+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)

108+

109+

110+-- | How wide is the console?

111+data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

112+ | ColsWide Int -- ^ Manually specified - must be positive

113+ | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

114+ deriving (Show, Eq, Generic)

115+

116+data HowMuchDocs = FullDocs | OverviewDocs

117+

118+data OutputFmt = HTMLOutput | LaTeXOutput

119+

120+data Optimisation = PETransform -- ^ partial eval and associated transforms

121+ deriving (Show, Eq, Generic)

122+

123+-- | Recognised logging categories for the Idris compiler.

124+--

125+-- @TODO add in sub categories.

126+data LogCat = IParse

127+ | IElab

128+ | ICodeGen

129+ | IErasure

130+ | ICoverage

131+ | IIBC

132+ deriving (Show, Eq, Ord, Generic)

133+

134+strLogCat :: LogCat -> String

135+strLogCat IParse = "parser"

136+strLogCat IElab = "elab"

137+strLogCat ICodeGen = "codegen"

138+strLogCat IErasure = "erasure"

139+strLogCat ICoverage = "coverage"

140+strLogCat IIBC = "ibc"

141+

142+codegenCats :: [LogCat]

143+codegenCats = [ICodeGen]

144+

145+parserCats :: [LogCat]

146+parserCats = [IParse]

147+

148+elabCats :: [LogCat]

149+elabCats = [IElab]

150+

151+loggingCatsStr :: String

152+loggingCatsStr = unlines

153+ [ (strLogCat IParse)

154+ , (strLogCat IElab)

155+ , (strLogCat ICodeGen)

156+ , (strLogCat IErasure)

157+ , (strLogCat ICoverage)

158+ , (strLogCat IIBC)

159+ ]

160+

161+getFile :: Opt -> Maybe String

162+getFile (Filename s) = Just s

163+getFile _ = Nothing

164+

165+getBC :: Opt -> Maybe String

166+getBC (BCAsm s) = Just s

167+getBC _ = Nothing

168+

169+getOutput :: Opt -> Maybe String

170+getOutput (Output s) = Just s

171+getOutput _ = Nothing

172+

173+getIBCSubDir :: Opt -> Maybe String

174+getIBCSubDir (IBCSubDir s) = Just s

175+getIBCSubDir _ = Nothing

176+

177+getImportDir :: Opt -> Maybe String

178+getImportDir (ImportDir s) = Just s

179+getImportDir _ = Nothing

180+

181+getSourceDir :: Opt -> Maybe String

182+getSourceDir (SourceDir s) = Just s

183+getSourceDir _ = Nothing

184+

185+getPkgDir :: Opt -> Maybe String

186+getPkgDir (Pkg s) = Just s

187+getPkgDir _ = Nothing

188+

189+getPkg :: Opt -> Maybe (Bool, String)

190+getPkg (PkgBuild s) = Just (False, s)

191+getPkg (PkgInstall s) = Just (True, s)

192+getPkg _ = Nothing

193+

194+getPkgClean :: Opt -> Maybe String

195+getPkgClean (PkgClean s) = Just s

196+getPkgClean _ = Nothing

197+

198+getPkgREPL :: Opt -> Maybe String

199+getPkgREPL (PkgREPL s) = Just s

200+getPkgREPL _ = Nothing

201+

202+getPkgCheck :: Opt -> Maybe String

203+getPkgCheck (PkgCheck s) = Just s

204+getPkgCheck _ = Nothing

205+

206+-- | Returns None if given an Opt which is not PkgMkDoc

207+-- Otherwise returns Just x, where x is the contents of PkgMkDoc

208+getPkgMkDoc :: Opt -- ^ Opt to extract

209+ -> Maybe (Bool, String) -- ^ Result

210+getPkgMkDoc (PkgDocBuild str) = Just (False,str)

211+getPkgMkDoc (PkgDocInstall str) = Just (True,str)

212+getPkgMkDoc _ = Nothing

213+

214+getPkgTest :: Opt -- ^ the option to extract

215+ -> Maybe String -- ^ the package file to test

216+getPkgTest (PkgTest f) = Just f

217+getPkgTest _ = Nothing

218+

219+getCodegen :: Opt -> Maybe Codegen

220+getCodegen (UseCodegen x) = Just x

221+getCodegen _ = Nothing

222+

223+getCodegenArgs :: Opt -> Maybe String

224+getCodegenArgs (CodegenArgs args) = Just args

225+getCodegenArgs _ = Nothing

226+

227+getConsoleWidth :: Opt -> Maybe ConsoleWidth

228+getConsoleWidth (UseConsoleWidth x) = Just x

229+getConsoleWidth _ = Nothing

230+

231+getExecScript :: Opt -> Maybe String

232+getExecScript (InterpretScript expr) = Just expr

233+getExecScript _ = Nothing

234+

235+getPkgIndex :: Opt -> Maybe FilePath

236+getPkgIndex (PkgIndex file) = Just file

237+getPkgIndex _ = Nothing

238+

239+getEvalExpr :: Opt -> Maybe String

240+getEvalExpr (EvalExpr expr) = Just expr

241+getEvalExpr _ = Nothing

242+

243+getOutputTy :: Opt -> Maybe OutputType

244+getOutputTy (OutputTy t) = Just t

245+getOutputTy _ = Nothing

246+

247+getLanguageExt :: Opt -> Maybe LanguageExt

248+getLanguageExt (Extension e) = Just e

249+getLanguageExt _ = Nothing

250+

251+getTriple :: Opt -> Maybe String

252+getTriple (TargetTriple x) = Just x

253+getTriple _ = Nothing

254+

255+getCPU :: Opt -> Maybe String

256+getCPU (TargetCPU x) = Just x

257+getCPU _ = Nothing

258+

259+getOptLevel :: Opt -> Maybe Int

260+getOptLevel (OptLevel x) = Just x

261+getOptLevel _ = Nothing

262+

263+getOptimisation :: Opt -> Maybe (Bool,Optimisation)

264+getOptimisation (AddOpt p) = Just (True, p)

265+getOptimisation (RemoveOpt p) = Just (False, p)

266+getOptimisation _ = Nothing

267+

268+getColour :: Opt -> Maybe Bool

269+getColour (ColourREPL b) = Just b

270+getColour _ = Nothing

271+

272+getClient :: Opt -> Maybe String

273+getClient (Client x) = Just x

274+getClient _ = Nothing

275+

276+-- Get the first valid port

277+getPort :: [Opt] -> Maybe REPLPort

278+getPort [] = Nothing

279+getPort (Port p : _ ) = Just p

280+getPort (_ : xs) = getPort xs

281+

282+opt :: (Opt -> Maybe a) -> [Opt] -> [a]

283+opt = mapMaybe

src/Idris/Output.hs+1

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

17import Idris.Delaborate

18import Idris.Docstrings

19import Idris.IdeMode

20+import Idris.Options

20

21

21import Util.Pretty

22import Util.Pretty

22import Util.ScreenSize (getScreenWidth)

23import Util.ScreenSize (getScreenWidth)

src/Idris/Package.hs+1−1

@@ -35,7 +35,7 @@ import Idris.IBC

35import Idris.IdrisDoc

36import Idris.Imports

37import Idris.Main (idris, idrisMain)

38−import Idris.Output (pshow)

38+import Idris.Options

39import Idris.Output

40import Idris.Parser (loadModule)

41import Idris.REPL

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

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

6-}

7module Idris.Package.Common where

8

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

10import Idris.Core.TT (Name)

9import Idris.Core.TT (Name)

10+import Idris.Options (Opt(..))

11

12-- | Description of an Idris package.

13data PkgDesc = PkgDesc {

src/Idris/Parser.hs+1

@@ -26,6 +26,7 @@ import Idris.ElabDecls

26import Idris.Error

27import Idris.IBC

28import Idris.Imports

29+import Idris.Options

29import Idris.Output

30import Idris.Output

30import Idris.Parser.Data

31import Idris.Parser.Data

31import Idris.Parser.Expr

32import Idris.Parser.Expr

src/Idris/Parser/Data.hs+1

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

13import Idris.Core.TT

14import Idris.Docstrings

15import Idris.DSL

16+import Idris.Options

16import Idris.Parser.Expr

17import Idris.Parser.Expr

17import Idris.Parser.Helpers

18import Idris.Parser.Helpers

18import Idris.Parser.Ops

19import Idris.Parser.Ops

src/Idris/Parser/Expr.hs+1

@@ -12,6 +12,7 @@ module Idris.Parser.Expr where

12import Idris.AbsSyntax

13import Idris.Core.TT

14import Idris.DSL

15+import Idris.Options

15import Idris.Parser.Helpers

16import Idris.Parser.Helpers

16import Idris.Parser.Ops

17import Idris.Parser.Ops

17

18

src/Idris/Parser/Helpers.hs+1

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

17import Idris.Core.TT

18import Idris.Delaborate (pprintErr)

19import Idris.Docstrings

20+import Idris.Options

20import Idris.Output (iWarn)

21import Idris.Output (iWarn)

21

22

22import qualified Util.Pretty as Pretty (text)

23import qualified Util.Pretty as Pretty (text)

src/Idris/Prover.hs+1

@@ -32,6 +32,7 @@ import Idris.Elab.Value

32import Idris.ElabDecls

33import Idris.Error

34import qualified Idris.IdeMode as IdeMode

35+import Idris.Options

35import Idris.Output

36import Idris.Output

36import Idris.Parser hiding (params)

37import Idris.Parser hiding (params)

37import Idris.TypeSearch (searchByType)

38import Idris.TypeSearch (searchByType)

src/Idris/REPL.hs+1

@@ -68,6 +68,7 @@ import Idris.Info

68import Idris.Inliner

69import Idris.Interactive

70import Idris.ModeCommon

71+import Idris.Options

71import Idris.Output

72import Idris.Output

72import Idris.Parser hiding (indent)

73import Idris.Parser hiding (indent)

73import Idris.Prover

74import Idris.Prover

src/Idris/REPL/Commands.hs+1

@@ -3,6 +3,7 @@ module Idris.REPL.Commands where

3import Idris.AbsSyntaxTree

4import Idris.Colours

5import Idris.Core.TT

6+import Idris.Options

6

7

7-- | REPL commands

8-- | REPL commands

8data Command = Quit

9data Command = Quit

src/Idris/REPL/Parser.hs+1

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

15import Idris.Colours

16import Idris.Core.TT

17import Idris.Help

18+import Idris.Options

18import qualified Idris.Parser as P

19import qualified Idris.Parser as P

19import Idris.REPL.Commands

20import Idris.REPL.Commands

20

21

src/Idris/Termination.hs+1

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

14import Idris.Core.TT

15import Idris.Delaborate

16import Idris.Error

17+import Idris.Options

17import Idris.Output (iWarn, iputStrLn)

18import Idris.Output (iWarn, iputStrLn)

18

19

19import Control.Monad.State.Strict

20import Control.Monad.State.Strict