idris-1.3.1: 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 :: * -> * #

Methods

from :: IOption -> Rep IOption x #

to :: Rep IOption x -> IOption #

NFData IOption # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 # 
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 :: * -> * #

Binary DefaultTotality # 
Instance details

Defined in Idris.IBC

NFData DefaultTotality # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep InteractiveOpts :: * -> * #

NFData InteractiveOpts # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> * #

Methods

from :: IState -> Rep IState x #

to :: Rep IState x -> IState #

NFData IState # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> * #

Binary SizeChange # 
Instance details

Defined in Idris.IBC

NFData SizeChange # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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
Show CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep CGInfo :: * -> * #

Methods

from :: CGInfo -> Rep CGInfo x #

to :: Rep CGInfo x -> CGInfo #

Binary CGInfo # 
Instance details

Defined in Idris.IBC

Methods

put :: CGInfo -> Put #

get :: Get CGInfo #

putList :: [CGInfo] -> Put #

NFData CGInfo # 
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 :: * -> * #

Methods

from :: IBCWrite -> Rep IBCWrite x #

to :: Rep IBCWrite x -> IBCWrite #

NFData IBCWrite # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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))))))))

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

Methods

from :: Fixity -> Rep Fixity x #

to :: Rep Fixity x -> Fixity #

Binary Fixity # 
Instance details

Defined in Idris.IBC

Methods

put :: Fixity -> Put #

get :: Get Fixity #

putList :: [Fixity] -> Put #

NFData Fixity # 
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 :: * -> * #

Methods

from :: FixDecl -> Rep FixDecl x #

to :: Rep FixDecl x -> FixDecl #

Binary FixDecl # 
Instance details

Defined in Idris.IBC

Methods

put :: FixDecl -> Put #

get :: Get FixDecl #

putList :: [FixDecl] -> Put #

NFData FixDecl # 
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 :: * -> * #

Methods

from :: Static -> Rep Static x #

to :: Rep Static x -> Static #

Binary Static # 
Instance details

Defined in Idris.IBC

Methods

put :: Static -> Put #

get :: Get Static #

putList :: [Static] -> Put #

NFData Static # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 # 
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 :: * -> * #

Methods

from :: Plicity -> Rep Plicity x #

to :: Rep Plicity x -> Plicity #

Binary Plicity # 
Instance details

Defined in Idris.IBC

Methods

put :: Plicity -> Put #

get :: Get Plicity #

putList :: [Plicity] -> Put #

NFData Plicity # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> * #

Methods

from :: FnOpt -> Rep FnOpt x #

to :: Rep FnOpt x -> FnOpt #

Binary FnOpt # 
Instance details

Defined in Idris.IBC

Methods

put :: FnOpt -> Put #

get :: Get FnOpt #

putList :: [FnOpt] -> Put #

NFData FnOpt # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: Maybe 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 :: Maybe 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
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) :: * -> * #

Methods

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

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

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

Defined in Idris.IBC

Methods

put :: ProvideWhat' t -> Put #

get :: Get (ProvideWhat' t) #

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

NFData t => NFData (ProvideWhat' t) # 
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) :: * -> * #

Methods

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

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

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

Defined in Idris.IBC

Methods

put :: PDecl' t -> Put #

get :: Get (PDecl' t) #

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

NFData t => NFData (PDecl' t) # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> * #

Binary Directive # 
Instance details

Defined in Idris.IBC

NFData Directive # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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) :: * -> * #

Methods

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

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

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

Defined in Idris.IBC

Methods

put :: PClause' t -> Put #

get :: Get (PClause' t) #

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

NFData t => NFData (PClause' t) # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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) :: * -> * #

Methods

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

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

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

Defined in Idris.IBC

Methods

put :: PData' t -> Put #

get :: Get (PData' t) #

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

NFData t => NFData (PData' t) # 
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 :: * -> * #

Methods

from :: PunInfo -> Rep PunInfo x #

to :: Rep PunInfo x -> PunInfo #

Binary PunInfo # 
Instance details

Defined in Idris.IBC

Methods

put :: PunInfo -> Put #

get :: Get PunInfo #

putList :: [PunInfo] -> Put #

NFData PunInfo # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 # 
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 :: * -> * #

Methods

from :: PTerm -> Rep PTerm x #

to :: Rep PTerm x -> PTerm #

Binary PTerm # 
Instance details

Defined in Idris.IBC

Methods

put :: PTerm -> Put #

get :: Get PTerm #

putList :: [PTerm] -> Put #

NFData PTerm # 
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.1-HMhXn3ahTlmAYa6dTdYaVB" 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 :: * -> *) :+: (C1 (MetaCons "PDoBlock" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PDo])) :+: C1 (MetaCons "PIdiom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: (C1 (MetaCons "PMetavar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: (C1 (MetaCons "PProof" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PTactic])) :+: C1 (MetaCons "PTactics" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [PTactic])))))) :+: (((C1 (MetaCons "PElabError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Err)) :+: C1 (MetaCons "PImpossible" PrefixI False) (U1 :: * -> *)) :+: (C1 (MetaCons "PCoerced" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :+: (C1 (MetaCons "PDisamb" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Text]]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :+: C1 (MetaCons "PUnifyLog" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))))) :+: ((C1 (MetaCons "PNoImplicits" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)) :+: (C1 (MetaCons "PQuasiquote" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe PTerm))) :+: C1 (MetaCons "PUnquote" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm)))) :+: (C1 (MetaCons "PQuoteName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC))) :+: (C1 (MetaCons "PRunElab" 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 [String]))) :+: C1 (MetaCons "PConstSugar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PTerm))))))))

