License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Core.Evaluate

Contents

Orphan instances

Description

Synopsis

normalise :: Context -> Env -> TT Name -> TT Name
normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
normaliseC :: Context -> Env -> TT Name -> TT Name
normaliseAll :: Context -> Env -> TT Name -> TT Name
normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
toValue :: Context -> Env -> TT Name -> Value
quoteTerm :: Value -> TT Name
rt_simplify :: Context -> Env -> TT Name -> TT Name
simplify :: Context -> Env -> TT Name -> TT Name
inlineSmall :: Context -> Env -> TT Name -> TT Name
specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)])
unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool
data Def
- = 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
data CaseInfo = CaseInfo {
- case_inlinable :: Bool
- case_alwaysinline :: Bool
- tc_dictionary :: Bool
}
data CaseDefs = CaseDefs {
- cases_compiletime :: !([Name], SC)
- cases_runtime :: !([Name], SC)
}
data Accessibility
- = Hidden
- | Public
- | Frozen
- | Private
type Injectivity = Bool
data Totality
- = Total [Int]
- | Productive
- | Partial PReason
- | Unchecked
- | Generated
type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
data PReason
- = Other [Name]
- | Itself
- | NotCovering
- | NotPositive
- | UseUndef Name
- | ExternalIO
- | BelieveMe
- | Mutual [Name]
- | NotProductive
data MetaInformation
- = EmptyMI
- | DataMI [Int]
data Context
initContext :: Context
ctxtAlist :: Context -> [(Name, Def)]
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
setRigCount :: Name -> RigCount -> 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)] -> Type -> Context -> TC Context
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
lookupNames :: Name -> Context -> [Name]
lookupTyName :: Name -> Context -> [(Name, Type)]
lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
lookupTy :: Name -> Context -> [Type]
lookupTyExact :: Name -> Context -> Maybe Type
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
tcReducible :: Name -> Context -> Bool
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
lookupTotal :: Name -> Context -> [Totality]
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
isTCDict :: Name -> Context -> Bool
isCanonical :: Type -> Context -> Bool
isDConName :: Name -> Context -> Bool
canBeDConName :: Name -> Context -> Bool
isTConName :: Name -> Context -> Bool
isConName :: Name -> Context -> Bool
isFnName :: Name -> Context -> Bool
conGuarded :: Context -> Name -> Term -> Bool
data Value
- = VP NameType Name Value
- | VV Int
- | VBind Bool Name (Binder Value) (Value -> Eval Value)
- | VBLet RigCount Int Name Value Value Value
- | VApp Value Value
- | VType UExp
- | VUType Universe
- | VErased
- | VImpossible
- | VConstant Const
- | VProj Value Int
- | VTmp Int
class Quote a where
- quote :: Int -> a -> Eval (TT Name)
initEval :: EvalState
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
definitions :: Context -> Ctxt TTDecl
visibleDefinitions :: Context -> Ctxt TTDecl
isUniverse :: Term -> Bool
linearCheck :: Context -> Type -> TC ()
linearCheckArg :: Context -> Type -> TC ()

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 lets

inlineSmall :: Context -> Env -> TT Name -> TT Name Source #

Like simplify, but we only reduce functions that are marked as okay to inline, and don't reduce lets

specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)]) Source #

unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name Source #

Unfold the given names in a term, the given number of times in a stack. Preserves 'let'. This is primarily to support inlining of the given names, and can also help with partial evaluation by allowing a rescursive definition to be unfolded once only. Specifically used to unfold definitions using interfaces before going to the totality checker (otherwise mutually recursive definitions in implementations will not work...)

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, Bool)] ![Either Term (Term, Term)] ![([Name], Term, Term)] !CaseDefs

Instances

Show Def Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Def -> ShowS # show :: Def -> String # showList :: [Def] -> ShowS #
Generic Def Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep Def :: Type -> Type # Methods from :: Def -> Rep Def x # to :: Rep Def x -> Def #
ToJSON Def Source #
Instance details Defined in IRTS.Portable Methods toJSON :: Def -> Value # toEncoding :: Def -> Encoding # toJSONList :: [Def] -> Value # toEncodingList :: [Def] -> Encoding #
Binary Def Source #
Instance details Defined in Idris.IBC Methods put :: Def -> Put # get :: Get Def # putList :: [Def] -> Put #
NFData Def Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: Def -> () #
type Rep Def Source #
Instance details Defined in Idris.Core.Evaluate type Rep Def = D1 (MetaData "Def" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Function" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Term)) :+: C1 (MetaCons "TyDecl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameType) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type))) :+: (C1 (MetaCons "Operator" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ([Value] -> Maybe Value)))) :+: C1 (MetaCons "CaseOp" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 CaseInfo) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Type, Bool)]))) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Either Term (Term, Term)]) :: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [([Name], Term, Term)]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 CaseDefs))))))

data CaseInfo Source #

Constructors

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

Instances

