git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Options.hs
283 lines 7.7 kB history raw
1{-|
2Module : Idris.Options
3Description : Compiler options for Idris.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
10module Idris.Options where
12import Data.Maybe
13import GHC.Generics (Generic)
14import IRTS.CodegenCommon (OutputType)
15import Network.Socket (PortNumber)
17data 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)
93data REPLPort = DontListen | ListenPort PortNumber
94 deriving (Eq, Generic, Show)
97data Codegen = Via IRFormat String
98 | Bytecode
99 deriving (Show, Eq, Generic)
102data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
103 | DSLNotation | ElabReflection | FCReflection
104 | LinearTypes
105 deriving (Show, Eq, Read, Ord, Generic)
107data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
110-- | How wide is the console?
111data 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)
116data HowMuchDocs = FullDocs | OverviewDocs
118data OutputFmt = HTMLOutput | LaTeXOutput
120data Optimisation = PETransform -- ^ partial eval and associated transforms
121 deriving (Show, Eq, Generic)
123-- | Recognised logging categories for the Idris compiler.
124--
125-- @TODO add in sub categories.
126data LogCat = IParse
127 | IElab
128 | ICodeGen
129 | IErasure
130 | ICoverage
131 | IIBC
132 deriving (Show, Eq, Ord, Generic)
134strLogCat :: LogCat -> String
135strLogCat IParse = "parser"
136strLogCat IElab = "elab"
137strLogCat ICodeGen = "codegen"
138strLogCat IErasure = "erasure"
139strLogCat ICoverage = "coverage"
140strLogCat IIBC = "ibc"
142codegenCats :: [LogCat]
143codegenCats = [ICodeGen]
145parserCats :: [LogCat]
146parserCats = [IParse]
148elabCats :: [LogCat]
149elabCats = [IElab]
151loggingCatsStr :: String
152loggingCatsStr = unlines
153 [ (strLogCat IParse)
154 , (strLogCat IElab)
155 , (strLogCat ICodeGen)
156 , (strLogCat IErasure)
157 , (strLogCat ICoverage)
158 , (strLogCat IIBC)
159 ]
161getFile :: Opt -> Maybe String
162getFile (Filename s) = Just s
163getFile _ = Nothing
165getBC :: Opt -> Maybe String
166getBC (BCAsm s) = Just s
167getBC _ = Nothing
169getOutput :: Opt -> Maybe String
170getOutput (Output s) = Just s
171getOutput _ = Nothing
173getIBCSubDir :: Opt -> Maybe String
174getIBCSubDir (IBCSubDir s) = Just s
175getIBCSubDir _ = Nothing
177getImportDir :: Opt -> Maybe String
178getImportDir (ImportDir s) = Just s
179getImportDir _ = Nothing
181getSourceDir :: Opt -> Maybe String
182getSourceDir (SourceDir s) = Just s
183getSourceDir _ = Nothing
185getPkgDir :: Opt -> Maybe String
186getPkgDir (Pkg s) = Just s
187getPkgDir _ = Nothing
189getPkg :: Opt -> Maybe (Bool, String)
190getPkg (PkgBuild s) = Just (False, s)
191getPkg (PkgInstall s) = Just (True, s)
192getPkg _ = Nothing
194getPkgClean :: Opt -> Maybe String
195getPkgClean (PkgClean s) = Just s
196getPkgClean _ = Nothing
198getPkgREPL :: Opt -> Maybe String
199getPkgREPL (PkgREPL s) = Just s
200getPkgREPL _ = Nothing
202getPkgCheck :: Opt -> Maybe String
203getPkgCheck (PkgCheck s) = Just s
204getPkgCheck _ = Nothing
206-- | Returns None if given an Opt which is not PkgMkDoc
207-- Otherwise returns Just x, where x is the contents of PkgMkDoc
208getPkgMkDoc :: Opt -- ^ Opt to extract
209 -> Maybe (Bool, String) -- ^ Result
210getPkgMkDoc (PkgDocBuild str) = Just (False,str)
211getPkgMkDoc (PkgDocInstall str) = Just (True,str)
212getPkgMkDoc _ = Nothing
214getPkgTest :: Opt -- ^ the option to extract
215 -> Maybe String -- ^ the package file to test
216getPkgTest (PkgTest f) = Just f
217getPkgTest _ = Nothing
219getCodegen :: Opt -> Maybe Codegen
220getCodegen (UseCodegen x) = Just x
221getCodegen _ = Nothing
223getCodegenArgs :: Opt -> Maybe String
224getCodegenArgs (CodegenArgs args) = Just args
225getCodegenArgs _ = Nothing
227getConsoleWidth :: Opt -> Maybe ConsoleWidth
228getConsoleWidth (UseConsoleWidth x) = Just x
229getConsoleWidth _ = Nothing
231getExecScript :: Opt -> Maybe String
232getExecScript (InterpretScript expr) = Just expr
233getExecScript _ = Nothing
235getPkgIndex :: Opt -> Maybe FilePath
236getPkgIndex (PkgIndex file) = Just file
237getPkgIndex _ = Nothing
239getEvalExpr :: Opt -> Maybe String
240getEvalExpr (EvalExpr expr) = Just expr
241getEvalExpr _ = Nothing
243getOutputTy :: Opt -> Maybe OutputType
244getOutputTy (OutputTy t) = Just t
245getOutputTy _ = Nothing
247getLanguageExt :: Opt -> Maybe LanguageExt
248getLanguageExt (Extension e) = Just e
249getLanguageExt _ = Nothing
251getTriple :: Opt -> Maybe String
252getTriple (TargetTriple x) = Just x
253getTriple _ = Nothing
255getCPU :: Opt -> Maybe String
256getCPU (TargetCPU x) = Just x
257getCPU _ = Nothing
259getOptLevel :: Opt -> Maybe Int
260getOptLevel (OptLevel x) = Just x
261getOptLevel _ = Nothing
263getOptimisation :: Opt -> Maybe (Bool,Optimisation)
264getOptimisation (AddOpt p) = Just (True, p)
265getOptimisation (RemoveOpt p) = Just (False, p)
266getOptimisation _ = Nothing
268getColour :: Opt -> Maybe Bool
269getColour (ColourREPL b) = Just b
270getColour _ = Nothing
272getClient :: Opt -> Maybe String
273getClient (Client x) = Just x
274getClient _ = Nothing
276-- Get the first valid port
277getPort :: [Opt] -> Maybe REPLPort
278getPort [] = Nothing
279getPort (Port p : _ ) = Just p
280getPort (_ : xs) = getPort xs
282opt :: (Opt -> Maybe a) -> [Opt] -> [a]
283opt = mapMaybe