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)

addHdr :: Codegen -> String -> Idris ()

addLangExt :: LanguageExt -> Idris ()

addTrans :: (Term, Term) -> Idris ()

addErrRev :: (Term, Term) -> Idris ()

totcheck :: (FC, Name) -> Idris ()

defer_totcheck :: (FC, Name) -> Idris ()

clear_totcheck :: Idris ()

setFlags :: Name -> [FnOpt] -> Idris ()

setAccessibility :: Name -> Accessibility -> Idris ()

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

getTotality :: Name -> Idris Totality

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

addToCG :: Name -> CGInfo -> Idris ()

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

Adds error handlers for a particular function and argument. If names are is 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 -> String -> Idris ()

addNameHint :: Name -> Name -> Idris ()

getNameHints :: IState -> Name -> [Name]

addToCalledG :: Name -> [Name] -> 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))

getHdrs :: Codegen -> Idris [String]

setErrLine :: Int -> Idris ()

clearErr :: Idris ()

getSO :: Idris (Maybe String)

setSO :: Maybe String -> Idris ()

getIState :: Idris IState

putIState :: IState -> 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' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

solveDeferred :: Name -> Idris ()

getUndefined :: Idris [Name]

getWidth :: Idris ConsoleWidth

setWidth :: ConsoleWidth -> Idris ()

renderWidth :: Idris Int

iRender :: Doc a -> Idris (SimpleDoc a)

ihPrintResult :: Handle -> String -> Idris ()

consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

Write a pretty-printed term to the console with semantic coloring

ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

Write pretty-printed output to IDESlave with semantic annotations

ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()

Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

type1Doc :: Doc OutputAnnotation

ihPrintError :: Handle -> String -> Idris ()

ihputStrLn :: Handle -> String -> Idris ()

iputStrLn :: String -> Idris ()

iPrintError :: String -> Idris ()

iPrintResult :: String -> Idris ()

iWarn :: FC -> String -> Idris ()

ideslavePutSExp :: SExpable a => String -> a -> Idris ()

iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

isetPrompt :: String -> Idris ()

ihWarn :: Handle -> FC -> String -> Idris ()

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

useREPL :: Idris Bool

setREPL :: Bool -> Idris ()

showOrigErr :: Idris Bool

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

setIdeSlave :: Bool -> Idris ()

setTargetTriple :: String -> Idris ()

targetTriple :: Idris String

setTargetCPU :: String -> Idris ()

targetCPU :: Idris String

setOptLevel :: Word -> Idris ()

optLevel :: Idris Word

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

setOutH :: Handle -> 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 ()

addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm

implicit' :: 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 :: IState -> PTerm -> PTerm

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

aiFn :: Bool -> Bool -> 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)

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