git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Options.hs
291 lines 8.4 kB history raw
1{-|
2Module : Idris.Options
3Description : Compiler options for Idris.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
10module Idris.Options (Codegen(..), ConsoleWidth(..), HowMuchDocs(..), IRFormat(..),
11 LanguageExt(..), LogCat(..), Opt(..), Optimisation(..),
12 OutputFmt(..), REPLPort(..), codegenCats, elabCats, getBC,
13 getClient, getCodegen, getCodegenArgs, getColour, getConsoleWidth,
14 getEvalExpr, getExecScript, getFile, getIBCSubDir, getImportDir,
15 getLanguageExt, getOptLevel, getOptimisation, getOutput,
16 getOutputTy, getPkg, getPkgCheck, getPkgClean, getPkgDir,
17 getPkgIndex, getPkgMkDoc, getPkgREPL, getPkgTest, getPort,
18 getSourceDir, loggingCatsStr, opt, parserCats, strLogCat) where
20import Data.Maybe
21import GHC.Generics (Generic)
22import IRTS.CodegenCommon (OutputType)
23import Network.Socket (PortNumber)
25data Opt = Filename String
26 | Quiet
27 | NoBanner
28 | ColourREPL Bool
29 | Idemode
30 | IdemodeSocket
31 | IndentWith Int
32 | IndentClause Int
33 | ShowAll
34 | ShowLibs
35 | ShowLibDir
36 | ShowDocDir
37 | ShowIncs
38 | ShowPkgs
39 | ShowLoggingCats
40 | NoBasePkgs
41 | NoPrelude
42 | NoBuiltins -- only for the really primitive stuff!
43 | NoREPL
44 | OLogging Int
45 | OLogCats [LogCat]
46 | Output String
47 | Interface
48 | TypeCase
49 | TypeInType
50 | DefaultTotal
51 | DefaultPartial
52 | WarnPartial
53 | WarnReach
54 | AuditIPkg
55 | EvalTypes
56 | NoCoverage
57 | ErrContext
58 | ShowImpl
59 | Verbose Int
60 | Port REPLPort -- ^ REPL TCP port
61 | IBCSubDir String
62 | ImportDir String
63 | SourceDir String
64 | PkgBuild String
65 | PkgInstall String
66 | PkgClean String
67 | PkgCheck String
68 | PkgREPL String
69 | PkgDocBuild String -- IdrisDoc
70 | PkgDocInstall String
71 | PkgTest String
72 | PkgIndex FilePath
73 | WarnOnly
74 | Pkg String
75 | BCAsm String
76 | DumpDefun String
77 | DumpCases String
78 | UseCodegen Codegen
79 | CodegenArgs String
80 | OutputTy OutputType
81 | Extension LanguageExt
82 | InterpretScript String
83 | EvalExpr String
84 | TargetTriple String
85 | TargetCPU String
86 | OptLevel Int
87 | AddOpt Optimisation
88 | RemoveOpt Optimisation
89 | Client String
90 | ShowOrigErr
91 | AutoWidth -- ^ Automatically adjust terminal width
92 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
93 | UseConsoleWidth ConsoleWidth
94 | DumpHighlights
95 | DesugarNats
96 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
97 | AllowCapitalizedPatternVariables -- ^ Allow pattern variables to be capitalized
98 deriving (Show, Eq, Generic)
101data REPLPort = DontListen | ListenPort PortNumber
102 deriving (Eq, Generic, Show)
105data Codegen = Via IRFormat String
106 | Bytecode
107 deriving (Show, Eq, Generic)
110data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
111 | DSLNotation | ElabReflection | FCReflection
112 | LinearTypes
113 deriving (Show, Eq, Read, Ord, Generic)
115data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
118-- | How wide is the console?
119data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
120 | ColsWide Int -- ^ Manually specified - must be positive
121 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
122 deriving (Show, Eq, Generic)
124data HowMuchDocs = FullDocs | OverviewDocs
126data OutputFmt = HTMLOutput | LaTeXOutput
128data Optimisation = PETransform | GeneralisedNatHack -- ^ partial eval and associated transforms
129 deriving (Show, Eq, Generic)
131-- | Recognised logging categories for the Idris compiler.
132--
133-- @TODO add in sub categories.
134data LogCat = IParse
135 | IElab
136 | ICodeGen
137 | IErasure
138 | ICoverage
139 | IIBC
140 deriving (Show, Eq, Ord, Generic)
142strLogCat :: LogCat -> String
143strLogCat IParse = "parser"
144strLogCat IElab = "elab"
145strLogCat ICodeGen = "codegen"
146strLogCat IErasure = "erasure"
147strLogCat ICoverage = "coverage"
148strLogCat IIBC = "ibc"
150codegenCats :: [LogCat]
151codegenCats = [ICodeGen]
153parserCats :: [LogCat]
154parserCats = [IParse]
156elabCats :: [LogCat]
157elabCats = [IElab]
159loggingCatsStr :: String
160loggingCatsStr = unlines
161 [ (strLogCat IParse)
162 , (strLogCat IElab)
163 , (strLogCat ICodeGen)
164 , (strLogCat IErasure)
165 , (strLogCat ICoverage)
166 , (strLogCat IIBC)
167 ]
169getFile :: Opt -> Maybe String
170getFile (Filename s) = Just s
171getFile _ = Nothing
173getBC :: Opt -> Maybe String
174getBC (BCAsm s) = Just s
175getBC _ = Nothing
177getOutput :: Opt -> Maybe String
178getOutput (Output s) = Just s
179getOutput _ = Nothing
181getIBCSubDir :: Opt -> Maybe String
182getIBCSubDir (IBCSubDir s) = Just s
183getIBCSubDir _ = Nothing
185getImportDir :: Opt -> Maybe String
186getImportDir (ImportDir s) = Just s
187getImportDir _ = Nothing
189getSourceDir :: Opt -> Maybe String
190getSourceDir (SourceDir s) = Just s
191getSourceDir _ = Nothing
193getPkgDir :: Opt -> Maybe String
194getPkgDir (Pkg s) = Just s
195getPkgDir _ = Nothing
197getPkg :: Opt -> Maybe (Bool, String)
198getPkg (PkgBuild s) = Just (False, s)
199getPkg (PkgInstall s) = Just (True, s)
200getPkg _ = Nothing
202getPkgClean :: Opt -> Maybe String
203getPkgClean (PkgClean s) = Just s
204getPkgClean _ = Nothing
206getPkgREPL :: Opt -> Maybe String
207getPkgREPL (PkgREPL s) = Just s
208getPkgREPL _ = Nothing
210getPkgCheck :: Opt -> Maybe String
211getPkgCheck (PkgCheck s) = Just s
212getPkgCheck _ = Nothing
214-- | Returns None if given an Opt which is not PkgMkDoc
215-- Otherwise returns Just x, where x is the contents of PkgMkDoc
216getPkgMkDoc :: Opt -- ^ Opt to extract
217 -> Maybe (Bool, String) -- ^ Result
218getPkgMkDoc (PkgDocBuild str) = Just (False,str)
219getPkgMkDoc (PkgDocInstall str) = Just (True,str)
220getPkgMkDoc _ = Nothing
222getPkgTest :: Opt -- ^ the option to extract
223 -> Maybe String -- ^ the package file to test
224getPkgTest (PkgTest f) = Just f
225getPkgTest _ = Nothing
227getCodegen :: Opt -> Maybe Codegen
228getCodegen (UseCodegen x) = Just x
229getCodegen _ = Nothing
231getCodegenArgs :: Opt -> Maybe String
232getCodegenArgs (CodegenArgs args) = Just args
233getCodegenArgs _ = Nothing
235getConsoleWidth :: Opt -> Maybe ConsoleWidth
236getConsoleWidth (UseConsoleWidth x) = Just x
237getConsoleWidth _ = Nothing
239getExecScript :: Opt -> Maybe String
240getExecScript (InterpretScript expr) = Just expr
241getExecScript _ = Nothing
243getPkgIndex :: Opt -> Maybe FilePath
244getPkgIndex (PkgIndex file) = Just file
245getPkgIndex _ = Nothing
247getEvalExpr :: Opt -> Maybe String
248getEvalExpr (EvalExpr expr) = Just expr
249getEvalExpr _ = Nothing
251getOutputTy :: Opt -> Maybe OutputType
252getOutputTy (OutputTy t) = Just t
253getOutputTy _ = Nothing
255getLanguageExt :: Opt -> Maybe LanguageExt
256getLanguageExt (Extension e) = Just e
257getLanguageExt _ = Nothing
259getTriple :: Opt -> Maybe String
260getTriple (TargetTriple x) = Just x
261getTriple _ = Nothing
263getCPU :: Opt -> Maybe String
264getCPU (TargetCPU x) = Just x
265getCPU _ = Nothing
267getOptLevel :: Opt -> Maybe Int
268getOptLevel (OptLevel x) = Just x
269getOptLevel _ = Nothing
271getOptimisation :: Opt -> Maybe (Bool,Optimisation)
272getOptimisation (AddOpt p) = Just (True, p)
273getOptimisation (RemoveOpt p) = Just (False, p)
274getOptimisation _ = Nothing
276getColour :: Opt -> Maybe Bool
277getColour (ColourREPL b) = Just b
278getColour _ = Nothing
280getClient :: Opt -> Maybe String
281getClient (Client x) = Just x
282getClient _ = Nothing
284-- Get the first valid port
285getPort :: [Opt] -> Maybe REPLPort
286getPort [] = Nothing
287getPort (Port p : _ ) = Just p
288getPort (_ : xs) = getPort xs
290opt :: (Opt -> Maybe a) -> [Opt] -> [a]
291opt = mapMaybe