Idris.AbsSyntaxTree

Documentation

data ElabWhat

Constructors

ETypes

EDefns

EAll

Instances

Eq ElabWhat

Show ElabWhat

data ElabInfo

Constructors

EInfo

Fields

params :: [(Name, PTerm)]

inblock :: Ctxt [Name]

liftname :: Name -> Name

namespace :: Maybe [String]

elabFC :: Maybe FC

rhs_trans :: PTerm -> PTerm

rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

toplevel :: ElabInfo

eInfoNames :: ElabInfo -> [Name]

data IOption

Constructors

IOption

Fields

opt_logLevel :: Int

opt_logcats :: [LogCat]

List of logging categories.

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_cmdline :: [Opt]

opt_origerr :: Bool

opt_autoSolve :: Bool

automatically apply "solve" tactic in prover

opt_autoImport :: [FilePath]

e.g. Builtins+Prelude

opt_optimise :: [Optimisation]

opt_printdepth :: Maybe Int

opt_evaltypes :: Bool

normalise types in :t

opt_desugarnats :: Bool

opt_autoimpls :: Bool

Instances

Eq IOption

Show IOption

defaultOpts :: IOption

data PPOption

Constructors

PPOption

Fields

ppopt_impl :: Bool

^ whether to show implicits

ppopt_desugarnats :: Bool

ppopt_pinames :: Bool

^ whether to show names in pi bindings

ppopt_depth :: Maybe Int

Instances

Show PPOption

data Optimisation

Constructors

PETransform

Instances

Eq Optimisation

Show Optimisation

defaultOptimise :: [Optimisation]

defaultPPOption :: PPOption

Pretty printing options with default verbosity.

verbosePPOption :: PPOption

Pretty printing options with the most verbosity.

ppOption :: IOption -> PPOption

Get pretty printing options from the big options record.

ppOptionIst :: IState -> PPOption

Get pretty printing options from an idris state record.

data LanguageExt

Constructors

TypeProviders

ErrorReflection

Instances

Eq LanguageExt

Ord LanguageExt

Read LanguageExt

Show LanguageExt

data OutputMode

The output mode in use

Constructors

RawOutput Handle

Print user output directly to the handle

IdeMode Integer Handle

Send IDE output for some request ID to the handle

Instances

Show OutputMode

data ConsoleWidth

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

Show ConsoleWidth

data DefaultTotality

If a function has no totality annotation, what do we assume?

Constructors

DefaultCheckingTotal

Total

DefaultCheckingPartial

Partial

DefaultCheckingCovering

Total coverage, but may diverge

Instances

Eq DefaultTotality

Show DefaultTotality

data IState

The global state used in the Idris monad

Constructors

IState

Fields

tt_ctxt :: Context

All the currently defined names and their terms

idris_constraints :: Set ConstraintFC

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_openimpls :: [Name]

Privileged implementations, will resolve immediately

idris_records :: Ctxt RecordInfo

idris_dsls :: Ctxt DSL

idris_optimisation :: Ctxt OptInfo

idris_datatypes :: Ctxt TypeInfo

idris_namehints :: Ctxt [Name]

idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])

list of lhs/rhs, and a list of missing clauses

idris_flags :: Ctxt [FnOpt]

idris_callgraph :: Ctxt CGInfo

idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])

idris_moduledocs :: Ctxt (Docstring DocTerm)

module documentation is saved in a special MN so the context mechanism can be used for disambiguation

idris_tyinfodata :: Ctxt TIData

idris_fninfo :: Ctxt FnInfo

idris_transforms :: Ctxt [(Term, Term)]

idris_autohints :: Ctxt [Name]

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, [Name], Bool, Bool))]

The currently defined but not proven metavariables. The Int is the number of vars to display as a context, the Maybe Name is its top-level function, the [Name] is the list of local variables available for proof search and the Bools are whether :p is allowed, and whether the variable is definable at all (Metavariables are not definable if they are applied in a term which still has hole bindings)

idris_coercions :: [Name]

idris_errRev :: [(Term, Term)]

syntax_rules :: SyntaxRules

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, Bool)]

Imported ibc file names, whether public

