Idris.Core.Evaluate

Documentation

normalise :: Context -> Env -> TT Name -> TT Name

normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name

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

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

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

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

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

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

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

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

Reduce a term to head normal form

convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC' Err Bool

data Def

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

Constructors

Function !Type !Term

TyDecl NameType !Type

Operator Type Int ([Value] -> Maybe Value)

CaseOp CaseInfo !Type ![Type] ![Either Term (Term, Term)] ![([Name], Term, Term)] !CaseDefs

Instances

Show Def

Binary Def

Apropos Def

data CaseInfo

Constructors

CaseInfo

Fields

case_inlinable :: Bool

tc_dictionary :: Bool

Instances

Binary CaseInfo

data CaseDefs

Constructors

CaseDefs

Fields

cases_totcheck :: !([Name], SC)

cases_compiletime :: !([Name], SC)

cases_inlined :: !([Name], SC)

cases_runtime :: !([Name], SC)

Instances

Binary CaseDefs

data Accessibility

Constructors

Public

Frozen

Hidden

Instances

Eq Accessibility

Show Accessibility

Binary Accessibility

data Totality

The result of totality checking

Constructors

Total [Int]

well-founded arguments

Productive

productive

Partial PReason

Unchecked

Instances

Eq Totality

Show Totality

Binary Totality

data PReason

Reasons why a function may not be total

Constructors

Other [Name]

Itself

NotCovering

NotPositive

UseUndef Name

ExternalIO

BelieveMe

Mutual [Name]

NotProductive

Instances

Eq PReason

Show PReason

Binary PReason

data MetaInformation

Constructors

EmptyMI

No meta-information

DataMI [Int]

Meta information for a data declaration with position of parameters

Instances

Eq MetaInformation

Show MetaInformation

Binary MetaInformation

data Context

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

Instances

Show Context

initContext :: Context

The initial empty context

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

Get the definitions from a context

uconstraints :: Context -> [UConstraint]

next_tvar :: Context -> Int

addToCtxt :: Name -> Term -> Type -> Context -> Context

setAccess :: Name -> Accessibility -> Context -> Context

setTotal :: Name -> Totality -> Context -> Context

setMetaInformation :: Name -> MetaInformation -> Context -> Context

addCtxtDef :: Name -> Def -> Context -> Context

addTyDecl :: Name -> NameType -> Type -> Context -> Context

addDatatype :: Datatype Name -> Context -> Context

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

simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

lookupNames :: Name -> Context -> [Name]

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

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

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

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]

Get the types that match some name

lookupTyExact :: Name -> Context -> Maybe Type

Get the single type that matches some name precisely

lookupP :: Name -> Context -> [Term]

lookupDef :: Name -> Context -> [Def]

lookupNameDef :: Name -> Context -> [(Name, Def)]

lookupDefExact :: Name -> Context -> Maybe Def

lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)]

lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)

lookupVal :: Name -> Context -> [Value]

mapDefCtxt :: (Def -> Def) -> Context -> Context

lookupTotal :: Name -> Context -> [Totality]

lookupNameTotal :: Name -> Context -> [(Name, Totality)]

lookupMetaInformation :: Name -> Context -> [MetaInformation]

lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

isDConName :: Name -> Context -> Bool

isTConName :: Name -> Context -> Bool

isConName :: Name -> Context -> Bool

isFnName :: Name -> Context -> Bool

data Value

A HOAS representation of values

Constructors

VP NameType Name Value

VV Int

VBind Bool Name (Binder Value) (Value -> Eval Value)

VBLet Int Name Value Value Value

VApp Value Value

VType UExp

VUType Universe

VErased

VImpossible

VConstant Const

VProj Value Int

VTmp Int

Instances

Eq Value

Show Value

Quote Value

class Quote a where

Methods

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

Instances

Quote Value

initEval :: EvalState

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

Create a unique name given context and other existing names

uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name

definitions :: Context -> Ctxt (Def, Accessibility, Totality, MetaInformation)

isUniverse :: Term -> Bool