Generic CaseInfo Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep CaseInfo :: Type -> Type # Methods from :: CaseInfo -> Rep CaseInfo x # to :: Rep CaseInfo x -> CaseInfo #
ToJSON CaseInfo Source #
Instance details Defined in IRTS.Portable Methods toJSON :: CaseInfo -> Value # toEncoding :: CaseInfo -> Encoding # toJSONList :: [CaseInfo] -> Value # toEncodingList :: [CaseInfo] -> Encoding #
Binary CaseInfo Source #
Instance details Defined in Idris.IBC Methods put :: CaseInfo -> Put # get :: Get CaseInfo # putList :: [CaseInfo] -> Put #
NFData CaseInfo Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: CaseInfo -> () #
type Rep CaseInfo Source #
Instance details Defined in Idris.Core.Evaluate type Rep CaseInfo = D1 (MetaData "CaseInfo" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "CaseInfo" PrefixI True) (S1 (MetaSel (Just "case_inlinable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :: (S1 (MetaSel (Just "case_alwaysinline") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :: S1 (MetaSel (Just "tc_dictionary") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))

data CaseDefs Source #

Constructors

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

Instances

Generic CaseDefs Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep CaseDefs :: Type -> Type # Methods from :: CaseDefs -> Rep CaseDefs x # to :: Rep CaseDefs x -> CaseDefs #
ToJSON CaseDefs Source #
Instance details Defined in IRTS.Portable Methods toJSON :: CaseDefs -> Value # toEncoding :: CaseDefs -> Encoding # toJSONList :: [CaseDefs] -> Value # toEncodingList :: [CaseDefs] -> Encoding #
Binary CaseDefs Source #
Instance details Defined in Idris.IBC Methods put :: CaseDefs -> Put # get :: Get CaseDefs # putList :: [CaseDefs] -> Put #
NFData CaseDefs Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: CaseDefs -> () #
type Rep CaseDefs Source #
Instance details Defined in Idris.Core.Evaluate type Rep CaseDefs = D1 (MetaData "CaseDefs" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "CaseDefs" PrefixI True) (S1 (MetaSel (Just "cases_compiletime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC)) :*: S1 (MetaSel (Just "cases_runtime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))))

data Accessibility Source #

Constructors

Hidden
Public
Frozen
Private

Instances

Eq Accessibility Source #
Instance details Defined in Idris.Core.Evaluate Methods (==) :: Accessibility -> Accessibility -> Bool # (/=) :: Accessibility -> Accessibility -> Bool #
Ord Accessibility Source #
Instance details Defined in Idris.Core.Evaluate 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 Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Accessibility -> ShowS # show :: Accessibility -> String # showList :: [Accessibility] -> ShowS #
Generic Accessibility Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep Accessibility :: Type -> Type # Methods from :: Accessibility -> Rep Accessibility x # to :: Rep Accessibility x -> Accessibility #
ToJSON Accessibility Source #
Instance details Defined in IRTS.Portable Methods toJSON :: Accessibility -> Value # toEncoding :: Accessibility -> Encoding # toJSONList :: [Accessibility] -> Value # toEncodingList :: [Accessibility] -> Encoding #
Binary Accessibility Source #
Instance details Defined in Idris.IBC Methods put :: Accessibility -> Put # get :: Get Accessibility # putList :: [Accessibility] -> Put #
NFData Accessibility Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: Accessibility -> () #
type Rep Accessibility Source #
Instance details Defined in Idris.Core.Evaluate type Rep Accessibility = D1 (MetaData "Accessibility" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Hidden" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Public" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Frozen" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Private" PrefixI False) (U1 :: Type -> Type)))

type Injectivity = Bool 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 #
Instance details Defined in Idris.Core.Evaluate Methods (==) :: Totality -> Totality -> Bool # (/=) :: Totality -> Totality -> Bool #
Show Totality Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Totality -> ShowS # show :: Totality -> String # showList :: [Totality] -> ShowS #
Generic Totality Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep Totality :: Type -> Type # Methods from :: Totality -> Rep Totality x # to :: Rep Totality x -> Totality #
ToJSON Totality Source #
Instance details Defined in IRTS.Portable Methods toJSON :: Totality -> Value # toEncoding :: Totality -> Encoding # toJSONList :: [Totality] -> Value # toEncodingList :: [Totality] -> Encoding #
Binary Totality Source #
Instance details Defined in Idris.IBC Methods put :: Totality -> Put # get :: Get Totality # putList :: [Totality] -> Put #
NFData Totality Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: Totality -> () #
type Rep Totality Source #
Instance details Defined in Idris.Core.Evaluate type Rep Totality = D1 (MetaData "Totality" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Total" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int])) :+: C1 (MetaCons "Productive" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Partial" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PReason)) :+: (C1 (MetaCons "Unchecked" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Generated" PrefixI False) (U1 :: Type -> Type))))

type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation) 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 #
Instance details Defined in Idris.Core.Evaluate Methods (==) :: PReason -> PReason -> Bool # (/=) :: PReason -> PReason -> Bool #
Show PReason Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> PReason -> ShowS # show :: PReason -> String # showList :: [PReason] -> ShowS #
Generic PReason Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep PReason :: Type -> Type # Methods from :: PReason -> Rep PReason x # to :: Rep PReason x -> PReason #
Binary PReason Source #
Instance details Defined in Idris.IBC Methods put :: PReason -> Put # get :: Get PReason # putList :: [PReason] -> Put #
NFData PReason Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: PReason -> () #
type Rep PReason Source #
Instance details Defined in Idris.Core.Evaluate type Rep PReason = D1 (MetaData "PReason" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (((C1 (MetaCons "Other" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name])) :+: C1 (MetaCons "Itself" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "NotCovering" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NotPositive" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "UseUndef" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "ExternalIO" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "BelieveMe" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Mutual" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name])) :+: C1 (MetaCons "NotProductive" PrefixI False) (U1 :: Type -> Type)))))

