Copyright	License : BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Options

Description

Synopsis

Documentation

data Opt Source #

Constructors

Filename String
Quiet
NoBanner
ColourREPL Bool
Idemode
IdemodeSocket
IndentWith Int
IndentClause Int
ShowAll
ShowLibs
ShowLibDir
ShowDocDir
ShowIncs
ShowPkgs
ShowLoggingCats
NoBasePkgs
NoPrelude
NoBuiltins
NoREPL
OLogging Int
OLogCats [LogCat]
Output String
Interface
TypeCase
TypeInType
DefaultTotal
DefaultPartial
WarnPartial
WarnReach
AuditIPkg
EvalTypes
NoCoverage
ErrContext
ShowImpl
Verbose Int
Port REPLPort	REPL TCP port
IBCSubDir String
ImportDir String
SourceDir String
PkgBuild String
PkgInstall String
PkgClean String
PkgCheck String
PkgREPL String
PkgDocBuild String
PkgDocInstall String
PkgTest String
PkgIndex FilePath
WarnOnly
Pkg String
BCAsm String
DumpDefun String
DumpCases String
UseCodegen Codegen
CodegenArgs String
OutputTy OutputType
Extension LanguageExt
InterpretScript String
EvalExpr String
TargetTriple String
TargetCPU String
OptLevel Int
AddOpt Optimisation
RemoveOpt Optimisation
Client String
ShowOrigErr
AutoWidth	Automatically adjust terminal width
AutoSolve	Automatically issue "solve" tactic in old-style interactive prover
UseConsoleWidth ConsoleWidth
DumpHighlights
DesugarNats
NoElimDeprecationWarnings	Don't show deprecation warnings for %elim
NoOldTacticDeprecationWarnings	Don't show deprecation warnings for old-style tactics

Instances

Eq Opt Source #
Methods (==) :: Opt -> Opt -> Bool # (/=) :: Opt -> Opt -> Bool #
Show Opt Source #
Methods showsPrec :: Int -> Opt -> ShowS # show :: Opt -> String # showList :: [Opt] -> ShowS #
Generic Opt Source #
Associated Types type Rep Opt :: * -> * # Methods from :: Opt -> Rep Opt x # to :: Rep Opt x -> Opt #
type Rep Opt Source #
type Rep Opt = D1 (MetaData "Opt" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "Filename" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "Quiet" PrefixI False) U1)) ((:+:) (C1 (MetaCons "NoBanner" PrefixI False) U1) (C1 (MetaCons "ColourREPL" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) ((:+:) ((:+:) (C1 (MetaCons "Idemode" PrefixI False) U1) (C1 (MetaCons "IdemodeSocket" PrefixI False) U1)) ((:+:) (C1 (MetaCons "IndentWith" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) ((:+:) (C1 (MetaCons "IndentClause" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) (C1 (MetaCons "ShowAll" PrefixI False) U1))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ShowLibs" PrefixI False) U1) (C1 (MetaCons "ShowLibDir" PrefixI False) U1)) ((:+:) (C1 (MetaCons "ShowDocDir" PrefixI False) U1) (C1 (MetaCons "ShowIncs" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "ShowPkgs" PrefixI False) U1) (C1 (MetaCons "ShowLoggingCats" PrefixI False) U1)) ((:+:) (C1 (MetaCons "NoBasePkgs" PrefixI False) U1) ((:+:) (C1 (MetaCons "NoPrelude" PrefixI False) U1) (C1 (MetaCons "NoBuiltins" PrefixI False) U1)))))) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "NoREPL" PrefixI False) U1) (C1 (MetaCons "OLogging" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) ((:+:) (C1 (MetaCons "OLogCats" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [LogCat]))) (C1 (MetaCons "Output" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))) ((:+:) ((:+:) (C1 (MetaCons "Interface" PrefixI False) U1) (C1 (MetaCons "TypeCase" PrefixI False) U1)) ((:+:) (C1 (MetaCons "TypeInType" PrefixI False) U1) ((:+:) (C1 (MetaCons "DefaultTotal" PrefixI False) U1) (C1 (MetaCons "DefaultPartial" PrefixI False) U1))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "WarnPartial" PrefixI False) U1) (C1 (MetaCons "WarnReach" PrefixI False) U1)) ((:+:) (C1 (MetaCons "AuditIPkg" PrefixI False) U1) (C1 (MetaCons "EvalTypes" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "NoCoverage" PrefixI False) U1) (C1 (MetaCons "ErrContext" PrefixI False) U1)) ((:+:) (C1 (MetaCons "ShowImpl" PrefixI False) U1) ((:+:) (C1 (MetaCons "Verbose" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) (C1 (MetaCons "Port" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 REPLPort))))))))) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "IBCSubDir" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "ImportDir" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "SourceDir" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "PkgBuild" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))) ((:+:) ((:+:) (C1 (MetaCons "PkgInstall" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "PkgClean" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "PkgCheck" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) ((:+:) (C1 (MetaCons "PkgREPL" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "PkgDocBuild" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "PkgDocInstall" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "PkgTest" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "PkgIndex" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath))) (C1 (MetaCons "WarnOnly" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "Pkg" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "BCAsm" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "DumpDefun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) ((:+:) (C1 (MetaCons "DumpCases" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "UseCodegen" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen)))))))) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "CodegenArgs" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "OutputTy" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 OutputType)))) ((:+:) (C1 (MetaCons "Extension" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 LanguageExt))) (C1 (MetaCons "InterpretScript" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))) ((:+:) ((:+:) (C1 (MetaCons "EvalExpr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "TargetTriple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "TargetCPU" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) ((:+:) (C1 (MetaCons "OptLevel" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) (C1 (MetaCons "AddOpt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Optimisation))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "RemoveOpt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Optimisation))) (C1 (MetaCons "Client" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "ShowOrigErr" PrefixI False) U1) ((:+:) (C1 (MetaCons "AutoWidth" PrefixI False) U1) (C1 (MetaCons "AutoSolve" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "UseConsoleWidth" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ConsoleWidth))) (C1 (MetaCons "DumpHighlights" PrefixI False) U1)) ((:+:) (C1 (MetaCons "DesugarNats" PrefixI False) U1) ((:+:) (C1 (MetaCons "NoElimDeprecationWarnings" PrefixI False) U1) (C1 (MetaCons "NoOldTacticDeprecationWarnings" PrefixI False) U1))))))))

