idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Options

Description

 
Synopsis

Documentation

data Codegen Source #

Constructors

Via IRFormat String 
Bytecode 
Instances
Eq Codegen Source # 
Instance details

Defined in Idris.Options

Methods

(==) :: Codegen -> Codegen -> Bool #

(/=) :: Codegen -> Codegen -> Bool #

Show Codegen Source # 
Instance details

Defined in Idris.Options

Generic Codegen Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep Codegen :: * -> * #

Methods

from :: Codegen -> Rep Codegen x #

to :: Rep Codegen x -> Codegen #

Binary Codegen # 
Instance details

Defined in Idris.IBC

Methods

put :: Codegen -> Put #

get :: Get Codegen #

putList :: [Codegen] -> Put #

NFData Codegen # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Codegen -> () #

type Rep Codegen Source # 
Instance details

Defined in Idris.Options

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 # 
Instance details

Defined in Idris.Options

Show ConsoleWidth Source # 
Instance details

Defined in Idris.Options

Generic ConsoleWidth Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep ConsoleWidth :: * -> * #

NFData ConsoleWidth # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: ConsoleWidth -> () #

type Rep ConsoleWidth Source # 
Instance details

Defined in Idris.Options

type Rep ConsoleWidth = D1 (MetaData "ConsoleWidth" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "InfinitelyWide" PrefixI False) (U1 :: * -> *) :+: (C1 (MetaCons "ColsWide" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "AutomaticWidth" PrefixI False) (U1 :: * -> *)))

data IRFormat Source #

Constructors

IBCFormat 
JSONFormat 
Instances
Eq IRFormat Source # 
Instance details

Defined in Idris.Options

Show IRFormat Source # 
Instance details

Defined in Idris.Options

Generic IRFormat Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep IRFormat :: * -> * #

Methods

from :: IRFormat -> Rep IRFormat x #

to :: Rep IRFormat x -> IRFormat #

Binary IRFormat # 
Instance details

Defined in Idris.IBC

Methods

put :: IRFormat -> Put #

get :: Get IRFormat #

putList :: [IRFormat] -> Put #

NFData IRFormat # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: IRFormat -> () #

type Rep IRFormat Source # 
Instance details

Defined in Idris.Options

type Rep IRFormat = D1 (MetaData "IRFormat" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "IBCFormat" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "JSONFormat" PrefixI False) (U1 :: * -> *))

data LanguageExt Source #

Instances
Eq LanguageExt Source # 
Instance details

Defined in Idris.Options

Ord LanguageExt Source # 
Instance details

Defined in Idris.Options

Read LanguageExt Source # 
Instance details

Defined in Idris.Options

Show LanguageExt Source # 
Instance details

Defined in Idris.Options

Generic LanguageExt Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep LanguageExt :: * -> * #

Binary LanguageExt # 
Instance details

Defined in Idris.IBC

NFData LanguageExt # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: LanguageExt -> () #

type Rep LanguageExt Source # 
Instance details

Defined in Idris.Options

type Rep LanguageExt = D1 (MetaData "LanguageExt" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" 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 LogCat Source #

Recognised logging categories for the Idris compiler.

@TODO add in sub categories.

Instances
Eq LogCat Source # 
Instance details

Defined in Idris.Options

Methods

(==) :: LogCat -> LogCat -> Bool #

(/=) :: LogCat -> LogCat -> Bool #

Ord LogCat Source # 
Instance details

Defined in Idris.Options

Show LogCat Source # 
Instance details

Defined in Idris.Options

Generic LogCat Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep LogCat :: * -> * #

Methods

from :: LogCat -> Rep LogCat x #

to :: Rep LogCat x -> LogCat #

NFData LogCat # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: LogCat -> () #

type Rep LogCat Source # 
Instance details

Defined in Idris.Options

type Rep LogCat = D1 (MetaData "LogCat" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> *))))

data Opt Source #

Instances
Eq Opt Source # 
Instance details

Defined in Idris.Options

Methods

