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

Normalise everything, whether abstract, private or public

normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name

As normaliseAll, but with an explicit list of names *not* to reduce

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

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

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

Instances

Show Def

Methods

showsPrec :: Int -> Def -> ShowS

show :: Def -> String

showList :: [Def] -> ShowS

Generic Def

Associated Types

type Rep Def :: * -> *

Methods

from :: Def -> Rep Def x

to :: Rep Def x -> Def

type Rep Def

type Rep Def = D1 (MetaData "Def" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) (C1 (MetaCons "Function" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Term)))) (C1 (MetaCons "TyDecl" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameType)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type))))) ((:+:) (C1 (MetaCons "Operator" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ([Value] -> Maybe Value)))))) (C1 (MetaCons "CaseOp" PrefixI False) ((:*:) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 CaseInfo)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Type, Bool)])))) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Either Term (Term, Term)])) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [([Name], Term, Term)])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 CaseDefs))))))))

data CaseInfo

Constructors

CaseInfo

Fields

• case_inlinable :: Bool
• case_alwaysinline :: Bool
• tc_dictionary :: Bool

Instances

Generic CaseInfo

Associated Types

type Rep CaseInfo :: * -> *

Methods

from :: CaseInfo -> Rep CaseInfo x

to :: Rep CaseInfo x -> CaseInfo

type Rep CaseInfo

type Rep CaseInfo = D1 (MetaData "CaseInfo" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "CaseInfo" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "case_inlinable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) ((:*:) (S1 (MetaSel (Just Symbol "case_alwaysinline") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "tc_dictionary") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))))

data CaseDefs

Constructors

CaseDefs

Fields

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

Instances

Generic CaseDefs

Associated Types

type Rep CaseDefs :: * -> *

Methods

from :: CaseDefs -> Rep CaseDefs x

to :: Rep CaseDefs x -> CaseDefs

type Rep CaseDefs

type Rep CaseDefs = D1 (MetaData "CaseDefs" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "CaseDefs" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "cases_totcheck") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))) (S1 (MetaSel (Just Symbol "cases_compiletime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC)))) ((:*:) (S1 (MetaSel (Just Symbol "cases_inlined") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))) (S1 (MetaSel (Just Symbol "cases_runtime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))))))

data Accessibility

Constructors

Hidden

Public

Frozen

Private

Instances

Eq Accessibility

Methods

(==) :: Accessibility -> Accessibility -> Bool

(/=) :: Accessibility -> Accessibility -> Bool

Ord Accessibility

Methods

compare :: Accessibility -> Accessibility -> Ordering

(<) :: Accessibility -> Accessibility -> Bool

(<=) :: Accessibility -> Accessibility -> Bool

(>) :: Accessibility -> Accessibility -> Bool

(>=) :: Accessibility -> Accessibility -> Bool

max :: Accessibility -> Accessibility -> Accessibility

min :: Accessibility -> Accessibility -> Accessibility

Show Accessibility

Methods

showsPrec :: Int -> Accessibility -> ShowS

show :: Accessibility -> String

showList :: [Accessibility] -> ShowS

Generic Accessibility

Associated Types

type Rep Accessibility :: * -> *

Methods

from :: Accessibility -> Rep Accessibility x

to :: Rep Accessibility x -> Accessibility

type Rep Accessibility

