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] elabFC :: Maybe FC 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_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 Source

data PPOption Source

Constructors

PPOption
Fields ppopt_impl :: Bool ^ whether to show implicits

Instances

Show PPOption

data Optimisation Source

Constructors

PETransform

Instances

Eq Optimisation
Show Optimisation

defaultOptimise :: [Optimisation] Source

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

Instances

Eq ConsoleWidth
Show ConsoleWidth

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

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

data IBCWrite Source

Constructors

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 (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
IBCTotCheckErr FC String
IBCParsedRegion FC
IBCModDocs Name	The name is the special name used to track module docs
IBCUsage (Name, Int)
IBCExport Name

Instances

Show IBCWrite

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

throwError :: Err -> Idris a Source

data Codegen Source

Constructors

Via String
Bytecode

Instances

Eq Codegen
Show Codegen
Binary Codegen
NFData Codegen

data HowMuchDocs Source

Constructors

FullDocs
OverviewDocs

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
Core PTerm
DocStr (Either Name Const) HowMuchDocs
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
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
MakeDoc String
Warranty
PrintDef Name
PPrint OutputFmt Int PTerm
TransformInfo Name
DebugInfo Name
DebugUnify PTerm PTerm

data OutputFmt Source

Constructors

HTMLOutput
LaTeXOutput

data Opt Source

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 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
Data Static
Show Static
Binary Static
NFData Static
Typeable * Static

data Plicity Source

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 Source

impl :: Plicity Source

forall_imp :: Plicity Source

forall_constraint :: 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)
Binary t => Binary (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 (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

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

data EState Source

Constructors

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

initEState :: EState Source

type ElabD a = Elab' EState 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 (Maybe Name) [PDecl' t]
PClauseR FC [t] t [PDecl' t]
PWithR FC [t] t (Maybe Name) [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 (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

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
Data PunInfo
Show PunInfo
Binary PunInfo
NFData PunInfo
Typeable * PunInfo

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

Instances

Eq PTerm
Data PTerm
Show PTerm
Show PClause
Show PData
Show PDecl
Binary PTerm
NFData PTerm
Typeable * 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
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 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)
Data t => Data (PDo' t)
Binary t => Binary (PDo' t)
NFData t => NFData (PDo' t)
Typeable (* -> *) PDo'

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

data ArgOpt Source

Constructors

AlwaysShow
HideDisplay
InaccessibleArg

Instances

Eq ArgOpt
Data ArgOpt
Show ArgOpt
Binary ArgOpt
NFData ArgOpt
Typeable * 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

highestFC :: PTerm -> Maybe FC Source

Get the highest FC in a term, if one exists

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] class_determiners :: [Int]

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

syntaxNames :: Syntax -> [Name] Source

syntaxSymbols :: Syntax -> [SSymbol] Source

data SSymbol Source

Constructors

Keyword Name
Symbol String
Binding Name
Expr Name
SimpleExpr Name

Instances

Eq SSymbol
Show SSymbol
Binary SSymbol
NFData SSymbol

newtype SyntaxRules Source

Constructors

SyntaxRules
Fields syntaxRulesList :: [Syntax]

emptySyntaxRules :: SyntaxRules Source

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

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

unitTy :: Name Source

unitCon :: Name Source

falseDoc :: Docstring (Err' t) Source

falseTy :: Name Source

pairTy :: Name Source

pairCon :: Name Source

upairTy :: Name Source

upairCon :: Name Source

eqTy :: Name Source

eqCon :: Name Source

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

eqDecl :: PData' PTerm Source

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

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.

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

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

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