Safe Haskell	None

Idris.AbsSyntaxTree

Synopsis

Documentation

data IOption Source

Constructors

IOption

Fields

opt_logLevel :: Int
opt_typecase :: Bool
opt_typeintype :: Bool
opt_coverage :: Bool
opt_showimp :: Bool: ^ show implicits
opt_errContext :: Bool
opt_repl :: Bool
opt_verbose :: Bool
opt_nobanner :: Bool
opt_quiet :: Bool
opt_codegen :: Codegen
opt_outputTy :: OutputType
opt_ibcsubdir :: FilePath
opt_importdirs :: [FilePath]
opt_triple :: String
opt_cpu :: String
opt_optLevel :: Word
opt_cmdline :: [Opt]
opt_origerr :: Bool

Instances

Eq IOption
Show IOption

defaultOpts :: IOption Source

data LanguageExt Source

Constructors

TypeProviders
ErrorReflection

Instances

Eq LanguageExt
Ord LanguageExt
Read LanguageExt
Show LanguageExt

data OutputMode Source

The output mode in use

Constructors

RawOutput
IdeSlave Integer

Instances

Show OutputMode

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

data IState Source

The global state used in the Idris monad

Constructors

IState

Fields

tt_ctxt :: Context: All the currently defined names and their terms
idris_constraints :: [(UConstraint, FC)]: A list of universe constraints and their corresponding source locations
idris_infixes :: [FixDecl]: Currently defined infix operators
idris_implicits :: Ctxt [PArg]
idris_statics :: Ctxt [Bool]
idris_classes :: Ctxt ClassInfo
idris_dsls :: Ctxt DSL
idris_optimisation :: Ctxt OptInfo
idris_datatypes :: Ctxt TypeInfo
idris_namehints :: Ctxt [Name]
idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]): list of lhs/rhs, and a list of missing clauses
idris_flags :: Ctxt [FnOpt]
idris_callgraph :: Ctxt CGInfo
idris_calledgraph :: Ctxt [Name]
idris_docstrings :: Ctxt String
idris_totcheck :: [(FC, Name)]
idris_defertotcheck :: [(FC, Name)]
idris_options :: IOption
idris_name :: Int
idris_lineapps :: [((FilePath, Int), PTerm)]: Full application LHS on source line
idris_metavars :: [(Name, (Maybe Name, Int, Bool))]: The currently defined but not proven metavariables
idris_coercions :: [Name]
idris_transforms :: [(Term, Term)]
idris_errRev :: [(Term, Term)]
syntax_rules :: [Syntax]
syntax_keywords :: [String]
imported :: [FilePath]: The imported modules
idris_scprims :: [(Name, (Int, PrimFn))]
idris_objs :: [(Codegen, FilePath)]
idris_libs :: [(Codegen, String)]
idris_cgflags :: [(Codegen, String)]
idris_hdrs :: [(Codegen, String)]
proof_list :: [(Name, [String])]
errLine :: Maybe Int
lastParse :: Maybe Name
indent_stack :: [Int]
brace_stack :: [Maybe Int]
hide_list :: [(Name, Maybe Accessibility)]
default_access :: Accessibility
default_total :: Bool
ibc_write :: [IBCWrite]
compiled_so :: Maybe String
idris_dynamic_libs :: [DynamicLib]
idris_language_extensions :: [LanguageExt]
idris_outputmode :: OutputMode
idris_colourRepl :: Bool
idris_colourTheme :: ColourTheme
idris_outh :: Handle
idris_errorhandlers :: [Name]: Global error handlers
idris_nameIdx :: (Int, Ctxt (Int, Name))
idris_function_errorhandlers :: Ctxt (Map Name (Set Name)): Specific error handlers
module_aliases :: Map [Text] [Text]
idris_consolewidth :: ConsoleWidth: How many chars wide is the console?

data SizeChange Source

Constructors

Smaller
Same
Bigger
Unknown

Instances

