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_optLevel :: Word
- opt_cmdline :: [Opt]
- opt_origerr :: Bool
- opt_autoSolve :: Bool
- opt_autoImport :: [FilePath]
- defaultOpts :: IOption
- data PPOption = PPOption {
- ppopt_impl :: Bool
- defaultPPOption :: PPOption
- verbosePPOption :: PPOption
- ppOption :: IOption -> PPOption
- ppOptionIst :: IState -> PPOption
- data LanguageExt
- data OutputMode
- data ConsoleWidth
- data IState = IState {
- tt_ctxt :: Context
- idris_constraints :: [(UConstraint, FC)]
- 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, [(Name, Docstring)])
- idris_tyinfodata :: Ctxt TIData
- idris_fninfo :: Ctxt FnInfo
- 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, Bool))]
- idris_coercions :: [Name]
- idris_transforms :: [(Term, Term)]
- idris_errRev :: [(Term, Term)]
- syntax_rules :: [Syntax]
- 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]
- proof_list :: [(Name, [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_whocalls :: Maybe (Map Name [Name])
- idris_callswho :: Maybe (Map Name [Name])
- idris_repl_defs :: [Name]
- 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 Name Name
- | IBCDSL Name
- | IBCData Name
- | IBCOpt Name
- | IBCMetavar Name
- | IBCSyntax Syntax
- | IBCKeyword String
- | IBCImport 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 (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
- | IBCTotCheckErr FC String
- | IBCParsedRegion FC
- idrisInit :: IState
- type Idris = StateT IState (ErrorT Err IO)
- data Codegen
- data Command
- = Quit
- | Help
- | Eval PTerm
- | NewDefn [PDecl]
- | Undefine [Name]
- | Check PTerm
- | DocStr (Either Name Const)
- | TotCheck Name
- | Reload
- | Load FilePath (Maybe Int)
- | ChangeDirectory FilePath
- | ModImport String
- | Edit
- | Compile Codegen String
- | Execute
- | ExecVal PTerm
- | Metavars
- | Prove Name
- | AddProof (Maybe Name)
- | RmProof Name
- | ShowProof Name
- | Proofs
- | Universes
- | LogLvl Int
- | Spec PTerm
- | HNF PTerm
- | TestInline PTerm
- | Defn Name
- | Missing Name
- | DynamicLink FilePath
- | ListDynamic
- | Pattelab PTerm
- | DebugInfo Name
- | Search PTerm
- | CaseSplitAt Bool Int Name
- | AddClauseFrom Bool Int Name
- | AddProofClauseFrom Bool Int Name
- | AddMissing Bool Int Name
- | MakeWith 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
- | Apropos String
- | WhoCalls Name
- | CallsWho Name
- | MakeDoc String
- | Warranty
- data Opt
- = Filename String
- | Quiet
- | NoBanner
- | ColourREPL Bool
- | Ideslave
- | IdeslaveSocket
- | ShowLibs
- | ShowLibdir
- | ShowIncs
- | NoBasePkgs
- | NoPrelude
- | NoBuiltins
- | NoREPL
- | OLogging Int
- | Output String
- | TypeCase
- | TypeInType
- | DefaultTotal
- | DefaultPartial
- | WarnPartial
- | WarnReach
- | NoCoverage
- | ErrContext
- | ShowImpl
- | Verbose
- | IBCSubDir String
- | ImportDir String
- | PkgBuild String
- | PkgInstall String
- | PkgClean String
- | PkgCheck String
- | PkgREPL String
- | PkgMkDoc String
- | PkgTest String
- | WarnOnly
- | Pkg String
- | BCAsm String
- | DumpDefun String
- | DumpCases String
- | UseCodegen Codegen
- | OutputTy OutputType
- | Extension LanguageExt
- | InterpretScript String
- | EvalExpr String
- | TargetTriple String
- | TargetCPU String
- | OptLevel Word
- | Client String
- | ShowOrigErr
- | AutoWidth
- | AutoSolve
- data Fixity
- data FixDecl = Fix Fixity String
- data Static
- data Plicity
- impl :: Plicity
- expl :: Plicity
- expl_param :: Plicity
- constraint :: Plicity
- tacimpl :: PTerm -> Plicity
- data FnOpt
- type FnOpts = [FnOpt]
- inlinable :: FnOpts -> Bool
- dictionary :: FnOpts -> Bool
- data DataOpt
- type DataOpts = [DataOpt]
- data ProvideWhat' t
- = ProvTerm t t
- | ProvPostulate t
- type ProvideWhat = ProvideWhat' PTerm
- data PDecl' t
- = PFix FC Fixity [String]
- | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t
- | PPostulate Docstring SyntaxInfo FC FnOpts Name t
- | PClauses FC FnOpts Name [PClause' t]
- | PCAF FC Name t
- | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t)
- | PParams FC [(Name, t)] [PDecl' t]
- | PNamespace String [PDecl' t]
- | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t
- | PClass Docstring SyntaxInfo FC [t] Name [(Name, t)] [(Name, Docstring)] [PDecl' t]
- | PInstance SyntaxInfo FC [t] Name [t] t (Maybe Name) [PDecl' t]
- | PDSL Name (DSL' t)
- | PSyntax FC Syntax
- | PMutual FC [PDecl' t]
- | PDirective (Idris ())
- | PProvider SyntaxInfo FC (ProvideWhat' t) Name
- | PTransform FC Bool t t
- type ElabD a = Elab' [PDecl] a
- data PClause' t
- data PData' t
- type PDecl = PDecl' PTerm
- type PData = PData' PTerm
- type PClause = PClause' PTerm
- 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 Name
- | PInferRef FC Name
- | PPatvar FC Name
- | PLam Name PTerm PTerm
- | PPi Plicity Name PTerm PTerm
- | PLet Name PTerm PTerm PTerm
- | PTyped PTerm PTerm
- | PApp FC PTerm [PArg]
- | PAppBind FC PTerm [PArg]
- | PMatchApp FC Name
- | PCase FC PTerm [(PTerm, PTerm)]
- | PTrue FC PunInfo
- | PFalse FC
- | PRefl FC PTerm
- | PResolveTC FC
- | PEq FC PTerm PTerm PTerm PTerm
- | PRewrite FC PTerm PTerm (Maybe PTerm)
- | PPair FC PunInfo PTerm PTerm
- | PDPair FC PunInfo PTerm PTerm PTerm
- | PAlternative Bool [PTerm]
- | PHidden PTerm
- | PType
- | PUniverse Universe
- | PGoal FC PTerm Name PTerm
- | PConstant Const
- | Placeholder
- | PDoBlock [PDo]
- | PIdiom FC PTerm
- | PReturn FC
- | PMetavar Name
- | PProof [PTactic]
- | PTactics [PTactic]
- | PElabError Err
- | PImpossible
- | PCoerced PTerm
- | PDisamb [[Text]] PTerm
- | PUnifyLog PTerm
- | PNoImplicits PTerm
- | PQuasiquote PTerm (Maybe PTerm)
- | PUnquote 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
- | MatchRefine Name
- | LetTac Name t
- | LetTacTy Name t t
- | Exact t
- | Compute
- | Trivial
- | TCInstance
- | ProofSearch Bool Bool Int (Maybe 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
- 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
- data ClassInfo = CI {
- instanceName :: Name
- class_methods :: [(Name, (FnOpts, PTerm))]
- class_defaults :: [(Name, (Name, PDecl))]
- class_default_superclasses :: [PDecl]
- class_params :: [Name]
- class_instances :: [Name]
- data TIData
- = TIPartial
- | TISolution [Term]
- data FnInfo = FnInfo {}
- data OptInfo = Optimise {
- inaccessible :: [(Int, Name)]
- detaggable :: Bool
- data TypeInfo = TI {}
- 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 = Rule [SSymbol] PTerm SynContext
- data SSymbol
- initDSL :: DSL' PTerm
- data Using
- data SyntaxInfo = Syn {
- using :: [Using]
- syn_params :: [(Name, PTerm)]
- syn_namespace :: [String]
- no_imp :: [Name]
- decoration :: Name -> Name
- inPattern :: Bool
- implicitAllowed :: Bool
- maxline :: Maybe Int
- mut_nesting :: Int
- dsl_info :: DSL
- syn_in_quasiquote :: Bool
- 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]
- unitDoc :: Doc
- unitTy :: Name
- unitCon :: Name
- unitDecl :: PData' PTerm
- unitOpts :: [DataOpt]
- falseDoc :: Doc
- falseTy :: Name
- falseDecl :: PData' PTerm
- falseOpts :: [t]
- pairDoc :: Doc
- pairTy :: Name
- pairCon :: Name
- pairDecl :: PData' PTerm
- pairOpts :: [t]
- pairParamDoc :: [(Name, Doc)]
- eqTy :: Name
- eqCon :: Name
- eqDoc :: Doc
- eqDecl :: PData' PTerm
- eqParamDoc :: [(Name, Doc)]
- eqOpts :: [t]
- elimName :: Name
- elimMethElimTy :: Name
- elimMethElim :: Name
- elimDecl :: PDecl' PTerm
- sigmaTy :: Name
- existsCon :: Name
- piBind :: [(Name, PTerm)] -> PTerm -> PTerm
- piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
- 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
- prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
- bindingOf :: Name -> Bool -> Doc OutputAnnotation
- 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
- 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 | |
|
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 (ErrorT 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))
REPL commands
Filename String | |
Quiet | |
NoBanner | |
ColourREPL Bool | |
Ideslave | |
IdeslaveSocket | |
ShowLibs | |
ShowLibdir | |
ShowIncs | |
NoBasePkgs | |
NoPrelude | |
NoBuiltins | |
NoREPL | |
OLogging Int | |
Output String | |
TypeCase | |
TypeInType | |
DefaultTotal | |
DefaultPartial | |
WarnPartial | |
WarnReach | |
NoCoverage | |
ErrContext | |
ShowImpl | |
Verbose | |
IBCSubDir String | |
ImportDir String | |
PkgBuild String | |
PkgInstall String | |
PkgClean String | |
PkgCheck String | |
PkgREPL String | |
PkgMkDoc String | |
PkgTest String | |
WarnOnly | |
Pkg String | |
BCAsm String | |
DumpDefun String | |
DumpCases String | |
UseCodegen Codegen | |
OutputTy OutputType | |
Extension LanguageExt | |
InterpretScript String | |
EvalExpr String | |
TargetTriple String | |
TargetCPU String | |
OptLevel Word | |
Client String | |
ShowOrigErr | |
AutoWidth | Automatically adjust terminal width |
AutoSolve | Automatically issue "solve" tactic in interactive prover |
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 |
dictionary :: FnOpts -> Bool Source
Data declaration options
Codata | Set if the the data-type is coinductive |
DefaultEliminator | Set if an eliminator should be generated for data type |
DefaultCaseFun | Set if a case function should be generated for data type |
DataErrRev |
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) | |
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 [(Name, Docstring)] SyntaxInfo FC FnOpts Name t | Type declaration |
PPostulate Docstring SyntaxInfo FC FnOpts Name t | Postulate |
PClauses FC FnOpts Name [PClause' t] | Pattern clause |
PCAF FC Name t | Top level constant |
PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) | Data declaration. |
PParams FC [(Name, t)] [PDecl' t] | Params block |
PNamespace String [PDecl' t] | New namespace |
PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t | Record declaration |
PClass Docstring SyntaxInfo FC [t] Name [(Name, t)] [(Name, Docstring)] [PDecl' t] | Type class: arguments are documentation, syntax info, source location, constraints, class name, parameters, method declarations |
PInstance SyntaxInfo FC [t] Name [t] t (Maybe Name) [PDecl' t] | Instance declaration: arguments are 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 (Idris ()) | Compiler directive. The parser inserts the corresponding action in the Idris monad. |
PProvider SyntaxInfo FC (ProvideWhat' t) Name | Type provider. The first t is the type, the second is the term |
PTransform FC Bool t t | Source-to-source transformation rule. If bool is True, lhs and rhs must be convertible |
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 |
tldeclared :: PDecl -> [Name] Source
High level language terms
PQuote Raw | |
PRef FC Name | |
PInferRef FC Name | A name to be defined later |
PPatvar FC Name | |
PLam Name PTerm PTerm | |
PPi Plicity Name PTerm PTerm | (n : t1) -> t2 |
PLet Name PTerm PTerm PTerm | |
PTyped PTerm PTerm | Term with explicit type |
PApp FC PTerm [PArg] | e.g. IO (), List Char, length x |
PAppBind FC PTerm [PArg] | implicitly bound application |
PMatchApp FC Name | Make an application by type matching |
PCase FC PTerm [(PTerm, PTerm)] | |
PTrue FC PunInfo | Unit type..? |
PFalse FC | _|_ |
PRefl FC PTerm | |
PResolveTC FC | |
PEq FC PTerm PTerm PTerm PTerm | Heterogeneous equality type: A = B |
PRewrite FC PTerm PTerm (Maybe PTerm) | |
PPair FC PunInfo PTerm PTerm | |
PDPair FC PunInfo PTerm PTerm PTerm | |
PAlternative Bool [PTerm] | |
PHidden PTerm | Irrelevant or hidden pattern |
PType |
|
PUniverse Universe | Some universe |
PGoal FC PTerm Name PTerm | |
PConstant Const | Builtin types |
Placeholder | |
PDoBlock [PDo] | |
PIdiom FC PTerm | |
PReturn FC | |
PMetavar Name | |
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 |
Intro [Name] | |
Intros | |
Focus Name | |
Refine Name [Bool] | |
Rewrite t | |
DoUnify | |
Induction t | |
CaseTac t | |
Equiv t | |
MatchRefine Name | |
LetTac Name t | |
LetTacTy Name t t | |
Exact t | |
Compute | |
Trivial | |
TCInstance | |
ProofSearch Bool Bool Int (Maybe 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 |
CI | |
|
TIPartial | a function with a partially defined type |
TISolution [Term] | possible solutions to a metavariable in a type |
Miscellaneous information about functions
Optimise | |
|
DSL | |
|
data SynContext Source
data SyntaxInfo Source
Syn | |
|
expandNS :: SyntaxInfo -> Name -> Name Source
getInferTerm :: Term -> Term Source
getInferType :: Term -> Term Source
pairParamDoc :: [(Name, Doc)] Source
eqParamDoc :: [(Name, Doc)] Source
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.
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
prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation Source
:: Name | ^ the bound name |
-> Bool | ^ whether the name is implicit |
-> Doc OutputAnnotation |
Pretty-printer helper for the binding site of a name
:: 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
allNamesIn :: PTerm -> [Name] Source
boundNamesIn :: PTerm -> [Name] Source
getErasureInfo :: IState -> Name -> [Int] Source