idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.AbsSyntaxTree

Description

 

Synopsis

Documentation

data ElabInfo Source #

Data to pass to recursively called elaborators; e.g. for where blocks, paramaterised declarations, etc.

rec_elabDecl is used to pass the top level elaborator into other elaborators, so that we can have mutually recursive elaborators in separate modules without having to muck about with cyclic modules.

Constructors

EInfo 

Fields

data IOption Source #

Constructors

IOption 

Fields

Instances

Eq IOption Source # 

Methods

(==) :: IOption -> IOption -> Bool #

(/=) :: IOption -> IOption -> Bool #

Show IOption Source # 
Generic IOption Source # 

Associated Types

type Rep IOption :: * -> * #

Methods

from :: IOption -> Rep IOption x #

to :: Rep IOption x -> IOption #

type Rep IOption Source # 
type Rep IOption = D1 * (MetaData "IOption" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "IOption" PrefixI True) ((:*:) * ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_logLevel") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_logcats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [LogCat])) (S1 * (MetaSel (Just Symbol "opt_typecase") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)))) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_typeintype") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_coverage") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "opt_showimp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_errContext") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_repl") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "opt_verbose") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_nobanner") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "opt_quiet") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_codegen") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Just Symbol "opt_outputTy") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * OutputType)))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_ibcsubdir") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FilePath)) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_importdirs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FilePath])) (S1 * (MetaSel (Just Symbol "opt_sourcedirs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FilePath])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_triple") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)) (S1 * (MetaSel (Just Symbol "opt_cpu") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_cmdline") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Opt])) (S1 * (MetaSel (Just Symbol "opt_origerr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_autoSolve") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_autoImport") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FilePath])) (S1 * (MetaSel (Just Symbol "opt_optimise") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Optimisation])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "opt_printdepth") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Int))) (S1 * (MetaSel (Just Symbol "opt_evaltypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Just Symbol "opt_desugarnats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "opt_autoimpls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))))))))

data PPOption Source #

Constructors

PPOption 

Fields

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

data DefaultTotality Source #

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 Source # 
Show DefaultTotality Source # 
Generic DefaultTotality Source # 
type Rep DefaultTotality Source # 
type Rep DefaultTotality = D1 * (MetaData "DefaultTotality" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "DefaultCheckingTotal" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "DefaultCheckingPartial" PrefixI False) (U1 *)) (C1 * (MetaCons "DefaultCheckingCovering" PrefixI False) (U1 *))))

data InteractiveOpts Source #

Configuration options for interactive editing.

Instances

Show InteractiveOpts Source # 
Generic InteractiveOpts Source # 
type Rep InteractiveOpts Source # 
type Rep InteractiveOpts = D1 * (MetaData "InteractiveOpts" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "InteractiveOpts" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "interactiveOpts_indentWith") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "interactiveOpts_indentClause") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int))))

data IState Source #

The global state used in the Idris monad

Constructors

IState 

Fields

Instances

Show IState Source # 
Generic IState Source # 

Associated Types

type Rep IState :: * -> * #

Methods

from :: IState -> Rep IState x #

to :: Rep IState x -> IState #

type Rep IState Source # 
type Rep IState = D1 * (MetaData "IState" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "IState" PrefixI True) ((:*:) * ((:*:) * ((:*:) * ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "tt_ctxt") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Context)) (S1 * (MetaSel (Just Symbol "idris_constraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Set ConstraintFC)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_infixes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FixDecl])) (S1 * (MetaSel (Just Symbol "idris_implicits") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [PArg]))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_statics") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [Bool]))) (S1 * (MetaSel (Just Symbol "idris_interfaces") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt InterfaceInfo)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_openimpls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_records") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt RecordInfo))) (S1 * (MetaSel (Just Symbol "idris_dsls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt DSL))))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_optimisation") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt OptInfo))) (S1 * (MetaSel (Just Symbol "idris_datatypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt TypeInfo)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_namehints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [Name]))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_patdefs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt ([([(Name, Term)], Term, Term)], [PTerm])))) (S1 * (MetaSel (Just Symbol "idris_flags") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [FnOpt])))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_callgraph") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt CGInfo))) (S1 * (MetaSel (Just Symbol "idris_docstrings") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]))))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_moduledocs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt (Docstring DocTerm)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_tyinfodata") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt TIData))) (S1 * (MetaSel (Just Symbol "idris_fninfo") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt FnInfo)))))))) ((:*:) * ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_transforms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [(Term, Term)]))) (S1 * (MetaSel (Just Symbol "idris_autohints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt [Name])))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_totcheck") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, Name)])) (S1 * (MetaSel (Just Symbol "idris_defertotcheck") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, Name)])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_totcheckfail") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, String)])) (S1 * (MetaSel (Just Symbol "idris_options") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * IOption))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_name") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_lineapps") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [((FilePath, Int), PTerm)])) (S1 * (MetaSel (Just Symbol "idris_metavars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, (Maybe Name, Int, [Name], Bool, Bool))])))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_coercions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Just Symbol "idris_errRev") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Term, Term)]))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_errReduce") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) ((:*:) * (S1 * (MetaSel (Just Symbol "syntax_rules") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxRules)) (S1 * (MetaSel (Just Symbol "syntax_keywords") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String]))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "imported") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FilePath])) (S1 * (MetaSel (Just Symbol "idris_scprims") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, (Int, PrimFn))]))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_objs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Codegen, FilePath)])) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_libs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Codegen, String)])) (S1 * (MetaSel (Just Symbol "idris_cgflags") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Codegen, String)])))))))) ((:*:) * ((:*:) * ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_hdrs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Codegen, String)])) (S1 * (MetaSel (Just Symbol "idris_imported") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FilePath, Bool)]))) ((:*:) * (S1 * (MetaSel (Just Symbol "proof_list") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, (Bool, [String]))])) (S1 * (MetaSel (Just Symbol "errSpan") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe FC))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "parserWarnings") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, Err)])) (S1 * (MetaSel (Just Symbol "lastParse") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Name)))) ((:*:) * (S1 * (MetaSel (Just Symbol "indent_stack") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Int])) ((:*:) * (S1 * (MetaSel (Just Symbol "brace_stack") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Maybe Int])) (S1 * (MetaSel (Just Symbol "idris_parsedSpan") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe FC))))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "hide_list") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt Accessibility))) (S1 * (MetaSel (Just Symbol "default_access") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Accessibility))) ((:*:) * (S1 * (MetaSel (Just Symbol "default_total") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * DefaultTotality)) ((:*:) * (S1 * (MetaSel (Just Symbol "ibc_write") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [IBCWrite])) (S1 * (MetaSel (Just Symbol "compiled_so") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe String)))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_dynamic_libs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [DynamicLib])) (S1 * (MetaSel (Just Symbol "idris_language_extensions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [LanguageExt]))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_outputmode") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * OutputMode)) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_colourRepl") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "idris_colourTheme") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * ColourTheme))))))) ((:*:) * ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_errorhandlers") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Just Symbol "idris_nameIdx") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Int, Ctxt (Int, Name))))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_function_errorhandlers") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt (Map Name (Set Name))))) (S1 * (MetaSel (Just Symbol "module_aliases") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Map [Text] [Text]))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_consolewidth") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * ConsoleWidth)) (S1 * (MetaSel (Just Symbol "idris_postulates") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Set Name)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_externs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Set (Name, Int)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_erasureUsed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Int)])) (S1 * (MetaSel (Just Symbol "idris_repl_defs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "elab_stack") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Bool)])) (S1 * (MetaSel (Just Symbol "idris_symbols") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Map Name Name)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_exports") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_highlightedRegions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, OutputAnnotation)])) (S1 * (MetaSel (Just Symbol "idris_parserHighlights") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(FC, OutputAnnotation)]))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "idris_deprecated") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt String))) (S1 * (MetaSel (Just Symbol "idris_inmodule") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Set Name)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_ttstats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Map Term (Int, Term)))) ((:*:) * (S1 * (MetaSel (Just Symbol "idris_fragile") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Ctxt String))) (S1 * (MetaSel (Just Symbol "idris_interactiveOpts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * InteractiveOpts))))))))))

