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

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

toValue :: Context -> Env -> TT Name -> Value Source

quoteTerm :: Value -> 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 Source

data CaseInfo Source

Constructors

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

data CaseDefs Source

Constructors

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

data Accessibility Source

Constructors

Hidden
Public
Frozen
Private

Instances

Eq Accessibility Source
Ord Accessibility Source
Show Accessibility Source

data Totality Source

The result of totality checking

Constructors

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

Instances

Eq Totality Source
Show Totality Source

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 Source
Show PReason Source

data MetaInformation Source

Constructors

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

Instances

Eq MetaInformation Source
Show MetaInformation Source

data Context Source

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

Instances

Show Context Source

initContext :: Context Source

The initial empty context

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

Get the definitions from a context

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

simplifyCasedef :: Name -> ErasureInfo -> Context -> TC 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 -> 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

lookupTotalExact :: Name -> Context -> Maybe 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 Source
Show Value Source
Quote Value Source

class Quote a where Source

Methods

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

Instances

Quote Value Source

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