243e02f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev into add_regression_test_js_unexpected_con_as_glob

commit243e02fb38b5bd0563fbb7202bb41c7fac6e3f9a authorRui Barreiro <rui.barreiro@gmail.com> dateSat 22 Jul 2017, 07:48 (9 years ago) parentcfd6084 e32f5cd

39 files changed+338−266

compare with master

unifiedsplit

codegen/idris-codegen-c/Main.hs+1 codegen/idris-codegen-javascript/Main.hs+1 codegen/idris-codegen-node/Main.hs+1 idris.cabal+1 main/Main.hs+1 src/IRTS/Compiler.hs+1 src/IRTS/JavaScript/Codegen.hs+2−1 src/IRTS/JavaScript/LangTransforms.hs+13 src/Idris/ASTUtils.hs+1 src/Idris/AbsSyntax.hs+2−123 src/Idris/AbsSyntaxTree.hs+3−133 src/Idris/CmdOptions.hs+1−4 src/Idris/DeepSeq.hs+1 src/Idris/Docs.hs+2−1 src/Idris/Elab/Clause.hs+1 src/Idris/Elab/Provider.hs+1 src/Idris/Elab/Term.hs+1 src/Idris/Elab/Type.hs+1 src/Idris/ElabDecls.hs+1 src/Idris/Erasure.hs+1 src/Idris/IBC.hs+1 src/Idris/IdrisDoc.hs+1 src/Idris/Info.hs+1−1 src/Idris/Main.hs+1 src/Idris/ModeCommon.hs+1 src/Idris/Options.hs+283 src/Idris/Output.hs+1 src/Idris/Package.hs+1−1 src/Idris/Package/Common.hs+1−1 src/Idris/Parser.hs+1 src/Idris/Parser/Data.hs+1 src/Idris/Parser/Expr.hs+1 src/Idris/Parser/Helpers.hs+1 src/Idris/Prover.hs+1 src/Idris/REPL.hs+1 src/Idris/REPL/Commands.hs+1 src/Idris/REPL/Parser.hs+1 src/Idris/Termination.hs+1 test/regression003/regression003.idr+1−1

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

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

44import Idris.Core.TT

55import Idris.ElabDecls

66import Idris.Main

7+import Idris.Options

78import IRTS.CodegenC

89import IRTS.Compiler

910

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

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

44import Idris.Core.TT

55import Idris.ElabDecls

66import Idris.Main

7+import Idris.Options

78import IRTS.CodegenJavaScript

89import IRTS.Compiler

910

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

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

44import Idris.Core.TT

55import Idris.ElabDecls

66import Idris.Main

7+import Idris.Options

78import IRTS.CodegenJavaScript

89import IRTS.Compiler

910

idris.cabal+1

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

196196 , Idris.Output

197197 , Idris.Main

198198 , Idris.ModeCommon

199+ , Idris.Options

199200 , Idris.Parser

200201 , Idris.Parser.Helpers

201202 , Idris.Parser.Ops

main/Main.hs+1

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

1111import Idris.Error

1212import Idris.Info.Show

1313import Idris.Main

14+import Idris.Options

1415import Idris.Package

1516

1617import Util.System (setupBundledCC)

src/IRTS/Compiler.hs+1

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

1717import Idris.Core.TT

1818import Idris.Erasure

1919import Idris.Error

20+import Idris.Options

2021import Idris.Output

2122import IRTS.CodegenC

2223import IRTS.CodegenCommon

src/IRTS/JavaScript/Codegen.hs+2−1

@@ -98,7 +98,8 @@ codegenJs :: CGConf -> CodeGenerator

9898codegenJs conf ci =

9999 do

100100 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"

101− let defs = Map.fromList $ liftDecls ci

101+ let defs' = Map.fromList $ liftDecls ci

102+ let defs = globlToCon defs'

102103 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]

103104 if debug then

104105 do

src/IRTS/JavaScript/LangTransforms.hs+13

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