(==) :: Opt -> Opt -> Bool #

(/=) :: Opt -> Opt -> Bool #

Show Opt Source # 
Instance details

Defined in Idris.Options

Methods

showsPrec :: Int -> Opt -> ShowS #

show :: Opt -> String #

showList :: [Opt] -> ShowS #

Generic Opt Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep Opt :: * -> * #

Methods

from :: Opt -> Rep Opt x #

to :: Rep Opt x -> Opt #

NFData Opt # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Opt -> () #

type Rep Opt Source # 
Instance details

Defined in Idris.Options

type Rep Opt = D1 (MetaData "Opt" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) ((((((C1 (MetaCons "Filename" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 :: Maybe 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 :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "IndentClause" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) :+: (C1 (MetaCons "OLogCats" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [LogCat])) :+: C1 (MetaCons "Output" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "Port" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 REPLPort)))))))) :+: (((((C1 (MetaCons "IBCSubDir" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "ImportDir" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "SourceDir" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "PkgBuild" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "PkgInstall" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "PkgClean" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "PkgCheck" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "PkgREPL" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "PkgDocBuild" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))))) :+: (((C1 (MetaCons "PkgDocInstall" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "PkgTest" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "PkgIndex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath)) :+: C1 (MetaCons "WarnOnly" PrefixI False) (U1 :: * -> *))) :+: ((C1 (MetaCons "Pkg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "BCAsm" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "DumpDefun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "DumpCases" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "UseCodegen" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen))))))) :+: ((((C1 (MetaCons "CodegenArgs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "OutputTy" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 OutputType))) :+: (C1 (MetaCons "Extension" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 LanguageExt)) :+: C1 (MetaCons "InterpretScript" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "EvalExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "TargetTriple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "TargetCPU" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "OptLevel" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "AddOpt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Optimisation)))))) :+: (((C1 (MetaCons "RemoveOpt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Optimisation)) :+: C1 (MetaCons "Client" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ConsoleWidth)) :+: C1 (MetaCons "DumpHighlights" PrefixI False) (U1 :: * -> *)) :+: (C1 (MetaCons "DesugarNats" PrefixI False) (U1 :: * -> *) :+: (C1 (MetaCons "NoOldTacticDeprecationWarnings" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "AllowCapitalizedPatternVariables" PrefixI False) (U1 :: * -> *))))))))

data Optimisation Source #

Constructors

PETransform

partial eval and associated transforms

Instances
Eq Optimisation Source # 
Instance details

Defined in Idris.Options

Show Optimisation Source # 
Instance details

Defined in Idris.Options

Generic Optimisation Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep Optimisation :: * -> * #

NFData Optimisation # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Optimisation -> () #

type Rep Optimisation Source # 
Instance details

Defined in Idris.Options

type Rep Optimisation = D1 (MetaData "Optimisation" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "PETransform" PrefixI False) (U1 :: * -> *))

data REPLPort Source #

Instances
Eq REPLPort Source # 
Instance details

Defined in Idris.Options

Show REPLPort Source # 
Instance details

Defined in Idris.Options

Generic REPLPort Source # 
Instance details

Defined in Idris.Options

Associated Types

type Rep REPLPort :: * -> * #

Methods

from :: REPLPort -> Rep REPLPort x #

to :: Rep REPLPort x -> REPLPort #

NFData REPLPort # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: REPLPort -> () #

type Rep REPLPort Source # 
Instance details

Defined in Idris.Options

type Rep REPLPort = D1 (MetaData "REPLPort" "Idris.Options" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "DontListen" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "ListenPort" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PortNumber)))

getPkgMkDoc Source #

Arguments

:: Opt

Opt to extract

-> Maybe (Bool, String)

Result

Returns None if given an Opt which is not PkgMkDoc Otherwise returns Just x, where x is the contents of PkgMkDoc

getPkgTest Source #

Arguments

:: Opt

the option to extract

-> Maybe String

the package file to test

opt :: (Opt -> Maybe a) -> [Opt] -> [a] Source #