Safe Haskell	None
Language	Haskell98

Idris.AbsSyntaxTree

Synopsis

Documentation

data ElabWhat Source

Constructors

ETypes
EDefns
EAll

Instances

Eq ElabWhat
Show ElabWhat

data ElabInfo Source

Constructors

EInfo
Fields params :: [(Name, PTerm)] inblock :: Ctxt [Name] liftname :: Name -> Name namespace :: Maybe [String] rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

toplevel :: ElabInfo Source

eInfoNames :: ElabInfo -> [Name] Source

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
opt_autoSolve :: Bool: automatically apply "solve" tactic in prover
opt_autoImport :: [FilePath]: e.g. Builtins+Prelude

Instances

Eq IOption
Show IOption

defaultOpts :: IOption Source

data PPOption Source

Constructors

PPOption
Fields ppopt_impl :: Bool ^ whether to show implicits

Instances

Show PPOption

defaultPPOption :: PPOption Source

Pretty printing options with default verbosity.

verbosePPOption :: PPOption Source

Pretty printing options with the most verbosity.

ppOption :: IOption -> PPOption Source

Get pretty printing options from the big options record.

ppOptionIst :: IState -> PPOption Source

Get pretty printing options from an idris state record.

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 Handle	Print user output directly to the handle
IdeSlave Integer Handle	Send IDE output for some request ID to the handle

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 (Docstring, [(Name, Docstring)])
idris_tyinfodata :: Ctxt TIData
idris_fninfo :: Ctxt FnInfo
idris_totcheck :: [(FC, Name)]
idris_defertotcheck :: [(FC, Name)]
idris_totcheckfail :: [(FC, String)]
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)]
idris_imported :: [FilePath]: Imported ibc file names
proof_list :: [(Name, [String])]
errSpan :: Maybe FC
parserWarnings :: [(FC, Err)]
lastParse :: Maybe Name
indent_stack :: [Int]
brace_stack :: [Maybe Int]
lastTokenSpan :: Maybe FC: What was the span of the latest token parsed?
idris_parsedSpan :: Maybe FC
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_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?
idris_postulates :: Set Name
idris_whocalls :: Maybe (Map Name [Name])
idris_callswho :: Maybe (Map Name [Name])
idris_repl_defs :: [Name]: List of names that were defined in the repl, and can be re-/un-defined

Instances

Show IState
TokenParsing IdrisParser

data SizeChange Source

Constructors

Smaller
Same
Bigger
Unknown

Instances

Eq SizeChange
Show SizeChange
Binary SizeChange
NFData SizeChange

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

type UsageReason = (Name, Int) Source

data CGInfo Source

Constructors

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

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

Via String
Bytecode

Instances

Eq Codegen
Show Codegen
Binary Codegen

data Command Source

REPL commands

Constructors

Quit
Help
Eval PTerm
NewDefn [PDecl]	Each `PDecl` should be either a type declaration (at most one) or a clause defining the same name.
Undefine [Name]
Check PTerm
DocStr (Either Name Const)
TotCheck Name
Reload
Load FilePath (Maybe Int)
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
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
MakeLemma Bool Int Name
DoProofSearch Bool Bool Int Name [Name]	the first bool is whether to update, the second is whether to search recursively (i.e. for the arguments)
SetOpt Opt
UnsetOpt Opt
NOP
SetColour ColourType IdrisColour
ColourOn
ColourOff
ListErrorHandlers
SetConsoleWidth ConsoleWidth
Apropos String
WhoCalls Name
CallsWho Name
MakeDoc String
Warranty

data Opt Source

Constructors

Filename String
Quiet
NoBanner
ColourREPL Bool
Ideslave
IdeslaveSocket
ShowLibs
ShowLibdir
ShowIncs
NoBasePkgs
NoPrelude
NoBuiltins
NoREPL
OLogging Int
Output String
TypeCase
TypeInType
DefaultTotal
DefaultPartial
WarnPartial
WarnReach
NoCoverage
ErrContext
ShowImpl
Verbose
IBCSubDir String
ImportDir String
PkgBuild String
PkgInstall String
PkgClean String
PkgCheck String
PkgREPL String
PkgMkDoc String
PkgTest String
WarnOnly
Pkg String
BCAsm String
DumpDefun String
DumpCases String
UseCodegen Codegen
OutputTy OutputType
Extension LanguageExt
InterpretScript String
EvalExpr String
TargetTriple String
TargetCPU String
OptLevel Word
Client String
ShowOrigErr
AutoWidth	Automatically adjust terminal width
AutoSolve	Automatically issue "solve" tactic in interactive prover

