idris-1.3.2: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.AbsSyntaxTree

Description

 
Synopsis

Documentation

data ElabWhat Source #

Constructors

ETypes 
EDefns 
EAll 
Instances
Eq ElabWhat Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Show ElabWhat Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IOption :: Type -> Type #

Methods

from :: IOption -> Rep IOption x #

to :: Rep IOption x -> IOption #

NFData IOption Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: IOption -> () #

type Rep IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data PPOption Source #

Constructors

PPOption 

Fields

Instances
Show PPOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

defaultPPOption :: PPOption Source #

Pretty printing options with default verbosity.

verbosePPOption :: PPOption Source #

Pretty printing options with the most verbosity.

ppOption :: IOption -> PPOption Source #

Get pretty printing options from the big options record.

ppOptionIst :: IState -> PPOption Source #

Get pretty printing options from an idris state record.

data OutputMode Source #

The output mode in use

Constructors

RawOutput Handle

Print user output directly to the handle

IdeMode Integer Handle

Send IDE output for some request ID to the handle

Instances
Show OutputMode Source # 
Instance details

Defined in Idris.AbsSyntaxTree

NFData OutputMode Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: OutputMode -> () #

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Show DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep DefaultTotality :: Type -> Type #

Binary DefaultTotality Source # 
Instance details

Defined in Idris.IBC

NFData DefaultTotality Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DefaultTotality -> () #

type Rep DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep DefaultTotality = D1 (MetaData "DefaultTotality" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "DefaultCheckingTotal" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "DefaultCheckingPartial" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "DefaultCheckingCovering" PrefixI False) (U1 :: Type -> Type)))

data InteractiveOpts Source #

Configuration options for interactive editing.

Instances
Show InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep InteractiveOpts :: Type -> Type #

NFData InteractiveOpts Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: InteractiveOpts -> () #

