idris-0.9.12: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.Evaluate

Synopsis

Documentation

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

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

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

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

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

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.

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

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

Instances

data CaseInfo Source

Constructors

CaseInfo 

Instances

data CaseDefs Source

Constructors

CaseDefs 

Fields

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

Instances

data Totality Source

The result of totality checking

Constructors

Total [Int]

well-founded arguments

Productive

productive

Partial PReason 
Unchecked 

data PReason Source

Reasons why a function may not be total

data MetaInformation Source

Constructors

EmptyMI

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.

Instances

initContext :: ContextSource

The initial empty context

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

Get the definitions from a context

addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool -> [Type] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> ContextSource

class Quote a whereSource

Methods

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

Instances

initEval :: EvalStateSource

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

Create a unique name given context and other existing names