data SizeChange Source #

Constructors

Smaller 
Same 
Bigger 
Unknown 

Instances

Eq SizeChange Source # 
Show SizeChange Source # 
Generic SizeChange Source # 

Associated Types

type Rep SizeChange :: * -> * #

type Rep SizeChange Source # 
type Rep SizeChange = D1 * (MetaData "SizeChange" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "Smaller" PrefixI False) (U1 *)) (C1 * (MetaCons "Same" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "Bigger" PrefixI False) (U1 *)) (C1 * (MetaCons "Unknown" PrefixI False) (U1 *))))

data CGInfo Source #

Constructors

CGInfo 

Fields

Instances

data IBCWrite Source #

Instances

Show IBCWrite Source # 
Generic IBCWrite Source # 

Associated Types

type Rep IBCWrite :: * -> * #

Methods

from :: IBCWrite -> Rep IBCWrite x #

to :: Rep IBCWrite x -> IBCWrite #

type Rep IBCWrite Source # 
type Rep IBCWrite = D1 * (MetaData "IBCWrite" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "IBCFix" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FixDecl))) ((:+:) * (C1 * (MetaCons "IBCImp" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCStatic" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "IBCInterface" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "IBCRecord" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCImplementation" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "IBCDSL" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "IBCData" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCOpt" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "IBCMetavar" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "IBCSyntax" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Syntax))) (C1 * (MetaCons "IBCKeyword" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "IBCImport" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Bool, FilePath)))) ((:+:) * (C1 * (MetaCons "IBCImportDir" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FilePath))) (C1 * (MetaCons "IBCSourceDir" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FilePath))))) ((:+:) * (C1 * (MetaCons "IBCObj" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FilePath)))) ((:+:) * (C1 * (MetaCons "IBCLib" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) (C1 * (MetaCons "IBCCGFlag" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "IBCDyLib" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))) ((:+:) * (C1 * (MetaCons "IBCHeader" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) (C1 * (MetaCons "IBCAccess" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Accessibility)))))) ((:+:) * (C1 * (MetaCons "IBCMetaInformation" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * MetaInformation)))) ((:+:) * (C1 * (MetaCons "IBCTotal" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Totality)))) (C1 * (MetaCons "IBCInjective" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Injectivity))))))))) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "IBCFlags" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "IBCFnInfo" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FnInfo)))) (C1 * (MetaCons "IBCTrans" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Term, Term))))))) ((:+:) * (C1 * (MetaCons "IBCErrRev" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Term, Term)))) ((:+:) * (C1 * (MetaCons "IBCErrReduce" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCCG" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "IBCDoc" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "IBCCoercion" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCDef" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "IBCNameHint" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Name, Name)))) ((:+:) * (C1 * (MetaCons "IBCLineApp" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FilePath)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) (C1 * (MetaCons "IBCErrorHandler" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "IBCFunctionErrorHandler" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "IBCPostulate" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCExtern" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Name, Int)))))) ((:+:) * (C1 * (MetaCons "IBCTotCheckErr" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) ((:+:) * (C1 * (MetaCons "IBCParsedRegion" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))) (C1 * (MetaCons "IBCModDocs" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "IBCUsage" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Name, Int)))) ((:+:) * (C1 * (MetaCons "IBCExport" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "IBCAutoHint" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * (C1 * (MetaCons "IBCDeprecate" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) ((:+:) * (C1 * (MetaCons "IBCFragile" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) (C1 * (MetaCons "IBCConstraint" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * UConstraint))))))))))

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

Infixr 

Fields

InfixN 

Fields

PrefixN 

Fields

Instances

data Static Source #

Mark bindings with their explicitness, and laziness

Constructors

Static 
Dynamic 

Instances

Eq Static Source # 

Methods

(==) :: Static -> Static -> Bool #

(/=) :: Static -> Static -> Bool #

Data Static Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Static -> c Static #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Static #

toConstr :: Static -> Constr #

dataTypeOf :: Static -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Static) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Static) #

gmapT :: (forall b. Data b => b -> b) -> Static -> Static #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Static -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Static -> r #

gmapQ :: (forall d. Data d => d -> u) -> Static -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Static -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Static -> m Static #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Static -> m Static #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Static -> m Static #