proof_list :: [(Name, (Bool, [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 :: Ctxt Accessibility

default_access :: Accessibility

default_total :: DefaultTotality

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_externs :: Set (Name, Int)

idris_erasureUsed :: [(Name, Int)]

Function/constructor name, argument position is used

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

elab_stack :: [(Name, Bool)]

Stack of names currently being elaborated, Bool set if it's an instance (instances appear twice; also as a funtion name)

idris_symbols :: Map Name Name

Symbol table (preserves sharing of names)

idris_exports :: [Name]

Functions with ExportList

idris_highlightedRegions :: [(FC, OutputAnnotation)]

Highlighting information to output

idris_parserHighlights :: [(FC, OutputAnnotation)]

Highlighting information from the parser

idris_deprecated :: Ctxt String

Deprecated names and explanation

idris_inmodule :: Set Name

Names defined in current module

idris_ttstats :: Map Term (Int, Term)

idris_fragile :: Ctxt String

Fragile names and explanation.

Instances

Show IState

TokenParsing IdrisParser

HasLastTokenSpan IdrisParser

data SizeChange

Constructors

Smaller

Same

Bigger

Unknown

Instances

Eq SizeChange

Show SizeChange

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

type UsageReason = (Name, Int)

data CGInfo

Constructors

CGInfo

Fields

calls :: [Name]

scg :: [SCGEntry]

usedpos :: [(Int, [UsageReason])]

Instances

Show CGInfo

primDefs :: [Name]

data IBCWrite

Constructors

IBCFix FixDecl

IBCImp Name

IBCStatic Name

IBCClass Name

IBCRecord Name

IBCInstance Bool Bool Name Name

IBCDSL Name

IBCData Name

IBCOpt Name

IBCMetavar Name

IBCSyntax Syntax

IBCKeyword String

IBCImport (Bool, 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

IBCInjective Name Injectivity

IBCFlags Name [FnOpt]

IBCFnInfo Name FnInfo

IBCTrans Name (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

IBCExtern (Name, Int)

IBCTotCheckErr FC String

IBCParsedRegion FC

IBCModDocs Name

The name is the special name used to track module docs

IBCUsage (Name, Int)

IBCExport Name

IBCAutoHint Name Name

IBCDeprecate Name String

IBCFragile Name String

Instances

Show IBCWrite

idrisInit :: IState

The initial state for the compiler

type Idris = StateT IState (ExceptT Err IO)

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))

catchError :: Idris a -> (Err -> Idris a) -> Idris a

throwError :: Err -> Idris a

data Codegen

Constructors

Via IRFormat String

Bytecode

Instances

Eq Codegen

Show Codegen

data IRFormat

Constructors

IBCFormat

JSONFormat

Instances

Eq IRFormat

Show IRFormat

data HowMuchDocs

Constructors

FullDocs

OverviewDocs

data Command

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

Core PTerm

DocStr (Either Name Const) HowMuchDocs

TotCheck Name

Reload

Watch

Load FilePath (Maybe Int)

ChangeDirectory FilePath

ModImport String

Edit

Compile Codegen String

Execute PTerm

ExecVal PTerm

Metavars

Prove Bool Name

If false, use prover, if true, use elab shell

AddProof (Maybe Name)

RmProof Name

ShowProof Name

Proofs

Universes

LogLvl Int

LogCategory [LogCat]

Spec PTerm

WHNF PTerm

TestInline PTerm

Defn Name

Missing Name

DynamicLink FilePath

ListDynamic

Pattelab PTerm

Search [String] PTerm

CaseSplitAt Bool Int Name

AddClauseFrom Bool Int Name

AddProofClauseFrom Bool Int Name

AddMissing Bool Int Name

MakeWith Bool Int Name

MakeCase Bool Int Name

MakeLemma Bool Int Name

DoProofSearch Bool Bool Int Name [Name]

SetOpt Opt

UnsetOpt Opt

NOP

SetColour ColourType IdrisColour

ColourOn

ColourOff

ListErrorHandlers

SetConsoleWidth ConsoleWidth

SetPrinterDepth (Maybe Int)

Apropos [String] String

WhoCalls Name

CallsWho Name

Browse [String]

MakeDoc String

Warranty

PrintDef Name

PPrint OutputFmt Int PTerm

TransformInfo Name

DebugInfo Name

DebugUnify PTerm PTerm

data OutputFmt

Constructors

HTMLOutput

LaTeXOutput

data LogCat

Recognised logging categories for the Idris compiler.

@TODO add in sub categories.

Constructors

IParse

IElab

ICodeGen

IErasure

ICoverage

IIBC

Instances

Eq LogCat

Ord LogCat

Show LogCat

strLogCat :: LogCat -> String

codegenCats :: [LogCat]

parserCats :: [LogCat]

elabCats :: [LogCat]

loggingCatsStr :: String

data Opt

Constructors

Filename String

Quiet

NoBanner

ColourREPL Bool

Idemode

IdemodeSocket

ShowLibs

ShowLibdir

ShowIncs

ShowPkgs

ShowLoggingCats

NoBasePkgs

NoPrelude

NoBuiltins

NoREPL

OLogging Int

OLogCats [LogCat]

Output String

Interface

TypeCase

TypeInType

DefaultTotal

DefaultPartial

WarnPartial

WarnReach

EvalTypes

NoCoverage

ErrContext

ShowImpl

Verbose

Port String

IBCSubDir String

ImportDir String

PkgBuild String

PkgInstall String

PkgClean String

PkgCheck String

PkgREPL String

PkgMkDoc 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

Show Opt

data ElabShellCmd

Constructors

EQED

EAbandon

EUndo

EProofState

EProofTerm

EEval PTerm

ECheck PTerm

ESearch PTerm

EDocStr (Either Name Const)

Instances

Eq ElabShellCmd

Show ElabShellCmd

data Fixity

Constructors

Infixl

Fields

prec :: Int

Infixr

Fields

prec :: Int

InfixN

Fields

prec :: Int

PrefixN

Fields

prec :: Int

Instances

Eq Fixity

Show Fixity

data FixDecl

Constructors

Fix Fixity String

Instances

Eq FixDecl

Ord FixDecl

Show FixDecl

data Static

Constructors

Static

Dynamic

Instances

Eq Static

Data Static

Show Static

data Plicity

Constructors

Imp

Fields

pargopts :: [ArgOpt]

pstatic :: Static

pparam :: Bool

pscoped :: Maybe ImplicitInfo

pinsource :: 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

Data Plicity

Show Plicity

is_scoped :: Plicity -> Maybe ImplicitInfo

impl :: Plicity

forall_imp :: Plicity

forall_constraint :: Plicity

expl :: Plicity

expl_param :: Plicity

constraint :: Plicity

tacimpl :: PTerm -> Plicity

data FnOpt

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

AutoHint

PEGenerated

Instances

Eq FnOpt

Show FnOpt

type FnOpts = [FnOpt]

inlinable :: FnOpts -> Bool

dictionary :: FnOpts -> Bool

data ProvideWhat' t

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)

type ProvideWhat = ProvideWhat' PTerm

data PDecl' t

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

Constructors

PFix FC Fixity [String]

Fixity declaration

PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t

Type declaration (last FC is precise name location)

PPostulate Bool (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t

Postulate, second FC is precise name location

PClauses FC FnOpts Name [PClause' t]

Pattern clause

PCAF FC Name t

Top level constant

PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)

Data declaration.

PParams FC [(Name, t)] [PDecl' t]

Params block

POpenInterfaces FC [Name] [PDecl' t]

Open block/declaration

PNamespace String FC [PDecl' t]

New namespace, where FC is accurate location of the namespace in the file

PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts Name FC [(Name, FC, Plicity, t)] [(Name, Docstring (Either Err t))] [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] (Maybe (Name, FC)) (Docstring (Either Err t)) SyntaxInfo

Record declaration

PClass (Docstring (Either Err t)) SyntaxInfo FC [(Name, t)] Name FC [(Name, FC, t)] [(Name, Docstring (Either Err t))] [(Name, FC)] [PDecl' t] (Maybe (Name, FC)) (Docstring (Either Err t))

Type class: arguments are documentation, syntax info, source location, constraints, class name, class name location, parameters, method declarations, optional constructor name

PInstance (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC [(Name, t)] [Name] Accessibility FnOpts Name FC [t] [(Name, t)] t (Maybe Name) [PDecl' t]

Instance declaration: arguments are documentation, 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 Directive

Compiler directive.

PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name

Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.

PTransform FC Bool t t

Source-to-source transformation rule. If bool is True, lhs and rhs must be convertible

PRunElabDecl FC t [String]

FC is decl-level, for errors, and Strings represent the namespace

Instances

Functor PDecl'

Show PDecl

data Directive

The set of source directives

Constructors

DLib Codegen String

DLink Codegen String

DFlag Codegen String

DInclude Codegen String

DHide Name

DFreeze Name

DInjective Name

DAccess Accessibility

DDefault DefaultTotality

DLogging Integer

DDynamicLibs [String]

DNameHint Name FC [(Name, FC)]

DErrorHandlers Name FC Name FC [(Name, FC)]

DLanguage LanguageExt

DDeprecate Name String

DFragile Name String

DAutoImplicits Bool

DUsed FC Name Name

data RDeclInstructions

A set of instructions for things that need to happen in IState after a term elaboration when there's been reflected elaboration.

Constructors

RTyDeclInstrs Name FC [PArg] Type

RClausesInstrs Name [([(Name, Term)], Term, Term)]

RAddInstance Name Name

RDatatypeDeclInstrs Name [PArg]

RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]

Datatype, constructors

data EState

For elaborator state

Constructors

EState

Fields

case_decls :: [(Name, PDecl)]

delayed_elab :: [(Int, Elab' EState ())]

new_tyDecls :: [RDeclInstructions]

highlighting :: [(FC, OutputAnnotation)]

auto_binds :: [Name]

implicit_warnings :: [(FC, Name)]

initEState :: EState

type ElabD a = Elab' EState a

highlightSource :: FC -> OutputAnnotation -> ElabD ()

data PClause' t

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

1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
2. The list of extra with patterns
3. The right-hand side
4. 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 (Maybe (Name, FC)) [PDecl' t]

PClauseR FC [t] t [PDecl' t]

PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]

Instances

Functor PClause'

Show PClause

data PData' t

Data declaration

Constructors

PDatadecl

Data declaration

Fields

d_name :: Name

The name of the datatype

d_name_fc :: FC

The precise location of the type constructor name

d_tcon :: t

Type constructor

d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]

Constructors

PLaterdecl

Placeholder for data whose constructors are defined later

Fields

d_name :: Name

The name of the datatype

d_name_fc :: FC

The precise location of the type constructor name

d_tcon :: t

Type constructor

Instances

Functor PData'

Show PData

mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData

Transform the FCs in a PData and its associated terms. The first function transforms the general-purpose FCs, and the second transforms those that are used for semantic source highlighting, so they can be treated specially.

type PDecl = PDecl' PTerm

type PData = PData' PTerm

type PClause = PClause' PTerm

mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl

Transform the FCs in a PTerm. The first function transforms the general-purpose FCs, and the second transforms those that are used for semantic source highlighting, so they can be treated specially.

declared :: PDecl -> [Name]

Get all the names declared in a declaration

tldeclared :: PDecl -> [Name]

defined :: PDecl -> [Name]

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

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

data PunInfo

Constructors

IsType

IsTerm

TypeOrTerm

Instances

Eq PunInfo

Data PunInfo

Show PunInfo

data PTerm

High level language terms

Constructors

PQuote Raw

Inclusion of a core term into the high-level language

PRef FC [FC] Name

A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.

PInferRef FC [FC] Name

A name to be defined later

PPatvar FC Name

A pattern variable

PLam FC Name FC PTerm PTerm

A lambda abstraction. Second FC is name span.

PPi Plicity Name FC PTerm PTerm

(n : t1) -> t2, where the FC is for the precise location of the variable

PLet FC Name FC PTerm PTerm PTerm

A let binding (second FC is precise name location)

PTyped PTerm PTerm

Term with explicit type

PApp FC PTerm [PArg]

e.g. IO (), List Char, length x

PWithApp FC PTerm PTerm

Application plus a with argument

PAppImpl PTerm [ImplicitInfo]

Implicit argument application (introduced during elaboration only)

PAppBind FC PTerm [PArg]

implicitly bound application

PMatchApp FC Name

Make an application by type matching

PIfThenElse FC PTerm PTerm PTerm

Conditional expressions - elaborated to an overloading of ifThenElse

PCase FC PTerm [(PTerm, PTerm)]

A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

PTrue FC PunInfo

Unit type..?

PResolveTC FC

Solve this dictionary by type class resolution

PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

"rewrite" syntax, with optional rewriting function and optional result type

PPair FC [FC] PunInfo PTerm PTerm

A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

PDPair FC [FC] PunInfo PTerm PTerm PTerm

A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

PAs FC Name PTerm

@-pattern, valid LHS only

PAlternative [(Name, Name)] PAltType [PTerm]

(| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

PHidden PTerm

Irrelevant or hidden pattern

PType FC

Type type

PUniverse Universe

Some universe

PGoal FC PTerm Name PTerm

quoteGoal, used for %reflection functions

PConstant FC Const

Builtin types

Placeholder

Underscore

PDoBlock [PDo]

Do notation

PIdiom FC PTerm

Idiom brackets

PReturn FC

PMetavar FC Name

A metavariable, ?name, and its precise location

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

PQuoteName Name Bool FC

`{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.

PRunElab FC PTerm [String]

%runElab tm - New-style proof script. Args are location, script, enclosing namespace.

PConstSugar FC PTerm

A desugared constant. The FC is a precise source location that will be used to highlight it later.

Instances

Eq PTerm

Data PTerm

Show PTerm

Show PClause

Show PData

Show PDecl

data PAltType

Constructors

ExactlyOne Bool

flag sets whether delay is allowed

FirstSuccess

TryImplicit

Instances

Eq PAltType

Data PAltType

mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm

Transform the FCs in a PTerm. The first function transforms the general-purpose FCs, and the second transforms those that are used for semantic source highlighting, so they can be treated specially.

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

data PTactic' t

Constructors

Intro [Name]

Intros

Focus Name

Refine Name [Bool]

Rewrite t

DoUnify

Induction t

CaseTac t

Equiv t

Claim Name t

Unfocus

MatchRefine Name

LetTac Name t

LetTacTy Name t t

Exact t

Compute

Trivial

TCInstance

ProofSearch Bool Bool Int (Maybe Name) [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

SourceFC

Instances

Functor PTactic'

Foldable PTactic'

Traversable PTactic'

Eq t => Eq (PTactic' t)

Data t => Data (PTactic' t)

Show t => Show (PTactic' t)

type PTactic = PTactic' PTerm

data PDo' t

Constructors

DoExp FC t

DoBind FC Name FC t

second FC is precise name location

DoBindP FC t t [(t, t)]

DoLet FC Name FC t t

second FC is precise name location

DoLetP FC t t

Instances

Functor PDo'

Eq t => Eq (PDo' t)

Data t => Data (PDo' t)

type PDo = PDo' PTerm

data PArg' t

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)

Data t => Data (PArg' t)

Show t => Show (PArg' t)

data ArgOpt

Constructors

AlwaysShow

HideDisplay

InaccessibleArg

UnknownImp

Instances

Eq ArgOpt

Data ArgOpt

Show ArgOpt

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

pexp :: t -> PArg' t

pconst :: t -> PArg' t

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

type PArg = PArg' PTerm

highestFC :: PTerm -> Maybe FC

Get the highest FC in a term, if one exists

data ClassInfo

Constructors

CI

Fields

instanceCtorName :: Name

class_methods :: [(Name, (Bool, FnOpts, PTerm))]

class_defaults :: [(Name, (Name, PDecl))]

class_default_superclasses :: [PDecl]

class_params :: [Name]

class_instances :: [(Name, Bool)]

class_determiners :: [Int]

Instances

Show ClassInfo

data RecordInfo

Constructors

RI

Fields

record_parameters :: [(Name, PTerm)]

record_constructor :: Name

record_projections :: [Name]

Instances

Show RecordInfo

data TIData

Constructors

TIPartial

a function with a partially defined type

TISolution [Term]

possible solutions to a metavariable in a type

Instances

Show TIData

data FnInfo

Miscellaneous information about functions

Constructors

FnInfo

Fields

fn_params :: [Int]

Instances

Show FnInfo

data OptInfo

Constructors

Optimise

Fields

inaccessible :: [(Int, Name)]

detaggable :: Bool

Instances

Show OptInfo

data DSL' t

Syntactic sugar info

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)

type DSL = DSL' PTerm

data SynContext

Constructors

PatternSyntax

TermSyntax

AnySyntax

Instances

Show SynContext

data Syntax

Constructors

Rule [SSymbol] PTerm SynContext

DeclRule [SSymbol] [PDecl]

Instances

Show Syntax

syntaxNames :: Syntax -> [Name]

syntaxSymbols :: Syntax -> [SSymbol]

data SSymbol

Constructors

Keyword Name

Symbol String

Binding Name

Expr Name

SimpleExpr Name

Instances

Eq SSymbol

Show SSymbol

newtype SyntaxRules

Constructors

SyntaxRules

Fields

syntaxRulesList :: [Syntax]

emptySyntaxRules :: SyntaxRules

updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules

initDSL :: DSL' PTerm

data Using

Constructors

UImplicit Name PTerm

UConstraint Name [Name]

Instances

Eq Using

Data Using

Show Using

data SyntaxInfo

Constructors

Syn

Fields

using :: [Using]

syn_params :: [(Name, PTerm)]

syn_namespace :: [String]

no_imp :: [Name]

imp_methods :: [Name]

decoration :: Name -> Name

inPattern :: Bool

implicitAllowed :: Bool

constraintAllowed :: Bool

maxline :: Maybe Int

mut_nesting :: Int

dsl_info :: DSL

syn_in_quasiquote :: Int

syn_toplevel :: Bool

withAppAllowed :: Bool

Instances

Show SyntaxInfo

defaultSyntax :: SyntaxInfo

expandNS :: SyntaxInfo -> Name -> Name

bi :: FC

inferTy :: Name

inferCon :: Name

inferDecl :: PData' PTerm

inferOpts :: [t]

infTerm :: PTerm -> PTerm

infP :: TT Name

getInferTerm :: Term -> Term

getInferType :: Term -> Term

primNames :: [Name]

unitTy :: Name

unitCon :: Name

falseDoc :: Docstring (Err' t)

falseTy :: Name

pairTy :: Name

pairCon :: Name

upairTy :: Name

upairCon :: Name

eqTy :: Name

eqCon :: Name

eqDoc :: Docstring (Either (Err' t) b)

eqDecl :: PData' PTerm

eqParamDoc :: [(Name, Docstring (Either (Err' t) b))]

eqOpts :: [t]

modDocName :: Name

The special name to be used in the module documentation context - not for use in the main definition context. The namespace around it will determine the module to which the docs adhere.

sigmaTy :: Name

sigmaCon :: Name

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

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

annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour

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.

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

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. Note that strings produced this way will not be coloured on Windows, so the use of the colour rendering functions in Idris.Output is to be preferred.

isPostulateName :: Name -> IState -> Bool

prettyImp

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

Serialise something to base64 using its Binary instance.

Do the right thing for rendering a term in an IState

pprintPTerm

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

basename :: Name -> Name

Strip away namespace information

isHoleName :: Name -> Bool

Determine whether a name was the one inserted for a hole or guess by the delaborator

containsHole :: PTerm -> Bool

Check whether a PTerm has been delaborated from a Term containing a Hole or Guess

prettyName

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

showDImp :: PPOption -> PData -> Doc OutputAnnotation

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

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

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

getExps :: [PArg] -> [PTerm]

getShowArgs :: [PArg] -> [PArg]

getConsts :: [PArg] -> [PTerm]

getAll :: [PArg] -> [PTerm]

showName

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

Arguments

:: IState

^ the Idris state, for information about identifiers and colours

-> PTerm

^ the term to show

-> String

showTmImpls :: PTerm -> String

Show a term with implicits, no colours

showTmOpts :: PPOption -> PTerm -> String

Show a term with specific options

getPArity :: PTerm -> Int

allNamesIn :: PTerm -> [Name]

boundNamesIn :: PTerm -> [Name]

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

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

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

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