Safe Haskell	None

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 Source

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

Reduce a term to head normal form

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

convEq' :: Context -> 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 ![Either Term (Term, Term)] ![([Name], Term, Term)] !CaseDefs

Instances

Show Def
Binary Def

data CaseInfo Source

Constructors

CaseInfo
Fields case_inlinable :: Bool tc_dictionary :: Bool

Instances

Binary 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

data Accessibility Source

Constructors

Public
Frozen
Hidden

Instances

Eq Accessibility
Show Accessibility
Binary 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

data PReason Source

Reasons why a function may not be total

Constructors

Other [Name]
Itself
NotCovering
NotPositive
UseUndef Name
BelieveMe
Mutual [Name]
NotProductive

Instances

Eq PReason
Show PReason
Binary PReason

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

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

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

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

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

simplifyCasedef :: Name -> Context -> Context Source

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

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

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

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

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

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

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

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

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

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

isDConName :: Name -> Context -> Bool Source

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
VErased
VImpossible
VConstant Const
VProj Value Int
VTmp Int

Instances

Eq Value
Show Value
Quote Value

class Quote a whereSource

Methods

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

Instances

Quote Value

initEval :: EvalStateSource