Ord Static Source # 
Show Static Source # 
Generic Static Source # 

Associated Types

type Rep Static :: * -> * #

Methods

from :: Static -> Rep Static x #

to :: Rep Static x -> Static #

type Rep Static Source # 
type Rep Static = D1 * (MetaData "Static" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "Static" PrefixI False) (U1 *)) (C1 * (MetaCons "Dynamic" PrefixI False) (U1 *)))

data Plicity Source #

Constructors

Imp 

Fields

Exp 

Fields

Constraint 
TacImp 

Instances

Eq Plicity Source # 

Methods

(==) :: Plicity -> Plicity -> Bool #

(/=) :: Plicity -> Plicity -> Bool #

Data Plicity Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Plicity -> c Plicity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Plicity #

toConstr :: Plicity -> Constr #

dataTypeOf :: Plicity -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Plicity) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Plicity) #

gmapT :: (forall b. Data b => b -> b) -> Plicity -> Plicity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Plicity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Plicity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Plicity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Plicity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Plicity -> m Plicity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Plicity -> m Plicity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Plicity -> m Plicity #

Ord Plicity Source # 
Show Plicity Source # 
Generic Plicity Source # 

Associated Types

type Rep Plicity :: * -> * #

Methods

from :: Plicity -> Rep Plicity x #

to :: Rep Plicity x -> Plicity #

type Rep Plicity Source # 
type Rep Plicity = D1 * (MetaData "Plicity" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "Imp" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt])) ((:*:) * (S1 * (MetaSel (Just Symbol "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Static)) (S1 * (MetaSel (Just Symbol "pparam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)))) ((:*:) * (S1 * (MetaSel (Just Symbol "pscoped") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe ImplicitInfo))) ((:*:) * (S1 * (MetaSel (Just Symbol "pinsource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount)))))) (C1 * (MetaCons "Exp" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt])) (S1 * (MetaSel (Just Symbol "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Static))) ((:*:) * (S1 * (MetaSel (Just Symbol "pparam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount)))))) ((:+:) * (C1 * (MetaCons "Constraint" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt])) ((:*:) * (S1 * (MetaSel (Just Symbol "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Static)) (S1 * (MetaSel (Just Symbol "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount))))) (C1 * (MetaCons "TacImp" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt])) (S1 * (MetaSel (Just Symbol "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Static))) ((:*:) * (S1 * (MetaSel (Just Symbol "pscript") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Just Symbol "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount)))))))

data FnOpt Source #

Constructors

Inlinable

always evaluate when simplifying

TotalFn 
PartialFn 
CoveringFn 
AllGuarded

all delayed arguments guaranteed guarded by constructors

AssertTotal 
Dictionary

interface dictionary, eval only when a function argument, and further evaluation results.

OverlappingDictionary

Interface dictionary which may overlap

Implicit

implicit coercion

NoImplicit

do not apply implicit coercions

CExport String

export, with a C name

ErrorHandler

an error handler for use with the ErrorReflection extension

ErrorReverse

attempt to reverse normalise before showing in error

ErrorReduce

unfold definition before showing an error

Reflection

a reflecting function, compile-time only

Specialise [(Name, Maybe Int)]

specialise it, freeze these names

Constructor

Data constructor type

AutoHint

use in auto implicit search

PEGenerated

generated by partial evaluator

StaticFn

Marked static, to be evaluated by partial evaluator

Instances

Eq FnOpt Source # 

Methods

(==) :: FnOpt -> FnOpt -> Bool #

(/=) :: FnOpt -> FnOpt -> Bool #

Show FnOpt Source # 

Methods

showsPrec :: Int -> FnOpt -> ShowS #

show :: FnOpt -> String #

showList :: [FnOpt] -> ShowS #

Generic FnOpt Source # 

Associated Types

type Rep FnOpt :: * -> * #

Methods

from :: FnOpt -> Rep FnOpt x #

to :: Rep FnOpt x -> FnOpt #

type Rep FnOpt Source # 
type Rep FnOpt = D1 * (MetaData "FnOpt" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "Inlinable" PrefixI False) (U1 *)) (C1 * (MetaCons "TotalFn" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "PartialFn" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "CoveringFn" PrefixI False) (U1 *)) (C1 * (MetaCons "AllGuarded" PrefixI False) (U1 *))))) ((:+:) * ((:+:) * (C1 * (MetaCons "AssertTotal" PrefixI False) (U1 *)) (C1 * (MetaCons "Dictionary" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "OverlappingDictionary" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Implicit" PrefixI False) (U1 *)) (C1 * (MetaCons "NoImplicit" PrefixI False) (U1 *)))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "CExport" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))) (C1 * (MetaCons "ErrorHandler" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "ErrorReverse" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "ErrorReduce" PrefixI False) (U1 *)) (C1 * (MetaCons "Reflection" PrefixI False) (U1 *))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Specialise" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Maybe Int)]))) (C1 * (MetaCons "Constructor" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "AutoHint" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "PEGenerated" PrefixI False) (U1 *)) (C1 * (MetaCons "StaticFn" PrefixI False) (U1 *)))))))

type FnOpts = [FnOpt] 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

data PDecl' t Source #

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

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

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

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

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

Implementation declaration: arguments are documentation, syntax info, source location, constraints, interface name, parameters, full Implementation 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' Source # 

Methods

fmap :: (a -> b) -> PDecl' a -> PDecl' b #

(<$) :: a -> PDecl' b -> PDecl' a #

Show PDecl Source # 

Methods

showsPrec :: Int -> PDecl -> ShowS #

show :: PDecl -> String #

showList :: [PDecl] -> ShowS #

