idris-0.11.2: Functional Programming Language with Dependent Types

Safe HaskellNone




normaliseC :: Context -> Env -> TT Name -> TT Name Source

Normalise fully type checked terms (so, assume all names/let bindings resolved)

normaliseAll :: Context -> Env -> TT Name -> TT Name Source

Normalise everything, whether abstract, private or public

normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name Source

As normaliseAll, but with an explicit list of names *not* to reduce

rt_simplify :: Context -> Env -> TT Name -> TT Name Source

Simplify for run-time (i.e. basic inlining)

simplify :: Context -> Env -> TT Name -> TT Name Source

Like normalise, but we only reduce functions that are marked as okay to inline (and probably shouldn't reduce lets?) 20130908: now only used to reduce for totality checking. Inlining should be done elsewhere.

specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)]) Source

hnf :: Context -> Env -> TT Name -> TT Name Source

Reduce a term to head normal form

data Def Source

A definition is either a simple function (just an expression with a type), a constant, which could be a data or type constructor, an axiom or as an yet undefined function, or an Operator. An Operator is a function which explains how to reduce. A CaseOp is a function defined by a simple case tree


data CaseDefs Source




cases_totcheck :: !([Name], SC)
cases_compiletime :: !([Name], SC)
cases_inlined :: !([Name], SC)
cases_runtime :: !([Name], SC)

data Totality Source

The result of totality checking


Total [Int]

well-founded arguments



Partial PReason 

data PReason Source

Reasons why a function may not be total

data MetaInformation Source



No meta-information

DataMI [Int]

Meta information for a data declaration with position of parameters

data Context Source

Contexts used for global definitions and for proof state. They contain universe constraints and existing definitions.


initContext :: Context Source

The initial empty context

ctxtAlist :: Context -> [(Name, Def)] Source

Get the definitions from a context

addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> Bool -> Bool -> [Type] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context Source

lookupTyName :: Name -> Context -> [(Name, Type)] Source

Get the list of pairs of fully-qualified names and their types that match some name

lookupTyNameExact :: Name -> Context -> Maybe (Name, Type) Source

Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

lookupTy :: Name -> Context -> [Type] Source

Get the types that match some name

lookupTyExact :: Name -> Context -> Maybe Type Source

Get the single type that matches some name precisely

isDConName :: Name -> Context -> Bool Source

Check whether a resolved name is certainly a data constructor

canBeDConName :: Name -> Context -> Bool Source

Check whether any overloading of a name is a data constructor

class Quote a where Source


quote :: Int -> a -> Eval (TT Name) Source


initEval :: EvalState Source

uniqueNameCtxt :: Context -> Name -> [Name] -> Name Source

Create a unique name given context and other existing names