idris-0.9.17.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.AbsSyntaxTree

Synopsis

Documentation

data ElabWhat Source

Constructors

ETypes 
EDefns 
EAll 

Instances

data ElabInfo Source

Constructors

EInfo 

data PPOption Source

Constructors

PPOption 

Fields

ppopt_impl :: Bool

^ whether to show implicits

Instances

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

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

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 :: 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_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_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]

Stack of names currently being elaborated

idris_symbols :: Map Name Name

Symbol table (preserves sharing of names)

idris_exports :: [Name]

Functions with ExportList

data CGInfo Source

Constructors

CGInfo 

Fields

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

idrisInit :: IState Source

The initial state for the compiler

type Idris = StateT IState (ExceptT 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))

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

data Fixity Source

Constructors

Infixl 

Fields

prec :: Int
 
Infixr 

Fields

prec :: Int
 
InfixN 

Fields

prec :: Int
 
PrefixN 

Fields

prec :: Int
 

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 

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 

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

data PDecl' t Source

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 t

Type declaration

PPostulate (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 [PDecl' t]

New namespace

PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t

Record declaration

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

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

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

Compiler directive. The parser inserts the corresponding action in the Idris monad.

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

data EState Source

Constructors

EState 

Fields

case_decls :: [PDecl]
 
delayed_elab :: [Elab' EState ()]
 
new_tyDecls :: [(Name, FC, [PArg], Type)]
 

data PClause' t Source

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) [PDecl' t] 
PClauseR FC [t] t [PDecl' t] 
PWithR FC [t] t (Maybe Name) [PDecl' 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 (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], 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

data PTerm Source

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

A lambda abstraction

PPi Plicity Name PTerm PTerm

(n : t1) -> t2

PLet FC Name PTerm PTerm PTerm

A let binding

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

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..?

PRefl FC PTerm

The canonical proof of the equality type

PResolveTC FC

Solve this dictionary by type class resolution

PEq FC PTerm PTerm PTerm PTerm

Heterogeneous equality type: A = B

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 Bool [PTerm]

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

PHidden PTerm

Irrelevant or hidden pattern

PType

Type type

PUniverse Universe

Some universe

PGoal FC PTerm Name PTerm

quoteGoal, used for %reflection functions

PConstant Const

Builtin types

Placeholder

Underscore

PDoBlock [PDo]

Do notation

PIdiom FC PTerm

Idiom brackets

PReturn FC 
PMetavar Name

A metavariable, ?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

PRunTactics FC PTerm

%runTactics tm - New-style proof script

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) 
Data t => Data (PDo' t) 
Binary t => Binary (PDo' t) 
NFData t => NFData (PDo' t) 
Typeable (* -> *) PDo' 

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) 
Data t => Data (PArg' t) 
Show t => Show (PArg' t) 
Binary t => Binary (PArg' t) 
NFData t => NFData (PArg' t) 
Typeable (* -> *) PArg' 

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

pexp :: t -> PArg' t Source

pconst :: t -> PArg' t Source

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

highestFC :: PTerm -> Maybe FC Source

Get the highest FC in a term, if one exists

data TIData Source

Constructors

TIPartial

a function with a partially defined type

TISolution [Term]

possible solutions to a metavariable in a type

Instances

data FnInfo Source

Miscellaneous information about functions

Constructors

FnInfo 

Fields

fn_params :: [Int]
 

data OptInfo Source

Constructors

Optimise 

Fields

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

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) 

newtype SyntaxRules Source

Constructors

SyntaxRules 

Fields

syntaxRulesList :: [Syntax]
 

eqOpts :: [t] Source

modDocName :: Name Source

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.

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

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

isHoleName :: Name -> Bool Source

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

containsHole :: PTerm -> Bool Source

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

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

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

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