Idris.AbsSyntax

Documentation

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)

get the accessibility of a name outside this module

setTotality :: Name -> Totality -> 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 ()

Adds error handlers for a particular function and argument. If names are ambiguous, all matching handlers are updated.

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)

push_estack :: Name -> Bool -> Idris ()

pop_estack :: Idris ()

addInstance

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

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

A version of liftIO that puts errors into the exception type of the Idris monad

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'

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 ()

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 ()

Tell clients how much was parsed and loaded

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 ()

Log an action of the parser

logElab :: Int -> String -> Idris ()

Log an action of the elaborator.

logCodeGen :: Int -> String -> Idris ()

Log an action of the compiler.

logIBC :: Int -> String -> Idris ()

logLvlCats

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

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)

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

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 :: 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

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).

addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

aiFn

Arguments

:: Name

-> Bool

-> Bool

-> Bool

-> [Name]

-> IState

-> FC

-> Name

function being applied

-> FC

-> [[Text]]

-> [PArg]

initial arguments (if in a pattern)

-> Either Err PTerm

impIn :: [PArg] -> PArg -> Bool

expArg :: PArg' t -> Bool

stripLinear :: IState -> PTerm -> PTerm

stripUnmatchable :: IState -> PTerm -> PTerm

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).

mkPApp :: FC -> Int -> PTerm -> [PArg] -> PTerm

findStatics :: IState -> PTerm -> (PTerm, [Bool])

data EitherErr a b

Constructors

LeftErr a

RightOK b

Instances

Monad (EitherErr a)

Functor (EitherErr a)

Applicative (EitherErr a)

toEither :: EitherErr a b -> Either a b

matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

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.

matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

substMatches :: [(Name, PTerm)] -> PTerm -> PTerm

substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

substMatch :: Name -> PTerm -> PTerm -> PTerm

substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm

shadow :: Name -> Name -> PTerm -> PTerm

mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

Rename any binders which are repeated (so that we don't have to mess about with shadowing anywhere else).

module Idris.AbsSyntaxTree