Generic (PDecl' t) Source # 

Associated Types

type Rep (PDecl' t) :: * -> * #

Methods

from :: PDecl' t -> Rep (PDecl' t) x #

to :: Rep (PDecl' t) x -> PDecl' t #

type Rep (PDecl' t) Source # 
type Rep (PDecl' t) = D1 * (MetaData "PDecl'" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PFix" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Fixity)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String]))))) (C1 * (MetaCons "PTy" PrefixI False) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Docstring (Either Err t))]))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FnOpts)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))))) ((:+:) * (C1 * (MetaCons "PPostulate" PrefixI False) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t))))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FnOpts))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))) (C1 * (MetaCons "PClauses" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FnOpts))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PClause' t]))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "PCAF" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) (C1 * (MetaCons "PData" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Docstring (Either Err t))])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * DataOpts)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PData' t)))))))) ((:+:) * (C1 * (MetaCons "PParams" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, t)])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))) ((:+:) * (C1 * (MetaCons "POpenInterfaces" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))) (C1 * (MetaCons "PNamespace" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PRecord" PrefixI False) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * DataOpts)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, FC, Plicity, t)])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Docstring (Either Err t))])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))])))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe (Name, FC)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo))))))) (C1 * (MetaCons "PInterface" PrefixI False) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, t)])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, FC, t)])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Docstring (Either Err t))])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, FC)])))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe (Name, FC)))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))))))))) ((:+:) * (C1 * (MetaCons "PImplementation" PrefixI False) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Docstring (Either Err t))])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, t)]))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Accessibility))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FnOpts)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [t])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, t)])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Name))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))))) ((:+:) * (C1 * (MetaCons "PDSL" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (DSL' t))))) (C1 * (MetaCons "PSyntax" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Syntax))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "PMutual" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t])))) (C1 * (MetaCons "PDirective" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Directive)))) ((:+:) * (C1 * (MetaCons "PProvider" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Docstring (Either Err t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SyntaxInfo)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (ProvideWhat' t))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * (C1 * (MetaCons "PTransform" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) (C1 * (MetaCons "PRunElabDecl" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String]))))))))))

data Directive Source #

The set of source directives

Instances

Generic Directive Source # 

Associated Types

type Rep Directive :: * -> * #

type Rep Directive Source # 
type Rep Directive = D1 * (MetaData "Directive" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "DLib" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) (C1 * (MetaCons "DLink" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))))) ((:+:) * (C1 * (MetaCons "DFlag" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) ((:+:) * (C1 * (MetaCons "DInclude" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Codegen)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) (C1 * (MetaCons "DHide" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "DFreeze" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "DThaw" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))) ((:+:) * (C1 * (MetaCons "DInjective" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:+:) * (C1 * (MetaCons "DSetTotal" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "DAccess" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Accessibility))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "DDefault" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * DefaultTotality))) (C1 * (MetaCons "DLogging" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Integer)))) ((:+:) * (C1 * (MetaCons "DDynamicLibs" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String]))) ((:+:) * (C1 * (MetaCons "DNameHint" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, FC)]))))) (C1 * (MetaCons "DErrorHandlers" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, FC)]))))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "DLanguage" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * LanguageExt))) (C1 * (MetaCons "DDeprecate" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))))) ((:+:) * (C1 * (MetaCons "DFragile" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)))) ((:+:) * (C1 * (MetaCons "DAutoImplicits" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) (C1 * (MetaCons "DUsed" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))))))))

data RDeclInstructions Source #

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

data EState Source #

For elaborator state

Constructors

EState 

Fields

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

Instances

Functor PClause' Source # 

Methods

fmap :: (a -> b) -> PClause' a -> PClause' b #

(<$) :: a -> PClause' b -> PClause' a #

