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

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

toplevel :: ElabInfo

eInfoNames :: ElabInfo -> [Name]

data IOption

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

opt_origerr :: Bool

opt_autoSolve :: Bool

automatically apply "solve" tactic in prover

opt_autoImport :: [FilePath]

e.g. Builtins+Prelude

opt_optimise :: [Optimisation]

Instances

Eq IOption

Show IOption

defaultOpts :: IOption

data PPOption

Constructors

PPOption

Fields

ppopt_impl :: Bool

^ whether to show implicits

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 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_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 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, 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, and the Bool is whether :p is allowed

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, [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_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

Instances

Show IState

TokenParsing IdrisParser

HasLastTokenSpan IdrisParser

data SizeChange

Constructors

Smaller

Same

Bigger

Unknown

Instances

Eq SizeChange

Show SizeChange

Binary SizeChange

NFData SizeChange

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

type UsageReason = (Name, Int)

data CGInfo

Constructors

CGInfo

Fields

argsdef :: [Name]

calls :: [(Name, [[Name]])]

scg :: [SCGEntry]

argsused :: [Name]

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

Instances

Show CGInfo

Binary CGInfo

NFData CGInfo

primDefs :: [Name]

data IBCWrite

Constructors

IBCFix FixDecl

IBCImp Name

IBCStatic Name

IBCClass 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

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

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 String

Bytecode

Instances

Eq Codegen

Show Codegen

Binary Codegen

NFData Codegen

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

Load FilePath (Maybe Int)

ChangeDirectory FilePath

ModImport String

Edit

Compile Codegen String

Execute PTerm

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

Search [String] 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] 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 Opt

Constructors

Filename String

Quiet

NoBanner

ColourREPL Bool

Idemode

IdemodeSocket

ShowLibs

ShowLibdir

ShowIncs

ShowPkgs

NoBasePkgs

NoPrelude

NoBuiltins

NoREPL

OLogging Int

Output String

Interface

TypeCase

TypeInType

DefaultTotal

DefaultPartial

WarnPartial

WarnReach

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

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 interactive prover

UseConsoleWidth ConsoleWidth

Instances

Eq Opt

Show Opt

data Fixity

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

Constructors

Fix Fixity String

Instances

Eq FixDecl

Ord FixDecl

Show FixDecl

Binary FixDecl

NFData FixDecl

data Static

Constructors

Static

Dynamic

Instances

Eq Static

Data Static

Show Static

Binary Static

NFData Static

Typeable * Static

data Plicity

Constructors

Imp

Fields

pargopts :: [ArgOpt]

pstatic :: Static

pparam :: Bool

pscoped :: Maybe ImplicitInfo

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

Binary Plicity

NFData Plicity

Typeable * 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

Instances

Eq FnOpt

Show FnOpt

Binary FnOpt

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

Binary t => Binary (ProvideWhat' t)

NFData t => NFData (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 PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t

Type declaration (last FC is precise name location)

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

Postulate

PClauses FC FnOpts Name [PClause' t]

Pattern clause

PCAF FC Name t

Top level constant

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

Data declaration.

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

Params block

PNamespace String FC [PDecl' t]

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

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

Record declaration

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

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 PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC [(Name, t)] Name FC [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 PTerm)) 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)

data Directive

The set of source directives

Constructors

DLib Codegen String

DLink Codegen String

DFlag Codegen String

DInclude Codegen String

DHide Name

DFreeze Name

DAccess Accessibility

DDefault Bool

DLogging Integer

DDynamicLibs [String]

DNameHint Name [Name]

DErrorHandlers Name Name [Name]

DLanguage LanguageExt

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

RAddInstance Name Name

data EState

For elaborator state

Constructors

EState

Fields

case_decls :: [(Name, PDecl)]

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

new_tyDecls :: [RDeclInstructions]

highlighting :: [(FC, OutputAnnotation)]

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

Binary t => Binary (PClause' t)

NFData t => NFData (PClause' t)

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

Binary t => Binary (PData' t)

NFData t => NFData (PData' t)

type PDecl = PDecl' PTerm

type PData = PData' PTerm

type PClause = PClause' PTerm

declared :: PDecl -> [Name]

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

Binary PunInfo

NFData PunInfo

Typeable * PunInfo

data PTerm

High level language terms

Constructors

PQuote Raw

Inclusion of a core term into the high-level language

PRef FC Name

A reference to a variable

PInferRef 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

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 PTerm PTerm (Maybe PTerm)

"rewrite" syntax, with optional result type

PPair FC PunInfo PTerm PTerm

A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

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

PAs FC Name PTerm

@-pattern, valid LHS only

PAlternative PAltType [PTerm]

True if only one may work. (| A, B, C|)

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

`{n}

PRunElab FC PTerm

%runElab tm - New-style proof script

Instances

Eq PTerm

Data PTerm

Show PTerm

Show PClause

Show PData

Show PDecl

Binary PTerm

NFData PTerm

Typeable * PTerm

data PAltType

Constructors

ExactlyOne Bool

flag sets whether delay is allowed

FirstSuccess

Instances

Eq PAltType

Data PAltType

Binary PAltType

NFData PAltType

Typeable * PAltType

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]

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)

Binary t => Binary (PTactic' t)

NFData t => NFData (PTactic' t)

Typeable (* -> *) PTactic'

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)

Binary t => Binary (PDo' t)

NFData t => NFData (PDo' t)

Typeable (* -> *) PDo'

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)

Binary t => Binary (PArg' t)

NFData t => NFData (PArg' t)

Typeable (* -> *) PArg'

data ArgOpt

Constructors

AlwaysShow

HideDisplay

InaccessibleArg

UnknownImp

Instances

Eq ArgOpt

Data ArgOpt

Show ArgOpt

Binary ArgOpt

NFData ArgOpt

Typeable * 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, (FnOpts, PTerm))]

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

class_default_superclasses :: [PDecl]

class_params :: [Name]

class_instances :: [(Name, Bool)]

class_determiners :: [Int]

Instances

Show ClassInfo

Binary ClassInfo

NFData ClassInfo

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

Binary FnInfo

NFData FnInfo

data OptInfo

Constructors

Optimise

Fields

inaccessible :: [(Int, Name)]

detaggable :: Bool

Instances

Show OptInfo

Binary OptInfo

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

Binary t => Binary (DSL' t)

NFData t => NFData (DSL' t)

type DSL = DSL' PTerm

data SynContext

Constructors

PatternSyntax

TermSyntax

AnySyntax

Instances

Show SynContext

Binary SynContext

NFData SynContext

data Syntax

Constructors

Rule [SSymbol] PTerm SynContext

Instances

Show Syntax

Binary Syntax

NFData 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

Binary SSymbol

NFData 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

Show Using

Binary Using

NFData 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

maxline :: Maybe Int

mut_nesting :: Int

dsl_info :: DSL

syn_in_quasiquote :: Int

Instances

Show SyntaxInfo

Binary SyntaxInfo

NFData 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

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.

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

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]