| 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 {}
- defaultOptimise :: [Optimisation]
- defaultPPOption :: PPOption
- verbosePPOption :: PPOption
- ppOption :: IOption -> PPOption
- ppOptionIst :: IState -> PPOption
- data OutputMode
- data DefaultTotality
- data InteractiveOpts = InteractiveOpts {}
- 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
- 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
- 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 {}
- 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
Constructors
| PPOption | |
Fields
| |
defaultPPOption :: PPOption Source #
Pretty printing options with default verbosity.
verbosePPOption :: PPOption Source #
Pretty printing options with the most verbosity.
ppOptionIst :: IState -> PPOption Source #
Get pretty printing options from an idris state record.
data OutputMode Source #
The output mode in use
Constructors
| RawOutput Handle | Print user output directly to the handle |
| IdeMode Integer Handle | Send IDE output for some request ID to the handle |
Instances
| Show OutputMode Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> OutputMode -> ShowS # show :: OutputMode -> String # showList :: [OutputMode] -> ShowS # | |
| NFData OutputMode Source # | |
Defined in Idris.DeepSeq Methods rnf :: OutputMode -> () # | |
data DefaultTotality Source #
If a function has no totality annotation, what do we assume?
Constructors
| DefaultCheckingTotal | Total |
| DefaultCheckingPartial | Partial |
| DefaultCheckingCovering | Total coverage, but may diverge |
Instances
data InteractiveOpts Source #
Configuration options for interactive editing.
Constructors
| InteractiveOpts | |
Fields | |
Instances
| Show InteractiveOpts Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> InteractiveOpts -> ShowS # show :: InteractiveOpts -> String # showList :: [InteractiveOpts] -> ShowS # | |
| Generic InteractiveOpts Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep InteractiveOpts :: Type -> Type # Methods from :: InteractiveOpts -> Rep InteractiveOpts x # to :: Rep InteractiveOpts x -> InteractiveOpts # | |
| NFData InteractiveOpts Source # | |
Defined in Idris.DeepSeq Methods rnf :: InteractiveOpts -> () # | |
| type Rep InteractiveOpts Source # | |
Defined in Idris.AbsSyntaxTree type Rep InteractiveOpts = D1 (MetaData "InteractiveOpts" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "InteractiveOpts" PrefixI True) (S1 (MetaSel (Just "interactiveOpts_indentWith") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: S1 (MetaSel (Just "interactiveOpts_indentClause") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) | |
The global state used in the Idris monad
Constructors
| IState | |
Fields
| |
Instances
data SizeChange Source #
Instances
| Eq SizeChange Source # | |
Defined in Idris.AbsSyntaxTree | |
| Show SizeChange Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SizeChange -> ShowS # show :: SizeChange -> String # showList :: [SizeChange] -> ShowS # | |
| Generic SizeChange Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SizeChange :: Type -> Type # | |
| Binary SizeChange Source # | |
Defined in Idris.IBC | |
| NFData SizeChange Source # | |
Defined in Idris.DeepSeq Methods rnf :: SizeChange -> () # | |
| type Rep SizeChange Source # | |
Defined in Idris.AbsSyntaxTree type Rep SizeChange = D1 (MetaData "SizeChange" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Smaller" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Same" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Bigger" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Unknown" PrefixI False) (U1 :: Type -> Type))) | |
type UsageReason = (Name, Int) Source #
Constructors
| CGInfo | |
Instances
| Show CGInfo Source # | |
| Generic CGInfo Source # | |
| Binary CGInfo Source # | |
| NFData CGInfo Source # | |
Defined in Idris.DeepSeq | |
| type Rep CGInfo Source # | |
Defined in Idris.AbsSyntaxTree type Rep CGInfo = D1 (MetaData "CGInfo" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
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
| Eq ElabShellCmd Source # | |
Defined in Idris.AbsSyntaxTree | |
| Show ElabShellCmd Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> ElabShellCmd -> ShowS # show :: ElabShellCmd -> String # showList :: [ElabShellCmd] -> ShowS # | |
Instances
| Eq Fixity Source # | |
| Show Fixity Source # | |
| Generic Fixity Source # | |
| Binary Fixity Source # | |
| NFData Fixity Source # | |
Defined in Idris.DeepSeq | |
| type Rep Fixity Source # | |
Defined in Idris.AbsSyntaxTree type Rep Fixity = D1 (MetaData "Fixity" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Eq FixDecl Source # | |
| Ord FixDecl Source # | |
| Show FixDecl Source # | |
| Generic FixDecl Source # | |
| Binary FixDecl Source # | |
| NFData FixDecl Source # | |
Defined in Idris.DeepSeq | |
| type Rep FixDecl Source # | |
Defined in Idris.AbsSyntaxTree type Rep FixDecl = D1 (MetaData "FixDecl" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Eq Static Source # | |
| 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 # toConstr :: Static -> Constr # dataTypeOf :: Static -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Static) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Static) # gmapT :: (forall b. Data b => b -> b) -> Static -> Static # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Static -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Static -> r # gmapQ :: (forall d. Data d => d -> u) -> Static -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Static -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Static -> m Static # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Static -> m Static # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Static -> m Static # | |
| Ord Static Source # | |
| Show Static Source # | |
| Generic Static Source # | |
| Binary Static Source # | |
| NFData Static Source # | |
Defined in Idris.DeepSeq | |
| type Rep Static Source # | |
Constructors
| Imp | |
| Exp | |
| Constraint | |
| TacImp | |
Instances
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
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
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
The set of source directives
Constructors
Instances
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
Data declaration
Constructors
| PDatadecl | Data declaration |
| PLaterdecl | Placeholder for data whose constructors are defined later |
Instances
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
| Eq PunInfo Source # | |
| 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 # toConstr :: PunInfo -> Constr # dataTypeOf :: PunInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PunInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PunInfo) # gmapT :: (forall b. Data b => b -> b) -> PunInfo -> PunInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PunInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PunInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> PunInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PunInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PunInfo -> m PunInfo # | |
| Ord PunInfo Source # | |
| Show PunInfo Source # | |
| Generic PunInfo Source # | |
| Binary PunInfo Source # | |
| NFData PunInfo Source # | |
Defined in Idris.DeepSeq | |
| type Rep PunInfo Source # | |
Defined in Idris.AbsSyntaxTree | |
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
Constructors
| ExactlyOne Bool | flag sets whether delay is allowed |
| FirstSuccess | |
| TryImplicit |
Instances
| Eq PAltType Source # | |
| 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PAltType -> r # gmapQ :: (forall d. Data d => d -> u) -> PAltType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PAltType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PAltType -> m PAltType # | |
| Ord PAltType Source # | |
Defined in Idris.AbsSyntaxTree | |
| Generic PAltType Source # | |
| Binary PAltType Source # | |
| NFData PAltType Source # | |
Defined in Idris.DeepSeq | |
| type Rep PAltType Source # | |
Defined in Idris.AbsSyntaxTree type Rep PAltType = D1 (MetaData "PAltType" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
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
Constructors
| PImp | |
| PExp | |
| PConstraint | |
| PTacImplicit | |
Instances
Constructors
| AlwaysShow | |
| HideDisplay | |
| InaccessibleArg | |
| UnknownImp |
Instances
| Eq ArgOpt Source # | |
| 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 # toConstr :: ArgOpt -> Constr # dataTypeOf :: ArgOpt -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgOpt) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgOpt) # gmapT :: (forall b. Data b => b -> b) -> ArgOpt -> ArgOpt # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgOpt -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgOpt -> r # gmapQ :: (forall d. Data d => d -> u) -> ArgOpt -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgOpt -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgOpt -> m ArgOpt # | |
| Ord ArgOpt Source # | |
| Show ArgOpt Source # | |
| Generic ArgOpt Source # | |
| Binary ArgOpt Source # | |
| NFData ArgOpt Source # | |
Defined in Idris.DeepSeq | |
| type Rep ArgOpt Source # | |
Defined in Idris.AbsSyntaxTree type Rep ArgOpt = D1 (MetaData "ArgOpt" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
data RecordInfo Source #
Constructors
| RI | |
Fields
| |
Instances
| Show RecordInfo Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> RecordInfo -> ShowS # show :: RecordInfo -> String # showList :: [RecordInfo] -> ShowS # | |
| Generic RecordInfo Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep RecordInfo :: Type -> Type # | |
| Binary RecordInfo Source # | |
Defined in Idris.IBC | |
| NFData RecordInfo Source # | |
Defined in Idris.DeepSeq Methods rnf :: RecordInfo -> () # | |
| type Rep RecordInfo Source # | |
Defined in Idris.AbsSyntaxTree type Rep RecordInfo = D1 (MetaData "RecordInfo" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Show TIData Source # | |
| Generic TIData Source # | |
| NFData TIData Source # | |
Defined in Idris.DeepSeq | |
| type Rep TIData Source # | |
Defined in Idris.AbsSyntaxTree type Rep TIData = D1 (MetaData "TIData" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
Constructors
| Optimise | |
Fields
| |
Instances
| Show OptInfo Source # | |
| Generic OptInfo Source # | |
| Binary OptInfo Source # | |
| NFData OptInfo Source # | |
Defined in Idris.DeepSeq | |
| type Rep OptInfo Source # | |
Defined in Idris.AbsSyntaxTree type Rep OptInfo = D1 (MetaData "OptInfo" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
data SynContext Source #
Constructors
| PatternSyntax | |
| TermSyntax | |
| AnySyntax |
Instances
| Show SynContext Source # | |
Defined in Idris.AbsSyntaxTree Methods showsPrec :: Int -> SynContext -> ShowS # show :: SynContext -> String # showList :: [SynContext] -> ShowS # | |
| Generic SynContext Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SynContext :: Type -> Type # | |
| Binary SynContext Source # | |
Defined in Idris.IBC | |
| NFData SynContext Source # | |
Defined in Idris.DeepSeq Methods rnf :: SynContext -> () # | |
| type Rep SynContext Source # | |
Defined in Idris.AbsSyntaxTree type Rep SynContext = D1 (MetaData "SynContext" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Show Syntax Source # | |
| Generic Syntax Source # | |
| Binary Syntax Source # | |
| NFData Syntax Source # | |
Defined in Idris.DeepSeq | |
| type Rep Syntax Source # | |
Defined in Idris.AbsSyntaxTree type Rep Syntax = D1 (MetaData "Syntax" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
newtype SyntaxRules Source #
Constructors
| SyntaxRules | |
Fields
| |
Instances
| Generic SyntaxRules Source # | |
Defined in Idris.AbsSyntaxTree Associated Types type Rep SyntaxRules :: Type -> Type # | |
| NFData SyntaxRules Source # | |
Defined in Idris.DeepSeq Methods rnf :: SyntaxRules -> () # | |
| type Rep SyntaxRules Source # | |
Defined in Idris.AbsSyntaxTree type Rep SyntaxRules = D1 (MetaData "SyntaxRules" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" True) (C1 (MetaCons "SyntaxRules" PrefixI True) (S1 (MetaSel (Just "syntaxRulesList") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Syntax]))) | |
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules Source #
Instances
| Eq Using Source # | |
| 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using -> r # gmapQ :: (forall d. Data d => d -> u) -> Using -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Using -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Using -> m Using # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Using -> m Using # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Using -> m Using # | |
| Show Using Source # | |
| Generic Using Source # | |
| Binary Using Source # | |
| NFData Using Source # | |
Defined in Idris.DeepSeq | |
| type Rep Using Source # | |
Defined in Idris.AbsSyntaxTree type Rep Using = D1 (MetaData "Using" "Idris.AbsSyntaxTree" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
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.
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
allNamesIn :: PTerm -> [Name] Source #
boundNamesIn :: PTerm -> [Name] Source #