Show PClause Source # 
Generic (PClause' t) Source # 

Associated Types

type Rep (PClause' t) :: * -> * #

Methods

from :: PClause' t -> Rep (PClause' t) x #

to :: Rep (PClause' t) x -> PClause' t #

type Rep (PClause' t) Source # 
type Rep (PClause' t) = D1 * (MetaData "PClause'" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "PClause" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [t])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t])))))) (C1 * (MetaCons "PWith" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [t])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe (Name, FC)))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))))) ((:+:) * (C1 * (MetaCons "PClauseR" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [t]))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))) (C1 * (MetaCons "PWithR" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [t]))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe (Name, FC)))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl' t]))))))))

data PData' t Source #

Data declaration

Constructors

PDatadecl

Data declaration

Fields

PLaterdecl

Placeholder for data whose constructors are defined later

Fields

Instances

Functor PData' Source # 

Methods

fmap :: (a -> b) -> PData' a -> PData' b #

(<$) :: a -> PData' b -> PData' a #

Show PData Source # 

Methods

showsPrec :: Int -> PData -> ShowS #

show :: PData -> String #

showList :: [PData] -> ShowS #

Generic (PData' t) Source # 

Associated Types

type Rep (PData' t) :: * -> * #

Methods

from :: PData' t -> Rep (PData' t) x #

to :: Rep (PData' t) x -> PData' t #

type Rep (PData' t) Source # 

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

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.

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

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

Get all the names declared in a declaration

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

data PunInfo Source #

Constructors

IsType 
IsTerm 
TypeOrTerm 

Instances

Eq PunInfo Source # 

Methods

(==) :: PunInfo -> PunInfo -> Bool #

(/=) :: PunInfo -> PunInfo -> Bool #

Data PunInfo Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PunInfo -> c PunInfo #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PunInfo #

toConstr :: PunInfo -> Constr #

dataTypeOf :: PunInfo -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PunInfo) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PunInfo) #

gmapT :: (forall b. Data b => b -> b) -> PunInfo -> PunInfo #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PunInfo -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PunInfo -> r #

gmapQ :: (forall d. Data d => d -> u) -> PunInfo -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PunInfo -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo #

Ord PunInfo Source # 
Show PunInfo Source # 
Generic PunInfo Source # 

Associated Types

type Rep PunInfo :: * -> * #

Methods

from :: PunInfo -> Rep PunInfo x #

to :: Rep PunInfo x -> PunInfo #

type Rep PunInfo Source # 
type Rep PunInfo = D1 * (MetaData "PunInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "IsType" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "IsTerm" PrefixI False) (U1 *)) (C1 * (MetaCons "TypeOrTerm" PrefixI False) (U1 *))))

data PTerm Source #

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 RigCount 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 interface 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 FC 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

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

Methods

(==) :: PTerm -> PTerm -> Bool #

(/=) :: PTerm -> PTerm -> Bool #

Data PTerm Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PTerm -> c PTerm #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PTerm #

toConstr :: PTerm -> Constr #

dataTypeOf :: PTerm -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PTerm) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PTerm) #

gmapT :: (forall b. Data b => b -> b) -> PTerm -> PTerm #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PTerm -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PTerm -> r #

gmapQ :: (forall d. Data d => d -> u) -> PTerm -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PTerm -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PTerm -> m PTerm #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PTerm -> m PTerm #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PTerm -> m PTerm #

Ord PTerm Source # 

Methods

compare :: PTerm -> PTerm -> Ordering #

(<) :: PTerm -> PTerm -> Bool #

(<=) :: PTerm -> PTerm -> Bool #

(>) :: PTerm -> PTerm -> Bool #

(>=) :: PTerm -> PTerm -> Bool #

max :: PTerm -> PTerm -> PTerm #

min :: PTerm -> PTerm -> PTerm #

Show PTerm Source # 

Methods

showsPrec :: Int -> PTerm -> ShowS #

show :: PTerm -> String #

showList :: [PTerm] -> ShowS #

Show PClause Source # 
Show PData Source # 

Methods

showsPrec :: Int -> PData -> ShowS #

show :: PData -> String #

showList :: [PData] -> ShowS #

Show PDecl Source # 

Methods

showsPrec :: Int -> PDecl -> ShowS #

show :: PDecl -> String #

showList :: [PDecl] -> ShowS #

Generic PTerm Source # 

Associated Types

type Rep PTerm :: * -> * #

Methods

from :: PTerm -> Rep PTerm x #

to :: Rep PTerm x -> PTerm #

type Rep PTerm Source # 
type Rep PTerm = D1 * (MetaData "PTerm" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PQuote" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Raw))) (C1 * (MetaCons "PRef" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FC])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))))) ((:+:) * (C1 * (MetaCons "PInferRef" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FC])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "PPatvar" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))) (C1 * (MetaCons "PLam" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "PPi" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Plicity)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) ((:+:) * (C1 * (MetaCons "PLet" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) (C1 * (MetaCons "PTyped" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) ((:+:) * (C1 * (MetaCons "PApp" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PArg]))))) ((:+:) * (C1 * (MetaCons "PWithApp" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) (C1 * (MetaCons "PAppImpl" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ImplicitInfo])))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PAppBind" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PArg]))))) (C1 * (MetaCons "PMatchApp" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))))) ((:+:) * (C1 * (MetaCons "PIfThenElse" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) ((:+:) * (C1 * (MetaCons "PCase" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(PTerm, PTerm)]))))) (C1 * (MetaCons "PTrue" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PunInfo))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "PResolveTC" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))) ((:+:) * (C1 * (MetaCons "PRewrite" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Name)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe PTerm))))))) (C1 * (MetaCons "PPair" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FC]))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PunInfo)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))))) ((:+:) * (C1 * (MetaCons "PDPair" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [FC])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PunInfo)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) ((:+:) * (C1 * (MetaCons "PAs" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) (C1 * (MetaCons "PAlternative" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Name)])) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PAltType)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PTerm])))))))))) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PHidden" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) (C1 * (MetaCons "PType" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)))) ((:+:) * (C1 * (MetaCons "PUniverse" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Universe)))) ((:+:) * (C1 * (MetaCons "PGoal" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) (C1 * (MetaCons "PConstant" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Const))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Placeholder" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "PDoBlock" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDo]))) (C1 * (MetaCons "PIdiom" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) ((:+:) * (C1 * (MetaCons "PMetavar" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))) ((:+:) * (C1 * (MetaCons "PProof" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PTactic]))) (C1 * (MetaCons "PTactics" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PTactic]))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "PElabError" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Err))) (C1 * (MetaCons "PImpossible" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "PCoerced" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) ((:+:) * (C1 * (MetaCons "PDisamb" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [[Text]])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))) (C1 * (MetaCons "PUnifyLog" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "PNoImplicits" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))) ((:+:) * (C1 * (MetaCons "PQuasiquote" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe PTerm))))) (C1 * (MetaCons "PUnquote" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))) ((:+:) * (C1 * (MetaCons "PQuoteName" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC))))) ((:+:) * (C1 * (MetaCons "PRunElab" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String]))))) (C1 * (MetaCons "PConstSugar" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * PTerm))))))))))

data PAltType Source #

Constructors

ExactlyOne Bool

flag sets whether delay is allowed

FirstSuccess 
TryImplicit 

Instances

Eq PAltType Source # 
Data PAltType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PAltType -> c PAltType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PAltType #

toConstr :: PAltType -> Constr #

dataTypeOf :: PAltType -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PAltType) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PAltType) #

gmapT :: (forall b. Data b => b -> b) -> PAltType -> PAltType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PAltType -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PAltType -> r #

gmapQ :: (forall d. Data d => d -> u) -> PAltType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PAltType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType #

Ord PAltType Source # 
Generic PAltType Source # 

Associated Types

type Rep PAltType :: * -> * #

Methods

from :: PAltType -> Rep PAltType x #

to :: Rep PAltType x -> PAltType #

type Rep PAltType Source # 
type Rep PAltType = D1 * (MetaData "PAltType" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "ExactlyOne" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:+:) * (C1 * (MetaCons "FirstSuccess" PrefixI False) (U1 *)) (C1 * (MetaCons "TryImplicit" PrefixI False) (U1 *))))

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

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.

data PTactic' t Source #

Instances

Functor PTactic' Source # 

Methods

fmap :: (a -> b) -> PTactic' a -> PTactic' b #

(<$) :: a -> PTactic' b -> PTactic' a #

Foldable PTactic' Source # 

Methods

fold :: Monoid m => PTactic' m -> m #

foldMap :: Monoid m => (a -> m) -> PTactic' a -> m #

foldr :: (a -> b -> b) -> b -> PTactic' a -> b #

foldr' :: (a -> b -> b) -> b -> PTactic' a -> b #

foldl :: (b -> a -> b) -> b -> PTactic' a -> b #

foldl' :: (b -> a -> b) -> b -> PTactic' a -> b #

foldr1 :: (a -> a -> a) -> PTactic' a -> a #

foldl1 :: (a -> a -> a) -> PTactic' a -> a #

toList :: PTactic' a -> [a] #

