idris-0.9.12: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.AbsSyntaxTree

Synopsis

Documentation

data OutputMode Source

The output mode in use

Constructors

RawOutput 
IdeSlave Integer 

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 :: [(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_totcheck :: [(FC, Name)]
 
idris_defertotcheck :: [(FC, Name)]
 
idris_options :: IOption
 
idris_name :: Int
 
idris_lineapps :: [((FilePath, Int), PTerm)]

Full application LHS on source line

idris_metavars :: [(Name, (Maybe Name, Int, Bool))]

The currently defined but not proven metavariables

idris_coercions :: [Name]
 
idris_transforms :: [(Term, Term)]
 
idris_errRev :: [(Term, Term)]
 
syntax_rules :: [Syntax]
 
syntax_keywords :: [String]
 
imported :: [FilePath]

The imported modules

idris_scprims :: [(Name, (Int, PrimFn))]
 
idris_objs :: [(Codegen, FilePath)]
 
idris_libs :: [(Codegen, String)]
 
idris_cgflags :: [(Codegen, String)]
 
idris_hdrs :: [(Codegen, String)]
 
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?

hide_list :: [(Name, Maybe Accessibility)]
 
default_access :: Accessibility
 
default_total :: Bool
 
ibc_write :: [IBCWrite]
 
compiled_so :: Maybe String
 
idris_dynamic_libs :: [DynamicLib]
 
idris_language_extensions :: [LanguageExt]
 
idris_outputmode :: OutputMode
 
idris_colourRepl :: Bool
 
idris_colourTheme :: ColourTheme
 
idris_outh :: Handle
 
idris_errorhandlers :: [Name]

Global error handlers

idris_nameIdx :: (Int, Ctxt (Int, Name))
 
idris_function_errorhandlers :: Ctxt (Map Name (Set Name))

Specific error handlers

module_aliases :: Map [Text] [Text]
 
idris_consolewidth :: ConsoleWidth

How many chars wide is the console?

data CGInfo Source

Constructors

CGInfo 

Fields

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

idrisInit :: IStateSource

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

data DataOpt Source

Data declaration options

data ProvideWhat Source

Type provider - what to provide

Constructors

ProvTerm

only allow providing terms

ProvPostulate

only allow postulates

ProvAny

either is ok

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 Docstring Name t

Record declaration

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

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

PInstance SyntaxInfo FC [t] Name [t] t (Maybe Name) [PDecl' t]

Instance declaration: arguments are syntax info, source location, constraints, class name, parameters, full instance type, optional explicit name, and definitions

PDSL Name (DSL' t)

DSL declaration

PSyntax FC Syntax

Syntax definition

PMutual FC [PDecl' t]

Mutual block

PDirective (Idris ())

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

PProvider SyntaxInfo FC ProvideWhat Name t t

Type provider. The first t is the type, the second is the term

PTransform FC Bool t t

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

Instances

type ElabD a = Elab' [PDecl] aSource

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 [PDecl' t] 
PClauseR FC [t] t [PDecl' t] 
PWithR FC [t] t [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, [(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

data PTerm Source

High level language terms

Constructors

PQuote Raw 
PRef FC Name 
PInferRef FC Name

A name to be defined later

PPatvar FC Name 
PLam Name PTerm PTerm 
PPi Plicity Name PTerm PTerm 
PLet Name PTerm PTerm PTerm 
PTyped PTerm PTerm

Term with explicit type

PApp FC PTerm [PArg] 
PAppBind FC PTerm [PArg]

implicitly bound application

PMatchApp FC Name

Make an application by type matching

PCase FC PTerm [(PTerm, PTerm)] 
PTrue FC PunInfo 
PFalse FC 
PRefl FC PTerm 
PResolveTC FC 
PEq FC PTerm PTerm 
PRewrite FC PTerm PTerm (Maybe PTerm) 
PPair FC PunInfo PTerm PTerm 
PDPair FC PunInfo PTerm PTerm PTerm 
PAlternative Bool [PTerm] 
PHidden PTerm

Irrelevant or hidden pattern

PType 
PGoal FC PTerm Name PTerm 
PConstant Const 
Placeholder 
PDoBlock [PDo] 
PIdiom FC PTerm 
PReturn FC 
PMetavar Name 
PProof [PTactic]

Proof script

PTactics [PTactic]

As PProof, but no auto solving

PElabError Err

Error to report on elaboration

PImpossible

Special case for declaring when an LHS can't typecheck

PCoerced PTerm

To mark a coerced argument, so as not to coerce twice

PDisamb [[Text]] PTerm

Preferences for explicit namespaces

PUnifyLog PTerm

dump a trace of unifications when building term

PNoImplicits PTerm

never run implicit converions on the term

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) 

data PArg' t Source

Constructors

PImp 

Fields

priority :: Int
 
machine_inf :: Bool
 
argopts :: [ArgOpt]
 
pname :: Name
 
getTm :: t
 
PExp 

Fields

priority :: Int
 
argopts :: [ArgOpt]
 
getTm :: t
 
PConstraint 

Fields

priority :: Int
 
argopts :: [ArgOpt]
 
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) 

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

pexp :: t -> PArg' tSource

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

data TIData Source

Constructors

TIPartial

a function with a partially defined type

TISolution [Term]

possible solutions to a metavariable in a type

Instances

data TypeInfo Source

Constructors

TI 

data DSL' t Source

Constructors

DSL 

Fields

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

Instances

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

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

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.

prettyImpSource

Arguments

:: Bool

^ whether to show implicits

-> PTerm

^ the term to pretty-print

-> Doc OutputAnnotation 

Pretty-print a high-level closed Idris term

pprintPTermSource

Arguments

:: Bool

^ whether to show implicits

-> [(Name, Bool)]

^ the currently-bound names and whether they are implicit

-> [Name]

^ names to always show in pi, even if not used

-> PTerm

^ the term to pretty-print

-> Doc OutputAnnotation 

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

bindingOfSource

Arguments

:: Name

^ the bound name

-> Bool

^ whether the name is implicit

-> Doc OutputAnnotation 

Pretty-printer helper for the binding site of a name

prettyNameSource

Arguments

:: Bool

^ whether to show namespaces

-> [(Name, Bool)]

^ the current bound variables and whether they are implicit

-> Name

^ the name to pprint

-> Doc OutputAnnotation 

Pretty-printer helper for names that attaches the correct annotations

showNameSource

Arguments

:: Maybe IState

^ the Idris state, for information about names and colours

-> [(Name, Bool)]

^ the bound variables and whether they're implicit

-> Bool

^ whether to show implicits

-> Bool

^ whether to colourise

-> Name

^ the term to show

-> String 

Show Idris name

showTmSource

Arguments

:: IState

^ the Idris state, for information about identifiers and colours

-> PTerm

^ the term to show

-> String 

showTmImpls :: PTerm -> StringSource

Show a term with implicits, no colours