Safe Haskell | None |
---|
- 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
- defaultOpts :: IOption
- 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 String
- idris_totcheck :: [(FC, Name)]
- idris_defertotcheck :: [(FC, Name)]
- 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)]
- proof_list :: [(Name, [String])]
- errLine :: Maybe Int
- lastParse :: Maybe Name
- indent_stack :: [Int]
- brace_stack :: [Maybe Int]
- 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_outh :: Handle
- 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
- data SizeChange
- type SCGEntry = (Name, [Maybe (Int, SizeChange)])
- 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
- | IBCSyntax Syntax
- | IBCKeyword String
- | IBCImport 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]
- | 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
- idrisInit :: IState
- type Idris = StateT IState (ErrorT Err IO)
- data Codegen
- data Command
- = Quit
- | Help
- | Eval PTerm
- | Check PTerm
- | DocStr Name
- | TotCheck Name
- | Reload
- | Load FilePath
- | 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
- | Info 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
- | DoProofSearch Bool Int Name [Name]
- | SetOpt Opt
- | UnsetOpt Opt
- | NOP
- | SetColour ColourType IdrisColour
- | ColourOn
- | ColourOff
- | ListErrorHandlers
- | SetConsoleWidth ConsoleWidth
- data Opt
- = Filename String
- | Ver
- | Usage
- | Quiet
- | NoBanner
- | ColourREPL Bool
- | Ideslave
- | ShowLibs
- | ShowLibdir
- | ShowIncs
- | NoBasePkgs
- | NoPrelude
- | NoBuiltins
- | NoREPL
- | OLogging Int
- | Output String
- | TypeCase
- | TypeInType
- | DefaultTotal
- | DefaultPartial
- | WarnPartial
- | NoCoverage
- | ErrContext
- | ShowImpl
- | Verbose
- | IBCSubDir String
- | ImportDir String
- | PkgBuild String
- | PkgInstall String
- | PkgClean String
- | PkgCheck String
- | PkgREPL String
- | WarnOnly
- | Pkg String
- | BCAsm String
- | DumpDefun String
- | DumpCases String
- | UseCodegen Codegen
- | OutputTy OutputType
- | Extension LanguageExt
- | InterpretScript String
- | TargetTriple String
- | TargetCPU String
- | OptLevel Word
- | Client String
- | ShowOrigErr
- | AutoWidth
- data Fixity
- data FixDecl = Fix Fixity String
- data Static
- data Plicity
- = Imp { }
- | Exp { }
- | Constraint { }
- | TacImp { }
- plazy :: Plicity -> Bool
- impl :: Plicity
- expl :: Plicity
- expl_param :: Plicity
- constraint :: Plicity
- tacimpl :: PTerm -> Plicity
- data FnOpt
- = Inlinable
- | TotalFn
- | PartialFn
- | Coinductive
- | AssertTotal
- | Dictionary
- | Implicit
- | CExport String
- | ErrorHandler
- | ErrorReverse
- | Reflection
- | Specialise [(Name, Maybe Int)]
- type FnOpts = [FnOpt]
- inlinable :: FnOpts -> Bool
- dictionary :: FnOpts -> Bool
- data DataOpt
- type DataOpts = [DataOpt]
- data PDecl' t
- = PFix FC Fixity [String]
- | PTy String SyntaxInfo FC FnOpts Name t
- | PPostulate String SyntaxInfo FC FnOpts Name t
- | PClauses FC FnOpts Name [PClause' t]
- | PCAF FC Name t
- | PData String SyntaxInfo FC DataOpts (PData' t)
- | PParams FC [(Name, t)] [PDecl' t]
- | PNamespace String [PDecl' t]
- | PRecord String SyntaxInfo FC Name t String Name t
- | PClass String SyntaxInfo FC [t] Name [(Name, t)] [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 Name t t
- | 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
- | PRewrite FC PTerm PTerm (Maybe PTerm)
- | PPair FC PunInfo PTerm PTerm
- | PDPair FC PTerm PTerm PTerm
- | PAlternative Bool [PTerm]
- | PHidden PTerm
- | PType
- | 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
- mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
- data PTactic' t
- = Intro [Name]
- | Intros
- | Focus Name
- | Refine Name [Bool]
- | Rewrite t
- | Induction Name
- | Equiv t
- | MatchRefine Name
- | LetTac Name t
- | LetTacTy Name t t
- | Exact t
- | Compute
- | Trivial
- | TCInstance
- | ProofSearch (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)
- | Qed
- | Abandon
- type PTactic = PTactic' PTerm
- data PDo' t
- type PDo = PDo' PTerm
- data PArg' t
- = PImp { }
- | PExp { }
- | PConstraint { }
- | PTacImplicit { }
- data ArgOpt
- = Lazy
- | HideDisplay
- lazyarg :: PArg' t -> Bool
- 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 Forceability
- data OptInfo = Optimise {
- collapsible :: Bool
- isnewtype :: Bool
- forceable :: [(Int, Forceability)]
- recursive :: [Int]
- 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
- type DSL = DSL' PTerm
- data SynContext
- = PatternSyntax
- | TermSyntax
- | AnySyntax
- 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
- dsl_info :: DSL
- defaultSyntax :: SyntaxInfo
- expandNS :: SyntaxInfo -> Name -> Name
- bi :: 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
- unitDecl :: PData' PTerm
- unitOpts :: [DataOpt]
- falseTy :: Name
- falseDecl :: PData' PTerm
- falseOpts :: [a]
- pairTy :: Name
- pairCon :: Name
- pairDecl :: PData' PTerm
- pairOpts :: [a]
- eqTy :: Name
- eqCon :: Name
- eqDecl :: PData' PTerm
- eqOpts :: [a]
- 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
- prettyImp :: Bool -> PTerm -> Doc OutputAnnotation
- pprintPTerm :: Bool -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
- bindingOf :: Name -> Bool -> Doc OutputAnnotation
- prettyName :: Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
- showCImp :: Bool -> PClause -> Doc OutputAnnotation
- showDImp :: Bool -> PData -> Doc OutputAnnotation
- showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
- showDeclImp :: Bool -> PDecl' PTerm -> Doc OutputAnnotation
- getImps :: [PArg] -> [(Name, PTerm)]
- getExps :: [PArg] -> [PTerm]
- getConsts :: [PArg] -> [PTerm]
- getAll :: [PArg] -> [PTerm]
- showName :: Maybe IState -> [(Name, Bool)] -> Bool -> Bool -> Name -> String
- showTm :: IState -> PTerm -> String
- showTmImpls :: PTerm -> String
- getPArity :: PTerm -> Int
- allNamesIn :: PTerm -> [Name]
- boundNamesIn :: PTerm -> [Name]
- namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
- usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
Documentation
IOption | |
|
data LanguageExt Source
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 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
Inlinable | |
TotalFn | |
PartialFn | |
Coinductive | |
AssertTotal | |
Dictionary | |
Implicit | |
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)] |
dictionary :: FnOpts -> BoolSource
Data declaration options
Top-level declarations such as compiler directives, definitions, datatypes and typeclasses.
PFix FC Fixity [String] | Fixity declaration |
PTy String SyntaxInfo FC FnOpts Name t | Type declaration |
PPostulate String SyntaxInfo FC FnOpts Name t | Postulate |
PClauses FC FnOpts Name [PClause' t] | Pattern clause |
PCAF FC Name t | Top level constant |
PData String SyntaxInfo FC DataOpts (PData' t) | Data declaration. |
PParams FC [(Name, t)] [PDecl' t] | Params block |
PNamespace String [PDecl' t] | New namespace |
PRecord String SyntaxInfo FC Name t String Name t | Record declaration |
PClass String SyntaxInfo FC [t] Name [(Name, t)] [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 Name t t | 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 | |
PLet Name PTerm PTerm PTerm | |
PTyped PTerm PTerm | Term with explicit type |
PApp FC PTerm [PArg] | |
PAppBind FC PTerm [PArg] | implicitly bound application |
PMatchApp FC Name | Make an application by type matching |
PCase FC PTerm [(PTerm, PTerm)] | |
PTrue FC PunInfo | |
PFalse FC | |
PRefl FC PTerm | |
PResolveTC FC | |
PEq FC PTerm PTerm | |
PRewrite FC PTerm PTerm (Maybe PTerm) | |
PPair FC PunInfo PTerm PTerm | |
PDPair FC PTerm PTerm PTerm | |
PAlternative Bool [PTerm] | |
PHidden PTerm | Irrelevant or hidden pattern |
PType | |
PGoal FC PTerm Name PTerm | |
PConstant Const | |
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 |
Intro [Name] | |
Intros | |
Focus Name | |
Refine Name [Bool] | |
Rewrite t | |
Induction Name | |
Equiv t | |
MatchRefine Name | |
LetTac Name t | |
LetTacTy Name t t | |
Exact t | |
Compute | |
Trivial | |
TCInstance | |
ProofSearch (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) | |
Qed | |
Abandon |
CI | |
|
data Forceability Source
Optimise | |
|
DSL | |
|
data SynContext Source
data SyntaxInfo Source
Syn | |
|
expandNS :: SyntaxInfo -> Name -> NameSource
getInferTerm :: Term -> TermSource
getInferType :: Term -> TermSource
consoleDecorate :: IState -> OutputAnnotation -> String -> StringSource
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.
:: Bool | ^ whether to show implicits |
-> PTerm | ^ the term to pretty-print |
-> Doc OutputAnnotation |
Pretty-print a high-level closed Idris term
:: Bool | ^ whether to show implicits |
-> [(Name, Bool)] | ^ the currently-bound names and whether they are implicit |
-> PTerm | ^ the term to pretty-print |
-> Doc OutputAnnotation |
Pretty-print a high-level Idris term in some bindings context
:: Name | ^ the bound name |
-> Bool | ^ whether the name is implicit |
-> Doc OutputAnnotation |
Pretty-printer helper for the binding site of a name
:: 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 :: Bool -> PDecl' PTerm -> Doc OutputAnnotationSource
:: Maybe IState | ^ the Idris state, for information about names and colours |
-> [(Name, Bool)] | ^ the bound variables and whether they're implicit |
-> Bool | ^ whether to show implicits |
-> Bool | ^ whether to colourise |
-> Name | ^ the term to show |
-> String |
Show Idris name
showTmImpls :: PTerm -> StringSource
Show a term with implicits, no colours
allNamesIn :: PTerm -> [Name]Source
boundNamesIn :: PTerm -> [Name]Source