data REPLPort Source #

Constructors

DontListen
ListenPort PortNumber

Instances

Eq REPLPort Source #
Methods (==) :: REPLPort -> REPLPort -> Bool # (/=) :: REPLPort -> REPLPort -> Bool #
Show REPLPort Source #
Methods showsPrec :: Int -> REPLPort -> ShowS # show :: REPLPort -> String # showList :: [REPLPort] -> ShowS #
Generic REPLPort Source #
Associated Types type Rep REPLPort :: * -> * # Methods from :: REPLPort -> Rep REPLPort x # to :: Rep REPLPort x -> REPLPort #
type Rep REPLPort Source #
type Rep REPLPort = D1 (MetaData "REPLPort" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) (C1 (MetaCons "DontListen" PrefixI False) U1) (C1 (MetaCons "ListenPort" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PortNumber))))

data Codegen Source #

Constructors

Via IRFormat String
Bytecode

Instances

Eq Codegen Source #
Methods (==) :: Codegen -> Codegen -> Bool # (/=) :: Codegen -> Codegen -> Bool #
Show Codegen Source #
Methods showsPrec :: Int -> Codegen -> ShowS # show :: Codegen -> String # showList :: [Codegen] -> ShowS #
Generic Codegen Source #
Associated Types type Rep Codegen :: * -> * # Methods from :: Codegen -> Rep Codegen x # to :: Rep Codegen x -> Codegen #
type Rep Codegen Source #
type Rep Codegen = D1 (MetaData "Codegen" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) (C1 (MetaCons "Via" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IRFormat)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) (C1 (MetaCons "Bytecode" PrefixI False) U1))

data LanguageExt Source #

Constructors

TypeProviders
ErrorReflection
UniquenessTypes
DSLNotation
ElabReflection
FCReflection
LinearTypes

Instances

Eq LanguageExt Source #
Methods (==) :: LanguageExt -> LanguageExt -> Bool # (/=) :: LanguageExt -> LanguageExt -> Bool #
Ord LanguageExt Source #
Methods compare :: LanguageExt -> LanguageExt -> Ordering # (<) :: LanguageExt -> LanguageExt -> Bool # (<=) :: LanguageExt -> LanguageExt -> Bool # (>) :: LanguageExt -> LanguageExt -> Bool # (>=) :: LanguageExt -> LanguageExt -> Bool # max :: LanguageExt -> LanguageExt -> LanguageExt # min :: LanguageExt -> LanguageExt -> LanguageExt #
Read LanguageExt Source #
Methods readsPrec :: Int -> ReadS LanguageExt # readList :: ReadS [LanguageExt] # readPrec :: ReadPrec LanguageExt # readListPrec :: ReadPrec [LanguageExt] #
Show LanguageExt Source #
Methods showsPrec :: Int -> LanguageExt -> ShowS # show :: LanguageExt -> String # showList :: [LanguageExt] -> ShowS #
Generic LanguageExt Source #
Associated Types type Rep LanguageExt :: * -> * # Methods from :: LanguageExt -> Rep LanguageExt x # to :: Rep LanguageExt x -> LanguageExt #
type Rep LanguageExt Source #
type Rep LanguageExt = D1 (MetaData "LanguageExt" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) ((:+:) (C1 (MetaCons "TypeProviders" PrefixI False) U1) ((:+:) (C1 (MetaCons "ErrorReflection" PrefixI False) U1) (C1 (MetaCons "UniquenessTypes" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "DSLNotation" PrefixI False) U1) (C1 (MetaCons "ElabReflection" PrefixI False) U1)) ((:+:) (C1 (MetaCons "FCReflection" PrefixI False) U1) (C1 (MetaCons "LinearTypes" PrefixI False) U1))))