null :: PTactic' a -> Bool #

length :: PTactic' a -> Int #

elem :: Eq a => a -> PTactic' a -> Bool #

maximum :: Ord a => PTactic' a -> a #

minimum :: Ord a => PTactic' a -> a #

sum :: Num a => PTactic' a -> a #

product :: Num a => PTactic' a -> a #

Traversable PTactic' Source # 

Methods

traverse :: Applicative f => (a -> f b) -> PTactic' a -> f (PTactic' b) #

sequenceA :: Applicative f => PTactic' (f a) -> f (PTactic' a) #

mapM :: Monad m => (a -> m b) -> PTactic' a -> m (PTactic' b) #

sequence :: Monad m => PTactic' (m a) -> m (PTactic' a) #

Eq t => Eq (PTactic' t) Source # 

Methods

(==) :: PTactic' t -> PTactic' t -> Bool #

(/=) :: PTactic' t -> PTactic' t -> Bool #

Data t => Data (PTactic' t) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PTactic' t -> c (PTactic' t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PTactic' t) #

toConstr :: PTactic' t -> Constr #

dataTypeOf :: PTactic' t -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PTactic' t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PTactic' t)) #

gmapT :: (forall b. Data b => b -> b) -> PTactic' t -> PTactic' t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PTactic' t -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PTactic' t -> r #

gmapQ :: (forall d. Data d => d -> u) -> PTactic' t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PTactic' t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PTactic' t -> m (PTactic' t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PTactic' t -> m (PTactic' t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PTactic' t -> m (PTactic' t) #

Ord t => Ord (PTactic' t) Source # 

Methods

compare :: PTactic' t -> PTactic' t -> Ordering #

(<) :: PTactic' t -> PTactic' t -> Bool #

(<=) :: PTactic' t -> PTactic' t -> Bool #

(>) :: PTactic' t -> PTactic' t -> Bool #

(>=) :: PTactic' t -> PTactic' t -> Bool #

max :: PTactic' t -> PTactic' t -> PTactic' t #

min :: PTactic' t -> PTactic' t -> PTactic' t #

Show t => Show (PTactic' t) Source # 

Methods

showsPrec :: Int -> PTactic' t -> ShowS #

show :: PTactic' t -> String #

showList :: [PTactic' t] -> ShowS #

Generic (PTactic' t) Source # 

Associated Types

type Rep (PTactic' t) :: * -> * #

Methods

from :: PTactic' t -> Rep (PTactic' t) x #

to :: Rep (PTactic' t) x -> PTactic' t #

type Rep (PTactic' t) Source # 
type Rep (PTactic' t) = D1 * (MetaData "PTactic'" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "Intro" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name]))) (C1 * (MetaCons "Intros" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "Focus" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "Refine" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Bool])))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Rewrite" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) (C1 * (MetaCons "DoUnify" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "Equiv" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:+:) * (C1 * (MetaCons "Claim" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) (C1 * (MetaCons "Unfocus" PrefixI False) (U1 *)))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "MatchRefine" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons "LetTac" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) ((:+:) * (C1 * (MetaCons "LetTacTy" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) ((:+:) * (C1 * (MetaCons "Exact" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) (C1 * (MetaCons "Compute" PrefixI False) (U1 *))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Trivial" PrefixI False) (U1 *)) (C1 * (MetaCons "TCImplementation" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "ProofSearch" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])))))) ((:+:) * (C1 * (MetaCons "Solve" PrefixI False) (U1 *)) (C1 * (MetaCons "Attack" PrefixI False) (U1 *))))))) ((:+:) * ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "ProofState" PrefixI False) (U1 *)) (C1 * (MetaCons "ProofTerm" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "Undo" PrefixI False) (U1 *)) (C1 * (MetaCons "Try" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PTactic' t))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PTactic' t))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "TSeq" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PTactic' t))) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PTactic' t))))) (C1 * (MetaCons "ApplyTactic" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) ((:+:) * (C1 * (MetaCons "ByReflection" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:+:) * (C1 * (MetaCons "Reflect" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) (C1 * (MetaCons "Fill" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))))) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "GoalType" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (PTactic' t))))) (C1 * (MetaCons "TCheck" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) ((:+:) * (C1 * (MetaCons "TEval" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:+:) * (C1 * (MetaCons "TDocStr" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Either Name Const)))) (C1 * (MetaCons "TSearch" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Skip" PrefixI False) (U1 *)) (C1 * (MetaCons "TFail" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ErrorReportPart])))) ((:+:) * (C1 * (MetaCons "Qed" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Abandon" PrefixI False) (U1 *)) (C1 * (MetaCons "SourceFC" PrefixI False) (U1 *))))))))

data PDo' t Source #

Constructors

DoExp FC t 
DoBind FC Name FC t

second FC is precise name location

DoBindP FC t t [(t, t)] 
DoLet FC RigCount Name FC t t

second FC is precise name location

DoLetP FC t t [(t, t)] 
DoRewrite FC t 

Instances

Functor PDo' Source # 

Methods

fmap :: (a -> b) -> PDo' a -> PDo' b #

(<$) :: a -> PDo' b -> PDo' a #

Eq t => Eq (PDo' t) Source # 

Methods

(==) :: PDo' t -> PDo' t -> Bool #

(/=) :: PDo' t -> PDo' t -> Bool #

Data t => Data (PDo' t) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PDo' t -> c (PDo' t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PDo' t) #

toConstr :: PDo' t -> Constr #

dataTypeOf :: PDo' t -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PDo' t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PDo' t)) #

gmapT :: (forall b. Data b => b -> b) -> PDo' t -> PDo' t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PDo' t -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PDo' t -> r #

gmapQ :: (forall d. Data d => d -> u) -> PDo' t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PDo' t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PDo' t -> m (PDo' t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PDo' t -> m (PDo' t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PDo' t -> m (PDo' t) #

Ord t => Ord (PDo' t) Source # 

Methods

compare :: PDo' t -> PDo' t -> Ordering #

(<) :: PDo' t -> PDo' t -> Bool #

(<=) :: PDo' t -> PDo' t -> Bool #

(>) :: PDo' t -> PDo' t -> Bool #

(>=) :: PDo' t -> PDo' t -> Bool #

max :: PDo' t -> PDo' t -> PDo' t #

min :: PDo' t -> PDo' t -> PDo' t #

Generic (PDo' t) Source # 

Associated Types

type Rep (PDo' t) :: * -> * #

Methods

from :: PDo' t -> Rep (PDo' t) x #

to :: Rep (PDo' t) x -> PDo' t #

type Rep (PDo' t) Source # 
type Rep (PDo' t) = D1 * (MetaData "PDo'" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "DoExp" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))) ((:+:) * (C1 * (MetaCons "DoBind" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) (C1 * (MetaCons "DoBindP" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(t, t)]))))))) ((:+:) * (C1 * (MetaCons "DoLet" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * RigCount)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))) ((:+:) * (C1 * (MetaCons "DoLetP" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(t, t)]))))) (C1 * (MetaCons "DoRewrite" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * FC)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))))

data PArg' t Source #

Constructors

PImp 

Fields

PExp 

Fields

PConstraint 

Fields

PTacImplicit 

Fields

Instances

Functor PArg' Source # 

Methods

fmap :: (a -> b) -> PArg' a -> PArg' b #

(<$) :: a -> PArg' b -> PArg' a #

Eq t => Eq (PArg' t) Source # 

Methods

(==) :: PArg' t -> PArg' t -> Bool #

(/=) :: PArg' t -> PArg' t -> Bool #

Data t => Data (PArg' t) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PArg' t -> c (PArg' t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PArg' t) #

toConstr :: PArg' t -> Constr #

dataTypeOf :: PArg' t -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PArg' t)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PArg' t)) #

gmapT :: (forall b. Data b => b -> b) -> PArg' t -> PArg' t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PArg' t -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PArg' t -> r #

gmapQ :: (forall d. Data d => d -> u) -> PArg' t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PArg' t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PArg' t -> m (PArg' t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PArg' t -> m (PArg' t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PArg' t -> m (PArg' t) #

Ord t => Ord (PArg' t) Source # 

Methods

compare :: PArg' t -> PArg' t -> Ordering #

(<) :: PArg' t -> PArg' t -> Bool #

(<=) :: PArg' t -> PArg' t -> Bool #

(>) :: PArg' t -> PArg' t -> Bool #

(>=) :: PArg' t -> PArg' t -> Bool #

max :: PArg' t -> PArg' t -> PArg' t #

min :: PArg' t -> PArg' t -> PArg' t #

Show t => Show (PArg' t) Source # 

Methods

showsPrec :: Int -> PArg' t -> ShowS #

show :: PArg' t -> String #

showList :: [PArg' t] -> ShowS #

Generic (PArg' t) Source # 

Associated Types

type Rep (PArg' t) :: * -> * #

Methods

from :: PArg' t -> Rep (PArg' t) x #

to :: Rep (PArg' t) x -> PArg' t #

type Rep (PArg' t) Source # 
type Rep (PArg' t) = D1 * (MetaData "PArg'" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "PImp" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "priority") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "machine_inf") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Just Symbol "argopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt])) ((:*:) * (S1 * (MetaSel (Just Symbol "pname") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Just Symbol "getTm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))) (C1 * (MetaCons "PExp" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "priority") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "argopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt]))) ((:*:) * (S1 * (MetaSel (Just Symbol "pname") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Just Symbol "getTm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))))) ((:+:) * (C1 * (MetaCons "PConstraint" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "priority") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "argopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt]))) ((:*:) * (S1 * (MetaSel (Just Symbol "pname") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Just Symbol "getTm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))) (C1 * (MetaCons "PTacImplicit" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "priority") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "argopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [ArgOpt]))) ((:*:) * (S1 * (MetaSel (Just Symbol "pname") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Just Symbol "getScript") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Just Symbol "getTm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))))))

data ArgOpt Source #

Instances

Eq ArgOpt Source # 

Methods

(==) :: ArgOpt -> ArgOpt -> Bool #

(/=) :: ArgOpt -> ArgOpt -> Bool #

Data ArgOpt Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArgOpt -> c ArgOpt #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgOpt #

toConstr :: ArgOpt -> Constr #

dataTypeOf :: ArgOpt -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ArgOpt) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgOpt) #

gmapT :: (forall b. Data b => b -> b) -> ArgOpt -> ArgOpt #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgOpt -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgOpt -> r #

gmapQ :: (forall d. Data d => d -> u) -> ArgOpt -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgOpt -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt #

Ord ArgOpt Source # 
Show ArgOpt Source # 
Generic ArgOpt Source # 

Associated Types

type Rep ArgOpt :: * -> * #

Methods

from :: ArgOpt -> Rep ArgOpt x #

to :: Rep ArgOpt x -> ArgOpt #

type Rep ArgOpt Source # 
type Rep ArgOpt = D1 * (MetaData "ArgOpt" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * ((:+:) * (C1 * (MetaCons "AlwaysShow" PrefixI False) (U1 *)) (C1 * (MetaCons "HideDisplay" PrefixI False) (U1 *))) ((:+:) * (C1 * (MetaCons "InaccessibleArg" PrefixI False) (U1 *)) (C1 * (MetaCons "UnknownImp" PrefixI False) (U1 *))))

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 InterfaceInfo Source #

Constructors

CI 

Fields

Instances

Show InterfaceInfo Source # 
Generic InterfaceInfo Source # 

Associated Types

type Rep InterfaceInfo :: * -> * #

type Rep InterfaceInfo Source # 
type Rep InterfaceInfo = D1 * (MetaData "InterfaceInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "CI" PrefixI True) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "implementationCtorName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Just Symbol "interface_methods") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, (Bool, FnOpts, PTerm))]))) ((:*:) * (S1 * (MetaSel (Just Symbol "interface_defaults") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, (Name, PDecl))])) (S1 * (MetaSel (Just Symbol "interface_default_super_interfaces") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PDecl])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "interface_impparams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Just Symbol "interface_params") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name]))) ((:*:) * (S1 * (MetaSel (Just Symbol "interface_constraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [PTerm])) ((:*:) * (S1 * (MetaSel (Just Symbol "interface_implementations") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, Bool)])) (S1 * (MetaSel (Just Symbol "interface_determiners") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Int])))))))

data RecordInfo Source #

Instances

Show RecordInfo Source # 
Generic RecordInfo Source # 

Associated Types

type Rep RecordInfo :: * -> * #

type Rep RecordInfo Source # 
type Rep RecordInfo = D1 * (MetaData "RecordInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "RI" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "record_parameters") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, PTerm)])) ((:*:) * (S1 * (MetaSel (Just Symbol "record_constructor") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Just Symbol "record_projections") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])))))

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 Source # 
Generic TIData Source # 

Associated Types

type Rep TIData :: * -> * #

Methods

from :: TIData -> Rep TIData x #

to :: Rep TIData x -> TIData #

type Rep TIData Source # 
type Rep TIData = D1 * (MetaData "TIData" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "TIPartial" PrefixI False) (U1 *)) (C1 * (MetaCons "TISolution" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Term]))))