88{-# LANGUAGE DeriveDataTypeable, OverloadedStrings, StandaloneDeriving #-}

1010module IRTS.JavaScript.LangTransforms( removeDeadCode

11+ , globlToCon

1112 ) where

1213

1314

@@ -94,3 +95,15 @@ removeDeadCode dcls start =

9495 remCons = removeUnusedBranches (getUsedConstructors used) used

9596 in if Map.keys remCons == Map.keys dcls then remCons

9697 else removeDeadCode remCons start

98+

99+

100+globlToCon :: Map Name LDecl -> Map Name LDecl

101+globlToCon x =

102+ transformBi (f x) x

103+ where

104+ f :: Map Name LDecl -> LExp -> LExp

105+ f y x@(LV (Glob n)) =

106+ case Map.lookup n y of

107+ Just (LConstructor _ conId arity) -> LCon Nothing conId n []

108+ _ -> x

109+ f y x = x

src/Idris/ASTUtils.hs+1

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

4848import Idris.AbsSyntaxTree

4949import Idris.Core.Evaluate

5050import Idris.Core.TT

51+import Idris.Options

5152

5253import Prelude hiding (id, (.))

5354

src/Idris/AbsSyntax.hs+2−123

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

1919import Idris.Core.TT

2020import Idris.Docstrings

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

22+import Idris.Options

2223import IRTS.CodegenCommon

2324

2425import System.Directory (canonicalizePath, doesFileExist)

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

26022603

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

26042605

2605−getFile :: Opt -> Maybe String

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

2606+

src/Idris/AbsSyntaxTree.hs+3−133

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

1414import Idris.Core.Evaluate

1515import Idris.Core.TT

1616import Idris.Docstrings

17+import Idris.Options

1718import IRTS.CodegenCommon

1819import IRTS.Lang

1920import Util.DynamicLinker

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

146147 , ppopt_depth :: Maybe Int

147148 } deriving (Show)

148149

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

150− deriving (Show, Eq, Generic)

150+

151151

152152defaultOptimise :: [Optimisation]

153153defaultOptimise = []

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

183183ppOptionIst :: IState -> PPOption

184184ppOptionIst = ppOption . idris_options

185185

186−data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

187− | DSLNotation | ElabReflection | FCReflection

188− | LinearTypes

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

190186

191187-- | The output mode in use

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

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

194190 deriving Show

195191

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)

201192

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

203194data DefaultTotality = DefaultCheckingTotal -- ^ Total

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

434425

435426-- Commands in the REPL

436427

437−data Codegen = Via IRFormat String

438− | Bytecode

439− deriving (Show, Eq, Generic)

440428

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− ]

484429

485430

486431data ElabShellCmd = EQED

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

494439 | EDocStr (Either Name Const)

495440 deriving (Show, Eq)

496441

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)

571442

572−data REPLPort = DontListen | ListenPort PortNumber

573− deriving (Eq, Generic, Show)

443+

574444

575445-- Parsed declarations

576446

src/Idris/CmdOptions.hs+1−4

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

1616 , getPkgREPL, getPkgTest, getPort, getIBCSubDir

1717 ) where

1818

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

20− getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,

21− getPort, opt)

22−import Idris.AbsSyntaxTree

2319import Idris.Info (getIdrisVersion)

20+import Idris.Options

2421import IRTS.CodegenCommon

2522

2623import Control.Monad.Trans (lift)

src/Idris/DeepSeq.hs+1

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

1818import Idris.Core.TT

1919import Idris.Docstrings

2020import qualified Idris.Docstrings as D

21+import Idris.Options

2122import IRTS.CodegenCommon (OutputType(..))

2223import IRTS.Lang (PrimFn(..))

2324

src/Idris/Docs.hs+2−1

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

1515 , FunDoc, FunDoc'(..), Docs, Docs'(..)

1616 ) where

1717

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

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

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

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

2121 getIState, modDocName, ppOptionIst, pprintPTerm,

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

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

2727 nullDocstring, overview, renderDocTerm,

2828 renderDocstring)

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

2930

3031import Util.Pretty

3132

src/Idris/Elab/Clause.hs+1

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

3131import Idris.Error

3232import Idris.Imports

3333import Idris.Inliner

34+import Idris.Options

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

3536import Idris.PartialEval

3637import Idris.Primitives

src/Idris/Elab/Provider.hs+1

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

3030import Idris.Error

3131import Idris.Imports

3232import Idris.Inliner

33+import Idris.Options

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

3435import Idris.PartialEval

3536import Idris.Primitives

src/Idris/Elab/Term.hs+1

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

2727import Idris.Elab.Utils

2828import Idris.Error

2929import Idris.ErrReverse (errReverse)

30+import Idris.Options

3031import Idris.Output (pshow)

3132import Idris.ProofSearch

3233import Idris.Reflection

src/Idris/Elab/Type.hs+1

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

3232import Idris.Error

3333import Idris.Imports

3434import Idris.Inliner

35+import Idris.Options

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

3637import Idris.PartialEval

3738import Idris.Primitives

src/Idris/ElabDecls.hs+1

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

4141import Idris.Error

4242import Idris.Imports

4343import Idris.Inliner

44+import Idris.Options

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

4546import Idris.PartialEval

4647import Idris.Primitives

src/Idris/Erasure.hs+1

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

1515import Idris.Core.Evaluate

1616import Idris.Core.TT

1717import Idris.Error

18+import Idris.Options

1819import Idris.Primitives

1920

2021import Prelude hiding (id, (.))

src/Idris/IBC.hs+1

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