data IRFormat Source #

Constructors

IBCFormat
JSONFormat

Instances

Eq IRFormat Source #
Methods (==) :: IRFormat -> IRFormat -> Bool # (/=) :: IRFormat -> IRFormat -> Bool #
Show IRFormat Source #
Methods showsPrec :: Int -> IRFormat -> ShowS # show :: IRFormat -> String # showList :: [IRFormat] -> ShowS #
Generic IRFormat Source #
Associated Types type Rep IRFormat :: * -> * # Methods from :: IRFormat -> Rep IRFormat x # to :: Rep IRFormat x -> IRFormat #
type Rep IRFormat Source #
type Rep IRFormat = D1 (MetaData "IRFormat" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) (C1 (MetaCons "IBCFormat" PrefixI False) U1) (C1 (MetaCons "JSONFormat" PrefixI False) U1))

data ConsoleWidth Source #

How wide is the console?

Constructors

InfinitelyWide	Have pretty-printer assume that lines should not be broken
ColsWide Int	Manually specified - must be positive
AutomaticWidth	Attempt to determine width, or 80 otherwise

Instances

Eq ConsoleWidth Source #
Methods (==) :: ConsoleWidth -> ConsoleWidth -> Bool # (/=) :: ConsoleWidth -> ConsoleWidth -> Bool #
Show ConsoleWidth Source #
Methods showsPrec :: Int -> ConsoleWidth -> ShowS # show :: ConsoleWidth -> String # showList :: [ConsoleWidth] -> ShowS #
Generic ConsoleWidth Source #
Associated Types type Rep ConsoleWidth :: * -> * # Methods from :: ConsoleWidth -> Rep ConsoleWidth x # to :: Rep ConsoleWidth x -> ConsoleWidth #
type Rep ConsoleWidth Source #
type Rep ConsoleWidth = D1 (MetaData "ConsoleWidth" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) (C1 (MetaCons "InfinitelyWide" PrefixI False) U1) ((:+:) (C1 (MetaCons "ColsWide" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) (C1 (MetaCons "AutomaticWidth" PrefixI False) U1)))

data HowMuchDocs Source #

Constructors

FullDocs
OverviewDocs

data OutputFmt Source #

Constructors

HTMLOutput
LaTeXOutput

data Optimisation Source #

Constructors

PETransform

partial eval and associated transforms

Instances

Eq Optimisation Source #
Methods (==) :: Optimisation -> Optimisation -> Bool # (/=) :: Optimisation -> Optimisation -> Bool #
Show Optimisation Source #
Methods showsPrec :: Int -> Optimisation -> ShowS # show :: Optimisation -> String # showList :: [Optimisation] -> ShowS #
Generic Optimisation Source #
Associated Types type Rep Optimisation :: * -> * # Methods from :: Optimisation -> Rep Optimisation x # to :: Rep Optimisation x -> Optimisation #
type Rep Optimisation Source #
type Rep Optimisation = D1 (MetaData "Optimisation" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) (C1 (MetaCons "PETransform" PrefixI False) U1)

data LogCat Source #

Recognised logging categories for the Idris compiler.

@TODO add in sub categories.

Constructors

IParse
IElab
ICodeGen
IErasure
ICoverage
IIBC

Instances

Eq LogCat Source #
Methods (==) :: LogCat -> LogCat -> Bool # (/=) :: LogCat -> LogCat -> Bool #
Ord LogCat Source #
Methods compare :: LogCat -> LogCat -> Ordering # (<) :: LogCat -> LogCat -> Bool # (<=) :: LogCat -> LogCat -> Bool # (>) :: LogCat -> LogCat -> Bool # (>=) :: LogCat -> LogCat -> Bool # max :: LogCat -> LogCat -> LogCat # min :: LogCat -> LogCat -> LogCat #
Show LogCat Source #
Methods showsPrec :: Int -> LogCat -> ShowS # show :: LogCat -> String # showList :: [LogCat] -> ShowS #
Generic LogCat Source #
Associated Types type Rep LogCat :: * -> * # Methods from :: LogCat -> Rep LogCat x # to :: Rep LogCat x -> LogCat #
type Rep LogCat Source #
type Rep LogCat = D1 (MetaData "LogCat" "Idris.Options" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" False) ((:+:) ((:+:) (C1 (MetaCons "IParse" PrefixI False) U1) ((:+:) (C1 (MetaCons "IElab" PrefixI False) U1) (C1 (MetaCons "ICodeGen" PrefixI False) U1))) ((:+:) (C1 (MetaCons "IErasure" PrefixI False) U1) ((:+:) (C1 (MetaCons "ICoverage" PrefixI False) U1) (C1 (MetaCons "IIBC" PrefixI False) U1))))