Safe Haskell | None |
---|---|
Language | Haskell98 |
- data ElabWhat
- data ElabInfo = EInfo {}
- toplevel :: ElabInfo
- eInfoNames :: ElabInfo -> [Name]
- data IOption = IOption {
- opt_logLevel :: Int
- opt_typecase :: Bool
- opt_typeintype :: Bool
- opt_coverage :: Bool
- opt_showimp :: Bool
- opt_errContext :: Bool
- opt_repl :: Bool
- opt_verbose :: Bool
- opt_nobanner :: Bool
- opt_quiet :: Bool
- opt_codegen :: Codegen
- opt_outputTy :: OutputType
- opt_ibcsubdir :: FilePath
- opt_importdirs :: [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
- defaultOpts :: IOption
- data PPOption = PPOption {
- ppopt_impl :: Bool
- ppopt_pinames :: Bool
- ppopt_depth :: Maybe Int
- data Optimisation = PETransform
- defaultOptimise :: [Optimisation]
- defaultPPOption :: PPOption
- verbosePPOption :: PPOption
- ppOption :: IOption -> PPOption
- ppOptionIst :: IState -> PPOption
- data LanguageExt
- data OutputMode
- data ConsoleWidth
- data IState = IState {
- tt_ctxt :: Context
- idris_constraints :: Set ConstraintFC
- idris_infixes :: [FixDecl]
- idris_implicits :: Ctxt [PArg]
- idris_statics :: Ctxt [Bool]
- idris_classes :: Ctxt ClassInfo
- idris_dsls :: Ctxt DSL
- idris_optimisation :: Ctxt OptInfo
- idris_datatypes :: Ctxt TypeInfo
- idris_namehints :: Ctxt [Name]
- idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm])
- idris_flags :: Ctxt [FnOpt]
- idris_callgraph :: Ctxt CGInfo
- idris_calledgraph :: Ctxt [Name]
- 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))]
- idris_coercions :: [Name]
- idris_errRev :: [(Term, Term)]
- 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]
- lastTokenSpan :: Maybe FC
- idris_parsedSpan :: Maybe FC
- hide_list :: [(Name, Maybe Accessibility)]
- default_access :: Accessibility
- default_total :: Bool
- 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_whocalls :: Maybe (Map Name [Name])
- idris_callswho :: Maybe (Map Name [Name])
- idris_repl_defs :: [Name]
- elab_stack :: [(Name, Bool)]
- idris_symbols :: Map Name Name
- idris_exports :: [Name]
- idris_highlightedRegions :: [(FC, OutputAnnotation)]
- idris_parserHighlights :: [(FC, OutputAnnotation)]
- 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
- | IBCClass Name
- | IBCInstance Bool Bool Name Name
- | IBCDSL Name
- | IBCData Name
- | IBCOpt Name
- | IBCMetavar Name
- | IBCSyntax Syntax
- | IBCKeyword String
- | IBCImport (Bool, FilePath)
- | IBCImportDir FilePath
- | IBCObj Codegen FilePath
- | IBCLib Codegen String
- | IBCCGFlag Codegen String
- | IBCDyLib String
- | IBCHeader Codegen String
- | IBCAccess Name Accessibility
- | IBCMetaInformation Name MetaInformation
- | IBCTotal Name Totality
- | IBCFlags Name [FnOpt]
- | IBCFnInfo Name FnInfo
- | IBCTrans Name (Term, Term)
- | IBCErrRev (Term, Term)
- | 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
- idrisInit :: IState
- type Idris = StateT IState (ExceptT Err IO)
- catchError :: Idris a -> (Err -> Idris a) -> Idris a
- throwError :: Err -> Idris a
- data Codegen
- data HowMuchDocs
- data Command
- = Quit
- | Help
- | Eval PTerm
- | NewDefn [PDecl]
- | Undefine [Name]
- | Check PTerm
- | Core PTerm
- | DocStr (Either Name Const) HowMuchDocs
- | TotCheck Name
- | Reload
- | Load FilePath (Maybe Int)
- | ChangeDirectory FilePath
- | ModImport String
- | Edit
- | Compile Codegen String
- | Execute PTerm
- | ExecVal PTerm
- | Metavars
- | Prove Bool Name
- | AddProof (Maybe Name)
- | RmProof Name
- | ShowProof Name
- | Proofs
- | Universes
- | LogLvl Int
- | Spec PTerm
- | WHNF PTerm
- | TestInline PTerm
- | Defn Name
- | Missing Name
- | DynamicLink FilePath
- | ListDynamic
- | Pattelab PTerm
- | Search [String] PTerm
- | CaseSplitAt Bool Int Name
- | AddClauseFrom Bool Int Name
- | AddProofClauseFrom Bool Int Name
- | AddMissing Bool Int Name
- | MakeWith Bool Int Name
- | MakeCase Bool Int Name
- | MakeLemma Bool Int Name
- | DoProofSearch Bool Bool Int Name [Name]
- | SetOpt Opt
- | UnsetOpt Opt
- | NOP
- | SetColour ColourType IdrisColour
- | ColourOn
- | ColourOff
- | ListErrorHandlers
- | SetConsoleWidth ConsoleWidth
- | SetPrinterDepth (Maybe Int)
- | Apropos [String] String
- | WhoCalls Name
- | CallsWho Name
- | Browse [String]
- | MakeDoc String
- | Warranty
- | PrintDef Name
- | PPrint OutputFmt Int PTerm
- | TransformInfo Name
- | DebugInfo Name
- | DebugUnify PTerm PTerm
- data OutputFmt
- data Opt
- = Filename String
- | Quiet
- | NoBanner
- | ColourREPL Bool
- | Idemode
- | IdemodeSocket
- | ShowLibs
- | ShowLibdir
- | ShowIncs
- | ShowPkgs
- | NoBasePkgs
- | NoPrelude
- | NoBuiltins
- | NoREPL
- | OLogging Int
- | Output String
- | Interface
- | TypeCase
- | TypeInType
- | DefaultTotal
- | DefaultPartial
- | WarnPartial
- | WarnReach
- | EvalTypes
- | NoCoverage
- | ErrContext
- | ShowImpl
- | Verbose
- | Port String
- | IBCSubDir String
- | ImportDir String
- | PkgBuild String
- | PkgInstall String
- | PkgClean String
- | PkgCheck String
- | PkgREPL String
- | PkgMkDoc String
- | PkgTest String
- | PkgIndex FilePath
- | WarnOnly
- | Pkg String
- | BCAsm String
- | DumpDefun String
- | DumpCases String
- | UseCodegen Codegen
- | CodegenArgs String
- | OutputTy OutputType
- | Extension LanguageExt
- | InterpretScript String
- | EvalExpr String
- | TargetTriple String
- | TargetCPU String
- | OptLevel Int
- | AddOpt Optimisation
- | RemoveOpt Optimisation
- | Client String
- | ShowOrigErr
- | AutoWidth
- | AutoSolve
- | UseConsoleWidth ConsoleWidth
- | DumpHighlights
- data ElabShellCmd
- data Fixity
- data FixDecl = Fix Fixity String
- data Static
- data Plicity
- is_scoped :: Plicity -> Maybe ImplicitInfo
- impl :: Plicity
- forall_imp :: Plicity
- forall_constraint :: Plicity
- expl :: Plicity
- expl_param :: 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]
- | 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
- | PClass (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))
- | PInstance (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC [(Name, t)] Name FC [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
- | DAccess Accessibility
- | DDefault Bool
- | DLogging Integer
- | DDynamicLibs [String]
- | DNameHint Name FC [(Name, FC)]
- | DErrorHandlers Name FC Name FC [(Name, FC)]
- | DLanguage LanguageExt
- | DUsed FC Name Name
- data RDeclInstructions
- = RTyDeclInstrs Name FC [PArg] Type
- | RClausesInstrs Name [([Name], Term, Term)]
- | RAddInstance Name Name
- data EState = EState {
- case_decls :: [(Name, PDecl)]
- delayed_elab :: [(Int, Elab' EState ())]
- new_tyDecls :: [RDeclInstructions]
- highlighting :: [(FC, OutputAnnotation)]
- 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 Name FC PTerm PTerm PTerm
- | PTyped PTerm PTerm
- | PApp FC PTerm [PArg]
- | 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 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 Universe
- | PGoal FC PTerm Name PTerm
- | PConstant FC Const
- | Placeholder
- | PDoBlock [PDo]
- | PIdiom FC PTerm
- | PReturn FC
- | 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 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
- | TCInstance
- | 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 ClassInfo = CI {
- instanceCtorName :: Name
- class_methods :: [(Name, (FnOpts, PTerm))]
- class_defaults :: [(Name, (Name, PDecl))]
- class_default_superclasses :: [PDecl]
- class_params :: [Name]
- class_instances :: [(Name, Bool)]
- class_determiners :: [Int]
- data TIData
- = TIPartial
- | TISolution [Term]
- data FnInfo = FnInfo {}
- data OptInfo = Optimise {
- inaccessible :: [(Int, Name)]
- detaggable :: Bool
- data DSL' t = DSL {
- dsl_bind :: t
- dsl_return :: 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
- maxline :: Maybe Int
- mut_nesting :: Int
- dsl_info :: DSL
- syn_in_quasiquote :: Int
- defaultSyntax :: SyntaxInfo
- expandNS :: SyntaxInfo -> Name -> Name
- bi :: FC
- inferTy :: Name
- inferCon :: Name
- inferDecl :: PData' PTerm
- inferOpts :: [t]
- 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 :: [t]
- 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
eInfoNames :: ElabInfo -> [Name] Source
IOption | |
|
PPOption | |
|
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 LanguageExt Source
data OutputMode Source
The output mode in use
data ConsoleWidth Source
How wide is the console?
InfinitelyWide | Have pretty-printer assume that lines should not be broken |
ColsWide Int | Manually specified - must be positive |
AutomaticWidth | Attempt to determine width, or 80 otherwise |
The global state used in the Idris monad
data SizeChange Source
type UsageReason = (Name, Int) Source
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
REPL commands
data ElabShellCmd Source
is_scoped :: Plicity -> Maybe ImplicitInfo Source
Inlinable | |
TotalFn | |
PartialFn | |
CoveringFn | |
Coinductive | |
AssertTotal | |
Dictionary | |
Implicit | |
NoImplicit | |
CExport String | |
ErrorHandler | ^ an error handler for use with the ErrorReflection extension |
ErrorReverse | ^ attempt to reverse normalise before showing in error |
Reflection | |
Specialise [(Name, Maybe Int)] | |
Constructor | |
AutoHint | |
PEGenerated |
dictionary :: FnOpts -> Bool Source
data ProvideWhat' t Source
Type provider - what to provide
ProvTerm t t | the first is the goal type, the second is the term |
ProvPostulate t | goal type must be Type, so only term |
Functor ProvideWhat' | |
Eq t => Eq (ProvideWhat' t) | |
Show t => Show (ProvideWhat' t) | |
Binary t => Binary (ProvideWhat' t) | |
NFData t => NFData (ProvideWhat' t) |
type ProvideWhat = ProvideWhat' PTerm Source
Top-level declarations such as compiler directives, definitions, datatypes and typeclasses.
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 |
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 declaration |
PClass (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)) | Type class: arguments are documentation, syntax info, source location, constraints, class name, class name location, parameters, method declarations, optional constructor name |
PInstance (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC [(Name, t)] Name FC [t] t (Maybe Name) [PDecl' t] | Instance declaration: arguments are documentation, syntax info, source location, constraints, class name, parameters, full instance 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
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.
RTyDeclInstrs Name FC [PArg] Type | |
RClausesInstrs Name [([Name], Term, Term)] | |
RAddInstance Name Name |
For elaborator state
EState | |
|
highlightSource :: FC -> OutputAnnotation -> ElabD () Source
One clause of a top-level definition. Term arguments to constructors are:
- The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
- The list of extra
with
patterns - The right-hand side
- The where block (PDecl' t)
Data declaration
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
High level language terms
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 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 |
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 type class resolution |
PRewrite FC PTerm PTerm (Maybe PTerm) | "rewrite" syntax, with 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 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 |
PReturn FC | |
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 FC | `{n} where the FC is the precise highlighting for the name in particular |
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. |
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.
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 | |
TCInstance | |
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 |
CI | |
|
TIPartial | a function with a partially defined type |
TISolution [Term] | possible solutions to a metavariable in a type |
Miscellaneous information about functions
Optimise | |
|
Syntactic sugar info
DSL | |
|
data SynContext Source
syntaxNames :: Syntax -> [Name] Source
syntaxSymbols :: Syntax -> [SSymbol] Source
newtype SyntaxRules Source
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules Source
data SyntaxInfo Source
Syn | |
|
expandNS :: SyntaxInfo -> Name -> Name Source
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
:: 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 instance.
Do the right thing for rendering a term in an IState
:: 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
:: 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
:: 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