Eq SizeChange
Show SizeChange
Binary SizeChange
NFData SizeChange

type SCGEntry = (Name, [Maybe (Int, SizeChange)])Source

data CGInfo Source

Constructors

CGInfo
Fields argsdef :: [Name] calls :: [(Name, [[Name]])] scg :: [SCGEntry] argsused :: [Name] unusedpos :: [Int]

Instances

Show CGInfo
Binary CGInfo
NFData CGInfo

primDefs :: [Name]Source

idrisInit :: IState Source

The initial state for the compiler

type Idris = StateT IState (ErrorT Err IO)Source

The monad for the main REPL - reading and processing files and updating global state (hence the IO inner monad). type Idris = WriterT [Either String (IO ())] (State IState a))

data Codegen Source

Constructors

ViaC
ViaJava
ViaNode
ViaJavaScript
ViaLLVM
Bytecode

Instances

Eq Codegen
Show Codegen
Binary Codegen

data Fixity Source

Constructors

Infixl
Fields prec :: Int
Infixr
Fields prec :: Int
InfixN
Fields prec :: Int
PrefixN
Fields prec :: Int

Instances

Eq Fixity
Show Fixity
Binary Fixity
NFData Fixity

data FixDecl Source

Constructors

Fix Fixity String

Instances

Eq FixDecl
Ord FixDecl
Show FixDecl
Binary FixDecl
NFData FixDecl

data Static Source

Constructors

Static
Dynamic

Instances

Eq Static
Show Static
Binary Static
NFData Static

data Plicity Source

Constructors

Imp
Fields pargopts :: [ArgOpt] pstatic :: Static pdocstr :: String pparam :: Bool
Exp
Fields pargopts :: [ArgOpt] pstatic :: Static pdocstr :: String pparam :: Bool
Constraint
Fields pargopts :: [ArgOpt] pstatic :: Static pdocstr :: String
TacImp
Fields pargopts :: [ArgOpt] pstatic :: Static pscript :: PTerm pdocstr :: String

Instances

Eq Plicity
Show Plicity
Binary Plicity
NFData Plicity

plazy :: Plicity -> Bool Source

impl :: Plicity Source

expl :: Plicity Source

expl_param :: Plicity Source

constraint :: Plicity Source

tacimpl :: PTerm -> Plicity Source

data FnOpt Source

Constructors

Inlinable
TotalFn
PartialFn
Coinductive
AssertTotal
Dictionary
Implicit
CExport String
ErrorHandler	^ an error handler for use with the ErrorReflection extension
ErrorReverse	^ attempt to reverse normalise before showing in error
Reflection
Specialise [(Name, Maybe Int)]

Instances

Eq FnOpt
Show FnOpt
Binary FnOpt
NFData FnOpt

type FnOpts = [FnOpt]Source

inlinable :: FnOpts -> Bool Source

dictionary :: FnOpts -> Bool Source

data DataOpt Source

Data declaration options

Constructors

Codata
DefaultEliminator
DataErrRev

Instances

Eq DataOpt
Show DataOpt
Binary DataOpt
NFData DataOpt

type DataOpts = [DataOpt]Source

data PDecl' t Source

Top-level declarations such as compiler directives, definitions, datatypes and typeclasses.

Constructors