2323import qualified Idris.Docstrings as D

2424import Idris.Error

2525import Idris.Imports

26+import Idris.Options

2627import Idris.Output

2728import IRTS.System (getIdrisLibDir)

2829

src/Idris/IdrisDoc.hs+1

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

1818import Idris.Docs

1919import Idris.Docstrings (nullDocstring)

2020import qualified Idris.Docstrings as Docstrings

21+import Idris.Options

2122import Idris.Parser.Helpers (opChars)

2223import IRTS.System (getIdrisDataFileByName)

2324

src/Idris/Info.hs+1−1

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

2525 , getIdrisDataFileByName

2626 ) where

2727

28−import Idris.AbsSyntax (loggingCatsStr)

2928import Idris.Imports (installedPackages)

29+import Idris.Options (loggingCatsStr)

3030import qualified IRTS.System as S

3131

3232import Paths_idris

src/Idris/Main.hs+1

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

2222import Idris.IBC

2323import Idris.Info

2424import Idris.ModeCommon

25+import Idris.Options

2526import Idris.Output

2627import Idris.Parser hiding (indent)

2728import Idris.REPL

src/Idris/ModeCommon.hs+1

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

1515import Idris.IBC

1616import Idris.Imports

1717import Idris.Info

18+import Idris.Options

1819import Idris.Output

1920import Idris.Parser hiding (indent)

2021import 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 #-}

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

1717import Idris.Delaborate

1818import Idris.Docstrings

1919import Idris.IdeMode

20+import Idris.Options

2021

2122import Util.Pretty

2223import Util.ScreenSize (getScreenWidth)

src/Idris/Package.hs+1−1

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

3535import Idris.IdrisDoc

3636import Idris.Imports

3737import Idris.Main (idris, idrisMain)

38−import Idris.Output (pshow)

38+import Idris.Options

3939import Idris.Output

4040import Idris.Parser (loadModule)

4141import Idris.REPL

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

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

66-}

77module Idris.Package.Common where

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

109import Idris.Core.TT (Name)

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

1111

1212-- | Description of an Idris package.

1313data PkgDesc = PkgDesc {

src/Idris/Parser.hs+1

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

2626import Idris.Error

2727import Idris.IBC

2828import Idris.Imports

29+import Idris.Options

2930import Idris.Output

3031import Idris.Parser.Data

3132import Idris.Parser.Expr

src/Idris/Parser/Data.hs+1

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

1313import Idris.Core.TT

1414import Idris.Docstrings

1515import Idris.DSL

16+import Idris.Options

1617import Idris.Parser.Expr

1718import Idris.Parser.Helpers

1819import Idris.Parser.Ops

src/Idris/Parser/Expr.hs+1

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

1212import Idris.AbsSyntax

1313import Idris.Core.TT

1414import Idris.DSL

15+import Idris.Options

1516import Idris.Parser.Helpers

1617import Idris.Parser.Ops

1718

src/Idris/Parser/Helpers.hs+1

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

1717import Idris.Core.TT

1818import Idris.Delaborate (pprintErr)

1919import Idris.Docstrings

20+import Idris.Options

2021import Idris.Output (iWarn)

2122

2223import qualified Util.Pretty as Pretty (text)

src/Idris/Prover.hs+1

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

3232import Idris.ElabDecls

3333import Idris.Error

3434import qualified Idris.IdeMode as IdeMode

35+import Idris.Options

3536import Idris.Output

3637import Idris.Parser hiding (params)

3738import Idris.TypeSearch (searchByType)

src/Idris/REPL.hs+1

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

6868import Idris.Inliner

6969import Idris.Interactive

7070import Idris.ModeCommon

71+import Idris.Options

7172import Idris.Output

7273import Idris.Parser hiding (indent)

7374import Idris.Prover

src/Idris/REPL/Commands.hs+1

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

33import Idris.AbsSyntaxTree

44import Idris.Colours

55import Idris.Core.TT

6+import Idris.Options

78-- | REPL commands

89data Command = Quit

src/Idris/REPL/Parser.hs+1

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

1515import Idris.Colours

1616import Idris.Core.TT

1717import Idris.Help

18+import Idris.Options

1819import qualified Idris.Parser as P

1920import Idris.REPL.Commands

2021

src/Idris/Termination.hs+1

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

1414import Idris.Core.TT

1515import Idris.Delaborate

1616import Idris.Error

17+import Idris.Options

1718import Idris.Output (iWarn, iputStrLn)

1819

1920import Control.Monad.State.Strict

test/regression003/regression003.idr+1−1

@@ -52,5 +52,5 @@ main : IO ()

5252main =

5353 do

5454 c <- foldFree interpret2 readFileF

55− putStr' c

55+ putStrLn' c

5656