type Rep InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep InteractiveOpts = D1 (MetaData "InteractiveOpts" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "InteractiveOpts" PrefixI True) (S1 (MetaSel (Just "interactiveOpts_indentWith") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: S1 (MetaSel (Just "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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic IState Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IState :: Type -> Type #

Methods

from :: IState -> Rep IState x #

to :: Rep IState x -> IState #

NFData IState Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: IState -> () #

type Rep IState Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data SizeChange Source #

Constructors

Smaller 
Same 
Bigger 
Unknown 
Instances
Eq SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Show SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SizeChange :: Type -> Type #

Binary SizeChange Source # 
Instance details

Defined in Idris.IBC

NFData SizeChange Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SizeChange -> () #

type Rep SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep SizeChange = D1 (MetaData "SizeChange" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Smaller" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Same" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Bigger" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Unknown" PrefixI False) (U1 :: Type -> Type)))

data CGInfo Source #

Constructors

CGInfo 

Fields

Instances
Show CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep CGInfo :: Type -> Type #

Methods

from :: CGInfo -> Rep CGInfo x #

to :: Rep CGInfo x -> CGInfo #

Binary CGInfo Source # 
Instance details

Defined in Idris.IBC

Methods

put :: CGInfo -> Put #

get :: Get CGInfo #

putList :: [CGInfo] -> Put #

NFData CGInfo Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: CGInfo -> () #

type Rep CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

data IBCWrite Source #

Instances
Show IBCWrite Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic IBCWrite Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IBCWrite :: Type -> Type #

Methods

from :: IBCWrite -> Rep IBCWrite x #

to :: Rep IBCWrite x -> IBCWrite #

NFData IBCWrite Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: IBCWrite -> () #

type Rep IBCWrite Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

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
Eq Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Fixity :: Type -> Type #

Methods

from :: Fixity -> Rep Fixity x #

to :: Rep Fixity x -> Fixity #

Binary Fixity Source # 
Instance details

Defined in Idris.IBC

Methods

put :: Fixity -> Put #

get :: Get Fixity #

putList :: [Fixity] -> Put #

NFData Fixity Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Fixity -> () #

type Rep Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

data FixDecl Source #

Constructors

Fix Fixity String 
Instances
Eq FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Ord FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Show FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FixDecl :: Type -> Type #

Methods

from :: FixDecl -> Rep FixDecl x #

to :: Rep FixDecl x -> FixDecl #

Binary FixDecl Source # 
Instance details

Defined in Idris.IBC

Methods

put :: FixDecl -> Put #

get :: Get FixDecl #

putList :: [FixDecl] -> Put #

NFData FixDecl Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: FixDecl -> () #

type Rep FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

data Static Source #

Mark bindings with their explicitness, and laziness

Constructors

Static 
Dynamic 
Instances
Eq Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Show Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Static :: Type -> Type #

Methods

from :: Static -> Rep Static x #

to :: Rep Static x -> Static #

Binary Static Source # 
Instance details

Defined in Idris.IBC

Methods

put :: Static -> Put #

get :: Get Static #

putList :: [Static] -> Put #

NFData Static Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Static -> () #

type Rep Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Static = D1 (MetaData "Static" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "Static" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Dynamic" PrefixI False) (U1 :: Type -> Type))

data Plicity Source #

Constructors

Imp 

Fields

Exp 

Fields

Constraint 
TacImp 
Instances
Eq Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Show Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Plicity :: Type -> Type #

Methods

from :: Plicity -> Rep Plicity x #

to :: Rep Plicity x -> Plicity #

Binary Plicity Source # 
Instance details

Defined in Idris.IBC

Methods

put :: Plicity -> Put #

get :: Get Plicity #

putList :: [Plicity] -> Put #

NFData Plicity Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Plicity -> () #

type Rep Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Plicity = D1 (MetaData "Plicity" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Imp" PrefixI True) ((S1 (MetaSel (Just "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ArgOpt]) :*: (S1 (MetaSel (Just "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Static) :*: S1 (MetaSel (Just "pparam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) :*: (S1 (MetaSel (Just "pscoped") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ImplicitInfo)) :*: (S1 (MetaSel (Just "pinsource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount)))) :+: C1 (MetaCons "Exp" PrefixI True) ((S1 (MetaSel (Just "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ArgOpt]) :*: S1 (MetaSel (Just "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Static)) :*: (S1 (MetaSel (Just "pparam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount)))) :+: (C1 (MetaCons "Constraint" PrefixI True) (S1 (MetaSel (Just "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ArgOpt]) :*: (S1 (MetaSel (Just "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Static) :*: S1 (MetaSel (Just "pcount") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount))) :+: C1 (MetaCons "TacImp" PrefixI True) ((S1 (MetaSel (Just "pargopts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ArgOpt]) :*: S1 (MetaSel (Just "pstatic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Static)) :*: (S1 (MetaSel (Just "pscript") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Just "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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> FnOpt -> ShowS #

show :: FnOpt -> String #

showList :: [FnOpt] -> ShowS #

Generic FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FnOpt :: Type -> Type #

Methods

from :: FnOpt -> Rep FnOpt x #

to :: Rep FnOpt x -> FnOpt #

Binary FnOpt Source # 
Instance details

Defined in Idris.IBC

Methods

put :: FnOpt -> Put #

get :: Get FnOpt #

putList :: [FnOpt] -> Put #

NFData FnOpt Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: FnOpt -> () #

type Rep FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

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
Functor ProvideWhat' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Eq t => Eq (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Show t => Show (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep (ProvideWhat' t) :: Type -> Type #

Methods

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

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

Binary t => Binary (ProvideWhat' t) Source # 
Instance details

Defined in Idris.IBC

Methods

put :: ProvideWhat' t -> Put #

get :: Get (ProvideWhat' t) #

putList :: [ProvideWhat' t] -> Put #

NFData t => NFData (ProvideWhat' t) Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: ProvideWhat' t -> () #

type Rep (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show PDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PDecl -> ShowS #

show :: PDecl -> String #

showList :: [PDecl] -> ShowS #

Generic (PDecl' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PDecl' t) Source # 
Instance details

Defined in Idris.IBC

Methods

put :: PDecl' t -> Put #

get :: Get (PDecl' t) #

putList :: [PDecl' t] -> Put #

NFData t => NFData (PDecl' t) Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PDecl' t -> () #

type Rep (PDecl' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data Directive Source #

The set of source directives

Instances
Generic Directive Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Directive :: Type -> Type #

Binary Directive Source # 
Instance details

Defined in Idris.IBC

NFData Directive Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Directive -> () #

type Rep Directive Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Directive = D1 (MetaData "Directive" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((((C1 (MetaCons "DLib" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "DLink" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "DFlag" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "DInclude" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Codegen) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "DHide" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))))) :+: ((C1 (MetaCons "DFreeze" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "DThaw" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :+: (C1 (MetaCons "DInjective" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: (C1 (MetaCons "DSetTotal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "DAccess" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Accessibility)))))) :+: (((C1 (MetaCons "DDefault" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DefaultTotality)) :+: C1 (MetaCons "DLogging" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer))) :+: (C1 (MetaCons "DDynamicLibs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String])) :+: (C1 (MetaCons "DNameHint" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, FC)]))) :+: C1 (MetaCons "DErrorHandlers" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, FC)]))))))) :+: ((C1 (MetaCons "DLanguage" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 LanguageExt)) :+: C1 (MetaCons "DDeprecate" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "DFragile" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "DAutoImplicits" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: C1 (MetaCons "DUsed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show PClause Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic (PClause' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PClause' t) Source # 
Instance details

Defined in Idris.IBC

Methods

put :: PClause' t -> Put #

get :: Get (PClause' t) #

putList :: [PClause' t] -> Put #

NFData t => NFData (PClause' t) Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PClause' t -> () #

type Rep (PClause' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PClause' t) = D1 (MetaData "PClause'" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "PClause" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [t]) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PDecl' t])))) :+: C1 (MetaCons "PWith" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :*: ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [t]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Name, FC))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PDecl' t]))))) :+: (C1 (MetaCons "PClauseR" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [t])) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PDecl' t]))) :+: C1 (MetaCons "PWithR" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [t])) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Name, FC))) :*: S1 (MetaSel (Nothing :: Maybe 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show PData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PData -> ShowS #

show :: PData -> String #

showList :: [PData] -> ShowS #

Generic (PData' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PData' t) Source # 
Instance details

Defined in Idris.IBC

Methods

put :: PData' t -> Put #

get :: Get (PData' t) #

putList :: [PData' t] -> Put #

NFData t => NFData (PData' t) Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PData' t -> () #

type Rep (PData' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Show PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PunInfo :: Type -> Type #

Methods

from :: PunInfo -> Rep PunInfo x #

to :: Rep PunInfo x -> PunInfo #

Binary PunInfo Source # 
Instance details

Defined in Idris.IBC

Methods

put :: PunInfo -> Put #

get :: Get PunInfo #

putList :: [PunInfo] -> Put #

NFData PunInfo Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PunInfo -> () #

type Rep PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep PunInfo = D1 (MetaData "PunInfo" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "IsType" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "IsTerm" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TypeOrTerm" PrefixI False) (U1 :: Type -> Type)))

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PTerm -> ShowS #

show :: PTerm -> String #

showList :: [PTerm] -> ShowS #

Show PClause Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Show PData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PData -> ShowS #

show :: PData -> String #

showList :: [PData] -> ShowS #

Show PDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PDecl -> ShowS #

show :: PDecl -> String #

showList :: [PDecl] -> ShowS #

Generic PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PTerm :: Type -> Type #

Methods

from :: PTerm -> Rep PTerm x #

to :: Rep PTerm x -> PTerm #

Binary PTerm Source # 
Instance details

Defined in Idris.IBC

Methods

put :: PTerm -> Put #

get :: Get PTerm #

putList :: [PTerm] -> Put #

NFData PTerm Source # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PTerm -> () #

type Rep PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep PTerm = D1 (MetaData "PTerm" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((((C1 (MetaCons "PQuote" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Raw)) :+: C1 (MetaCons "PRef" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [FC]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)))) :+: (C1 (MetaCons "PInferRef" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [FC]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :+: (C1 (MetaCons "PPatvar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "PLam" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))))))) :+: ((C1 (MetaCons "PPi" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Plicity) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: (C1 (MetaCons "PLet" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 RigCount) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :*: ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: C1 (MetaCons "PTyped" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: (C1 (MetaCons "PApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PArg]))) :+: (C1 (MetaCons "PWithApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))) :+: C1 (MetaCons "PAppImpl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [ImplicitInfo])))))) :+: (((C1 (MetaCons "PAppBind" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PArg]))) :+: C1 (MetaCons "PMatchApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) :+: (C1 (MetaCons "PIfThenElse" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))) :+: (C1 (MetaCons "PCase" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(PTerm, PTerm)]))) :+: C1 (MetaCons "PTrue" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PunInfo))))) :+: ((C1 (MetaCons "PResolveTC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC)) :+: (C1 (MetaCons "PRewrite" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe PTerm))))) :+: C1 (MetaCons "PPair" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [FC])) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PunInfo) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))))) :+: (C1 (MetaCons "PDPair" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [FC]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PunInfo))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: (C1 (MetaCons "PAs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))) :+: C1 (MetaCons "PAlternative" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, Name)]) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PAltType) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PTerm])))))))) :+: ((((C1 (MetaCons "PHidden" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :+: C1 (MetaCons "PType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC))) :+: (C1 (MetaCons "PUniverse" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Universe)) :+: (C1 (MetaCons "PGoal" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))) :+: C1 (MetaCons "PConstant" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Const))))) :+: ((C1 (MetaCons "Placeholder" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "PDoBlock" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol