idris-0.11.2: Functional Programming Language with Dependent Types

Safe HaskellNone





forCodegen :: Codegen -> [(Codegen, a)] -> [a] Source

getFromHideList :: Name -> Idris (Maybe Accessibility) Source

get the accessibility of a name outside this module

addCalls :: Name -> [Name] -> Idris () 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.

addInstance Source


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

withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b Source

withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris () Source

runIO :: IO a -> Idris a Source

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

addDeferred' Source


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

isetLoadedRegion :: Idris () Source

Tell clients how much was parsed and loaded

logParser :: Int -> String -> Idris () Source

Log an action of the parser

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

Log an action of the elaborator.

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

Log an action of the compiler.

logLvlCats Source


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

expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm Source

expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl Source

mapsnd :: (t -> t2) -> (t1, t) -> (t1, t2) 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)

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

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

aiFn Source


:: Name 
-> Bool 
-> Bool 
-> Bool 
-> [Name] 
-> IState 
-> FC 
-> Name

function being applied

-> FC 
-> [[Text]] 
-> [PArg]

initial arguments (if in a pattern)

-> Either Err PTerm 

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

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

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