Safe Haskell	None
Language	Haskell98

Idris.Core.Evaluate

Synopsis

Documentation

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

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

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

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

convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool Source

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

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

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

data CaseInfo Source

Constructors

CaseInfo
Fields case_inlinable :: Bool case_alwaysinline :: Bool tc_dictionary :: Bool

Instances

Binary CaseInfo
NFData CaseInfo

data CaseDefs Source

Constructors

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

Instances

Binary CaseDefs
NFData CaseDefs

data Accessibility Source

Constructors

Public
Frozen
Hidden

Instances

Eq Accessibility
Show Accessibility
Binary Accessibility
NFData Accessibility

data Totality Source

The result of totality checking

Constructors

Total [Int]	well-founded arguments
Productive	productive
Partial PReason
Unchecked

Instances

Eq Totality
Show Totality
Binary Totality
NFData Totality

data PReason Source

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

data MetaInformation Source

Constructors

EmptyMI	No meta-information
DataMI [Int]	Meta information for a data declaration with position of parameters

Instances

Eq MetaInformation
Show MetaInformation
Binary MetaInformation
NFData MetaInformation

data Context Source

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

Instances

Show Context

initContext :: Context Source

The initial empty context

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

Get the definitions from a context

uconstraints :: Context -> [UConstraint] Source

next_tvar :: Context -> Int Source

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

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

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

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

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

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

addDatatype :: Datatype Name -> Context -> Context Source

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

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

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

lookupNames :: Name -> Context -> [Name] 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

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

lookupP_all :: Bool -> Name -> Context -> [Term] Source

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

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

lookupDefExact :: Name -> Context -> Maybe Def Source

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

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

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

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

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

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

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

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

isTCDict :: Name -> Context -> Bool Source

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

isTConName :: Name -> Context -> Bool Source

isConName :: Name -> Context -> Bool Source

isFnName :: Name -> Context -> Bool Source

data Value Source

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 Source

Methods

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

Instances

Quote Value

initEval :: EvalState Source

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

Create a unique name given context and other existing names

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

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

isUniverse :: Term -> Bool Source