| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| 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
| NFData IOption | |||||
Defined in Idris.DeepSeq | |||||
| Generic IOption Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show IOption Source # | |||||
| Eq IOption Source # | |||||
| type Rep IOption Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep IOption = D1 ('MetaData "IOption" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData OutputMode | |
Defined in Idris.DeepSeq Methods rnf :: OutputMode -> () | |
| Show OutputMode Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> OutputMode -> ShowS show :: OutputMode -> String showList :: [OutputMode] -> ShowS | |
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
| Binary DefaultTotality | |||||
Defined in Idris.IBC | |||||
| NFData DefaultTotality | |||||
Defined in Idris.DeepSeq Methods rnf :: DefaultTotality -> () | |||||
| Generic DefaultTotality Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
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 | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData InteractiveOpts | |||||
Defined in Idris.DeepSeq Methods rnf :: InteractiveOpts -> () | |||||
| Generic InteractiveOpts Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
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 | |||||
| type Rep InteractiveOpts Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep InteractiveOpts = D1 ('MetaData "InteractiveOpts" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData IState | |||||
Defined in Idris.DeepSeq | |||||
| Generic IState Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show IState Source # | |||||
| type Rep IState Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep IState = D1 ('MetaData "IState" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary SizeChange | |||||
Defined in Idris.IBC | |||||
| NFData SizeChange | |||||
Defined in Idris.DeepSeq Methods rnf :: SizeChange -> () | |||||
| Generic SizeChange Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show SizeChange Source # | |||||
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SizeChange -> ShowS show :: SizeChange -> String showList :: [SizeChange] -> ShowS | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary CGInfo | |||||
| NFData CGInfo | |||||
Defined in Idris.DeepSeq | |||||
| Generic CGInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show CGInfo Source # | |||||
| type Rep CGInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep CGInfo = D1 ('MetaData "CGInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData IBCWrite | |||||
Defined in Idris.DeepSeq | |||||
| Generic IBCWrite Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show IBCWrite Source # | |||||
| type Rep IBCWrite Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep IBCWrite = D1 ('MetaData "IBCWrite" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary Fixity | |||||
| NFData Fixity | |||||
Defined in Idris.DeepSeq | |||||
| Generic Fixity Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show Fixity Source # | |||||
| Eq Fixity Source # | |||||
| type Rep Fixity Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep Fixity = D1 ('MetaData "Fixity" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary FixDecl | |||||
| NFData FixDecl | |||||
Defined in Idris.DeepSeq | |||||
| Generic FixDecl Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show FixDecl Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary Static | |||||
| NFData Static | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show Static Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "Static" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Dynamic" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
Constructors
| Imp | |
| Exp | |
| Constraint | |
| TacImp | |
Instances
| Binary Plicity | |||||
| NFData Plicity | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show Plicity Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary FnOpt | |||||
| NFData FnOpt | |||||
Defined in Idris.DeepSeq | |||||
| Generic FnOpt Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show FnOpt Source # | |||||
| Eq FnOpt Source # | |||||
| type Rep FnOpt Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep FnOpt = D1 ('MetaData "FnOpt" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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 | |||||
| Binary t => Binary (ProvideWhat' t) | |||||
Defined in Idris.IBC | |||||
| NFData t => NFData (ProvideWhat' t) | |||||
Defined in Idris.DeepSeq Methods rnf :: ProvideWhat' t -> () | |||||
| Generic (ProvideWhat' t) Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
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 | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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 # | |||||
| Binary t => Binary (PDecl' t) | |||||
| NFData t => NFData (PDecl' t) | |||||
Defined in Idris.DeepSeq | |||||
| Generic (PDecl' t) Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| type Rep (PDecl' t) Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep (PDecl' t) = D1 ('MetaData "PDecl'" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary Directive | |||||
| NFData Directive | |||||
Defined in Idris.DeepSeq | |||||
| Generic Directive Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| type Rep Directive Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep Directive = D1 ('MetaData "Directive" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
withpatterns - 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 # | |||||
| Binary t => Binary (PClause' t) | |||||
| NFData t => NFData (PClause' t) | |||||
Defined in Idris.DeepSeq | |||||
| Generic (PClause' t) Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| type Rep (PClause' t) Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep (PClause' t) = D1 ('MetaData "PClause'" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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 # | |||||
| Binary t => Binary (PData' t) | |||||
| NFData t => NFData (PData' t) | |||||
Defined in Idris.DeepSeq | |||||
| Generic (PData' t) Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| type Rep (PData' t) Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep (PData' t) = D1 ('MetaData "PData'" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary PunInfo | |||||
| NFData PunInfo | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show PunInfo Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary PTerm | |||||
| NFData PTerm | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show PClause Source # | |||||
| Show PData Source # | |||||
| Show PDecl Source # | |||||
| Show PTerm Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary PAltType | |||||
| NFData PAltType | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Functor PTactic' Source # | |||||
| 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 # | |||||
| Binary t => Binary (PTactic' t) | |||||
| NFData t => NFData (PTactic' t) | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show t => Show (PTactic' t) Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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 # | |||||
| Binary t => Binary (PDo' t) | |||||
| NFData t => NFData (PDo' t) | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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 # | |||||
| Binary t => Binary (PArg' t) | |||||
| NFData t => NFData (PArg' t) | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show t => Show (PArg' t) Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary ArgOpt | |||||
| NFData ArgOpt | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show ArgOpt Source # | |||||
| 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-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary InterfaceInfo | |||||
Defined in Idris.IBC | |||||
| NFData InterfaceInfo | |||||
Defined in Idris.DeepSeq Methods rnf :: InterfaceInfo -> () | |||||
| Generic InterfaceInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show InterfaceInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> InterfaceInfo -> ShowS show :: InterfaceInfo -> String showList :: [InterfaceInfo] -> ShowS | |||||
| type Rep InterfaceInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep InterfaceInfo = D1 ('MetaData "InterfaceInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary RecordInfo | |||||
Defined in Idris.IBC | |||||
| NFData RecordInfo | |||||
Defined in Idris.DeepSeq Methods rnf :: RecordInfo -> () | |||||
| Generic RecordInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show RecordInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> RecordInfo -> ShowS show :: RecordInfo -> String showList :: [RecordInfo] -> ShowS | |||||
| type Rep RecordInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep RecordInfo = D1 ('MetaData "RecordInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData TIData | |||||
Defined in Idris.DeepSeq | |||||
| Generic TIData Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show TIData Source # | |||||
| type Rep TIData Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep TIData = D1 ('MetaData "TIData" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary FnInfo | |||||
| NFData FnInfo | |||||
Defined in Idris.DeepSeq | |||||
| Generic FnInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show FnInfo Source # | |||||
| type Rep FnInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep FnInfo = D1 ('MetaData "FnInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "FnInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "fn_params") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]))) | |||||
Constructors
| Optimise | |
Fields
| |
Instances
| Binary OptInfo | |||||
| NFData OptInfo | |||||
Defined in Idris.DeepSeq | |||||
| Generic OptInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show OptInfo Source # | |||||
| type Rep OptInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep OptInfo = D1 ('MetaData "OptInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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 # | |||||
| Binary t => Binary (DSL' t) | |||||
| NFData t => NFData (DSL' t) | |||||
Defined in Idris.DeepSeq | |||||
| Generic (DSL' t) Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show t => Show (DSL' t) Source # | |||||
| type Rep (DSL' t) Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep (DSL' t) = D1 ('MetaData "DSL'" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary SynContext | |||||
Defined in Idris.IBC | |||||
| NFData SynContext | |||||
Defined in Idris.DeepSeq Methods rnf :: SynContext -> () | |||||
| Generic SynContext Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show SynContext Source # | |||||
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SynContext -> ShowS show :: SynContext -> String showList :: [SynContext] -> ShowS | |||||
| type Rep SynContext Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep SynContext = D1 ('MetaData "SynContext" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary Syntax | |||||
| NFData Syntax | |||||
Defined in Idris.DeepSeq | |||||
| Generic Syntax Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show Syntax Source # | |||||
| type Rep Syntax Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep Syntax = D1 ('MetaData "Syntax" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary SSymbol | |||||
| NFData SSymbol | |||||
Defined in Idris.DeepSeq | |||||
| Generic SSymbol Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show SSymbol Source # | |||||
| Eq SSymbol Source # | |||||
| type Rep SSymbol Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep SSymbol = D1 ('MetaData "SSymbol" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| NFData SyntaxRules | |||||
Defined in Idris.DeepSeq Methods rnf :: SyntaxRules -> () | |||||
| Generic SyntaxRules Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| type Rep SyntaxRules Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep SyntaxRules = D1 ('MetaData "SyntaxRules" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'True) (C1 ('MetaCons "SyntaxRules" 'PrefixI 'True) (S1 ('MetaSel ('Just "syntaxRulesList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Syntax]))) | |||||
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules Source #
Instances
| Binary Using | |||||
| NFData Using | |||||
Defined in Idris.DeepSeq | |||||
| 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 # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show Using Source # | |||||
| Eq Using Source # | |||||
| type Rep Using Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep Using = D1 ('MetaData "Using" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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
| Binary SyntaxInfo | |||||
Defined in Idris.IBC | |||||
| NFData SyntaxInfo | |||||
Defined in Idris.DeepSeq Methods rnf :: SyntaxInfo -> () | |||||
| Generic SyntaxInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Associated Types
| |||||
| Show SyntaxInfo Source # | |||||
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SyntaxInfo -> ShowS show :: SyntaxInfo -> String showList :: [SyntaxInfo] -> ShowS | |||||
| type Rep SyntaxInfo Source # | |||||
Defined in Idris.AbsSyntaxTree type Rep SyntaxInfo = D1 ('MetaData "SyntaxInfo" "Idris.AbsSyntaxTree" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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 #