data PAltType Source #

Constructors

ExactlyOne Bool

flag sets whether delay is allowed

FirstSuccess 
TryImplicit 
Instances
Eq PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Data PAltType 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) -> 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PAltType :: * -> * #

Methods

from :: PAltType -> Rep PAltType x #

to :: Rep PAltType x -> PAltType #

Binary PAltType # 
Instance details

Defined in Idris.IBC

Methods

put :: PAltType -> Put #

get :: Get PAltType #

putList :: [PAltType] -> Put #

NFData PAltType # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PAltType -> () #

type Rep PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep PAltType = D1 (MetaData "PAltType" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "ExactlyOne" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Foldable PTactic' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

Defined in Idris.AbsSyntaxTree

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data t => Data (PTactic' t) 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) -> 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 t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PTactic' t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

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

Defined in Idris.AbsSyntaxTree

Methods

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

show :: PTactic' t -> String #

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

Generic (PTactic' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PTactic' t) # 
Instance details

Defined in Idris.IBC

Methods

put :: PTactic' t -> Put #

get :: Get (PTactic' t) #

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

NFData t => NFData (PTactic' t) # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PTactic' t -> () #

type Rep (PTactic' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PTactic' t) = D1 (MetaData "PTactic'" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (((((C1 (MetaCons "Intro" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name])) :+: C1 (MetaCons "Intros" PrefixI False) (U1 :: * -> *)) :+: (C1 (MetaCons "Focus" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "Refine" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Bool])))) :+: ((C1 (MetaCons "Rewrite" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "DoUnify" PrefixI False) (U1 :: * -> *)) :+: (C1 (MetaCons "Equiv" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "Claim" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "Unfocus" PrefixI False) (U1 :: * -> *))))) :+: (((C1 (MetaCons "MatchRefine" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "LetTac" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :+: (C1 (MetaCons "LetTacTy" PrefixI False) (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))) :+: (C1 (MetaCons "Exact" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 :: 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 Int))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]) :*: S1 (MetaSel (Nothing :: Maybe 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 :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (PTactic' t)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (PTactic' t))))) :+: ((C1 (MetaCons "TSeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (PTactic' t)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (PTactic' t))) :+: C1 (MetaCons "ApplyTactic" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :+: (C1 (MetaCons "ByReflection" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "Reflect" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: C1 (MetaCons "Fill" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))))) :+: (((C1 (MetaCons "GoalType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (PTactic' t))) :+: C1 (MetaCons "TCheck" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))) :+: (C1 (MetaCons "TEval" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "TDocStr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either Name Const))) :+: C1 (MetaCons "TSearch" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t))))) :+: ((C1 (MetaCons "Skip" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "TFail" PrefixI False) (S1 (MetaSel (Nothing :: Maybe 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data t => Data (PDo' t) 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) -> 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 t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PDo' t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

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

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PDo' t) # 
Instance details

Defined in Idris.IBC

Methods

put :: PDo' t -> Put #

get :: Get (PDo' t) #

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

NFData t => NFData (PDo' t) # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PDo' t -> () #

type Rep (PDo' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PDo' t) = D1 (MetaData "PDo'" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) ((C1 (MetaCons "DoExp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)) :+: (C1 (MetaCons "DoBind" 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 t))) :+: C1 (MetaCons "DoBindP" 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 [(t, t)]))))) :+: (C1 (MetaCons "DoLet" 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 t) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))) :+: (C1 (MetaCons "DoLetP" 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 [(t, t)]))) :+: C1 (MetaCons "DoRewrite" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))))

data PArg' t Source #

Constructors

PImp 

Fields

PExp 

Fields

PConstraint 

Fields

PTacImplicit 

Fields

Instances
Functor PArg' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data t => Data (PArg' t) 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) -> 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 t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PArg' t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

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

Defined in Idris.AbsSyntaxTree

Methods

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

show :: PArg' t -> String #

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

Generic (PArg' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PArg' t) # 
Instance details

Defined in Idris.IBC

Methods

put :: PArg' t -> Put #

get :: Get (PArg' t) #

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

NFData t => NFData (PArg' t) # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: PArg' t -> () #

type Rep (PArg' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data ArgOpt Source #

Instances
Eq ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data ArgOpt 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) -> 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Show ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep ArgOpt :: * -> * #

Methods

from :: ArgOpt -> Rep ArgOpt x #

to :: Rep ArgOpt x -> ArgOpt #

Binary ArgOpt # 
Instance details

Defined in Idris.IBC

Methods

put :: ArgOpt -> Put #

get :: Get ArgOpt #

putList :: [ArgOpt] -> Put #

NFData ArgOpt # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: ArgOpt -> () #

type Rep ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep ArgOpt = D1 (MetaData "ArgOpt" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic InterfaceInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep InterfaceInfo :: * -> * #

Binary InterfaceInfo # 
Instance details

Defined in Idris.IBC

NFData InterfaceInfo # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: InterfaceInfo -> () #

type Rep InterfaceInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data RecordInfo Source #

Instances
Show RecordInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic RecordInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep RecordInfo :: * -> * #

Binary RecordInfo # 
Instance details

Defined in Idris.IBC

NFData RecordInfo # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: RecordInfo -> () #

type Rep RecordInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep RecordInfo = D1 (MetaData "RecordInfo" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "RI" PrefixI True) (S1 (MetaSel (Just "record_parameters") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Name, PTerm)]) :*: (S1 (MetaSel (Just "record_constructor") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Just "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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic TIData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep TIData :: * -> * #

Methods

from :: TIData -> Rep TIData x #

to :: Rep TIData x -> TIData #

NFData TIData # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: TIData -> () #

type Rep TIData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data FnInfo Source #

Miscellaneous information about functions

Constructors

FnInfo 

Fields

Instances
Show FnInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic FnInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FnInfo :: * -> * #

Methods

from :: FnInfo -> Rep FnInfo x #

to :: Rep FnInfo x -> FnInfo #

Binary FnInfo # 
Instance details

Defined in Idris.IBC

Methods

put :: FnInfo -> Put #

get :: Get FnInfo #

putList :: [FnInfo] -> Put #

NFData FnInfo # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: FnInfo -> () #

type Rep FnInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep FnInfo = D1 (MetaData "FnInfo" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "FnInfo" PrefixI True) (S1 (MetaSel (Just "fn_params") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int])))

data OptInfo Source #

Constructors

Optimise 

Fields

Instances
Show OptInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic OptInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep OptInfo :: * -> * #

Methods

from :: OptInfo -> Rep OptInfo x #

to :: Rep OptInfo x -> OptInfo #

Binary OptInfo # 
Instance details

Defined in Idris.IBC

Methods

put :: OptInfo -> Put #

get :: Get OptInfo #

putList :: [OptInfo] -> Put #

NFData OptInfo # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: OptInfo -> () #

type Rep OptInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data DSL' t Source #

Syntactic sugar info

Constructors

DSL 

Fields

Instances
Functor DSL' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

show :: DSL' t -> String #

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

Generic (DSL' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (DSL' t) # 
Instance details

Defined in Idris.IBC

Methods

put :: DSL' t -> Put #

get :: Get (DSL' t) #

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

NFData t => NFData (DSL' t) # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DSL' t -> () #

type Rep (DSL' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

data SynContext Source #

Instances
Show SynContext Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic SynContext Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SynContext :: * -> * #

Binary SynContext # 
Instance details

Defined in Idris.IBC

NFData SynContext # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SynContext -> () #

type Rep SynContext Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep SynContext = D1 (MetaData "SynContext" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" False) (C1 (MetaCons "PatternSyntax" PrefixI False) (U1 :: * -> *) :+: (C1 (MetaCons "TermSyntax" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "AnySyntax" PrefixI False) (U1 :: * -> *)))

data SSymbol Source #

Instances
Eq SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SSymbol :: * -> * #

Methods

from :: SSymbol -> Rep SSymbol x #

to :: Rep SSymbol x -> SSymbol #

Binary SSymbol # 
Instance details

Defined in Idris.IBC

Methods

put :: SSymbol -> Put #

get :: Get SSymbol #

putList :: [SSymbol] -> Put #

NFData SSymbol # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SSymbol -> () #

type Rep SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

newtype SyntaxRules Source #

Constructors

SyntaxRules 

Fields

Instances
Generic SyntaxRules Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SyntaxRules :: * -> * #

NFData SyntaxRules # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SyntaxRules -> () #

type Rep SyntaxRules Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep SyntaxRules = D1 (MetaData "SyntaxRules" "Idris.AbsSyntaxTree" "idris-1.3.1-HMhXn3ahTlmAYa6dTdYaVB" True) (C1 (MetaCons "SyntaxRules" PrefixI True) (S1 (MetaSel (Just "syntaxRulesList") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Syntax])))

data Using Source #

Instances
Eq Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Data Using 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) -> 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 # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Using -> ShowS #

show :: Using -> String #

showList :: [Using] -> ShowS #

Generic Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Using :: * -> * #

Methods

from :: Using -> Rep Using x #

to :: Rep Using x -> Using #

Binary Using # 
Instance details

Defined in Idris.IBC

Methods

put :: Using -> Put #

get :: Get Using #

putList :: [Using] -> Put #

NFData Using # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Using -> () #

type Rep Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

data SyntaxInfo Source #

Constructors

Syn 

Fields

Instances
Show SyntaxInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Generic SyntaxInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SyntaxInfo :: * -> * #

Binary SyntaxInfo # 
Instance details

Defined in Idris.IBC

NFData SyntaxInfo # 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SyntaxInfo -> () #

type Rep SyntaxInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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