Instances

Eq Opt
Show Opt

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 pparam :: Bool
Exp
Fields pargopts :: [ArgOpt] pstatic :: Static pparam :: Bool
Constraint
Fields pargopts :: [ArgOpt] pstatic :: Static
TacImp
Fields pargopts :: [ArgOpt] pstatic :: Static pscript :: PTerm

Instances

Eq Plicity
Show Plicity
Binary Plicity
NFData Plicity

impl :: Plicity Source

expl :: Plicity Source

expl_param :: Plicity Source

constraint :: Plicity Source

tacimpl :: PTerm -> Plicity Source

data FnOpt Source

Constructors

Inlinable
TotalFn
PartialFn
CoveringFn
Coinductive
AssertTotal
Dictionary
Implicit
NoImplicit
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)]
Constructor

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	Set if the the data-type is coinductive
DefaultEliminator	Set if an eliminator should be generated for data type
DefaultCaseFun	Set if a case function should be generated for data type
DataErrRev

Instances

Eq DataOpt
Show DataOpt
Binary DataOpt
NFData DataOpt

type DataOpts = [DataOpt] Source

data ProvideWhat' t Source

Type provider - what to provide

Constructors

ProvTerm t t	the first is the goal type, the second is the term
ProvPostulate t	goal type must be Type, so only term

Instances