data FnInfo Source #

Miscellaneous information about functions

Constructors

FnInfo 

Fields

Instances

Show FnInfo Source # 
Generic FnInfo Source # 

Associated Types

type Rep FnInfo :: * -> * #

Methods

from :: FnInfo -> Rep FnInfo x #

to :: Rep FnInfo x -> FnInfo #

type Rep FnInfo Source # 
type Rep FnInfo = D1 * (MetaData "FnInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "FnInfo" PrefixI True) (S1 * (MetaSel (Just Symbol "fn_params") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Int])))

data OptInfo Source #

Constructors

Optimise 

Fields

Instances

Show OptInfo Source # 
Generic OptInfo Source # 

Associated Types

type Rep OptInfo :: * -> * #

Methods

from :: OptInfo -> Rep OptInfo x #

to :: Rep OptInfo x -> OptInfo #

type Rep OptInfo Source # 
type Rep OptInfo = D1 * (MetaData "OptInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "Optimise" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "inaccessible") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Int, Name)])) ((:*:) * (S1 * (MetaSel (Just Symbol "detaggable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "forceable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Int])))))

data DSL' t Source #

Syntactic sugar info

Constructors

DSL 

Fields

Instances

Functor DSL' Source # 

Methods

fmap :: (a -> b) -> DSL' a -> DSL' b #

(<$) :: a -> DSL' b -> DSL' a #

Show t => Show (DSL' t) Source # 

Methods

showsPrec :: Int -> DSL' t -> ShowS #

show :: DSL' t -> String #

showList :: [DSL' t] -> ShowS #

Generic (DSL' t) Source # 

Associated Types

type Rep (DSL' t) :: * -> * #

Methods

from :: DSL' t -> Rep (DSL' t) x #

to :: Rep (DSL' t) x -> DSL' t #

type Rep (DSL' t) Source # 

data SynContext Source #

Instances

Show SynContext Source # 
Generic SynContext Source # 

Associated Types

type Rep SynContext :: * -> * #

type Rep SynContext Source # 
type Rep SynContext = D1 * (MetaData "SynContext" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "PatternSyntax" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "TermSyntax" PrefixI False) (U1 *)) (C1 * (MetaCons "AnySyntax" PrefixI False) (U1 *))))

newtype SyntaxRules Source #

Constructors

SyntaxRules 

Fields

Instances

Generic SyntaxRules Source # 

Associated Types

type Rep SyntaxRules :: * -> * #

type Rep SyntaxRules Source # 
type Rep SyntaxRules = D1 * (MetaData "SyntaxRules" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" True) (C1 * (MetaCons "SyntaxRules" PrefixI True) (S1 * (MetaSel (Just Symbol "syntaxRulesList") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Syntax])))

data Using Source #

Instances

Eq Using Source # 

Methods

(==) :: Using -> Using -> Bool #

(/=) :: Using -> Using -> Bool #

Data Using Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Using -> c Using #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Using #

toConstr :: Using -> Constr #

dataTypeOf :: Using -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Using) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Using) #

gmapT :: (forall b. Data b => b -> b) -> Using -> Using #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using -> r #

gmapQ :: (forall d. Data d => d -> u) -> Using -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Using -> m Using #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Using -> m Using #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Using -> m Using #

Show Using Source # 

Methods

showsPrec :: Int -> Using -> ShowS #

show :: Using -> String #

showList :: [Using] -> ShowS #

Generic Using Source # 

Associated Types

type Rep Using :: * -> * #

Methods

from :: Using -> Rep Using x #

to :: Rep Using x -> Using #

type Rep Using Source # 

data SyntaxInfo Source #

Constructors

Syn 

Fields

Instances

Show SyntaxInfo Source # 
Generic SyntaxInfo Source # 

Associated Types

type Rep SyntaxInfo :: * -> * #

type Rep SyntaxInfo Source # 
type Rep SyntaxInfo = D1 * (MetaData "SyntaxInfo" "Idris.AbsSyntaxTree" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "Syn" PrefixI True) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "using") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Using])) ((:*:) * (S1 * (MetaSel (Just Symbol "syn_params") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Name, PTerm)])) (S1 * (MetaSel (Just Symbol "syn_namespace") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [String])))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "no_imp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Just Symbol "imp_methods") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name]))) ((:*:) * (S1 * (MetaSel (Just Symbol "decoration") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Name -> Name))) (S1 * (MetaSel (Just Symbol "inPattern") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))))) ((:*:) * ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "implicitAllowed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "constraintAllowed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool))) ((:*:) * (S1 * (MetaSel (Just Symbol "maxline") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Maybe Int))) (S1 * (MetaSel (Just Symbol "mut_nesting") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "dsl_info") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * DSL)) (S1 * (MetaSel (Just Symbol "syn_in_quasiquote") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int))) ((:*:) * (S1 * (MetaSel (Just Symbol "syn_toplevel") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)) (S1 * (MetaSel (Just Symbol "withAppAllowed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Bool)))))))

eqOpts :: [a] 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.

annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour 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.

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

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

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.

basename :: Name -> Name Source #

Strip away namespace information

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

getImps :: [PArg] -> [(Name, 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

showTmOpts :: PPOption -> PTerm -> String Source #

Show a term with specific options

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