data MetaInformation Source #

Constructors

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

Instances

Eq MetaInformation Source #
Instance details Defined in Idris.Core.Evaluate Methods (==) :: MetaInformation -> MetaInformation -> Bool # (/=) :: MetaInformation -> MetaInformation -> Bool #
Show MetaInformation Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> MetaInformation -> ShowS # show :: MetaInformation -> String # showList :: [MetaInformation] -> ShowS #
Generic MetaInformation Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep MetaInformation :: Type -> Type # Methods from :: MetaInformation -> Rep MetaInformation x # to :: Rep MetaInformation x -> MetaInformation #
ToJSON MetaInformation Source #
Instance details Defined in IRTS.Portable Methods toJSON :: MetaInformation -> Value # toEncoding :: MetaInformation -> Encoding # toJSONList :: [MetaInformation] -> Value # toEncodingList :: [MetaInformation] -> Encoding #
Binary MetaInformation Source #
Instance details Defined in Idris.IBC Methods put :: MetaInformation -> Put # get :: Get MetaInformation # putList :: [MetaInformation] -> Put #
NFData MetaInformation Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: MetaInformation -> () #
type Rep MetaInformation Source #
Instance details Defined in Idris.Core.Evaluate type Rep MetaInformation = D1 (MetaData "MetaInformation" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "EmptyMI" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "DataMI" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int])))

data Context Source #

Contexts used for global definitions and for proof state. They contain universe constraints and existing definitions. Also store maximum RigCount of the name (can't bind a name at multiplicity 1 in a RigW, for example)

Instances

Show Context Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Context -> ShowS # show :: Context -> String # showList :: [Context] -> ShowS #
Generic Context Source #
Instance details Defined in Idris.Core.Evaluate Associated Types type Rep Context :: Type -> Type # Methods from :: Context -> Rep Context x # to :: Rep Context x -> Context #
NFData Context Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: Context -> () #
type Rep Context Source #
Instance details Defined in Idris.Core.Evaluate type Rep Context = D1 (MetaData "Context" "Idris.Core.Evaluate" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) (C1 (MetaCons "MkContext" PrefixI True) (S1 (MetaSel (Just "next_tvar") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: S1 (MetaSel (Just "definitions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Ctxt TTDecl))))

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 #

setInjective :: Name -> Injectivity -> Context -> Context Source #

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

setRigCount :: Name -> RigCount -> 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, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context Source #

simplifyCasedef :: Name -> [Name] -> [[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 #

tcReducible :: Name -> Context -> Bool Source #

lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)] Source #

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

lookupTotalExact :: Name -> Context -> Maybe Totality Source #

lookupInjectiveExact :: Name -> Context -> Maybe Injectivity Source #

lookupRigCount :: Name -> Context -> [Totality] Source #

lookupRigCountExact :: Name -> Context -> Maybe RigCount Source #

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

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

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

isTCDict :: Name -> Context -> Bool Source #

isCanonical :: Type -> Context -> Bool Source #

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 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 #

conGuarded :: Context -> Name -> Term -> 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 RigCount 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 #
Instance details Defined in Idris.Core.Evaluate Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
Show Value Source #
Instance details Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #
Quote Value Source #
Instance details Defined in Idris.Core.Evaluate Methods quote :: Int -> Value -> Eval (TT Name) Source #

class Quote a where Source #

Methods

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

Instances

Quote Value Source #
Instance details Defined in Idris.Core.Evaluate Methods quote :: Int -> Value -> Eval (TT Name) 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 TTDecl Source #

visibleDefinitions :: Context -> Ctxt TTDecl Source #

isUniverse :: Term -> Bool Source #

linearCheck :: Context -> Type -> TC () Source #

linearCheckArg :: Context -> Type -> TC () Source #

Orphan instances

Show (a -> b) Source #
Instance details Methods showsPrec :: Int -> (a -> b) -> ShowS # show :: (a -> b) -> String # showList :: [a -> b] -> ShowS #