| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.AbsSyntaxTree
Description
- 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 :: [(FC, OutputAnnotation)]
- idris_parserHighlights :: [(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
- 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 :: [(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
- | Induction t
- | CaseTac t
- | 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
| |
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
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
The global state used in the Idris monad
Constructors
| IState | |
Fields
| |
data SizeChange Source #
Instances
type UsageReason = (Name, Int) Source #
Constructors
| CGInfo | |
Constructors
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
Mark bindings with their explicitness, and laziness
Constructors
| Imp | |
| Exp | |
| Constraint | |
| TacImp | |
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 |
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 # | |
| Eq t => Eq (ProvideWhat' t) Source # | |
| Show t => Show (ProvideWhat' t) Source # | |
| Generic (ProvideWhat' t) Source # | |
| type Rep (ProvideWhat' t) Source # | |
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 |
The set of source directives
Constructors
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)
Data declaration
Constructors
| PDatadecl | Data declaration |
| PLaterdecl | Placeholder for data whose constructors are defined later |
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 |
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. |
Constructors
| ExactlyOne Bool | flag sets whether delay is allowed |
| FirstSuccess | |
| TryImplicit |
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 | |
| Induction t | |
| CaseTac t | |
| 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 |
Constructors
| PImp | |
| PExp | |
| PConstraint | |
| PTacImplicit | |
Constructors
| AlwaysShow | |
| HideDisplay | |
| InaccessibleArg | |
| UnknownImp |
data InterfaceInfo Source #
Constructors
| CI | |
Fields
| |
Instances
data RecordInfo Source #
Constructors
| RI | |
Fields
| |
Instances
Constructors
| TIPartial | a function with a partially defined type |
| TISolution [Term] | possible solutions to a metavariable in a type |
Miscellaneous information about functions
Constructors
| Optimise | |
Fields
| |
Syntactic sugar info
syntaxNames :: Syntax -> [Name] Source #
syntaxSymbols :: Syntax -> [SSymbol] Source #
newtype SyntaxRules Source #
Constructors
| SyntaxRules | |
Fields
| |
Instances
| Generic SyntaxRules Source # | |
| type Rep SyntaxRules Source # | |
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules Source #
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 #