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

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

setTotality :: Name -> Totality -> Idris ()

getTotality :: Name -> Idris Totality

getCoercionsTo :: IState -> Type -> [Name]

addToCG :: Name -> CGInfo -> 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]

addToCalledG :: Name -> [Name] -> Idris ()

push_estack :: Name -> Idris ()

pop_estack :: Idris ()

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

addClass :: Name -> ClassInfo -> Idris ()

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, Bool))] -> Idris ()

addDeferredTyCon :: [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

addDeferred'

Arguments

:: NameType

-> [(Name, (Int, Maybe Name, Type, 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 :: Name -> Idris ()

getUndefined :: Idris [Name]

isMetavarName :: Name -> IState -> Bool

getWidth :: Idris ConsoleWidth

setWidth :: ConsoleWidth -> Idris ()

type1Doc :: Doc OutputAnnotation

isetPrompt :: String -> Idris ()

isetLoadedRegion :: Idris ()

Tell clients how much was parsed and loaded

setLogLevel :: Int -> Idris ()

setCmdLine :: [Opt] -> Idris ()

getCmdLine :: Idris [Opt]

getDumpDefun :: Idris (Maybe FilePath)

getDumpCases :: Idris (Maybe FilePath)

logLevel :: Idris Int

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

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

cmdOptType :: Opt -> Idris Bool

iLOG :: String -> Idris ()

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 :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[Text]] -> [PArg] -> Either Err PTerm

stripLinear :: IState -> PTerm -> PTerm

stripUnmatchable :: IState -> PTerm -> PTerm

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

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] -> PTerm -> PTerm

module Idris.AbsSyntaxTree