idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.AbsSyntaxTree

Description

 
Synopsis

Documentation

data ElabWhat Source #

Constructors

ETypes 
EDefns 
EAll 

Instances

Instances details
Show ElabWhat Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> ElabWhat -> ShowS

show :: ElabWhat -> String

showList :: [ElabWhat] -> ShowS

Eq ElabWhat Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

(==) :: ElabWhat -> ElabWhat -> Bool

(/=) :: ElabWhat -> ElabWhat -> Bool

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

Instances details
Generic IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IOption :: Type -> Type

Methods

from :: IOption -> Rep IOption x

to :: Rep IOption x -> IOption

Show IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> IOption -> ShowS

show :: IOption -> String

showList :: [IOption] -> ShowS

NFData IOption 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: IOption -> ()

Eq IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

type Rep IOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep IOption = D1 ('MetaData "IOption" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Show PPOption Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PPOption -> ShowS

show :: PPOption -> String

showList :: [PPOption] -> ShowS

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

Instances details
Show OutputMode Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> OutputMode -> ShowS

show :: OutputMode -> String

showList :: [OutputMode] -> ShowS

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

Instances details
Generic DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep DefaultTotality :: Type -> Type

Show DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> DefaultTotality -> ShowS

show :: DefaultTotality -> String

showList :: [DefaultTotality] -> ShowS

Binary DefaultTotality 
Instance details

Defined in Idris.IBC

Methods

put :: DefaultTotality -> Put

get :: Get DefaultTotality

putList :: [DefaultTotality] -> Put

NFData DefaultTotality 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DefaultTotality -> ()

Eq DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep DefaultTotality Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data InteractiveOpts Source #

Configuration options for interactive editing.

Instances

Instances details
Generic InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep InteractiveOpts :: Type -> Type

Show InteractiveOpts Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> InteractiveOpts -> ShowS

show :: InteractiveOpts -> String

showList :: [InteractiveOpts] -> ShowS

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic IState Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IState :: Type -> Type

Methods

from :: IState -> Rep IState x

to :: Rep IState x -> IState

Show IState Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> IState -> ShowS

show :: IState -> String

showList :: [IState] -> ShowS

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SizeChange :: Type -> Type

Methods

from :: SizeChange -> Rep SizeChange x

to :: Rep SizeChange x -> SizeChange

Show SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> SizeChange -> ShowS

show :: SizeChange -> String

showList :: [SizeChange] -> ShowS

Binary SizeChange 
Instance details

Defined in Idris.IBC

Methods

put :: SizeChange -> Put

get :: Get SizeChange

putList :: [SizeChange] -> Put

NFData SizeChange 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: SizeChange -> ()

Eq SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

(==) :: SizeChange -> SizeChange -> Bool

(/=) :: SizeChange -> SizeChange -> Bool

type Rep SizeChange Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

type SCGEntry = (Name, [Maybe (Int, SizeChange)]) Source #

type UsageReason = (Name, Int) Source #

data CGInfo Source #

Constructors

CGInfo 

Fields

Instances

Instances details
Generic CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep CGInfo :: Type -> Type

Methods

from :: CGInfo -> Rep CGInfo x

to :: Rep CGInfo x -> CGInfo

Show CGInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> CGInfo -> ShowS

show :: CGInfo -> String

showList :: [CGInfo] -> ShowS

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

type Rep CGInfo = D1 ('MetaData "CGInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "CGInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "calls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Just "allCalls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Name]))) :*: (S1 ('MetaSel ('Just "scg") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SCGEntry]) :*: S1 ('MetaSel ('Just "usedpos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, [UsageReason])]))))

data IBCWrite Source #

Instances

Instances details
Generic IBCWrite Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep IBCWrite :: Type -> Type

Methods

from :: IBCWrite -> Rep IBCWrite x

to :: Rep IBCWrite x -> IBCWrite

Show IBCWrite Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> IBCWrite -> ShowS

show :: IBCWrite -> String

showList :: [IBCWrite] -> ShowS

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

idrisInit :: IState Source #

The initial state for the compiler

type Idris = StateT IState (ExceptT Err IO) Source #

The monad for the main REPL - reading and processing files and updating global state (hence the IO inner monad).

    type Idris = WriterT [Either String (IO ())] (State IState a))

catchError :: Idris a -> (Err -> Idris a) -> Idris a Source #

data ElabShellCmd Source #

Instances

Instances details
Show ElabShellCmd Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> ElabShellCmd -> ShowS

show :: ElabShellCmd -> String

showList :: [ElabShellCmd] -> ShowS

Eq ElabShellCmd Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

(==) :: ElabShellCmd -> ElabShellCmd -> Bool

(/=) :: ElabShellCmd -> ElabShellCmd -> Bool

data Fixity Source #

Constructors

Infixl 

Fields

Infixr 

Fields

InfixN 

Fields

PrefixN 

Fields

Instances

Instances details
Generic Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Fixity :: Type -> Type

Methods

from :: Fixity -> Rep Fixity x

to :: Rep Fixity x -> Fixity

Show Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

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

Eq Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

type Rep Fixity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Fixity = D1 ('MetaData "Fixity" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Infixl" 'PrefixI 'True) (S1 ('MetaSel ('Just "prec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Infixr" 'PrefixI 'True) (S1 ('MetaSel ('Just "prec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "InfixN" 'PrefixI 'True) (S1 ('MetaSel ('Just "prec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "PrefixN" 'PrefixI 'True) (S1 ('MetaSel ('Just "prec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

data FixDecl Source #

Constructors

Fix Fixity String 

Instances

Instances details
Generic FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FixDecl :: Type -> Type

Methods

from :: FixDecl -> Rep FixDecl x

to :: Rep FixDecl x -> FixDecl

Show FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> FixDecl -> ShowS

show :: FixDecl -> String

showList :: [FixDecl] -> ShowS

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

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

Methods

compare :: FixDecl -> FixDecl -> Ordering

(<) :: FixDecl -> FixDecl -> Bool

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

(>) :: FixDecl -> FixDecl -> Bool

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

max :: FixDecl -> FixDecl -> FixDecl

min :: FixDecl -> FixDecl -> FixDecl

type Rep FixDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep FixDecl = D1 ('MetaData "FixDecl" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Fix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

data Static Source #

Mark bindings with their explicitness, and laziness

Constructors

Static 
Dynamic 

Instances

Instances details
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 :: forall r r'. (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

Generic Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Static :: Type -> Type

Methods

from :: Static -> Rep Static x

to :: Rep Static x -> Static

Show Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Static -> ShowS

show :: Static -> String

showList :: [Static] -> ShowS

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

Eq Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Ord Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

compare :: Static -> Static -> Ordering

(<) :: Static -> Static -> Bool

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

(>) :: Static -> Static -> Bool

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

max :: Static -> Static -> Static

min :: Static -> Static -> Static

type Rep Static Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data Plicity Source #

Constructors

Imp 

Fields

Exp 

Fields

Constraint 
TacImp 

Instances

Instances details
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 :: forall r r'. (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

Generic Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Plicity :: Type -> Type

Methods

from :: Plicity -> Rep Plicity x

to :: Rep Plicity x -> Plicity

Show Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Plicity -> ShowS

show :: Plicity -> String

showList :: [Plicity] -> ShowS

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

Eq Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Ord Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

compare :: Plicity -> Plicity -> Ordering

(<) :: Plicity -> Plicity -> Bool

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

(>) :: Plicity -> Plicity -> Bool

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

max :: Plicity -> Plicity -> Plicity

min :: Plicity -> Plicity -> Plicity

type Rep Plicity Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Plicity = D1 ('MetaData "Plicity" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FnOpt :: Type -> Type

Methods

from :: FnOpt -> Rep FnOpt x

to :: Rep FnOpt x -> FnOpt

Show FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> FnOpt -> ShowS

show :: FnOpt -> String

showList :: [FnOpt] -> ShowS

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

Eq FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

type Rep FnOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

type FnOpts = [FnOpt] Source #

data ProvideWhat' t Source #

Type provider - what to provide

Constructors

ProvTerm t t

the first is the goal type, the second is the term

ProvPostulate t

goal type must be Type, so only term

Instances

Instances details
Functor ProvideWhat' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Generic (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

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

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> ProvideWhat' t -> ShowS

show :: ProvideWhat' t -> String

showList :: [ProvideWhat' t] -> ShowS

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

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

Defined in Idris.AbsSyntaxTree

Methods

(==) :: ProvideWhat' t -> ProvideWhat' t -> Bool

(/=) :: ProvideWhat' t -> ProvideWhat' t -> Bool

type Rep (ProvideWhat' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (ProvideWhat' t) = D1 ('MetaData "ProvideWhat'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "ProvTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "ProvPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

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

Instances details
Functor PDecl' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show PDecl Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PDecl -> ShowS

show :: PDecl -> String

showList :: [PDecl] -> ShowS

Generic (PDecl' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PDecl' t) 
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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic Directive Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Directive :: Type -> Type

Methods

from :: Directive -> Rep Directive x

to :: Rep Directive x -> Directive

Binary Directive 
Instance details

Defined in Idris.IBC

Methods

put :: Directive -> Put

get :: Get Directive

putList :: [Directive] -> Put

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
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

Methods

showsPrec :: Int -> PClause -> ShowS

show :: PClause -> String

showList :: [PClause] -> ShowS

Generic (PClause' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PClause' t) 
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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Functor PData' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Show PData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PData -> ShowS

show :: PData -> String

showList :: [PData] -> ShowS

Generic (PData' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

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

Methods

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

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

Binary t => Binary (PData' t) 
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

type Rep (PData' t) = D1 ('MetaData "PData'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "PDatadecl" 'PrefixI 'True) ((S1 ('MetaSel ('Just "d_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "d_name_fc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC)) :*: (S1 ('MetaSel ('Just "d_tcon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Just "d_cons") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]))) :+: C1 ('MetaCons "PLaterdecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "d_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Just "d_name_fc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC) :*: S1 ('MetaSel ('Just "d_tcon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))))

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

Instances details
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 :: forall r r'. (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

Generic PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PunInfo :: Type -> Type

Methods

from :: PunInfo -> Rep PunInfo x

to :: Rep PunInfo x -> PunInfo

Show PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PunInfo -> ShowS

show :: PunInfo -> String

showList :: [PunInfo] -> ShowS

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

Eq PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Ord PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

compare :: PunInfo -> PunInfo -> Ordering

(<) :: PunInfo -> PunInfo -> Bool

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

(>) :: PunInfo -> PunInfo -> Bool

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

max :: PunInfo -> PunInfo -> PunInfo

min :: PunInfo -> PunInfo -> PunInfo

type Rep PunInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

data PTerm Source #

High level language terms

Constructors

PQuote Raw

Inclusion of a core term into the high-level language

PRef FC [FC] Name

A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.

PInferRef FC [FC] Name

A name to be defined later

PPatvar FC Name

A pattern variable

PLam FC Name FC PTerm PTerm

A lambda abstraction. Second FC is name span.

PPi Plicity Name FC PTerm PTerm

(n : t1) -> t2, where the FC is for the precise location of the variable

PLet FC RigCount Name FC PTerm PTerm PTerm

A let binding (second FC is precise name location)

PTyped PTerm PTerm

Term with explicit type

PApp FC PTerm [PArg]

e.g. IO (), List Char, length x

PWithApp FC PTerm PTerm

Application plus a with argument

PAppImpl PTerm [ImplicitInfo]

Implicit argument application (introduced during elaboration only)

PAppBind FC PTerm [PArg]

implicitly bound application

PMatchApp FC Name

Make an application by type matching

PIfThenElse FC PTerm PTerm PTerm

Conditional expressions - elaborated to an overloading of ifThenElse

PCase FC PTerm [(PTerm, PTerm)]

A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

PTrue FC PunInfo

Unit type..?

PResolveTC FC

Solve this dictionary by interface resolution

PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

"rewrite" syntax, with optional rewriting function and optional result type

PPair FC [FC] PunInfo PTerm PTerm

A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

PDPair FC [FC] PunInfo PTerm PTerm PTerm

A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

PAs FC Name PTerm

@-pattern, valid LHS only

PAlternative [(Name, Name)] PAltType [PTerm]

(| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

PHidden PTerm

Irrelevant or hidden pattern

PType FC

Type type

PUniverse FC Universe

Some universe

PGoal FC PTerm Name PTerm

quoteGoal, used for %reflection functions

PConstant FC Const

Builtin types

Placeholder

Underscore

PDoBlock [PDo]

Do notation

PIdiom FC PTerm

Idiom brackets

PMetavar FC Name

A metavariable, ?name, and its precise location

PProof [PTactic]

Proof script

PTactics [PTactic]

As PProof, but no auto solving

PElabError Err

Error to report on elaboration

PImpossible

Special case for declaring when an LHS can't typecheck

PCoerced PTerm

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

PDisamb [[Text]] PTerm

Preferences for explicit namespaces

PUnifyLog PTerm

dump a trace of unifications when building term

PNoImplicits PTerm

never run implicit converions on the term

PQuasiquote PTerm (Maybe PTerm)

`(Term [: Term])

PUnquote PTerm

~Term

PQuoteName Name Bool FC

`{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.

PRunElab FC PTerm [String]

%runElab tm - New-style proof script. Args are location, script, enclosing namespace.

PConstSugar FC PTerm

A desugared constant. The FC is a precise source location that will be used to highlight it later.

Instances

Instances details
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 :: forall r r'. (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

Generic PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PTerm :: Type -> Type

Methods

from :: PTerm -> Rep PTerm x

to :: Rep PTerm x -> PTerm

Show PClause Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PClause -> ShowS

show :: PClause -> String

showList :: [PClause] -> ShowS

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

Show PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> PTerm -> ShowS

show :: PTerm -> String

showList :: [PTerm] -> ShowS

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

Eq PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

type Rep PTerm Source # 
Instance details

Defined in Idris.AbsSyntaxTree

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

Instances details
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 :: forall r r'. (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

Generic PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep PAltType :: Type -> Type

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

Eq PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

(==) :: PAltType -> PAltType -> Bool

(/=) :: PAltType -> PAltType -> Bool

Ord PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

compare :: PAltType -> PAltType -> Ordering

(<) :: PAltType -> PAltType -> Bool

(<=) :: PAltType -> PAltType -> Bool

(>) :: PAltType -> PAltType -> Bool

(>=) :: PAltType -> PAltType -> Bool

max :: PAltType -> PAltType -> PAltType

min :: PAltType -> PAltType -> PAltType

type Rep PAltType Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep PAltType = D1 ('MetaData "PAltType" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "ExactlyOne" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: (C1 ('MetaCons "FirstSuccess" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TryImplicit" 'PrefixI 'False) (U1 :: Type -> Type)))

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 #

Constructors

Intro [Name] 
Intros 
Focus Name 
Refine Name [Bool] 
Rewrite t 
DoUnify 
Equiv t 
Claim Name t 
Unfocus 
MatchRefine Name 
LetTac Name t 
LetTacTy Name t t 
Exact t 
Compute 
Trivial 
TCImplementation 
ProofSearch Bool Bool Int (Maybe Name) [Name] [Name]

the bool is whether to search recursively

Solve 
Attack 
ProofState 
ProofTerm 
Undo 
Try (PTactic' t) (PTactic' t) 
TSeq (PTactic' t) (PTactic' t) 
ApplyTactic t 
ByReflection t 
Reflect t 
Fill t 
GoalType String (PTactic' t) 
TCheck t 
TEval t 
TDocStr (Either Name Const) 
TSearch t 
Skip 
TFail [ErrorReportPart] 
Qed 
Abandon 
SourceFC 

Instances

Instances details
Foldable PTactic' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

foldMap :: Monoid m => (a -> m) -> PTactic' a -> 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)

Functor PTactic' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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 :: forall r r'. (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)

Generic (PTactic' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep (PTactic' t) :: Type -> Type

Methods

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

to :: Rep (PTactic' t) x -> 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

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

type Rep (PTactic' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PTactic' t) = D1 ('MetaData "PTactic'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((((C1 ('MetaCons "Intro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "Intros" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (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 :: Type -> Type)) :+: (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 :: Type -> Type))))) :+: (((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 :: Type -> Type)))) :+: ((C1 ('MetaCons "Trivial" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCImplementation" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (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 :: Type -> Type) :+: C1 ('MetaCons "Attack" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "ProofState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProofTerm" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Undo" 'PrefixI 'False) (U1 :: Type -> Type) :+: 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 :: Type -> Type) :+: C1 ('MetaCons "TFail" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ErrorReportPart]))) :+: (C1 ('MetaCons "Qed" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Abandon" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SourceFC" 'PrefixI 'False) (U1 :: Type -> Type)))))))

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

Instances details
Functor PDo' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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 :: forall r r'. (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)

Generic (PDo' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep (PDo' t) :: Type -> Type

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

type Rep (PDo' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PDo' t) = D1 ('MetaData "PDo'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Functor PArg' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

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 :: forall r r'. (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)

Generic (PArg' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep (PArg' t) :: Type -> Type

Methods

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

to :: Rep (PArg' t) x -> 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

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

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

Defined in Idris.AbsSyntaxTree

Methods

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

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

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

type Rep (PArg' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep (PArg' t) = D1 ('MetaData "PArg'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
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 :: forall r r'. (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

Generic ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep ArgOpt :: Type -> Type

Methods

from :: ArgOpt -> Rep ArgOpt x

to :: Rep ArgOpt x -> ArgOpt

Show ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> ArgOpt -> ShowS

show :: ArgOpt -> String

showList :: [ArgOpt] -> ShowS

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

Eq ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Ord ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

compare :: ArgOpt -> ArgOpt -> Ordering

(<) :: ArgOpt -> ArgOpt -> Bool

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

(>) :: ArgOpt -> ArgOpt -> Bool

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

max :: ArgOpt -> ArgOpt -> ArgOpt

min :: ArgOpt -> ArgOpt -> ArgOpt

type Rep ArgOpt Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep ArgOpt = D1 ('MetaData "ArgOpt" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "AlwaysShow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HideDisplay" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InaccessibleArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownImp" 'PrefixI 'False) (U1 :: Type -> Type)))

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

Instances details
Generic InterfaceInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep InterfaceInfo :: Type -> Type

Show InterfaceInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> InterfaceInfo -> ShowS

show :: InterfaceInfo -> String

showList :: [InterfaceInfo] -> ShowS

Binary InterfaceInfo 
Instance details

Defined in Idris.IBC

Methods

put :: InterfaceInfo -> Put

get :: Get InterfaceInfo

putList :: [InterfaceInfo] -> Put

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic RecordInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep RecordInfo :: Type -> Type

Methods

from :: RecordInfo -> Rep RecordInfo x

to :: Rep RecordInfo x -> RecordInfo

Show RecordInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> RecordInfo -> ShowS

show :: RecordInfo -> String

showList :: [RecordInfo] -> ShowS

Binary RecordInfo 
Instance details

Defined in Idris.IBC

Methods

put :: RecordInfo -> Put

get :: Get RecordInfo

putList :: [RecordInfo] -> Put

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Generic TIData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep TIData :: Type -> Type

Methods

from :: TIData -> Rep TIData x

to :: Rep TIData x -> TIData

Show TIData Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> TIData -> ShowS

show :: TIData -> String

showList :: [TIData] -> ShowS

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.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "TIPartial" 'PrefixI 'False) (U1 :: Type -> Type) :+: 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

Instances details
Generic FnInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep FnInfo :: Type -> Type

Methods

from :: FnInfo -> Rep FnInfo x

to :: Rep FnInfo x -> FnInfo

Show FnInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> FnInfo -> ShowS

show :: FnInfo -> String

showList :: [FnInfo] -> ShowS

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.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "FnInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "fn_params") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

data OptInfo Source #

Constructors

Optimise 

Fields

Instances

Instances details
Generic OptInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep OptInfo :: Type -> Type

Methods

from :: OptInfo -> Rep OptInfo x

to :: Rep OptInfo x -> OptInfo

Show OptInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> OptInfo -> ShowS

show :: OptInfo -> String

showList :: [OptInfo] -> ShowS

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Functor DSL' Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

Generic (DSL' t) Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep (DSL' t) :: Type -> Type

Methods

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

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

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

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

type Rep (DSL' t) = D1 ('MetaData "DSL'" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "DSL" 'PrefixI 'True) (((S1 ('MetaSel ('Just "dsl_bind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Just "dsl_apply") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :*: (S1 ('MetaSel ('Just "dsl_pure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Just "dsl_var") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)))) :*: ((S1 ('MetaSel ('Just "index_first") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)) :*: S1 ('MetaSel ('Just "index_next") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t))) :*: (S1 ('MetaSel ('Just "dsl_lambda") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)) :*: (S1 ('MetaSel ('Just "dsl_let") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)) :*: S1 ('MetaSel ('Just "dsl_pi") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)))))))

data SynContext Source #

Instances

Instances details
Generic SynContext Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SynContext :: Type -> Type

Methods

from :: SynContext -> Rep SynContext x

to :: Rep SynContext x -> SynContext

Show SynContext Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> SynContext -> ShowS

show :: SynContext -> String

showList :: [SynContext] -> ShowS

Binary SynContext 
Instance details

Defined in Idris.IBC

Methods

put :: SynContext -> Put

get :: Get SynContext

putList :: [SynContext] -> Put

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.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "PatternSyntax" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TermSyntax" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AnySyntax" 'PrefixI 'False) (U1 :: Type -> Type)))

data Syntax Source #

Instances

Instances details
Generic Syntax Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Syntax :: Type -> Type

Methods

from :: Syntax -> Rep Syntax x

to :: Rep Syntax x -> Syntax

Show Syntax Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Syntax -> ShowS

show :: Syntax -> String

showList :: [Syntax] -> ShowS

Binary Syntax 
Instance details

Defined in Idris.IBC

Methods

put :: Syntax -> Put

get :: Get Syntax

putList :: [Syntax] -> Put

NFData Syntax 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Syntax -> ()

type Rep Syntax Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Syntax = D1 ('MetaData "Syntax" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Rule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SSymbol]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PTerm) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SynContext))) :+: C1 ('MetaCons "DeclRule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SSymbol]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PDecl])))

data SSymbol Source #

Instances

Instances details
Generic SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SSymbol :: Type -> Type

Methods

from :: SSymbol -> Rep SSymbol x

to :: Rep SSymbol x -> SSymbol

Show SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> SSymbol -> ShowS

show :: SSymbol -> String

showList :: [SSymbol] -> ShowS

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

Eq SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

type Rep SSymbol Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep SSymbol = D1 ('MetaData "SSymbol" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Keyword" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "Symbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "Binding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Expr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "SimpleExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))

newtype SyntaxRules Source #

Constructors

SyntaxRules 

Fields

Instances

Instances details
Generic SyntaxRules Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SyntaxRules :: Type -> Type

Methods

from :: SyntaxRules -> Rep SyntaxRules x

to :: Rep SyntaxRules x -> 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.4-3WzTclJnDGuF9nqMis99Gw" 'True) (C1 ('MetaCons "SyntaxRules" 'PrefixI 'True) (S1 ('MetaSel ('Just "syntaxRulesList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Syntax])))