Functor ProvideWhat'
Eq t => Eq (ProvideWhat' t)
Show t => Show (ProvideWhat' t)
NFData t => NFData (ProvideWhat' t)

type ProvideWhat = ProvideWhat' PTerm Source

data PDecl' t Source

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

Constructors

PFix FC Fixity [String]	Fixity declaration
PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t	Type declaration
PPostulate Docstring SyntaxInfo FC FnOpts Name t	Postulate
PClauses FC FnOpts Name [PClause' t]	Pattern clause
PCAF FC Name t	Top level constant
PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t)	Data declaration.
PParams FC [(Name, t)] [PDecl' t]	Params block
PNamespace String [PDecl' t]	New namespace
PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t	Record declaration
PClass Docstring SyntaxInfo FC [t] Name [(Name, t)] [(Name, Docstring)] [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 (ProvideWhat' t) Name	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] a Source

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 :: [(Docstring, [(Name, Docstring)], 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	(n : t1) -> t2
PLet Name PTerm PTerm PTerm
PTyped PTerm PTerm	Term with explicit type
PApp FC PTerm [PArg]	e.g. IO (), List Char, length x
PAppBind FC PTerm [PArg]	implicitly bound application
PMatchApp FC Name	Make an application by type matching
PCase FC PTerm [(PTerm, PTerm)]
PTrue FC PunInfo	Unit type..?
PFalse FC	_\|_
PRefl FC PTerm
PResolveTC FC
PEq FC PTerm PTerm PTerm PTerm	Heterogeneous equality type: A = B
PRewrite FC PTerm PTerm (Maybe PTerm)
PPair FC PunInfo PTerm PTerm
PDPair FC PunInfo PTerm PTerm PTerm
PAlternative Bool [PTerm]
PHidden PTerm	Irrelevant or hidden pattern
PType	`Type` type
PUniverse Universe	Some universe
PGoal FC PTerm Name PTerm
PConstant Const	Builtin types
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
PQuasiquote PTerm (Maybe PTerm)	`(Term [: Term])
PUnquote PTerm	,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
DoUnify
Induction t
CaseTac t
Equiv t
MatchRefine Name
LetTac Name t
LetTacTy Name t t
Exact t
Compute
Trivial
TCInstance
ProofSearch Bool Bool Int (Maybe Name) [Name]	the bool is whether to search recursively
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)
TCheck t
TEval t
TDocStr (Either Name Const)
TSearch t
Skip
TFail [ErrorReportPart]
Qed
Abandon

Instances

Functor PTactic'
Foldable PTactic'
Traversable 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 [(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
PExp
Fields priority :: Int argopts :: [ArgOpt] pname :: Name getTm :: t
PConstraint
Fields priority :: Int argopts :: [ArgOpt] pname :: Name getTm :: t
PTacImplicit
Fields priority :: Int argopts :: [ArgOpt] pname :: Name getScript :: t getTm :: t

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

AlwaysShow
HideDisplay
InaccessibleArg

Instances

Eq ArgOpt
Show ArgOpt
Binary ArgOpt
NFData ArgOpt

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

pexp :: t -> PArg' t Source

pconst :: t -> PArg' t Source

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

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 TIData Source

Constructors

TIPartial	a function with a partially defined type
TISolution [Term]	possible solutions to a metavariable in a type

Instances

Show TIData

data FnInfo Source

Miscellaneous information about functions

Constructors

FnInfo
Fields fn_params :: [Int]

Instances

Show FnInfo
Binary FnInfo

data OptInfo Source

Constructors

Optimise
Fields inaccessible :: [(Int, Name)] detaggable :: Bool

Instances

Show OptInfo
Binary OptInfo
NFData OptInfo

data TypeInfo Source

Constructors

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

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 dsl_pi :: 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 maxline :: Maybe Int mut_nesting :: Int dsl_info :: DSL syn_in_quasiquote :: Bool

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 :: [t] Source

infTerm :: PTerm -> PTerm Source

infP :: TT Name Source

getInferTerm :: Term -> Term Source

getInferType :: Term -> Term Source

primNames :: [Name] Source

unitDoc :: Doc Source

unitTy :: Name Source

unitCon :: Name Source

unitDecl :: PData' PTerm Source

unitOpts :: [DataOpt] Source

falseDoc :: Doc Source

falseTy :: Name Source

falseDecl :: PData' PTerm Source

falseOpts :: [t] Source

pairDoc :: Doc Source

pairTy :: Name Source

pairCon :: Name Source

pairDecl :: PData' PTerm Source

pairOpts :: [t] Source

pairParamDoc :: [(Name, Doc)] Source

eqTy :: Name Source

eqCon :: Name Source

eqDoc :: Doc Source

eqDecl :: PData' PTerm Source

eqParamDoc :: [(Name, Doc)] Source

eqOpts :: [t] 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.

isPostulateName :: Name -> IState -> Bool Source

prettyImp Source

Arguments

:: PPOption	^ pretty printing options
-> PTerm	^ the term to pretty-print
-> Doc OutputAnnotation

Pretty-print a high-level closed Idris term with no information about precedence/associativity

prettyIst :: IState -> PTerm -> Doc OutputAnnotation Source

Serialise something to base64 using its Binary instance.

Do the right thing for rendering a term in an IState

pprintPTerm Source

Arguments

:: PPOption	^ pretty printing options
-> [(Name, Bool)]	^ the currently-bound names and whether they are implicit
-> [Name]	^ names to always show in pi, even if not used
-> [FixDecl]	^ Fixity declarations
-> PTerm	^ the term to pretty-print
-> Doc OutputAnnotation

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

prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation Source

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 the name should be parenthesised if it is an infix operator
-> 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 :: PPOption -> PClause -> Doc OutputAnnotation Source

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

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

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

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

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

getShowArgs :: [PArg] -> [PArg] 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
-> PPOption	^ pretty printing options
-> 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

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

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

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

getErasureInfo :: IState -> Name -> [Int] Source

IBCFix FixDecl
IBCImp Name
IBCStatic Name
IBCClass Name
IBCInstance Bool Name Name
IBCDSL Name
IBCData Name
IBCOpt Name
IBCMetavar Name
IBCSyntax Syntax
IBCKeyword String
IBCImport FilePath
IBCImportDir 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]
IBCFnInfo Name FnInfo
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
IBCPostulate Name
IBCTotCheckErr FC String
IBCParsedRegion FC