| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.AbsSyntax
Contents
- getContext :: Idris Context
- forCodegen :: Codegen -> [(Codegen, a)] -> [a]
- getObjectFiles :: Codegen -> Idris [FilePath]
- addObjectFile :: Codegen -> FilePath -> Idris ()
- getLibs :: Codegen -> Idris [String]
- addLib :: Codegen -> String -> Idris ()
- getFlags :: Codegen -> Idris [String]
- addFlag :: Codegen -> String -> Idris ()
- addDyLib :: [String] -> Idris (Either DynamicLib String)
- getAutoImports :: Idris [FilePath]
- addAutoImport :: FilePath -> Idris ()
- addDefinedName :: Name -> Idris ()
- getDefinedNames :: Idris [Name]
- addTT :: Term -> Idris (Maybe Term)
- dumpTT :: Idris ()
- addHdr :: Codegen -> String -> Idris ()
- addImported :: Bool -> FilePath -> Idris ()
- addLangExt :: LanguageExt -> Idris ()
- addTrans :: Name -> (Term, Term) -> Idris ()
- addErrRev :: (Term, Term) -> Idris ()
- addErasureUsage :: Name -> Int -> Idris ()
- addExport :: Name -> Idris ()
- addUsedName :: FC -> Name -> Name -> Idris ()
- getErasureUsage :: Idris [(Name, Int)]
- getExports :: Idris [Name]
- totcheck :: (FC, Name) -> Idris ()
- defer_totcheck :: (FC, Name) -> Idris ()
- clear_totcheck :: Idris ()
- setFlags :: Name -> [FnOpt] -> Idris ()
- setFnInfo :: Name -> FnInfo -> Idris ()
- setAccessibility :: Name -> Accessibility -> Idris ()
- getFromHideList :: Name -> Idris (Maybe Accessibility)
- setTotality :: Name -> Totality -> Idris ()
- setInjectivity :: Name -> Injectivity -> Idris ()
- getTotality :: Name -> Idris Totality
- getCoercionsTo :: IState -> Type -> [Name]
- addToCG :: Name -> CGInfo -> Idris ()
- addCalls :: Name -> [Name] -> Idris ()
- addTyInferred :: Name -> Idris ()
- addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
- isTyInferred :: Name -> Idris Bool
- addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
- getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
- getAllNames :: Name -> Idris [Name]
- allNames :: [Name] -> Name -> Idris [Name]
- addCoercion :: Name -> Idris ()
- addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
- addNameHint :: Name -> Name -> Idris ()
- getNameHints :: IState -> Name -> [Name]
- addDeprecated :: Name -> String -> Idris ()
- getDeprecated :: Name -> Idris (Maybe String)
- addFragile :: Name -> String -> Idris ()
- getFragile :: Name -> Idris (Maybe String)
- push_estack :: Name -> Bool -> Idris ()
- pop_estack :: Idris ()
- addInstance :: Bool -> Bool -> Name -> Name -> Idris ()
- addOpenImpl :: [Name] -> Idris [Name]
- setOpenImpl :: [Name] -> Idris ()
- getOpenImpl :: Idris [Name]
- addClass :: Name -> ClassInfo -> Idris ()
- addRecord :: Name -> RecordInfo -> Idris ()
- addAutoHint :: Name -> Name -> Idris ()
- getAutoHints :: Name -> Idris [Name]
- addIBC :: IBCWrite -> Idris ()
- clearIBC :: Idris ()
- resetNameIdx :: Idris ()
- addNameIdx :: Name -> Idris (Int, Name)
- addNameIdx' :: IState -> Name -> (IState, (Int, Name))
- getSymbol :: Name -> Idris Name
- getHdrs :: Codegen -> Idris [String]
- getImported :: Idris [(FilePath, Bool)]
- setErrSpan :: FC -> Idris ()
- clearErr :: Idris ()
- getSO :: Idris (Maybe String)
- setSO :: Maybe String -> Idris ()
- getIState :: Idris IState
- putIState :: IState -> Idris ()
- updateIState :: (IState -> IState) -> Idris ()
- withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
- withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
- runIO :: IO a -> Idris a
- getName :: Idris Int
- addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
- getInternalApp :: FilePath -> Int -> Idris PTerm
- clearOrigPats :: Idris ()
- clearPTypes :: Idris ()
- checkUndefined :: FC -> Name -> Idris ()
- isUndefined :: FC -> Name -> Idris Bool
- setContext :: Context -> Idris ()
- updateContext :: (Context -> Context) -> Idris ()
- addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
- addDeferred :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
- addDeferredTyCon :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
- addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
- solveDeferred :: FC -> Name -> Idris ()
- getUndefined :: Idris [Name]
- isMetavarName :: Name -> IState -> Bool
- getWidth :: Idris ConsoleWidth
- setWidth :: ConsoleWidth -> Idris ()
- setDepth :: Maybe Int -> Idris ()
- typeDescription :: String
- type1Doc :: Doc OutputAnnotation
- isetPrompt :: String -> Idris ()
- isetLoadedRegion :: Idris ()
- setLogLevel :: Int -> Idris ()
- setLogCats :: [LogCat] -> Idris ()
- setCmdLine :: [Opt] -> Idris ()
- getCmdLine :: Idris [Opt]
- getDumpHighlighting :: Idris Bool
- getDumpDefun :: Idris (Maybe FilePath)
- getDumpCases :: Idris (Maybe FilePath)
- logLevel :: Idris Int
- setAutoImpls :: Bool -> Idris ()
- getAutoImpls :: Idris Bool
- setErrContext :: Bool -> Idris ()
- errContext :: Idris Bool
- getOptimise :: Idris [Optimisation]
- setOptimise :: [Optimisation] -> Idris ()
- addOptimise :: Optimisation -> Idris ()
- removeOptimise :: Optimisation -> Idris ()
- setOptLevel :: Int -> Idris ()
- useREPL :: Idris Bool
- setREPL :: Bool -> Idris ()
- showOrigErr :: Idris Bool
- setShowOrigErr :: Bool -> Idris ()
- setAutoSolve :: Bool -> Idris ()
- setNoBanner :: Bool -> Idris ()
- getNoBanner :: Idris Bool
- setEvalTypes :: Bool -> Idris ()
- getDesugarNats :: Idris Bool
- setDesugarNats :: Bool -> Idris ()
- setQuiet :: Bool -> Idris ()
- getQuiet :: Idris Bool
- setCodegen :: Codegen -> Idris ()
- codegen :: Idris Codegen
- setOutputTy :: OutputType -> Idris ()
- outputTy :: Idris OutputType
- setIdeMode :: Bool -> Handle -> Idris ()
- setTargetTriple :: String -> Idris ()
- targetTriple :: Idris String
- setTargetCPU :: String -> Idris ()
- targetCPU :: Idris String
- verbose :: Idris Bool
- setVerbose :: Bool -> Idris ()
- typeInType :: Idris Bool
- setTypeInType :: Bool -> Idris ()
- coverage :: Idris Bool
- setCoverage :: Bool -> Idris ()
- setIBCSubDir :: FilePath -> Idris ()
- valIBCSubDir :: IState -> Idris FilePath
- addImportDir :: FilePath -> Idris ()
- setImportDirs :: [FilePath] -> Idris ()
- allImportDirs :: Idris [FilePath]
- colourise :: Idris Bool
- setColourise :: Bool -> Idris ()
- impShow :: Idris Bool
- setImpShow :: Bool -> Idris ()
- setColour :: ColourType -> IdrisColour -> Idris ()
- logLvl :: Int -> String -> Idris ()
- logCoverage :: Int -> String -> Idris ()
- logErasure :: Int -> String -> Idris ()
- logParser :: Int -> String -> Idris ()
- logElab :: Int -> String -> Idris ()
- logCodeGen :: Int -> String -> Idris ()
- logIBC :: Int -> String -> Idris ()
- logLvlCats :: [LogCat] -> Int -> String -> Idris ()
- cmdOptType :: Opt -> Idris Bool
- noErrors :: Idris Bool
- setTypeCase :: Bool -> Idris ()
- expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
- expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
- mapsnd :: (t -> t2) -> (t1, t) -> (t1, t2)
- expandInstanceScope :: t -> t1 -> [(Name, t3)] -> t2 -> PDecl' t3 -> PDecl' t3
- getPriority :: IState -> PTerm -> Int
- addStatics :: Name -> Term -> PTerm -> Idris ()
- addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
- addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
- addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
- getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
- implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
- implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
- implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
- addImplPat :: IState -> PTerm -> PTerm
- addImplBound :: IState -> [Name] -> PTerm -> PTerm
- addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
- addImpl :: [Name] -> IState -> PTerm -> PTerm
- addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
- aiFn :: Name -> Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[Text]] -> [PArg] -> Either Err PTerm
- impIn :: [PArg] -> PArg -> Bool
- expArg :: PArg' t -> Bool
- stripLinear :: IState -> PTerm -> PTerm
- stripUnmatchable :: IState -> PTerm -> PTerm
- mkPApp :: FC -> Int -> PTerm -> [PArg] -> PTerm
- findStatics :: IState -> PTerm -> (PTerm, [Bool])
- data EitherErr a b
- toEither :: EitherErr a b -> Either a b
- matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
- matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
- substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
- substMatch :: Name -> PTerm -> PTerm -> PTerm
- substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
- shadow :: Name -> Name -> PTerm -> PTerm
- mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
- module Idris.AbsSyntaxTree
Documentation
forCodegen :: Codegen -> [(Codegen, a)] -> [a] Source
getObjectFiles :: Codegen -> Idris [FilePath] Source
addObjectFile :: Codegen -> FilePath -> Idris () Source
addAutoImport :: FilePath -> Idris () Source
addDefinedName :: Name -> Idris () Source
getDefinedNames :: Idris [Name] Source
addImported :: Bool -> FilePath -> Idris () Source
addLangExt :: LanguageExt -> Idris () Source
addErasureUsage :: Name -> Int -> Idris () Source
getErasureUsage :: Idris [(Name, Int)] Source
getExports :: Idris [Name] Source
defer_totcheck :: (FC, Name) -> Idris () Source
clear_totcheck :: Idris () Source
setAccessibility :: Name -> Accessibility -> Idris () Source
getFromHideList :: Name -> Idris (Maybe Accessibility) Source
get the accessibility of a name outside this module
setTotality :: Name -> Totality -> Idris () Source
setInjectivity :: Name -> Injectivity -> Idris () Source
getTotality :: Name -> Idris Totality Source
getCoercionsTo :: IState -> Type -> [Name] Source
addTyInferred :: Name -> Idris () Source
isTyInferred :: Name -> Idris Bool Source
addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris () Source
Adds error handlers for a particular function and argument. If names are ambiguous, all matching handlers are updated.
getAllNames :: Name -> Idris [Name] Source
addCoercion :: Name -> Idris () Source
addNameHint :: Name -> Name -> Idris () Source
getNameHints :: IState -> Name -> [Name] Source
addDeprecated :: Name -> String -> Idris () Source
addFragile :: Name -> String -> Idris () Source
push_estack :: Name -> Bool -> Idris () Source
pop_estack :: Idris () Source
Arguments
| :: Bool | whether the name is an Integer instance |
| -> Bool | whether to include the instance in instance search |
| -> Name | the name of the class |
| -> Name | the name of the instance |
| -> Idris () |
Add a class instance function.
Precondition: the instance should have the correct type.
Dodgy hack 1: Put integer instances first in the list so they are resolved by default.
Dodgy hack 2: put constraint chasers (@@) last
addOpenImpl :: [Name] -> Idris [Name] Source
setOpenImpl :: [Name] -> Idris () Source
getOpenImpl :: Idris [Name] Source
addRecord :: Name -> RecordInfo -> Idris () Source
addAutoHint :: Name -> Name -> Idris () Source
getAutoHints :: Name -> Idris [Name] Source
resetNameIdx :: Idris () Source
getImported :: Idris [(FilePath, Bool)] Source
setErrSpan :: FC -> Idris () Source
updateIState :: (IState -> IState) -> Idris () Source
runIO :: IO a -> Idris a Source
A version of liftIO that puts errors into the exception type of the Idris monad
clearOrigPats :: Idris () Source
clearPTypes :: Idris () Source
checkUndefined :: FC -> Name -> Idris () Source
setContext :: Context -> Idris () Source
updateContext :: (Context -> Context) -> Idris () Source
addConstraints :: FC -> (Int, [UConstraint]) -> Idris () Source
Arguments
| :: NameType | |
| -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] | The Name is the name being made into a metavar, the Int is the number of vars that are part of a putative proof context, the Maybe Name is the top-level function containing the new metavariable, the Type is its type, and the Bool is whether :p is allowed |
| -> Idris () |
Save information about a name that is not yet defined
solveDeferred :: FC -> Name -> Idris () Source
getUndefined :: Idris [Name] Source
isMetavarName :: Name -> IState -> Bool Source
setWidth :: ConsoleWidth -> Idris () Source
isetPrompt :: String -> Idris () Source
isetLoadedRegion :: Idris () Source
Tell clients how much was parsed and loaded
setLogLevel :: Int -> Idris () Source
setLogCats :: [LogCat] -> Idris () Source
setCmdLine :: [Opt] -> Idris () Source
getCmdLine :: Idris [Opt] Source
getDumpDefun :: Idris (Maybe FilePath) Source
getDumpCases :: Idris (Maybe FilePath) Source
setAutoImpls :: Bool -> Idris () Source
setErrContext :: Bool -> Idris () Source
setOptimise :: [Optimisation] -> Idris () Source
addOptimise :: Optimisation -> Idris () Source
removeOptimise :: Optimisation -> Idris () Source
setOptLevel :: Int -> Idris () Source
setShowOrigErr :: Bool -> Idris () Source
setAutoSolve :: Bool -> Idris () Source
setNoBanner :: Bool -> Idris () Source
setEvalTypes :: Bool -> Idris () Source
setDesugarNats :: Bool -> Idris () Source
setCodegen :: Codegen -> Idris () Source
setOutputTy :: OutputType -> Idris () Source
setIdeMode :: Bool -> Handle -> Idris () Source
setTargetTriple :: String -> Idris () Source
setTargetCPU :: String -> Idris () Source
setVerbose :: Bool -> Idris () Source
setTypeInType :: Bool -> Idris () Source
setCoverage :: Bool -> Idris () Source
setIBCSubDir :: FilePath -> Idris () Source
valIBCSubDir :: IState -> Idris FilePath Source
addImportDir :: FilePath -> Idris () Source
setImportDirs :: [FilePath] -> Idris () Source
allImportDirs :: Idris [FilePath] Source
setColourise :: Bool -> Idris () Source
setImpShow :: Bool -> Idris () Source
setColour :: ColourType -> IdrisColour -> Idris () Source
logCoverage :: Int -> String -> Idris () Source
logErasure :: Int -> String -> Idris () Source
logCodeGen :: Int -> String -> Idris () Source
Log an action of the compiler.
Arguments
| :: [LogCat] | The categories that the message should appear under. |
| -> Int | The Logging level the message should appear. |
| -> String | The message to show the developer. |
| -> Idris () |
Log aspect of Idris execution
An empty set of logging levels is used to denote all categories.
@TODO update IDE protocol
cmdOptType :: Opt -> Idris Bool Source
setTypeCase :: Bool -> Idris () Source
expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl Source
expandInstanceScope :: t -> t1 -> [(Name, t3)] -> t2 -> PDecl' t3 -> PDecl' t3 Source
if it's just a type variable or concrete type, do it early (0)
if there's only type variables and injective constructors, do it next (1)
if there's a function type, next (2)
finally, everything else (3)
getPriority :: IState -> PTerm -> Int Source
addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm Source
addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm Source
implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg]) Source
addImplPat :: IState -> PTerm -> PTerm Source
addImpl :: [Name] -> IState -> PTerm -> PTerm Source
Add the implicit arguments to applications in the term [Name] gives the names to always expend, even when under a binder of that name (this is to expand methods with implicit arguments in dependent type classes).
stripLinear :: IState -> PTerm -> PTerm Source
stripUnmatchable :: IState -> PTerm -> PTerm Source
Remove functions which aren't applied to anything, which must then be resolved by unification. Assume names resolved and alternatives filled in (so no ambiguity).
matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] Source
Syntactic match of a against b, returning pair of variables in a and what they match. Returns the pair that failed if not a match.
mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm Source
Rename any binders which are repeated (so that we don't have to mess about with shadowing anywhere else).
module Idris.AbsSyntaxTree