PFix FC Fixity [String]	Fixity declaration
PTy String SyntaxInfo FC FnOpts Name t	Type declaration
PPostulate String SyntaxInfo FC FnOpts Name t	Postulate
PClauses FC FnOpts Name [PClause' t]	Pattern clause
PCAF FC Name t	Top level constant
PData String SyntaxInfo FC DataOpts (PData' t)	Data declaration.
PParams FC [(Name, t)] [PDecl' t]	Params block
PNamespace String [PDecl' t]	New namespace
PRecord String SyntaxInfo FC Name t String Name t	Record declaration
PClass String SyntaxInfo FC [t] Name [(Name, t)] [PDecl' t]	Type class: arguments are documentation, syntax info, source location, constraints, class name, parameters, method declarations
PInstance SyntaxInfo FC [t] Name [t] t (Maybe Name) [PDecl' t]	Instance declaration: arguments are syntax info, source location, constraints, class name, parameters, full instance type, optional explicit name, and definitions
PDSL Name (DSL' t)	DSL declaration
PSyntax FC Syntax	Syntax definition
PMutual FC [PDecl' t]	Mutual block
PDirective (Idris ())	Compiler directive. The parser inserts the corresponding action in the Idris monad.
PProvider SyntaxInfo FC Name t t	Type provider. The first t is the type, the second is the term
PTransform FC Bool t t	Source-to-source transformation rule. If bool is True, lhs and rhs must be convertible

Instances

Functor PDecl'
Show PDecl
Binary t => Binary (PDecl' t)
NFData t => NFData (PDecl' t)

type ElabD a = Elab' [PDecl] aSource

data PClause' t Source

One clause of a top-level definition. Term arguments to constructors are:

The whole application (missing for PClauseR and PWithR because they're within a with clause)
The list of extra with patterns
The right-hand side
The where block (PDecl' t)

Constructors

PClause FC Name t [t] t [PDecl' t]	A normal top-level definition.
PWith FC Name t [t] t [PDecl' t]
PClauseR FC [t] t [PDecl' t]
PWithR FC [t] t [PDecl' t]

Instances

Functor PClause'
Show PClause
Binary t => Binary (PClause' t)
NFData t => NFData (PClause' t)

data PData' t Source

Data declaration

Constructors

PDatadecl	Data declaration
Fields d_name :: Name The name of the datatype d_tcon :: t Type constructor d_cons :: [(String, Name, t, FC, [Name])] Constructors
PLaterdecl	Placeholder for data whose constructors are defined later
Fields d_name :: Name The name of the datatype d_tcon :: t Type constructor

Instances

Functor PData'
Show PData
Binary t => Binary (PData' t)
NFData t => NFData (PData' t)

type PDecl = PDecl' PTerm Source

type PData = PData' PTerm Source

type PClause = PClause' PTerm Source

declared :: PDecl -> [Name]Source

tldeclared :: PDecl -> [Name]Source

defined :: PDecl -> [Name]Source

updateN :: [(Name, Name)] -> Name -> Name Source

updateNs :: [(Name, Name)] -> PTerm -> PTerm Source

data PunInfo Source

Constructors

IsType
IsTerm
TypeOrTerm

Instances

Eq PunInfo
Show PunInfo
Binary PunInfo
NFData PunInfo

data PTerm Source

High level language terms

Constructors

PQuote Raw
PRef FC Name
PInferRef FC Name	A name to be defined later
PPatvar FC Name
PLam Name PTerm PTerm
PPi Plicity Name PTerm PTerm
PLet Name PTerm PTerm PTerm
PTyped PTerm PTerm	Term with explicit type
PApp FC PTerm [PArg]
PAppBind FC PTerm [PArg]	implicitly bound application
PMatchApp FC Name	Make an application by type matching
PCase FC PTerm [(PTerm, PTerm)]
PTrue FC PunInfo
PFalse FC
PRefl FC PTerm
PResolveTC FC
PEq FC PTerm PTerm
PRewrite FC PTerm PTerm (Maybe PTerm)
PPair FC PunInfo PTerm PTerm
PDPair FC PTerm PTerm PTerm
PAlternative Bool [PTerm]
PHidden PTerm	Irrelevant or hidden pattern
PType
PGoal FC PTerm Name PTerm
PConstant Const
Placeholder
PDoBlock [PDo]
PIdiom FC PTerm
PReturn FC
PMetavar Name
PProof [PTactic]	Proof script
PTactics [PTactic]	As PProof, but no auto solving
PElabError Err	Error to report on elaboration
PImpossible	Special case for declaring when an LHS can't typecheck
PCoerced PTerm	To mark a coerced argument, so as not to coerce twice
PDisamb [[Text]] PTerm	Preferences for explicit namespaces
PUnifyLog PTerm	dump a trace of unifications when building term
PNoImplicits PTerm	never run implicit converions on the term

Instances

Eq PTerm
Show PTerm
Show PClause
Show PData
Show PDecl
Binary PTerm
NFData PTerm

mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm Source

data PTactic' t Source

Constructors

Intro [Name]
Intros
Focus Name
Refine Name [Bool]
Rewrite t
Induction Name
Equiv t
MatchRefine Name
LetTac Name t
LetTacTy Name t t
Exact t
Compute
Trivial
TCInstance
ProofSearch (Maybe Name) Name [Name]
Solve
Attack
ProofState
ProofTerm
Undo
Try (PTactic' t) (PTactic' t)
TSeq (PTactic' t) (PTactic' t)
ApplyTactic t
ByReflection t
Reflect t
Fill t
GoalType String (PTactic' t)
Qed
Abandon

Instances

Functor PTactic'
Eq t => Eq (PTactic' t)
Show t => Show (PTactic' t)
Binary t => Binary (PTactic' t)
NFData t => NFData (PTactic' t)

type PTactic = PTactic' PTerm Source

data PDo' t Source

Constructors

DoExp FC t
DoBind FC Name t
DoBindP FC t t
DoLet FC Name t t
DoLetP FC t t

Instances

Functor PDo'
Eq t => Eq (PDo' t)
Binary t => Binary (PDo' t)
NFData t => NFData (PDo' t)

type PDo = PDo' PTerm Source

data PArg' t Source

Constructors

PImp
Fields priority :: Int machine_inf :: Bool argopts :: [ArgOpt] pname :: Name getTm :: t pargdoc :: String
PExp
Fields priority :: Int argopts :: [ArgOpt] getTm :: t pargdoc :: String
PConstraint
Fields priority :: Int argopts :: [ArgOpt] getTm :: t pargdoc :: String
PTacImplicit
Fields priority :: Int argopts :: [ArgOpt] pname :: Name getScript :: t getTm :: t pargdoc :: String

Instances

Functor PArg'
Eq t => Eq (PArg' t)
Show t => Show (PArg' t)
Binary t => Binary (PArg' t)
NFData t => NFData (PArg' t)

data ArgOpt Source

Constructors

Lazy
HideDisplay

Instances

Eq ArgOpt
Show ArgOpt
Binary ArgOpt
NFData ArgOpt

lazyarg :: PArg' t -> Bool Source

pimp :: Name -> t -> Bool -> PArg' tSource

pexp :: t -> PArg' tSource

pconst :: t -> PArg' tSource

ptacimp :: Name -> t -> t -> PArg' tSource

type PArg = PArg' PTerm Source

data ClassInfo Source

Constructors

CI
Fields instanceName :: Name class_methods :: [(Name, (FnOpts, PTerm))] class_defaults :: [(Name, (Name, PDecl))] class_default_superclasses :: [PDecl] class_params :: [Name] class_instances :: [Name]

Instances

Show ClassInfo
Binary ClassInfo
NFData ClassInfo

data Forceability Source

Constructors

Conditional
Unconditional

Instances

Bounded Forceability
Enum Forceability
Eq Forceability
Ord Forceability
Show Forceability
Binary Forceability
NFData Forceability

data OptInfo Source

Constructors

Optimise
Fields collapsible :: Bool isnewtype :: Bool forceable :: [(Int, Forceability)] recursive :: [Int]

Instances

Show OptInfo
Binary OptInfo
NFData OptInfo

data TypeInfo Source

Constructors

TI
Fields con_names :: [Name] codata :: Bool data_opts :: DataOpts param_pos :: [Int]

Instances

Show TypeInfo
Binary TypeInfo
NFData TypeInfo

data DSL' t Source

Constructors

DSL
Fields dsl_bind :: t dsl_return :: t dsl_apply :: t dsl_pure :: t dsl_var :: Maybe t index_first :: Maybe t index_next :: Maybe t dsl_lambda :: Maybe t dsl_let :: Maybe t

Instances

Functor DSL'
Show t => Show (DSL' t)
Binary t => Binary (DSL' t)
NFData t => NFData (DSL' t)

type DSL = DSL' PTerm Source

data SynContext Source

Constructors

PatternSyntax
TermSyntax
AnySyntax

Instances

Show SynContext
Binary SynContext
NFData SynContext

data Syntax Source

Constructors

Rule [SSymbol] PTerm SynContext

Instances

Show Syntax
Binary Syntax
NFData Syntax

data SSymbol Source

Constructors

Keyword Name
Symbol String
Binding Name
Expr Name
SimpleExpr Name

Instances

Show SSymbol
Binary SSymbol
NFData SSymbol

initDSL :: DSL' PTerm Source

data Using Source

Constructors

UImplicit Name PTerm
UConstraint Name [Name]

Instances

Eq Using
Show Using
Binary Using
NFData Using

data SyntaxInfo Source

Constructors

Syn
Fields using :: [Using] syn_params :: [(Name, PTerm)] syn_namespace :: [String] no_imp :: [Name] decoration :: Name -> Name inPattern :: Bool implicitAllowed :: Bool dsl_info :: DSL

Instances

Show SyntaxInfo
Binary SyntaxInfo
NFData SyntaxInfo

defaultSyntax :: SyntaxInfo Source

expandNS :: SyntaxInfo -> Name -> Name Source

bi :: FC Source

inferTy :: Name Source

inferCon :: Name Source

inferDecl :: PData' PTerm Source

inferOpts :: [a]Source

infTerm :: PTerm -> PTerm Source

infP :: TT Name Source

getInferTerm :: Term -> Term Source

getInferType :: Term -> Term Source

primNames :: [Name]Source

unitTy :: Name Source

unitCon :: Name Source

unitDecl :: PData' PTerm Source

unitOpts :: [DataOpt]Source

falseTy :: Name Source

falseDecl :: PData' PTerm Source

falseOpts :: [a]Source

pairTy :: Name Source

pairCon :: Name Source

pairDecl :: PData' PTerm Source

pairOpts :: [a]Source

eqTy :: Name Source

eqCon :: Name Source

eqDecl :: PData' PTerm Source

eqOpts :: [a]Source

elimName :: Name Source

elimMethElimTy :: Name Source

elimMethElim :: Name Source

elimDecl :: PDecl' PTerm Source

sigmaTy :: Name Source

existsCon :: Name Source

piBind :: [(Name, PTerm)] -> PTerm -> PTerm Source

piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm Source

consoleDecorate :: IState -> OutputAnnotation -> String -> String Source

Colourise annotations according to an Idris state. It ignores the names in the annotation, as there's no good way to show extended information on a terminal.

prettyImp Source

Arguments

:: Bool	^ whether to show implicits
-> PTerm	^ the term to pretty-print
-> Doc OutputAnnotation

Pretty-print a high-level closed Idris term

pprintPTerm Source

Arguments

:: Bool	^ whether to show implicits
-> [(Name, Bool)]	^ the currently-bound names and whether they are implicit
-> PTerm	^ the term to pretty-print
-> Doc OutputAnnotation

Pretty-print a high-level Idris term in some bindings context

bindingOf Source

Arguments

:: Name	^ the bound name
-> Bool	^ whether the name is implicit
-> Doc OutputAnnotation

Pretty-printer helper for the binding site of a name

prettyName Source

Arguments

:: Bool	^ whether to show namespaces
-> [(Name, Bool)]	^ the current bound variables and whether they are implicit
-> Name	^ the name to pprint
-> Doc OutputAnnotation

Pretty-printer helper for names that attaches the correct annotations

showCImp :: Bool -> PClause -> Doc OutputAnnotation Source

showDImp :: Bool -> PData -> Doc OutputAnnotation Source

showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation Source

showDeclImp :: Bool -> PDecl' PTerm -> Doc OutputAnnotation Source

getImps :: [PArg] -> [(Name, PTerm)]Source

getExps :: [PArg] -> [PTerm]Source

getConsts :: [PArg] -> [PTerm]Source

getAll :: [PArg] -> [PTerm]Source

showName Source

Arguments

:: Maybe IState	^ the Idris state, for information about names and colours
-> [(Name, Bool)]	^ the bound variables and whether they're implicit
-> Bool	^ whether to show implicits
-> Bool	^ whether to colourise
-> Name	^ the term to show
-> String

Show Idris name

showTm Source

Arguments

:: IState	^ the Idris state, for information about identifiers and colours
-> PTerm	^ the term to show
-> String

showTmImpls :: PTerm -> String Source

Show a term with implicits, no colours

getPArity :: PTerm -> Int Source

allNamesIn :: PTerm -> [Name]Source

boundNamesIn :: PTerm -> [Name]Source

namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]Source

usedNamesIn :: [Name] -> IState -> PTerm -> [Name]Source

IBCFix FixDecl
IBCImp Name
IBCStatic Name
IBCClass Name
IBCInstance Bool Name Name
IBCDSL Name
IBCData Name
IBCOpt Name
IBCSyntax Syntax
IBCKeyword String
IBCImport FilePath
IBCObj Codegen FilePath
IBCLib Codegen String
IBCCGFlag Codegen String
IBCDyLib String
IBCHeader Codegen String
IBCAccess Name Accessibility
IBCMetaInformation Name MetaInformation
IBCTotal Name Totality
IBCFlags Name [FnOpt]
IBCTrans (Term, Term)
IBCErrRev (Term, Term)
IBCCG Name
IBCDoc Name
IBCCoercion Name
IBCDef Name
IBCNameHint (Name, Name)
IBCLineApp FilePath Int PTerm
IBCErrorHandler Name
IBCFunctionErrorHandler Name Name Name

Quit
Help
Eval PTerm
Check PTerm
DocStr Name
TotCheck Name
Reload
Load FilePath
ChangeDirectory FilePath
ModImport String
Edit
Compile Codegen String
Execute
ExecVal PTerm
Metavars
Prove Name
AddProof (Maybe Name)
RmProof Name
ShowProof Name
Proofs
Universes
LogLvl Int
Spec PTerm
HNF PTerm
TestInline PTerm
Defn Name
Info Name
Missing Name
DynamicLink FilePath
ListDynamic
Pattelab PTerm
DebugInfo Name
Search PTerm
CaseSplitAt Bool Int Name
AddClauseFrom Bool Int Name
AddProofClauseFrom Bool Int Name
AddMissing Bool Int Name
MakeWith Bool Int Name
DoProofSearch Bool Int Name [Name]
SetOpt Opt
UnsetOpt Opt
NOP
SetColour ColourType IdrisColour
ColourOn
ColourOff
ListErrorHandlers
SetConsoleWidth ConsoleWidth

Filename String
Ver
Usage
Quiet
NoBanner
ColourREPL Bool
Ideslave
ShowLibs
ShowLibdir
ShowIncs
NoBasePkgs
NoPrelude
NoBuiltins
NoREPL
OLogging Int
Output String
TypeCase
TypeInType
DefaultTotal
DefaultPartial
WarnPartial
NoCoverage
ErrContext
ShowImpl
Verbose
IBCSubDir String
ImportDir String
PkgBuild String
PkgInstall String
PkgClean String
PkgCheck String
PkgREPL String
WarnOnly
Pkg String
BCAsm String
DumpDefun String
DumpCases String
UseCodegen Codegen
OutputTy OutputType
Extension LanguageExt
InterpretScript String
TargetTriple String
TargetCPU String
OptLevel Word
Client String
ShowOrigErr
AutoWidth	Automatically adjust terminal width