type Rep Accessibility = D1 (MetaData "Accessibility" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) (C1 (MetaCons "Hidden" PrefixI False) U1) (C1 (MetaCons "Public" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Frozen" PrefixI False) U1) (C1 (MetaCons "Private" PrefixI False) U1)))

type Injectivity = Bool

data Totality

The result of totality checking

Constructors

Total [Int]

well-founded arguments

Productive

productive

Partial PReason

Unchecked

Generated

Instances

Eq Totality

Methods

(==) :: Totality -> Totality -> Bool

(/=) :: Totality -> Totality -> Bool

Show Totality

Methods

showsPrec :: Int -> Totality -> ShowS

show :: Totality -> String

showList :: [Totality] -> ShowS

Generic Totality

Associated Types

type Rep Totality :: * -> *

Methods

from :: Totality -> Rep Totality x

to :: Rep Totality x -> Totality

type Rep Totality

type Rep Totality = D1 (MetaData "Totality" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) (C1 (MetaCons "Total" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int]))) (C1 (MetaCons "Productive" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Partial" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PReason))) ((:+:) (C1 (MetaCons "Unchecked" PrefixI False) U1) (C1 (MetaCons "Generated" PrefixI False) U1))))

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

Methods

(==) :: PReason -> PReason -> Bool

(/=) :: PReason -> PReason -> Bool

Show PReason

Methods

showsPrec :: Int -> PReason -> ShowS

show :: PReason -> String

showList :: [PReason] -> ShowS

Generic PReason

Associated Types

type Rep PReason :: * -> *

Methods

from :: PReason -> Rep PReason x

to :: Rep PReason x -> PReason

type Rep PReason

type Rep PReason = D1 (MetaData "PReason" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "Other" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))) (C1 (MetaCons "Itself" PrefixI False) U1)) ((:+:) (C1 (MetaCons "NotCovering" PrefixI False) U1) (C1 (MetaCons "NotPositive" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "UseUndef" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "ExternalIO" PrefixI False) U1)) ((:+:) (C1 (MetaCons "BelieveMe" PrefixI False) U1) ((:+:) (C1 (MetaCons "Mutual" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))) (C1 (MetaCons "NotProductive" PrefixI False) U1)))))

data MetaInformation

Constructors

EmptyMI

No meta-information

DataMI [Int]

Meta information for a data declaration with position of parameters

Instances

Eq MetaInformation

Methods

(==) :: MetaInformation -> MetaInformation -> Bool

(/=) :: MetaInformation -> MetaInformation -> Bool

Show MetaInformation

Methods

showsPrec :: Int -> MetaInformation -> ShowS

show :: MetaInformation -> String

showList :: [MetaInformation] -> ShowS

Generic MetaInformation

Associated Types

type Rep MetaInformation :: * -> *

Methods

from :: MetaInformation -> Rep MetaInformation x

to :: Rep MetaInformation x -> MetaInformation

type Rep MetaInformation

type Rep MetaInformation = D1 (MetaData "MetaInformation" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) (C1 (MetaCons "EmptyMI" PrefixI False) U1) (C1 (MetaCons "DataMI" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int]))))

data Context

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

Instances

Show Context

Methods

showsPrec :: Int -> Context -> ShowS

show :: Context -> String

showList :: [Context] -> ShowS

Generic Context

Associated Types

type Rep Context :: * -> *

Methods

from :: Context -> Rep Context x

to :: Rep Context x -> Context

type Rep Context

type Rep Context = D1 (MetaData "Context" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "MkContext" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "next_tvar") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Just Symbol "definitions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))))))

initContext :: Context

The initial empty context

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

Get the definitions from a context

next_tvar :: Context -> Int

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

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

setInjective :: Name -> Injectivity -> 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 -> SC -> Bool -> Bool -> [(Type, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context

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

lookupP_all :: Bool -> Bool -> 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]

lookupTotalExact :: Name -> Context -> Maybe Totality

lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

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

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

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

isTCDict :: Name -> Context -> Bool

isCanonical :: Type -> Context -> Bool

Return true if the given type is a concrete type familyor primitive False it it's a function to compute a type or a variable

isDConName :: Name -> Context -> Bool

Check whether a resolved name is certainly a data constructor

canBeDConName :: Name -> Context -> Bool

Check whether any overloading of a name is a data constructor

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

Methods

(==) :: Value -> Value -> Bool

(/=) :: Value -> Value -> Bool

Show Value

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

Quote Value

Methods

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

class Quote a where

Minimal complete definition

quote

Methods

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

Instances

Quote Value

Methods

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

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, Injectivity, Accessibility, Totality, MetaInformation)

isUniverse :: Term -> Bool

Orphan instances

Show (a -> b)

Methods

showsPrec :: Int -> (a -> b) -> ShowS

show :: (a -> b) -> String

showList :: [a -> b] -> ShowS