data Using Source #

Instances

Instances details
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 :: forall r r'. (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

Generic Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep Using :: Type -> Type

Methods

from :: Using -> Rep Using x

to :: Rep Using x -> Using

Show Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> Using -> ShowS

show :: Using -> String

showList :: [Using] -> ShowS

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

Eq Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

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

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

type Rep Using Source # 
Instance details

Defined in Idris.AbsSyntaxTree

type Rep Using = D1 ('MetaData "Using" "Idris.AbsSyntaxTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "UImplicit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PTerm)) :+: C1 ('MetaCons "UConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

data SyntaxInfo Source #

Constructors

Syn 

Fields

Instances

Instances details
Generic SyntaxInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Associated Types

type Rep SyntaxInfo :: Type -> Type

Methods

from :: SyntaxInfo -> Rep SyntaxInfo x

to :: Rep SyntaxInfo x -> SyntaxInfo

Show SyntaxInfo Source # 
Instance details

Defined in Idris.AbsSyntaxTree

Methods

showsPrec :: Int -> SyntaxInfo -> ShowS

show :: SyntaxInfo -> String

showList :: [SyntaxInfo] -> ShowS

Binary SyntaxInfo 
Instance details

Defined in Idris.IBC

Methods

put :: SyntaxInfo -> Put

get :: Get SyntaxInfo

putList :: [SyntaxInfo] -> Put

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.4-3WzTclJnDGuF9nqMis99Gw" '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))))))

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

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

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 #