License | BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Idris.AbsSyntaxTree
Description
Synopsis
- data ElabWhat
- data ElabInfo = EInfo {}
- toplevel :: ElabInfo
- toplevelWith :: String -> ElabInfo
- eInfoNames :: ElabInfo -> [Name]
- data IOption = IOption {
- opt_logLevel :: Int
- opt_logcats :: [LogCat]
- opt_typecase :: Bool
- opt_typeintype :: Bool
- opt_coverage :: Bool
- opt_showimp :: Bool
- opt_errContext :: Bool
- opt_repl :: Bool
- opt_verbose :: Int
- opt_nobanner :: Bool
- opt_quiet :: Bool
- opt_codegen :: Codegen
- opt_outputTy :: OutputType
- opt_ibcsubdir :: FilePath
- opt_importdirs :: [FilePath]
- opt_sourcedirs :: [FilePath]
- opt_triple :: String
- opt_cpu :: String
- opt_cmdline :: [Opt]
- opt_origerr :: Bool
- opt_autoSolve :: Bool
- opt_autoImport :: [FilePath]
- opt_optimise :: [Optimisation]
- opt_printdepth :: Maybe Int
- opt_evaltypes :: Bool
- opt_desugarnats :: Bool
- opt_autoimpls :: Bool
- defaultOpts :: IOption
- data PPOption = PPOption {
- ppopt_impl :: Bool
- ppopt_desugarnats :: Bool
- ppopt_pinames :: Bool
- ppopt_depth :: Maybe Int
- ppopt_displayrig :: Bool
- defaultOptimise :: [Optimisation]
- defaultPPOption :: PPOption
- verbosePPOption :: PPOption
- ppOption :: IOption -> PPOption
- ppOptionIst :: IState -> PPOption
- data OutputMode
- data DefaultTotality
- data InteractiveOpts = InteractiveOpts {
- interactiveOpts_indentWith :: Int
- interactiveOpts_indentClause :: Int
- data IState = IState {
- tt_ctxt :: Context
- idris_constraints :: Set ConstraintFC
- idris_infixes :: [FixDecl]
- idris_implicits :: Ctxt [PArg]
- idris_statics :: Ctxt [Bool]
- idris_interfaces :: Ctxt InterfaceInfo
- idris_openimpls :: [Name]
- idris_records :: Ctxt RecordInfo
- idris_dsls :: Ctxt DSL
- idris_optimisation :: Ctxt OptInfo
- idris_datatypes :: Ctxt TypeInfo
- idris_namehints :: Ctxt [Name]
- idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
- idris_flags :: Ctxt [FnOpt]
- idris_callgraph :: Ctxt CGInfo
- idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
- idris_moduledocs :: Ctxt (Docstring DocTerm)
- idris_tyinfodata :: Ctxt TIData
- idris_fninfo :: Ctxt FnInfo
- idris_transforms :: Ctxt [(Term, Term)]
- idris_autohints :: Ctxt [Name]
- idris_totcheck :: [(FC, Name)]
- idris_defertotcheck :: [(FC, Name)]
- idris_totcheckfail :: [(FC, String)]
- idris_options :: IOption
- idris_name :: Int
- idris_lineapps :: [((FilePath, Int), PTerm)]
- idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
- idris_coercions :: [Name]
- idris_errRev :: [(Term, Term)]
- idris_errReduce :: [Name]
- syntax_rules :: SyntaxRules
- syntax_keywords :: [String]
- imported :: [FilePath]
- idris_scprims :: [(Name, (Int, PrimFn))]
- idris_objs :: [(Codegen, FilePath)]
- idris_libs :: [(Codegen, String)]
- idris_cgflags :: [(Codegen, String)]
- idris_hdrs :: [(Codegen, String)]
- idris_imported :: [(FilePath, Bool)]
- proof_list :: [(Name, (Bool, [String]))]
- errSpan :: Maybe FC
- parserWarnings :: [(FC, Err)]
- lastParse :: Maybe Name
- indent_stack :: [Int]
- brace_stack :: [Maybe Int]
- idris_parsedSpan :: Maybe FC
- hide_list :: Ctxt Accessibility
- default_access :: Accessibility
- default_total :: DefaultTotality
- ibc_write :: [IBCWrite]
- compiled_so :: Maybe String
- idris_dynamic_libs :: [DynamicLib]
- idris_language_extensions :: [LanguageExt]
- idris_outputmode :: OutputMode
- idris_colourRepl :: Bool
- idris_colourTheme :: ColourTheme
- idris_errorhandlers :: [Name]
- idris_nameIdx :: (Int, Ctxt (Int, Name))
- idris_function_errorhandlers :: Ctxt (Map Name (Set Name))
- module_aliases :: Map [Text] [Text]
- idris_consolewidth :: ConsoleWidth
- idris_postulates :: Set Name
- idris_externs :: Set (Name, Int)
- idris_erasureUsed :: [(Name, Int)]
- idris_repl_defs :: [Name]
- elab_stack :: [(Name, Bool)]
- idris_symbols :: Map Name Name
- idris_exports :: [Name]
- idris_highlightedRegions :: Set (FC', OutputAnnotation)
- idris_parserHighlights :: Set (FC', OutputAnnotation)
- idris_deprecated :: Ctxt String
- idris_inmodule :: Set Name
- idris_ttstats :: Map Term (Int, Term)
- idris_fragile :: Ctxt String
- idris_interactiveOpts :: InteractiveOpts
- data SizeChange
- type SCGEntry = (Name, [Maybe (Int, SizeChange)])
- type UsageReason = (Name, Int)
- data CGInfo = CGInfo {}
- primDefs :: [Name]
- data IBCWrite
- = IBCFix FixDecl
- | IBCImp Name
- | IBCStatic Name
- | IBCInterface Name
- | IBCRecord Name
- | IBCImplementation Bool Bool Name Name
- | IBCDSL Name
- | IBCData Name
- | IBCOpt Name
- | IBCMetavar Name
- | IBCSyntax Syntax
- | IBCKeyword String
- | IBCImport (Bool, FilePath)
- | IBCImportDir FilePath
- | IBCSourceDir FilePath
- | IBCObj Codegen FilePath
- | IBCLib Codegen String
- | IBCCGFlag Codegen String
- | IBCDyLib String
- | IBCHeader Codegen String
- | IBCAccess Name Accessibility
- | IBCMetaInformation Name MetaInformation
- | IBCTotal Name Totality
- | IBCInjective Name Injectivity
- | IBCFlags Name
- | IBCFnInfo Name FnInfo
- | IBCTrans Name (Term, Term)
- | IBCErrRev (Term, Term)
- | IBCErrReduce Name
- | IBCCG Name
- | IBCDoc Name
- | IBCCoercion Name
- | IBCDef Name
- | IBCNameHint (Name, Name)
- | IBCLineApp FilePath Int PTerm
- | IBCErrorHandler Name
- | IBCFunctionErrorHandler Name Name Name
- | IBCPostulate Name
- | IBCExtern (Name, Int)
- | IBCTotCheckErr FC String
- | IBCParsedRegion FC
- | IBCModDocs Name
- | IBCUsage (Name, Int)
- | IBCExport Name
- | IBCAutoHint Name Name
- | IBCDeprecate Name String
- | IBCFragile Name String
- | IBCConstraint FC UConstraint
- | IBCImportHash FilePath Int
- initialInteractiveOpts :: InteractiveOpts
- idrisInit :: IState
- type Idris = StateT IState (ExceptT Err IO)
- catchError :: Idris a -> (Err -> Idris a) -> Idris a
- throwError :: Err -> Idris a
- data ElabShellCmd
- data Fixity
- data FixDecl = Fix Fixity String
- data Static
- data Plicity
- = Imp { }
- | Exp { }
- | Constraint { }
- | TacImp { }
- is_scoped :: Plicity -> Maybe ImplicitInfo
- impl :: Plicity
- impl_gen :: Plicity
- forall_imp :: Plicity
- forall_constraint :: Plicity
- expl :: Plicity
- expl_param :: Plicity
- expl_linear :: Plicity
- constraint :: Plicity
- tacimpl :: PTerm -> Plicity
- data FnOpt
- = Inlinable
- | TotalFn
- | PartialFn
- | CoveringFn
- | AllGuarded
- | AssertTotal
- | Dictionary
- | OverlappingDictionary
- | Implicit
- | NoImplicit
- | CExport String
- | ErrorHandler
- | ErrorReverse
- | ErrorReduce
- | Reflection
- | Specialise [(Name, Maybe Int)]
- | Constructor
- | AutoHint
- | PEGenerated
- | StaticFn
- type FnOpts = [FnOpt]
- inlinable :: FnOpts -> Bool
- dictionary :: FnOpts -> Bool
- data ProvideWhat' t
- = ProvTerm t t
- | ProvPostulate t
- type ProvideWhat = ProvideWhat' PTerm
- data PDecl' t
- = PFix FC Fixity [String]
- | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
- | PPostulate Bool (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
- | PClauses FC FnOpts Name [PClause' t]
- | PCAF FC Name t
- | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
- | PParams FC [(Name, t)] [PDecl' t]
- | POpenInterfaces FC [Name] [PDecl' t]
- | PNamespace String FC [PDecl' t]
- | 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
- | 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))
- | 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]
- | PDSL Name (DSL' t)
- | PSyntax FC Syntax
- | PMutual FC [PDecl' t]
- | PDirective Directive
- | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
- | PTransform FC Bool t t
- | PRunElabDecl FC t [String]
- data Directive
- = DLib Codegen String
- | DLink Codegen String
- | DFlag Codegen String
- | DInclude Codegen String
- | DHide Name
- | DFreeze Name
- | DThaw Name
- | DInjective Name
- | DSetTotal Name
- | DAccess Accessibility
- | DDefault DefaultTotality
- | DLogging Integer
- | DDynamicLibs [String]
- | DNameHint Name FC [(Name, FC)]
- | DErrorHandlers Name FC Name FC [(Name, FC)]
- | DLanguage LanguageExt
- | DDeprecate Name String
- | DFragile Name String
- | DAutoImplicits Bool
- | DUsed FC Name Name
- data RDeclInstructions
- = RTyDeclInstrs Name FC [PArg] Type
- | RClausesInstrs Name [([(Name, Term)], Term, Term)]
- | RAddImplementation Name Name
- | RDatatypeDeclInstrs Name [PArg]
- | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
- data EState = EState {
- case_decls :: [(Name, PDecl)]
- delayed_elab :: [(Int, Elab' EState ())]
- new_tyDecls :: [RDeclInstructions]
- highlighting :: Set (FC', OutputAnnotation)
- auto_binds :: [Name]
- implicit_warnings :: [(FC, Name)]
- initEState :: EState
- type ElabD a = Elab' EState a
- highlightSource :: FC -> OutputAnnotation -> ElabD ()
- data PClause' t
- data PData' t
- mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
- type PDecl = PDecl' PTerm
- type PData = PData' PTerm
- type PClause = PClause' PTerm
- mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
- declared :: PDecl -> [Name]
- tldeclared :: PDecl -> [Name]
- defined :: PDecl -> [Name]
- updateN :: [(Name, Name)] -> Name -> Name
- updateNs :: [(Name, Name)] -> PTerm -> PTerm
- data PunInfo
- = IsType
- | IsTerm
- | TypeOrTerm
- data PTerm
- = PQuote Raw
- | PRef FC [FC] Name
- | PInferRef FC [FC] Name
- | PPatvar FC Name
- | PLam FC Name FC PTerm PTerm
- | PPi Plicity Name FC PTerm PTerm
- | PLet FC RigCount Name FC PTerm PTerm PTerm
- | PTyped PTerm PTerm
- | PApp FC PTerm [PArg]
- | PWithApp FC PTerm PTerm
- | PAppImpl PTerm [ImplicitInfo]
- | PAppBind FC PTerm [PArg]
- | PMatchApp FC Name
- | PIfThenElse FC PTerm PTerm PTerm
- | PCase FC PTerm [(PTerm, PTerm)]
- | PTrue FC PunInfo
- | PResolveTC FC
- | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
- | PPair FC [FC] PunInfo PTerm PTerm
- | PDPair FC [FC] PunInfo PTerm PTerm PTerm
- | PAs FC Name PTerm
- | PAlternative [(Name, Name)] PAltType [PTerm]
- | PHidden PTerm
- | PType FC
- | PUniverse FC Universe
- | PGoal FC PTerm Name PTerm
- | PConstant FC Const
- | Placeholder
- | PDoBlock [PDo]
- | PIdiom FC PTerm
- | PMetavar FC Name
- | PProof [PTactic]
- | PTactics [PTactic]
- | PElabError Err
- | PImpossible
- | PCoerced PTerm
- | PDisamb [[Text]] PTerm
- | PUnifyLog PTerm
- | PNoImplicits PTerm
- | PQuasiquote PTerm (Maybe PTerm)
- | PUnquote PTerm
- | PQuoteName Name Bool FC
- | PRunElab FC PTerm [String]
- | PConstSugar FC PTerm
- data PAltType
- = ExactlyOne Bool
- | FirstSuccess
- | TryImplicit
- mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
- mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
- data PTactic' t
- = 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]
- | 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
- type PTactic = PTactic' PTerm
- data PDo' t
- type PDo = PDo' PTerm
- data PArg' t
- = PImp { }
- | PExp { }
- | PConstraint { }
- | PTacImplicit { }
- data ArgOpt
- pimp :: Name -> t -> Bool -> PArg' t
- pexp :: t -> PArg' t
- pconst :: t -> PArg' t
- ptacimp :: Name -> t -> t -> PArg' t
- type PArg = PArg' PTerm
- highestFC :: PTerm -> Maybe FC
- data InterfaceInfo = CI {
- implementationCtorName :: Name
- interface_methods :: [(Name, (Bool, FnOpts, PTerm))]
- interface_defaults :: [(Name, (Name, PDecl))]
- interface_default_super_interfaces :: [PDecl]
- interface_impparams :: [Name]
- interface_params :: [Name]
- interface_constraints :: [PTerm]
- interface_implementations :: [(Name, Bool)]
- interface_determiners :: [Int]
- data RecordInfo = RI {
- record_parameters :: [(Name, PTerm)]
- record_constructor :: Name
- record_projections :: [Name]
- data TIData
- = TIPartial
- | TISolution [Term]
- data FnInfo = FnInfo {
- fn_params :: [Int]
- data OptInfo = Optimise {
- inaccessible :: [(Int, Name)]
- detaggable :: Bool
- forceable :: [Int]
- data DSL' t = DSL {
- dsl_bind :: t
- dsl_apply :: t
- dsl_pure :: t
- dsl_var :: Maybe t
- index_first :: Maybe t
- index_next :: Maybe t
- dsl_lambda :: Maybe t
- dsl_let :: Maybe t
- dsl_pi :: Maybe t
- type DSL = DSL' PTerm
- data SynContext
- data Syntax
- syntaxNames :: Syntax -> [Name]
- syntaxSymbols :: Syntax -> [SSymbol]
- data SSymbol
- newtype SyntaxRules = SyntaxRules {
- syntaxRulesList :: [Syntax]
- emptySyntaxRules :: SyntaxRules
- updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
- initDSL :: DSL' PTerm
- data Using
- data SyntaxInfo = Syn {
- using :: [Using]
- syn_params :: [(Name, PTerm)]
- syn_namespace :: [String]
- no_imp :: [Name]
- imp_methods :: [Name]
- decoration :: Name -> Name
- inPattern :: Bool
- implicitAllowed :: Bool
- constraintAllowed :: Bool
- maxline :: Maybe Int
- mut_nesting :: Int
- dsl_info :: DSL
- syn_in_quasiquote :: Int
- syn_toplevel :: Bool
- withAppAllowed :: Bool
- defaultSyntax :: SyntaxInfo
- expandNS :: SyntaxInfo -> Name -> Name
- bi :: FC
- primfc :: FC
- inferTy :: Name
- inferCon :: Name
- inferDecl :: PData' PTerm
- inferOpts :: [a]
- infTerm :: PTerm -> PTerm
- infP :: TT Name
- getInferTerm :: Term -> Term
- getInferType :: Term -> Term
- primNames :: [Name]
- unitTy :: Name
- unitCon :: Name
- falseDoc :: Docstring (Err' t)
- falseTy :: Name
- pairTy :: Name
- pairCon :: Name
- upairTy :: Name
- upairCon :: Name
- eqTy :: Name
- eqCon :: Name
- eqDoc :: Docstring (Either (Err' t) b)
- eqDecl :: PData' PTerm
- eqParamDoc :: [(Name, Docstring (Either (Err' t) b))]
- eqOpts :: [a]
- modDocName :: Name
- sigmaTy :: Name
- sigmaCon :: Name
- piBind :: [(Name, PTerm)] -> PTerm -> PTerm
- piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
- annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
- consoleDecorate :: IState -> OutputAnnotation -> String -> String
- isPostulateName :: Name -> IState -> Bool
- prettyImp :: PPOption -> PTerm -> Doc OutputAnnotation
- prettyIst :: IState -> PTerm -> Doc OutputAnnotation
- pprintPTerm :: PPOption -> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> Doc OutputAnnotation
- basename :: Name -> Name
- isHoleName :: Name -> Bool
- containsHole :: PTerm -> Bool
- prettyName :: Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
- showCImp :: PPOption -> PClause -> Doc OutputAnnotation
- showDImp :: PPOption -> PData -> Doc OutputAnnotation
- showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
- showDeclImp :: PPOption -> PDecl' PTerm -> Doc OutputAnnotation
- getImps :: [PArg] -> [(Name, PTerm)]
- getExps :: [PArg] -> [PTerm]
- getShowArgs :: [PArg] -> [PArg]
- getConsts :: [PArg] -> [PTerm]
- getAll :: [PArg] -> [PTerm]
- showName :: Maybe IState -> [(Name, Bool)] -> PPOption -> Bool -> Name -> String
- showTm :: IState -> PTerm -> String
- showTmImpls :: PTerm -> String
- showTmOpts :: PPOption -> PTerm -> String
- getPArity :: PTerm -> Int
- allNamesIn :: PTerm -> [Name]
- boundNamesIn :: PTerm -> [Name]
- implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
- namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
- usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
- getErasureInfo :: IState -> Name -> [Int]
Documentation
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
|
toplevelWith :: String -> ElabInfo Source #
eInfoNames :: ElabInfo -> [Name] Source #
Constructors
IOption | |
Fields
|
Instances
Generic IOption Source # | |
Show IOption Source # | |
NFData IOption | |
Defined in Idris.DeepSeq | |
Eq IOption Source # | |
type Rep IOption Source # | |
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))))))) |
Constructors
PPOption | |
Fields
|
defaultPPOption :: PPOption Source #
Pretty printing options with default verbosity.
verbosePPOption :: PPOption Source #
Pretty printing options with the most verbosity.
ppOptionIst :: IState -> PPOption Source #
Get pretty printing options from an idris state record.
data OutputMode Source #
The output mode in use
Constructors
RawOutput Handle | Print user output directly to the handle |
IdeMode Integer Handle | Send IDE output for some request ID to the handle |
Instances
Show OutputMode Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> OutputMode -> ShowS show :: OutputMode -> String showList :: [OutputMode] -> ShowS | |
NFData OutputMode | |
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
Generic DefaultTotality Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep DefaultTotality :: Type -> Type Methods from :: DefaultTotality -> Rep DefaultTotality x to :: Rep DefaultTotality x -> DefaultTotality | |
Show DefaultTotality Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> DefaultTotality -> ShowS show :: DefaultTotality -> String showList :: [DefaultTotality] -> ShowS | |
Binary DefaultTotality | |
Defined in Idris.IBC | |
NFData DefaultTotality | |
Defined in Idris.DeepSeq Methods rnf :: DefaultTotality -> () | |
Eq DefaultTotality Source # | |
Defined in Idris.AbsSyntaxTree Methods (==) :: DefaultTotality -> DefaultTotality -> Bool (/=) :: DefaultTotality -> DefaultTotality -> Bool | |
type Rep DefaultTotality Source # | |
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.
Constructors
InteractiveOpts | |
Fields
|
Instances
Generic InteractiveOpts Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep InteractiveOpts :: Type -> Type Methods from :: InteractiveOpts -> Rep InteractiveOpts x to :: Rep InteractiveOpts x -> InteractiveOpts | |
Show InteractiveOpts Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> InteractiveOpts -> ShowS show :: InteractiveOpts -> String showList :: [InteractiveOpts] -> ShowS | |
NFData InteractiveOpts | |
Defined in Idris.DeepSeq Methods rnf :: InteractiveOpts -> () | |
type Rep InteractiveOpts Source # | |
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))) |
The global state used in the Idris monad
Constructors
IState | |
Fields
|
Instances
Generic IState Source # | |
Show IState Source # | |
NFData IState | |
Defined in Idris.DeepSeq | |
type Rep IState Source # | |
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 #
Instances
Generic SizeChange Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SizeChange :: Type -> Type | |
Show SizeChange Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SizeChange -> ShowS show :: SizeChange -> String showList :: [SizeChange] -> ShowS | |
Binary SizeChange | |
Defined in Idris.IBC | |
NFData SizeChange | |
Defined in Idris.DeepSeq Methods rnf :: SizeChange -> () | |
Eq SizeChange Source # | |
Defined in Idris.AbsSyntaxTree | |
type Rep SizeChange Source # | |
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 #
Constructors
CGInfo | |
Instances
Generic CGInfo Source # | |
Show CGInfo Source # | |
Binary CGInfo | |
NFData CGInfo | |
Defined in Idris.DeepSeq | |
type Rep CGInfo Source # | |
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])])))) |
Constructors
Instances
Generic IBCWrite Source # | |
Show IBCWrite Source # | |
NFData IBCWrite | |
Defined in Idris.DeepSeq | |
type Rep IBCWrite Source # | |
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)))))))) |
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))
throwError :: Err -> Idris a Source #
data ElabShellCmd Source #
Constructors
EQED | |
EAbandon | |
EUndo | |
EProofState | |
EProofTerm | |
EEval PTerm | |
ECheck PTerm | |
ESearch PTerm | |
EDocStr (Either Name Const) |
Instances
Show ElabShellCmd Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> ElabShellCmd -> ShowS show :: ElabShellCmd -> String showList :: [ElabShellCmd] -> ShowS | |
Eq ElabShellCmd Source # | |
Defined in Idris.AbsSyntaxTree |
Constructors
Infixl | |
Fields
| |
Infixr | |
Fields
| |
InfixN | |
Fields
| |
PrefixN | |
Fields
|
Instances
Generic Fixity Source # | |
Show Fixity Source # | |
Binary Fixity | |
NFData Fixity | |
Defined in Idris.DeepSeq | |
Eq Fixity Source # | |
type Rep Fixity Source # | |
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)))) |
Instances
Generic FixDecl Source # | |
Show FixDecl Source # | |
Binary FixDecl | |
NFData FixDecl | |
Defined in Idris.DeepSeq | |
Eq FixDecl Source # | |
Ord FixDecl Source # | |
type Rep FixDecl Source # | |
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))) |
Mark bindings with their explicitness, and laziness
Instances
Data Static Source # | |
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 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 # | |
Show Static Source # | |
Binary Static | |
NFData Static | |
Defined in Idris.DeepSeq | |
Eq Static Source # | |
Ord Static Source # | |
type Rep Static Source # | |
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)) |
Constructors
Imp | |
Exp | |
Constraint | |
TacImp | |
Instances
Data Plicity Source # | |
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 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 # | |
Show Plicity Source # | |
Binary Plicity | |
NFData Plicity | |
Defined in Idris.DeepSeq | |
Eq Plicity Source # | |
Ord Plicity Source # | |
type Rep Plicity Source # | |
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))))) |
is_scoped :: Plicity -> Maybe ImplicitInfo Source #
forall_imp :: Plicity Source #
expl_param :: Plicity Source #
constraint :: Plicity 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
Generic FnOpt Source # | |
Show FnOpt Source # | |
Binary FnOpt | |
NFData FnOpt | |
Defined in Idris.DeepSeq | |
Eq FnOpt Source # | |
type Rep FnOpt Source # | |
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)))))) |
dictionary :: FnOpts -> Bool Source #
data ProvideWhat' t Source #
Type provider - what to provide
Constructors
ProvTerm t t | the first is the goal type, the second is the term |
ProvPostulate t | goal type must be Type, so only term |
Instances
Functor ProvideWhat' Source # | |
Defined in Idris.AbsSyntaxTree Methods fmap :: (a -> b) -> ProvideWhat' a -> ProvideWhat' b (<$) :: a -> ProvideWhat' b -> ProvideWhat' a | |
Generic (ProvideWhat' t) Source # | |
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 # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> ProvideWhat' t -> ShowS show :: ProvideWhat' t -> String showList :: [ProvideWhat' t] -> ShowS | |
Binary t => Binary (ProvideWhat' t) | |
Defined in Idris.IBC | |
NFData t => NFData (ProvideWhat' t) | |
Defined in Idris.DeepSeq Methods rnf :: ProvideWhat' t -> () | |
Eq t => Eq (ProvideWhat' t) Source # | |
Defined in Idris.AbsSyntaxTree Methods (==) :: ProvideWhat' t -> ProvideWhat' t -> Bool (/=) :: ProvideWhat' t -> ProvideWhat' t -> Bool | |
type Rep (ProvideWhat' t) Source # | |
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))) |
type ProvideWhat = ProvideWhat' PTerm Source #
Top-level declarations such as compiler directives, definitions, datatypes and interfaces.
Constructors
PFix FC Fixity [String] | Fixity declaration |
PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t | Type declaration (last FC is precise name location) |
PPostulate Bool (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t | Postulate, second FC is precise name location |
PClauses FC FnOpts Name [PClause' t] | Pattern clause |
PCAF FC Name t | Top level constant |
PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) | Data declaration. |
PParams FC [(Name, t)] [PDecl' t] | Params block |
POpenInterfaces FC [Name] [PDecl' t] | Open block/declaration |
PNamespace String FC [PDecl' t] | New namespace, where FC is accurate location of the namespace in the file |
PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts Name FC [(Name, FC, Plicity, t)] [(Name, Docstring (Either Err t))] [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] (Maybe (Name, FC)) (Docstring (Either Err t)) SyntaxInfo | Record name. |
PInterface (Docstring (Either Err t)) SyntaxInfo FC [(Name, t)] Name FC [(Name, FC, t)] [(Name, Docstring (Either Err t))] [(Name, FC)] [PDecl' t] (Maybe (Name, FC)) (Docstring (Either Err t)) | Interface: arguments are documentation, syntax info, source location, constraints, interface name, interface name location, parameters, method declarations, optional constructor name |
PImplementation (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC [(Name, t)] [Name] Accessibility FnOpts Name FC [t] [(Name, t)] t (Maybe Name) [PDecl' t] | Implementation declaration: arguments are documentation, syntax info, source location, constraints, interface name, parameters, full Implementation type, optional explicit name, and definitions |
PDSL Name (DSL' t) | DSL declaration |
PSyntax FC Syntax | Syntax definition |
PMutual FC [PDecl' t] | Mutual block |
PDirective Directive | Compiler directive. |
PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name | Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location. |
PTransform FC Bool t t | Source-to-source transformation rule. If bool is True, lhs and rhs must be convertible. |
PRunElabDecl FC t [String] | FC is decl-level, for errors, and Strings represent the namespace |
Instances
Functor PDecl' Source # | |
Show PDecl Source # | |
Generic (PDecl' t) Source # | |
Binary t => Binary (PDecl' t) | |
NFData t => NFData (PDecl' t) | |
Defined in Idris.DeepSeq | |
type Rep (PDecl' t) Source # | |
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])))))))) |
The set of source directives
Constructors
DLib Codegen String | |
DLink Codegen String | |
DFlag Codegen String | |
DInclude Codegen String | |
DHide Name | |
DFreeze Name | |
DThaw Name | |
DInjective Name | |
DSetTotal Name | |
DAccess Accessibility | |
DDefault DefaultTotality | |
DLogging Integer | |
DDynamicLibs [String] | |
DNameHint Name FC [(Name, FC)] | |
DErrorHandlers Name FC Name FC [(Name, FC)] | |
DLanguage LanguageExt | |
DDeprecate Name String | |
DFragile Name String | |
DAutoImplicits Bool | |
DUsed FC Name Name |
Instances
Generic Directive Source # | |
Binary Directive | |
NFData Directive | |
Defined in Idris.DeepSeq | |
type Rep Directive Source # | |
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.
Constructors
RTyDeclInstrs Name FC [PArg] Type | |
RClausesInstrs Name [([(Name, Term)], Term, Term)] | |
RAddImplementation Name Name | |
RDatatypeDeclInstrs Name [PArg] | |
RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)] | Datatype, constructors |
For elaborator state
Constructors
EState | |
Fields
|
initEState :: EState Source #
highlightSource :: FC -> OutputAnnotation -> ElabD () Source #
One clause of a top-level definition. Term arguments to constructors are:
- The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
- The list of extra
with
patterns - The right-hand side
- The where block (PDecl' t)
Constructors
PClause FC Name t [t] t [PDecl' t] | A normal top-level definition. |
PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t] | |
PClauseR FC [t] t [PDecl' t] | |
PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t] |
Instances
Functor PClause' Source # | |
Show PClause Source # | |
Generic (PClause' t) Source # | |
Binary t => Binary (PClause' t) | |
NFData t => NFData (PClause' t) | |
Defined in Idris.DeepSeq | |
type Rep (PClause' t) Source # | |
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 declaration
Constructors
PDatadecl | Data declaration |
PLaterdecl | Placeholder for data whose constructors are defined later |
Instances
Functor PData' Source # | |
Show PData Source # | |
Generic (PData' t) Source # | |
Binary t => Binary (PData' t) | |
NFData t => NFData (PData' t) | |
Defined in Idris.DeepSeq | |
type Rep (PData' t) Source # | |
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.
tldeclared :: PDecl -> [Name] Source #
Constructors
IsType | |
IsTerm | |
TypeOrTerm |
Instances
Data PunInfo Source # | |
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 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 # | |
Show PunInfo Source # | |
Binary PunInfo | |
NFData PunInfo | |
Defined in Idris.DeepSeq | |
Eq PunInfo Source # | |
Ord PunInfo Source # | |
type Rep PunInfo Source # | |
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))) |
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 |
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 |
|
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
Data PTerm Source # | |
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 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 # | |
Show PClause Source # | |
Show PData Source # | |
Show PDecl Source # | |
Show PTerm Source # | |
Binary PTerm | |
NFData PTerm | |
Defined in Idris.DeepSeq | |
Eq PTerm Source # | |
Ord PTerm Source # | |
type Rep PTerm Source # | |
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)))))))) |
Constructors
ExactlyOne Bool | flag sets whether delay is allowed |
FirstSuccess | |
TryImplicit |
Instances
Data PAltType Source # | |
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 # | |
Binary PAltType | |
NFData PAltType | |
Defined in Idris.DeepSeq | |
Eq PAltType Source # | |
Ord PAltType Source # | |
Defined in Idris.AbsSyntaxTree | |
type Rep PAltType Source # | |
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.
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
Foldable PTactic' Source # | |
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 elem :: Eq a => a -> PTactic' a -> Bool maximum :: Ord a => PTactic' a -> a minimum :: Ord a => PTactic' a -> a | |
Traversable PTactic' Source # | |
Functor PTactic' Source # | |
Data t => Data (PTactic' t) Source # | |
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 # | |
Show t => Show (PTactic' t) Source # | |
Binary t => Binary (PTactic' t) | |
NFData t => NFData (PTactic' t) | |
Defined in Idris.DeepSeq | |
Eq t => Eq (PTactic' t) Source # | |
Ord t => Ord (PTactic' t) Source # | |
type Rep (PTactic' t) Source # | |
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))))))) |
Constructors
DoExp FC t | |
DoBind FC Name FC t | second FC is precise name location |
DoBindP FC t t [(t, t)] | |
DoLet FC RigCount Name FC t t | second FC is precise name location |
DoLetP FC t t [(t, t)] | |
DoRewrite FC t |
Instances
Functor PDo' Source # | |
Data t => Data (PDo' t) Source # | |
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) 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 # | |
Binary t => Binary (PDo' t) | |
NFData t => NFData (PDo' t) | |
Defined in Idris.DeepSeq | |
Eq t => Eq (PDo' t) Source # | |
Ord t => Ord (PDo' t) Source # | |
type Rep (PDo' t) Source # | |
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))))) |
Constructors
PImp | |
PExp | |
PConstraint | |
PTacImplicit | |
Instances
Functor PArg' Source # | |
Data t => Data (PArg' t) Source # | |
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) 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 # | |
Show t => Show (PArg' t) Source # | |
Binary t => Binary (PArg' t) | |
NFData t => NFData (PArg' t) | |
Defined in Idris.DeepSeq | |
Eq t => Eq (PArg' t) Source # | |
Ord t => Ord (PArg' t) Source # | |
type Rep (PArg' t) Source # | |
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)))))) |
Constructors
AlwaysShow | |
HideDisplay | |
InaccessibleArg | |
UnknownImp |
Instances
Data ArgOpt Source # | |
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 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 # | |
Show ArgOpt Source # | |
Binary ArgOpt | |
NFData ArgOpt | |
Defined in Idris.DeepSeq | |
Eq ArgOpt Source # | |
Ord ArgOpt Source # | |
type Rep ArgOpt Source # | |
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))) |
data InterfaceInfo Source #
Constructors
CI | |
Fields
|
Instances
Generic InterfaceInfo Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep InterfaceInfo :: Type -> Type | |
Show InterfaceInfo Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> InterfaceInfo -> ShowS show :: InterfaceInfo -> String showList :: [InterfaceInfo] -> ShowS | |
Binary InterfaceInfo | |
Defined in Idris.IBC | |
NFData InterfaceInfo | |
Defined in Idris.DeepSeq Methods rnf :: InterfaceInfo -> () | |
type Rep InterfaceInfo Source # | |
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 #
Constructors
RI | |
Fields
|
Instances
Generic RecordInfo Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep RecordInfo :: Type -> Type | |
Show RecordInfo Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> RecordInfo -> ShowS show :: RecordInfo -> String showList :: [RecordInfo] -> ShowS | |
Binary RecordInfo | |
Defined in Idris.IBC | |
NFData RecordInfo | |
Defined in Idris.DeepSeq Methods rnf :: RecordInfo -> () | |
type Rep RecordInfo Source # | |
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])))) |
Constructors
TIPartial | a function with a partially defined type |
TISolution [Term] | possible solutions to a metavariable in a type |
Instances
Generic TIData Source # | |
Show TIData Source # | |
NFData TIData | |
Defined in Idris.DeepSeq | |
type Rep TIData Source # | |
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]))) |
Miscellaneous information about functions
Instances
Generic FnInfo Source # | |
Show FnInfo Source # | |
Binary FnInfo | |
NFData FnInfo | |
Defined in Idris.DeepSeq | |
type Rep FnInfo Source # | |
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]))) |
Constructors
Optimise | |
Fields
|
Instances
Generic OptInfo Source # | |
Show OptInfo Source # | |
Binary OptInfo | |
NFData OptInfo | |
Defined in Idris.DeepSeq | |
type Rep OptInfo Source # | |
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])))) |
Syntactic sugar info
Constructors
DSL | |
Fields
|
Instances
Functor DSL' Source # | |
Generic (DSL' t) Source # | |
Show t => Show (DSL' t) Source # | |
Binary t => Binary (DSL' t) | |
NFData t => NFData (DSL' t) | |
Defined in Idris.DeepSeq | |
type Rep (DSL' t) Source # | |
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 #
Constructors
PatternSyntax | |
TermSyntax | |
AnySyntax |
Instances
Generic SynContext Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SynContext :: Type -> Type | |
Show SynContext Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SynContext -> ShowS show :: SynContext -> String showList :: [SynContext] -> ShowS | |
Binary SynContext | |
Defined in Idris.IBC | |
NFData SynContext | |
Defined in Idris.DeepSeq Methods rnf :: SynContext -> () | |
type Rep SynContext Source # | |
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))) |
Instances
Generic Syntax Source # | |
Show Syntax Source # | |
Binary Syntax | |
NFData Syntax | |
Defined in Idris.DeepSeq | |
type Rep Syntax Source # | |
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]))) |
syntaxNames :: Syntax -> [Name] Source #
syntaxSymbols :: Syntax -> [SSymbol] Source #
Instances
Generic SSymbol Source # | |
Show SSymbol Source # | |
Binary SSymbol | |
NFData SSymbol | |
Defined in Idris.DeepSeq | |
Eq SSymbol Source # | |
type Rep SSymbol Source # | |
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
Generic SyntaxRules Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SyntaxRules :: Type -> Type | |
NFData SyntaxRules | |
Defined in Idris.DeepSeq Methods rnf :: SyntaxRules -> () | |
type Rep SyntaxRules Source # | |
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]))) |
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules Source #
Instances
Data Using Source # | |
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 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 # | |
Show Using Source # | |
Binary Using | |
NFData Using | |
Defined in Idris.DeepSeq | |
Eq Using Source # | |
type Rep Using Source # | |
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
Generic SyntaxInfo Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SyntaxInfo :: Type -> Type | |
Show SyntaxInfo Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SyntaxInfo -> ShowS show :: SyntaxInfo -> String showList :: [SyntaxInfo] -> ShowS | |
Binary SyntaxInfo | |
Defined in Idris.IBC | |
NFData SyntaxInfo | |
Defined in Idris.DeepSeq Methods rnf :: SyntaxInfo -> () | |
type Rep SyntaxInfo Source # | |
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)))))) |
getInferTerm :: Term -> Term Source #
getInferType :: Term -> Term 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.
isPostulateName :: Name -> IState -> Bool 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
Arguments
:: PPOption | pretty printing options |
-> [(Name, Bool)] | the currently-bound names and whether they are implicit |
-> [Name] | names to always show in pi, even if not used |
-> [FixDecl] | Fixity declarations |
-> PTerm | the term to pretty-print |
-> Doc OutputAnnotation |
Pretty-print a high-level Idris term in some bindings context with infix info.
isHoleName :: Name -> Bool Source #
Determine whether a name was the one inserted for a hole or guess by the delaborator
containsHole :: PTerm -> Bool Source #
Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
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
showDeclImp :: PPOption -> PDecl' PTerm -> Doc OutputAnnotation Source #
getShowArgs :: [PArg] -> [PArg] 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
showTmImpls :: PTerm -> String Source #
Show a term with implicits, no colours
showTmOpts :: PPOption -> PTerm -> String Source #
Show a term with specific options
allNamesIn :: PTerm -> [Name] Source #
boundNamesIn :: PTerm -> [Name] Source #
getErasureInfo :: IState -> Name -> [Int] Source #