idris-0.9.19: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.AbsSyntax

Contents

Synopsis

Documentation

forCodegen :: Codegen -> [(Codegen, a)] -> [a] 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

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

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

Arguments

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

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

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

Arguments

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

function being applied

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

initial arguments

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

data EitherErr a b Source

Constructors

LeftErr a 
RightOK b 

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